lean4checker option not working with lean4checker >= 4.27

[jamespjh]

Describe the bug
The lean4checker option invokes lean4checker's test.sh script, but that script no longer exists

Expected behavior
The tests should now be invoked with lake test (I think - I am not the author of lean4checker!)

Link to workflow where bug was encountered:

Locally, running on nektos act to test my build, added lean4checker: true:

      - uses: leanprover/lean-action@v1
        with:
          build: true
          test: true
          build-args: --wfail
          lean4checker: true
          lake-package-directory: languages/lean/basic

Details

• lean-action version: v1
• GitHub runner: ubuntu-latest

Additional context

https://github.com/leanprover/lean4checker/tree/v4.27.0 has no test.sh
https://github.com/leanprover/lean4checker/blob/v4.26.0/test.sh exists.

[jamespjh]

I think the fix is as simple as changing line 27 of https://github.com/leanprover/lean-action/blob/main/scripts/run_lean4checker.sh

from

test.sh
to
lake test

[austinletson]

Thank you for reporting the bug and for the suggested fix!

I have submitted a PR to fix this. Note that for Lean versions >= 4.28.x we now use the built in leanchecker so this fix will only impact repos on 4.27.0.

[austinletson]

Closed by #160