You cannot select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
42 lines
1.0 KiB
Bash
42 lines
1.0 KiB
Bash
#/bin/bash
|
|
|
|
# Note: This fails if there is no default toolchain installed
|
|
LEAN_ROOT="$(cd $1 && lean --print-prefix)"
|
|
LEAN_PATH="$(cd $1 && lake env printenv LEAN_PATH)"
|
|
|
|
# $1 : the game directory
|
|
# $2 : the lean4game folder
|
|
# $3 : the gameserver executable
|
|
|
|
# # print commands as they are executed
|
|
# set -x
|
|
|
|
(exec bwrap\
|
|
--ro-bind $2 /lean4game \
|
|
--ro-bind $1 /game \
|
|
--ro-bind "$LEAN_ROOT" /lean \
|
|
--ro-bind /usr /usr \
|
|
--dev /dev \
|
|
--proc /proc \
|
|
--symlink usr/lib /lib\
|
|
--symlink usr/lib64 /lib64\
|
|
--symlink usr/bin /bin\
|
|
--symlink usr/sbin /sbin\
|
|
--clearenv \
|
|
--setenv PATH "/lean/bin" \
|
|
--setenv LAKE "/no" `# tries to invoke git otherwise` \
|
|
--setenv LEAN_PATH "$LEAN_PATH" \
|
|
--unshare-user \
|
|
--unshare-pid \
|
|
--unshare-net \
|
|
--unshare-uts \
|
|
--unshare-cgroup \
|
|
--die-with-parent \
|
|
--chdir "/game/.lake/packages/GameServer/server/.lake/build/bin/" \
|
|
./gameserver --server /game
|
|
)
|
|
|
|
# TODO
|
|
# --chdir "/game/.lake/packages/GameServer/server/.lake/build/bin/" \
|
|
# ./gameserver --server /game
|