bump toolchain

.gitignore

@@ -5,3 +5,4 @@ server/lakefile.olean
 server32bit
 **/lake-packages/
 **/.DS_Store
+client/public/server.*

server/.gitignore

@@ -1,5 +1,3 @@
-build
-build32
+.lake
 adam
-nng
 lakefile32.olean

server/lakefile32.lean

@@ -2,7 +2,7 @@ import Lake
 open Lake DSL
 
 package GameServer {
-  buildDir := "build32"
+  buildDir := ".lake/build32"
 }
 
 @[default_target]

server/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.2.0
+leanprover/lean4:v4.3.0-rc2

wasm.sh

@@ -1,23 +1,31 @@
 #!/bin/bash
 
-rm -rf server32bit
-cp -r server server32bit
+cd server
 
-cd server32bit
-/home/alex/Projects/lean4/build/test/stage1/bin/lake update -R
-/home/alex/Projects/lean4/build/test/stage1/bin/lake clean
-/home/alex/Projects/lean4/build/test/stage1/bin/lake build
+mkdir -p .lake/toolchains
+if [ ! -f .lake/toolchains/lean-4.3.0-rc2-linux_wasm32.tar.zst  ]
+then
+    wget -P .lake/toolchains https://github.com/leanprover/lean4/releases/download/v4.3.0-rc2/lean-4.3.0-rc2-linux_wasm32.tar.zst
+    tar --use-compress-program=unzstd -xvf .lake/toolchains/lean-4.3.0-rc2-linux_wasm32.tar.zst -C .lake/toolchains
+fi
+if [ ! -f .lake/toolchains/lean-4.3.0-rc2-linux_x86.tar.zst  ]
+then
+    wget -P .lake/toolchains https://github.com/leanprover/lean4/releases/download/v4.3.0-rc2/lean-4.3.0-rc2-linux_x86.tar.zst
+    tar --use-compress-program=unzstd -xvf .lake/toolchains/lean-4.3.0-rc2-linux_x86.tar.zst -C .lake/toolchains
+fi
+
+# Linking will fail, but that's ok. We only need the c files.
+.lake/toolchains/lean-4.3.0-rc2-linux_x86/bin/lake build -f=lakefile32.lean
 
-cd ../server
 
 lake build
 
 
 OUT_DIR=../client/public
-LEAN_SYSROOT=/home/alex/Projects/lean4/build/release/stage1
+LEAN_SYSROOT=.lake/toolchains/lean-4.3.0-rc2-linux_wasm32
 LEAN_LIBDIR=$LEAN_SYSROOT/lib/lean
 
-emcc -o $OUT_DIR/server.js main.c -I $LEAN_SYSROOT/include -L $LEAN_LIBDIR build/ir/GameServer/*.c -lInit -lLean -lleancpp -lleanrt \
+emcc -o $OUT_DIR/server.js main.c -I $LEAN_SYSROOT/include -L $LEAN_LIBDIR .lake/build/ir/GameServer/*.c -lInit -lLean -lleancpp -lleanrt \
   -sFORCE_FILESYSTEM -lnodefs.js -s EXIT_RUNTIME=0 -s MAIN_MODULE=1 -s LINKABLE=1 -s EXPORT_ALL=1 -s ALLOW_MEMORY_GROWTH=1 -fwasm-exceptions -pthread -flto \
   --preload-file "${LEAN_SYSROOT}/lib/lean/Init"@/lib/Init \
   --preload-file "${LEAN_SYSROOT}/lib/lean/Init.olean"@/lib/Init.olean \
@@ -25,4 +33,4 @@ emcc -o $OUT_DIR/server.js main.c -I $LEAN_SYSROOT/include -L $LEAN_LIBDIR build
   --preload-file "${LEAN_SYSROOT}/lib/lean/Lean"@/lib/Lean \
   --preload-file "${LEAN_SYSROOT}/lib/lean/Lean.olean"@/lib/Lean.olean \
   --preload-file "${LEAN_SYSROOT}/lib/lean/Lean.ilean"@/lib/Lean.ilean \
-  --preload-file "../server32bit/build/lib"@/gamelib
+  --preload-file "./.lake/build32/lib"@/gamelib