From 2613c16bbba6d90344e9c7b4b0f40e3774e027f3 Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Wed, 22 Nov 2023 18:26:16 +0100
Subject: [PATCH] bump toolchain

---
 .gitignore             |  1 +
 server/.gitignore      |  4 +---
 server/lakefile32.lean |  2 +-
 server/lean-toolchain  |  2 +-
 wasm.sh                | 28 ++++++++++++++++++----------
 5 files changed, 22 insertions(+), 15 deletions(-)

diff --git a/.gitignore b/.gitignore
index d9d65e8..23e5dd4 100644
--- a/.gitignore
+++ b/.gitignore
@@ -5,3 +5,4 @@ server/lakefile.olean
 server32bit
 **/lake-packages/
 **/.DS_Store
+client/public/server.*
diff --git a/server/.gitignore b/server/.gitignore
index 920cc59..905aaa8 100644
--- a/server/.gitignore
+++ b/server/.gitignore
@@ -1,5 +1,3 @@
-build
-build32
+.lake
 adam
-nng
 lakefile32.olean
diff --git a/server/lakefile32.lean b/server/lakefile32.lean
index da446ec..5ddfad4 100644
--- a/server/lakefile32.lean
+++ b/server/lakefile32.lean
@@ -2,7 +2,7 @@ import Lake
 open Lake DSL
 
 package GameServer {
-  buildDir := "build32"
+  buildDir := ".lake/build32"
 }
 
 @[default_target]
diff --git a/server/lean-toolchain b/server/lean-toolchain
index 2f868c6..24a3cdb 100644
--- a/server/lean-toolchain
+++ b/server/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.2.0
+leanprover/lean4:v4.3.0-rc2
diff --git a/wasm.sh b/wasm.sh
index 71c7cca..fa9a306 100755
--- a/wasm.sh
+++ b/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