From a568458fb28f1841ddae47fa07050f2656b90845 Mon Sep 17 00:00:00 2001 From: joneugster Date: Wed, 22 Nov 2023 13:15:12 +0100 Subject: [PATCH] update to v4.2.0 --- .devcontainer/devcontainer.json | 2 +- .github/workflows/build.yml | 57 ++++++++++++++++++++++++---- .github/workflows/build_non_main.yml | 27 +++++++++++-- lake-manifest.json | 48 +++++++++++------------ lakefile.lean | 7 +--- lean-toolchain | 2 +- 6 files changed, 101 insertions(+), 42 deletions(-) diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json index 55b2e25..ab268b5 100644 --- a/.devcontainer/devcontainer.json +++ b/.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": { diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 9bae80d..4331a63 100644 --- a/.github/workflows/build.yml +++ b/.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 - run: docker build . --file Dockerfile --tag game:latest + - uses: actions/checkout@v4 - - name: Store docker container as an artifact - uses: ishworkh/docker-image-artifact-upload@v1 + - 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: 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? - 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,,}" + # - 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,,}" diff --git a/.github/workflows/build_non_main.yml b/.github/workflows/build_non_main.yml index 196483c..23c541c 100644 --- a/.github/workflows/build_non_main.yml +++ b/.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 - run: docker build . --file Dockerfile --tag game:latest + - uses: actions/checkout@v4 + + - 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 diff --git a/lake-manifest.json b/lake-manifest.json index 8400816..b53957d 100644 --- a/lake-manifest.json +++ b/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", - "opts": {}, - "name": "Cli", - "inputRev?": "nightly", - "inherited": true}}, - {"git": - {"url": "https://github.com/gebner/quote4", - "subDir?": null, - "rev": "e75daed95ad1c92af4e577fea95e234d7a8401c1", + "rev": "a387c0eb611857e2460cf97a8e861c944286e6b2", "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", - "inputRev?": "master", + "name": "Cli", + "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", - "inputRev?": "v0.0.16", + "name": "aesop", + "inputRev?": "master", "inherited": true}}], "name": "Game"} diff --git a/lakefile.lean b/lakefile.lean index c21e680..bbbd889 100644 --- a/lakefile.lean +++ b/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 - | none => ``RemoteGameServer - | some "" => ``RemoteGameServer - | some "local" => ``LocalGameServer - | some _ => panic "env var LEAN4GAME must be 'local' or unset." + let gameServerName := if get_config? lean4game.local |>.isSome then + ``LocalGameServer else ``RemoteGameServer modifyEnv (fun env => Lake.packageDepAttr.ext.addEntry env gameServerName) : Elab.Command.CommandElabM Unit) diff --git a/lean-toolchain b/lean-toolchain index f8f5f5c..2f868c6 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.1.0 +leanprover/lean4:v4.2.0