make this action mathlib-independent

[Seasawher]

I tested this action here: https://github.com/Seasawher/mk-exercise

Changed so that Lean version updates are also performed in repositories that are not downstream of mathlib.

[Seasawher]

@oliver-butterley please review this PR.

[oliver-butterley]

Thanks for the PR! Sorry it's taken a while for me to respond.

Yes, great that it also handles more cases. I think at the moment there is part of the logic that isn't correct:

At the moment the action updates the lean-toolchain file by checking which version of lean is used by the latest version of mathlib. If the project doesn't depend on mathlib this isn't the right thing to do.

What is the right thing to do? Update lean-toolchain to the latest release of lean? or the latest stable release?

[Seasawher]

latest (pre)release of Lean.
now it should be v4.9.0-rc1

[Seasawher]

I think lake update overwrite lean-toolchain if the repository depends on mathlib. so the following workflow may work even if the repo is mathlib-downstream.

1. update lean-toolchain to latest release of Lean via downloading. don't fetch mathlib's toolchain!
2. run lake update

[oliver-butterley]

🤔 that could work. The mathlib post update hook which updates lean-toolchain doesn't always work but the only situations where I have seen it fail are when the current version of lean is too old. Consequently it is likely that your proposal is fine.

Is there an easy way to update lean-toolchain to the latest released version of lean? We could query the github api for releases of lean and then use that. Unless there is an easy way built into lake?

[Seasawher]

I think the command gh release list --repo leanprover/lean4 --limit 1 can get the latest release/prerelease of Lean 4. This will probably work, I tested it with mk-exercise.

[oliver-butterley]

Yes, that's a great solution, nicely done!

[Seasawher]

Note: when new release of lean-action come, this line should be updated.