ci: update (#45)

Author: astrainfinita

.github/workflows/build.yml

@@ -1,6 +1,5 @@
 on:
   push:
-  pull_request:
 
 name: continuous integration
 
@@ -16,23 +15,6 @@ jobs:
           all_but_latest: true
           access_token: ${{ github.token }}
 
-  check_imported:
-    name: Check all files imported
-    runs-on: ubuntu-latest
-    steps:
-      - name: cleanup
-        run: |
-          find . -name . -o -prune -exec rm -rf -- {} +
-
-      - uses: actions/checkout@v4
-
-      - name: update Algorithm.lean
-        run: |
-          git ls-files 'Algorithm/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Algorithm.lean
-
-      - name: check that all files are imported
-        run: git diff --exit-code
-
   build:
     name: Build
     runs-on: ubuntu-latest
@@ -56,18 +38,12 @@ jobs:
       - 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
+          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
           ./elan-init -y --default-toolchain none
           echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
 
       - uses: actions/checkout@v4
 
-      # We update `Algorithm.lean` as a convenience here,
-      # but verify that this didn't change anything in the `check_imported` job.
-      - name: update Algorithm.lean
-        run: |
-          find Algorithm -name "*.lean" | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Algorithm.lean
-
       - name: If using a lean-pr-release toolchain, uninstall
         run: |
           if [[ $(cat lean-toolchain) =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then
@@ -94,17 +70,71 @@ jobs:
           rm -rf .lake/packages/proofwidgets/.lake/build/ir
 
       - name: get cache
+        id: get
+        run: |
+          rm -rf .lake/build/lib/Mutable/
+          rm -rf .lake/build/lib/Algorithm/
+          # Fail quickly if the cache is completely cold, by checking for Mathlib.Init
+          lake exe cache get Mathlib.Init
+          lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
+
+      - name: update {Mutable, Algorithm}.lean
+        id: mk_all
         run: |
-          lake exe cache clean
-          lake exe cache get
+
+          if ! lake exe mk_all --check
+          then
+            echo "Not all lean files are in the import all files"
+            echo "mk_all=false" >> "${GITHUB_OUTPUT}"
+          else
+            echo "mk_all=true" >> "${GITHUB_OUTPUT}"
+          fi
 
       - name: build algorithm
         id: build
         uses: liskin/gh-problem-matcher-wrap@v3
         with:
           linters: gcc
           run: |
-            bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build -KCI | tee stdout.log"
+            bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
+
+      - name: Check {Mutable, Algorithm}.lean
+        run: |
+          if [ ${{ steps.mk_all.outputs.mk_all }} == "false" ]
+          then
+            echo "Please run 'lake exe mk_all' to regenerate the import all files"
+            exit 1
+          fi
+
+      - name: check for noisy stdout lines
+        id: noisy
+        run: |
+          buildMsgs="$(
+            ##  we exploit `lake`s replay feature: since the cache is present, running
+            ##  `lake build` will reproduce all the outputs without having to recompute
+            lake build Mutable Algorithm |
+            ##  we filter out the output lines that begin with `✔ [xx/yy]`, where xx, yy
+            ##  are either numbers or ?, and the "Build completed successfully." message.
+            ##  We keep the rest, which are actual outputs of the files
+            awk '!($0 ~ "^\\s*✔ \\[[?0-9]*/[?0-9]*\\]" || $0 == "Build completed successfully."){ print $0 }')"
+          if [ -n "${buildMsgs}" ]
+          then
+            printf $'%s\n' "${buildMsgs}"
+            exit 1
+          fi
+
+      - name: verify `lake exe graph` works
+        run: |
+          lake exe graph
+          rm import_graph.dot
+
+      # - name: test algorithm
+      #   id: test
+      #   uses: liskin/gh-problem-matcher-wrap@v3
+      #   with:
+      #     linters: gcc
+      #     run:
+      #       lake test
 
       - name: check for unused imports
         id: shake
@@ -120,10 +150,3 @@ jobs:
         with:
           linters: gcc
           run: env LEAN_ABORT_ON_PANIC=1 lake exe runLinter Algorithm
-
-      - name: check for noisy stdout lines
-        id: noisy
-        run: |
-          grep --after-context=1 "stdout" stdout.log && ret=0
-          grep --after-context=1 "stderr" stdout.log && new=0
-          if [ "${ret}" == "0" ] || [ "${new}"  == "0" ]; then exit 1; fi

lakefile.lean

@@ -34,3 +34,7 @@ extern_lib libleanffi pkg := do
   let name := nameToStaticLib "leanffi"
   let ffiO ← ffi.o.fetch
   buildStaticLib (pkg.nativeLibDir / name) #[ffiO]
+
+-- @[test_driver]
+-- lean_exe test where
+--   srcDir := "scripts"

scripts/test.lean

@@ -0,0 +1,21 @@
+/-
+Copyright (c) 2024 Kim Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+open IO.Process
+open System
+
+/--
+Run tests, via the Batteries test runner.
+
+When https://github.com/leanprover/lean4/issues/4121
+"allow using an upstream executable as a lake `@[test_runner]`"
+is resolved, this file can be replaced with a line in `lakefile.lean`.
+-/
+def main (args : List String) : IO Unit := do
+  -- ProofWidgets and Batteries may not have been completely built by `lake build` yet,
+  -- but they are needed by some tests.
+  _ ← (← spawn { cmd := "lake", args := #["build", "ProofWidgets", "Batteries"] }).wait
+  let exitcode ← (← spawn { cmd := "lake", args := #["exe", "batteries/test"] ++ args }).wait
+  exit exitcode.toUInt8

test/Mutable/thunk1.lean

@@ -22,25 +22,43 @@ protected def Thunk'.get (x : Thunk' α) : α :=
 
 /-! lean4/tests/lean/thunk.lean -/
 
-#eval (Thunk'.pure 1).get
-#eval (Thunk'.mk fun _ => 2).get
-#eval
+/-- info: 1 -/
+#guard_msgs in #eval
+  (Thunk'.pure 1).get
+/-- info: 2 -/
+#guard_msgs in #eval (Thunk'.mk fun _ => 2).get
+/--
+info: 3
+4
+5
+-/
+#guard_msgs in #eval
   let t1 := Thunk'.mk fun _ => dbg_trace 4; 5
   -- let t2 := Thunk'.mk fun _ => dbg_trace 3; 0
   -- let v2 := t2.get
   let v2 := dbg_trace 3; 0
 
   let v1 := t1.get
   v1 + v2
-#eval
+/--
+info: 6
+7
+8
+-/
+#guard_msgs in #eval
   let t1 := Thunk'.pure 8 |>.map fun n => dbg_trace 7; n
   -- let t2 := Thunk'.mk fun _ => dbg_trace 6; 0
   -- let v2 := t2.get
   let v2 := dbg_trace 6; 0
 
   let v1 := t1.get
   v1 + v2
-#eval
+/--
+info: 9
+10
+11
+-/
+#guard_msgs in #eval
   let t1 := Thunk'.pure 11 |>.bind fun n => dbg_trace 10; Thunk'.pure n
   -- let t2 := Thunk'.mk fun _ => dbg_trace 9; 0
   -- let v2 := t2.get

test/Mutable/thunk1.lean.expected.out

@@ -26,4 +26,5 @@ def test (t : Thunk' Nat) (n : Nat) : Nat :=
 def main : IO Unit :=
   IO.println (toString (test (compute 1) 100000))
 
-#eval main
+/-- info: 10000000000 -/
+#guard_msgs in #eval main -- TODO: 超时中断

test/Mutable/thunk2.lean

@@ -3,15 +3,24 @@ import Algorithm.Data.UnionFind
 abbrev Vector := Batteries.Vector
 abbrev UF := UnionFind (Fin 10) (Vector (Fin 10) 10) (Vector Nat 10)
 
-#eval show IO Unit from do
+/--
+info: 1
+2
+-/
+#guard_msgs in #eval show IO Unit from do
   let mut uf : UF := default
   IO.println (uf.find 1)
   uf := uf.union 1 2
   uf := uf.union 3 4
   uf := uf.union 2 4
   IO.println ((Quot.unquot (Mutable.get uf)).val.parent[(1 : Fin 10)])
 
-#eval show IO Unit from do
+/--
+info: 1
+4
+4
+-/
+#guard_msgs in #eval show IO Unit from do
   let mut uf : UF := default
   IO.println (uf.find 1)
   uf := uf.union 1 2