From 86b1a33d706021375a608ceba94f6b77ae310fce Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Thu, 12 Mar 2026 16:47:57 -0400 Subject: [PATCH 1/2] ci: set TEST_ARGS manually --- .github/workflows/lean_action_ci.yml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index ec930b8ca..1053d8a53 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -14,6 +14,10 @@ jobs: runs-on: ubuntu-latest steps: - uses: actions/checkout@v4 + - name: Set TEST_ARGS manually + run: | + echo "TEST_ARGS='--wfail --iofail'" >> $GITHUB_ENV + shell: bash - uses: leanprover/lean-action@v1 with: build-args: "--wfail --iofail" From d3d8ed0ea88f34869a5a42ff09f1a9a06f901ed5 Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Thu, 12 Mar 2026 16:54:30 -0400 Subject: [PATCH 2/2] implicit_reducible --- CslibTests/DFA.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/CslibTests/DFA.lean b/CslibTests/DFA.lean index f78e47c0d..3fc2af1f6 100644 --- a/CslibTests/DFA.lean +++ b/CslibTests/DFA.lean @@ -17,6 +17,7 @@ inductive Floor where | two deriving DecidableEq +@[implicit_reducible] def Floor.fintype : Fintype Floor := { elems := {.one, .two} complete floor := by grind [Floor] @@ -29,6 +30,7 @@ inductive Direction where | down deriving DecidableEq +@[implicit_reducible] def Direction.fintype : Fintype Direction := { elems := {.up, .down} complete dir := by grind [Direction]