lean-update action

Stream: general

[Asei Inoue]

I want to change the branch protection rules for lean-update, but it seems I don’t have the necessary permissions.
Could you grant me the required permissions?

https://github.com/leanprover-community/lean-update

[Kim Morrison]

@Asei Inoue, you already have "maintain" access there, so you should be able to change branch protection rules.

[Bryan Gin-ge Chen]

It looks like only people with the "Admin" role can change branch protection rules, according to GitHub.

[Kim Morrison]

@Asei Inoue, could you let us know how you'd like the rules changed?

[Asei Inoue]

@Kim Morrison Thank you.

I would like the following protection rules to be removed:

• The protection rule that prevents deletion of the develop branch

• The protection rule that prevents direct pushes to the main branch

[Kim Morrison]

Preventing direct pushes to the main branch seems like a very bad idea?

[Kim Morrison]

I've deleted the ruleset for develop.

[Asei Inoue]

@Kim Morrison Thank you!!

[Asei Inoue]

I am the sole maintainer of the lean-update action, but over the past few months I’ve lost focus and ended up neglecting it. I feel sorry for @Oliver Butterley and for those who were counting on it. I'm sorry.

[Oliver Butterley]

Thanks @Asei Inoue, you are thoughtful. Personally I no longer use this action because there are other ways I can achieve the same thing now. Anyway, you don't need to feel any obligation, you have to prioritize your time, all of us must do so.

[Asei Inoue]

I regularly use the lean-update action, but I feel it would become unnecessary if a more general version of the mathlib-update-action were developed.
Is there any plan to develop a generalized version of the mathlib-update-action?

[Asei Inoue]

who is the maintainer of https://github.com/leanprover-community/mathlib-update-action?

[Yaël Dillies]

@Anne Baanen I believe?

[Anne Baanen]

I am indeed currently the maintainer of mathlib-update-action :)

Asei Inoue said:

Is there any plan to develop a generalized version of the mathlib-update-action?

If we can make a concrete feature list, then sure! Right now there are a few ideas for how to keep in sync between Lean releases and dependency updates, but I do not believe the community agrees that one is indeed the best.

[Asei Inoue]

@Anne Baanen

I see, I didn’t know there was a debate about this. The current behavior of the lean-update action is to “always update to the latest release (including RCs),” but are there people who want something different?

[Anne Baanen]

I am not sure if it's so much a debate, we're still in the brainstorming phase I'd say :) Releases are good to follow, but the issue is more that updating to a release only happens once per month, and projects want to update more frequently than that, while still keeping versions consistent across Mathlib dependencies.

[Asei Inoue]

Do you mean that you want to run lake update at any frequency, and check whether there are updates and, if so, whether the build/tests still pass? If that’s the case, that’s exactly what lean-update is currently doing.

[Asei Inoue]

@Anne Baanen

[Anne Baanen]

That works well for individual projects! But it's not a solution for the ecosystem. For example, if two projects run lake update weekly but on different days, then their Mathlib versions will mismatch and it will be hard to import both projects simultaneously without errors.

[Kevin Buzzard]

Oh I was thinking about this recently. In the unlikely event that someone wants to depend on FLT, we will run into this issue too. I had wondered whether the correct thing to do would be to bump FLT weekly (which we are doing already) but also to ensure that we bump FLT each time mathlib has a new commit which changes the version of Lean they're doing (whether it be an RC or official release), and then make sure we have a tag indicating each such bump. Does mathlib have a new tag each time it bumps to a new version of Lean? I have no time right now to think about this sort of thing, I am only just learning about github actions.

[Ruben Van de Velde]

I think we want to support

1. Projects that depend on other non-mathlib projects
2. Projects that update more than once a month

but it's much lower priority to support

3. Projects that depend on other projects and want to update more than once a month

[Kim Morrison]

Kevin Buzzard said:

Does mathlib have a new tag each time it bumps to a new version of Lean?

Yes, Batteries/Mathlib/Cslib all create v4.X.0 and v4.X.0-rcK tags the first time they move to a new toolchain.

(Mathlib is a bit exceptional, but all the other repos in the "toolchain release process" actually make sure that these tagged releases depend on the corresponding tagged release of each upstream dependency.)

[Asei Inoue]

I am thinking about the features that the lean-update action should have.
One feature I personally want is: “When the lean-toolchain file is changed, create a PR, and once the PR is merged, issue a release tag and create a release.”
I have a question regarding implementing this.
What should the tag name be when updating the lean-toolchain?
If we use something like v4.22.0, it might be confused with the repository’s own version.
Would something like lean/v4.22.0 be better?

[Asei Inoue]

@Anne Baanen

But it's not a solution for the ecosystem. For example, if two projects run lake update weekly but on different days, then their Mathlib versions will mismatch and it will be hard to import both projects simultaneously without errors.

I hadn’t even thought of that problem! Thank you for pointing it out.
As a solution, I think one option is to limit updates of the mathlib version that the repository depends on to “only commits that have a tag.”
In other words, edit the lakefile to specify the mathlib version by tag, and then run lake update.

[Kim Morrison]

I agree we should move away from using the v4.X.0 tags, but this is a big decision, possibly not to be made in this thread, we'll see. :-)

[Kim Morrison]

One possibility is that we put the toolchain version number after a + symbol in the tag name, sort of like the "metadata" from SemVer. (I'm not claiming this suggestion is semver-consistent!!!)

If a project doesn't have releases, e.g. Mathlib, it could just call these tags master+v4.22.0, which hopefully is relatively easy to understand as "the master branch, as some moment (in fact, first) when it is on toolchain v4.22.0".

If the project does have releases, either using SemVer, CalVer, or something else, it could still append these +v4.22.0s to tags. So for example ProofWidgets might release v0.0.69+v4.22.0 indicating it is version 0.0.69 of the library itself, in a form that uses the v4.22.0 toolchain. That's not super intuitive to me, and suggests an even more verbose style, e.g. v0.0.69+toolchain-v4.22.0 (and similarly master+toolchain-v4.22.0 for Mathlib).

[Asei Inoue]

That means it’s not clear what exactly should be implemented in the lean-update action.

[Kim Morrison]

Yes -- the community needs to discuss this. Or just agree to my proposal above. :-)

[Kim Morrison]

But for now I think the tooling should support the status quo, which is that these tags are simply of the form v4.X.Y-rcK.

[Asei Inoue]

How about attaching multiple tags?
When the Lean toolchain changes, we could use a tag like lean/v4.X.Y, and for the library’s release, we could use a tag like vA.B.C.

[Asei Inoue]

At first, I wanted the lean-update action or its successor to be set up automatically when running lake new. However, when creating a GitHub repository, by default GitHub Actions does not have permission to create Pull Requests, which results in an error. Since having this error appear every time is annoying, I came to think it might be better if it is not set up during lake new.

[Asei Inoue]

Can you silence “PR permission denied” error?
If so, “lake new” could set up lean-update action.

[Asei Inoue]

I set up tests for the lean-update action so that whenever a PR is opened, the tests will run automatically.
Since I don’t have much knowledge about testing GitHub Actions, I’d love to hear from anyone who is more experienced in this area.

[Asei Inoue]

Now that I’ve managed to set up the minimum set of tests, I expect it will be easier to continue developing lean-update from here on.
I’m developing this GitHub Action primarily because I want to use it myself, and I’m satisfied with its current features, but I’ll be more than happy to hear your requests as well.

[Asei Inoue]

At first, I wanted the lean-update action or its successor to be set up automatically when running lake new. However, when creating a GitHub repository, by default GitHub Actions does not have permission to create Pull Requests, which results in an error. Since having this error appear every time is annoying, I came to think it might be better if it is not set up during lake new.

I think that if permissions are explicitly specified when defining the workflow, it should run without errors.
Therefore, it might be fine to bundle lean-update when running lake new.

[Adam Topaz]

@Asei Inoue Thanks for your work on lean-update. I noticed that when the action checks for the latest version of mathlib here it doesn't take into account release candidates. Is this intended? I'm happy to PR a fix if not.

[Asei Inoue]

@Adam Topaz

not intended! It seemed to have been working until now, but was that just by chance?

[Asei Inoue]

could you open a issue or PR?