update to v4.2.0

.devcontainer/devcontainer.json

@@ -13,7 +13,7 @@
   "overrideCommand": true,
   "onCreateCommand": {
     "npm_install": "(cd ~/lean4game && npm install)",
-    "lake_build": "(cd ~/game && lake clean && lake exe cache get && lake build)"
+    "lake_build": "(cd ~/game && lake update -R && lake exe cache get && lake build)"
   },
   "postStartCommand": "cd ~/lean4game && export VITE_LEAN4GAME_SINGLE=true && npm start",
   "customizations": {

.github/workflows/build.yml

@@ -9,15 +9,56 @@ jobs:
     runs-on: ubuntu-latest
     steps:
 
-      - uses: actions/checkout@v2
+      - name: install elan
+        run: |
+          set -o pipefail
+          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          ./elan-init -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
 
-      - name: build docker image
+      - uses: actions/checkout@v4
-        run: docker build . --file Dockerfile --tag game:latest
 
-      - name: Store docker container as an artifact
+      - name: print lean and lake versions
-        uses: ishworkh/docker-image-artifact-upload@v1
+        run: |
+          lean --version
+          lake --version
+
+      - name: get mathlib cache
+        continue-on-error: true
+        run: |
+          lake exe cache clean
+          # We've been seeing many failures at this step recently because of network errors.
+          # As a band-aid, we try twice.
+          # The 'sleep 1' is small pause to let the network recover.
+          lake exe cache get || (sleep 1; lake exe cache get)
+
+      - name: create timestamp file
+        run: touch tmp_timestamp
+
+      - name: building game
+        run: env LEAN_ABORT_ON_PANIC=1 lake build
+
+      - name: delete unused mathlib cache
+        continue-on-error: true
+        run: find ./lake-packages/mathlib/build/lib -type f \( -name "*.olean" -o -name "*.olean.hash" \) \! -neweraa ./tmp_timestamp -delete -print
+
+      - name: delete timestamp file
+        run: rm ./tmp_timestamp
+
+      - name: compress built game
+        run: tar -czvf ../game.tar.gz .
+        # run: zip game.zip ./* -r
+
+      - name: hack. move compressed artifact back
+        run: mv ../game.tar.gz ./game.tar.gz
+        # run: zip game.zip ./* -r
+
+      - name: upload compressed game folder
+        uses: actions/upload-artifact@v3
         with:
-          image: "game:latest"
+          name: build-for-server-import
+          path: |
+            game.tar.gz
 
-      - name: What next?
+      # - name: What next?
-        run: echo "To export the game to the Game Server, open https://adam.math.hhu.de/import/trigger/${GITHUB_REPOSITORY,,} \n Afterwards, you can play the game at https://adam.math.hhu.de/#/g/${GITHUB_REPOSITORY,,}"
+      #   run: echo "To export the game to the Game Server, open https://adam.math.hhu.de/import/trigger/${GITHUB_REPOSITORY,,} \n Afterwards, you can play the game at https://adam.math.hhu.de/#/g/${GITHUB_REPOSITORY,,}"

.github/workflows/build_non_main.yml

@@ -10,7 +10,28 @@ jobs:
     runs-on: ubuntu-latest
     steps:
 
-      - uses: actions/checkout@v2
+      - name: install elan
+        run: |
+          set -o pipefail
+          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          ./elan-init -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
 
-      - name: build docker image
+      - uses: actions/checkout@v4
-        run: docker build . --file Dockerfile --tag game:latest
+
+      - name: print lean and lake versions
+        run: |
+          lean --version
+          lake --version
+
+      - name: get mathlib cache
+        continue-on-error: true
+        run: |
+          lake exe cache clean
+          # We've been seeing many failures at this step recently because of network errors.
+          # As a band-aid, we try twice.
+          # The 'sleep 1' is small pause to let the network recover.
+          lake exe cache get || (sleep 1; lake exe cache get)
+
+      - name: building game
+        run: env LEAN_ABORT_ON_PANIC=1 lake build

lake-manifest.json

@@ -4,57 +4,57 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean4game.git",
     "subDir?": "server",
-    "rev": "8e4c993bd7113d86452df98142e67529f19c24a9",
+    "rev": "6f92d6138148e9222052f681b589c8d015750c47",
     "opts": {},
     "name": "GameServer",
-    "inputRev?": "main",
+    "inputRev?": "v4.2.0",
     "inherited": false}},
   {"git":
-   {"url": "https://github.com/leanprover-community/mathlib4",
+   {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "f203f2e0caf1d9ea25b7f2e4b8c2afebd2c6967b",
+    "rev": "753159252c585df6b6aa7c48d2b8828d58388b79",
     "opts": {},
     "name": "mathlib",
-    "inputRev?": "v4.1.0",
+    "inputRev?": "v4.2.0",
     "inherited": false}},
   {"git":
-   {"url": "https://github.com/mhuisi/lean4-cli.git",
+   {"url": "https://github.com/leanprover-community/quote4",
     "subDir?": null,
-    "rev": "21dac2e9cc7e3cf7da5800814787b833e680b2fd",
+    "rev": "a387c0eb611857e2460cf97a8e861c944286e6b2",
-    "opts": {},
-    "name": "Cli",
-    "inputRev?": "nightly",
-    "inherited": true}},
-  {"git":
-   {"url": "https://github.com/gebner/quote4",
-    "subDir?": null,
-    "rev": "e75daed95ad1c92af4e577fea95e234d7a8401c1",
     "opts": {},
     "name": "Qq",
     "inputRev?": "master",
     "inherited": true}},
   {"git":
-   {"url": "https://github.com/JLimperg/aesop",
+   {"url": "https://github.com/leanprover/lean4-cli",
     "subDir?": null,
-    "rev": "1a0cded2be292b5496e659b730d2accc742de098",
+    "rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa",
     "opts": {},
-    "name": "aesop",
+    "name": "Cli",
-    "inputRev?": "master",
+    "inputRev?": "nightly",
+    "inherited": true}},
+  {"git":
+   {"url": "https://github.com/leanprover-community/ProofWidgets4",
+    "subDir?": null,
+    "rev": "f1a5c7808b001305ba07d8626f45ee054282f589",
+    "opts": {},
+    "name": "proofwidgets",
+    "inputRev?": "v0.0.21",
     "inherited": true}},
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "67855403d60daf181775fa1ec63b04e70bcc3921",
+    "rev": "6747f41f28627bed83e6d5891683538211caa2c1",
     "opts": {},
     "name": "std",
     "inputRev?": "main",
     "inherited": true}},
   {"git":
-   {"url": "https://github.com/EdAyers/ProofWidgets4",
+   {"url": "https://github.com/leanprover-community/aesop",
     "subDir?": null,
-    "rev": "65bba7286e2395f3163fd0277110578f19b8170f",
+    "rev": "6749fa4e776919514dae85bfc0ad62a511bc42a7",
     "opts": {},
-    "name": "proofwidgets",
+    "name": "aesop",
-    "inputRev?": "v0.0.16",
+    "inputRev?": "master",
     "inherited": true}}],
  "name": "Game"}

lakefile.lean

@@ -17,11 +17,8 @@ def RemoteGameServer : Dependency := {
 /- Choose GameServer dependency depending on the environment variable `LEAN4GAME`. -/
 open Lean in
 #eval (do
-  let gameServerName := match (← IO.getEnv "LEAN4GAME") with
+  let gameServerName := if get_config? lean4game.local |>.isSome then
-    | none => ``RemoteGameServer
+    ``LocalGameServer else ``RemoteGameServer
-    | some "" => ``RemoteGameServer
-    | some "local" => ``LocalGameServer
-    | some _ => panic "env var LEAN4GAME must be 'local' or unset."
   modifyEnv (fun env => Lake.packageDepAttr.ext.addEntry env gameServerName)
   : Elab.Command.CommandElabM Unit)
 

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.1.0
+leanprover/lean4:v4.2.0