search

oliver-butterley / lean-update

The action attempts to update Lean and Mathlib. If an update is available then the updated version is tested. This allows for automatic committing of the updated project, opening PRs or opening issues.
MIT License
6 stars 2 forks source link

run `lake test` #16

Closed Seasawher closed 4 months ago

Seasawher commented 5 months ago

lake test need to be executed.

I think this should be done by https://github.com/leanprover/lean-action.

(There should be a function in lenprover/lean-action to automatically check whether test_runner is registered or not. I created a PR for leanprover/lean-action)

Seasawher commented 5 months ago

related: https://github.com/leanprover/lean-action/pull/55

oliver-butterley commented 5 months ago

Yes, I absolutely agree, it should use lean-action and also run the test. When I last looked it seemed that the test functionality of lean-action wasn't yet working properly. As soon as it is ready and functioning this should be standard.

Seasawher commented 5 months ago

good news! see: https://github.com/leanprover/lean-action/pull/61

oliver-butterley commented 5 months ago

Looks good! As far as I see, it will work fine if we just use lean-action with the auto-config option.