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

make this action mathlib-independent #17

Closed Seasawher closed 5 months ago

Seasawher commented 5 months ago

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 commented 5 months ago

@oliver-butterley please review this PR.

oliver-butterley commented 5 months ago

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 commented 5 months ago

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

Seasawher commented 5 months ago

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 commented 5 months ago

:thinking: 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 commented 5 months ago

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 commented 5 months ago

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