Add check NoCI to CI, but allow failure

utensil · Oct 22, 2024 · cadb3b5 · cadb3b5
1 parent 37e5713
commit cadb3b5
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 4 deletions.
diff --git a/.github/workflows/lean4.yml b/.github/workflows/lean4.yml
@@ -82,11 +82,16 @@ jobs:
           # lake env leanInk analyze examples/Help.lean
           cd ..
           just pages lean4
-      - name: Try mk_all
+      # - name: Try mk_all
+      #   shell: bash
+      #   run: |
+      #     cd lean4
+      #     rm -f .lake/packages/mathlib/lakefile.lean
+      #     mv lakefile-for-mathlib.lean .lake/packages/mathlib/lakefile.lean
+      #     lake -R exe mk_all || true
+      - name: Try check NoCI examples
         shell: bash
         run: |
           cd lean4
-          rm -f .lake/packages/mathlib/lakefile.lean
-          mv lakefile-for-mathlib.lean .lake/packages/mathlib/lakefile.lean
-          lake -R exe mk_all || true
+          ./check_noci.sh || true
 
diff --git a/lean4/check_noci.sh b/lean4/check_noci.sh
@@ -0,0 +1,11 @@
+# leanpkg configure
+# leanproject get-mathlib-cache
+
+set -e
+set -o pipefail
+
+export PATH=$HOME/.elan/bin:$PATH
+
+echo "checking RockPaperScissor"
+lake env lean --quiet --run Playground/NoCI/Zulip/RockPaperScissor.lean < Playground/NoCI/Zulip/RockPaperScissor_test1.txt
+