modify bubblewrap.sh

leanprover-community · Aug 25, 2024 · 4a226a5 · 4a226a5
1 parent 7a26dd5
commit 4a226a5
Showing 1 changed file with 10 additions and 5 deletions.
diff --git a/server/bubblewrap.sh b/server/bubblewrap.sh
@@ -1,11 +1,15 @@
 #/bin/bash
 
-ELAN_HOME=$(cd $1 && lake env printenv ELAN_HOME)
+LEAN_ROOT="$(cd $1 && lean --print-prefix)"
+LEAN_PATH="$(cd $1 && lake env printenv LEAN_PATH)"
+
+# # print commands as they are executed
+# set -x
 
 if command -v bwrap >/dev/null 2>&1; then
   (exec bwrap\
-    --ro-bind $1 /project \
-    --ro-bind $ELAN_HOME /elan \
+    --ro-bind "$1" /project \
+    --ro-bind "$LEAN_ROOT" /lean \
     --ro-bind /usr /usr \
     --dev /dev \
     --proc /proc \
@@ -14,8 +18,9 @@ if command -v bwrap >/dev/null 2>&1; then
     --symlink usr/bin /bin\
     --symlink usr/sbin /sbin\
     --clearenv \
-    --setenv PATH "/elan/bin:/bin" \
-    --setenv ELAN_HOME "/elan" \
+    --setenv PATH "/lean/bin" \
+    --setenv LAKE "/no" `# tries to invoke git otherwise` \
+    --setenv LEAN_PATH "$LEAN_PATH" \
     --unshare-user \
     --unshare-pid  \
     --unshare-net  \