lean-upgrade-action

Stream: general

[Ruben Van de Velde]

I attempted to make lean-upgrade-action work for lean 4 in https://github.com/leanprover-contrib/lean-upgrade-action/pull/10 , but I don't know how to test it. Any suggestions?

CC @Rob Lewis

[Kim Morrison]

I think a rewrite without using python, so it can be used in github CI as an action, would be worthwhile.

[Kim Morrison]

See also some related work happening at https://github.com/leanprover/lean4/issues/3950. I think for now @Austin Letson is thinking that the upgrade action (which would have to be triggered via cron) is out of scope for the initial version.

[Ruben Van de Velde]

Isn't this an action?

[Kim Morrison]

Oh, hmm, sorry, you're absolutely right. It seems pretty heavy weight for an action to rely on docker and python, in any case!

[Ruben Van de Velde]

I have no opinion. My idea was "something is better than nothing" :)

[Oliver Butterley]

Yes, the use of python for this action is rather heavy handed. How about a composite action for simplicity? This is what is being done for the testing action.

We have been testing this workflow which does something like the lean-upgrade-action. We could use this as the basis for the composite workflow so it is something easy for user to insert into their own project.

In which case, what precisely do we want the action to do? Check for update and then... open PR? auto update? open issue if there something which requires human intervention?

[Ruben Van de Velde]

Auto update if possible, open an issue otherwise

[Ruben Van de Velde]

This existed for lean 3 and worked well. I'd prefer having something similar instead of / while waiting for a complete redesign

[Oliver Butterley]

OK, I'll come back with a solid python-free version before the end of the weekend.

[Kim Morrison]

Ideally:

1. There would be a choice between auto-update and open a PR. (For some repos it's just not acceptable to have a bot push to master.)
2. When there is a problem, we check if there is already an open issue about problems updating, and don't create anymore noise if so.

[Oliver Butterley]

That's fine, the action can have default behaviour but also can be configured with options to suit different use cases.

[Oliver Butterley]

Here is a complete draft version of the action: https://github.com/oliver-butterley/lean-update-action

It has options for various different behaviour as requested above. There are a few niceties that I plan to add soon but all main functionality is present. I've tested it in various scenarios and seems to be fine but definitely an alpha version for the moment.

I would like to fix precisely how the action should behave. Others who have used Lean much more than me need to say what user experience is desired from such an action. All feedback very welcome and then I can modify to be it just as wanted!

[Oliver Butterley]

Currently the possibility to commit or open PRs or issues is internal to the action. However, after creating this version, I thought it might be better to have a more minimal action that just does the core behaviour of trying to update lean and checking if it is fine. Then it can be used in workflows for any given repo together with other actions to do the required follow tasks.

Like this seems rather cleaner to me and flexible for customization. Additionally I would have clear documentation which explains exactly the workflow yml to use for common use cases and so it was very easy for those with zero experience of github actions.

[Ruben Van de Velde]

As long as I can set it up with minimal effort and maintenance, I don't have an opinion on the design :)

[Yakov Pechersky]

My suggestion is to keep the functionality you have now, but with the option of creating a new PR left to a separate action, like gr2m/create-or-update-pull-request-action@v1.x

Here is an example of a repo I'm aware of that does a daily scheduled check against an upstream, changes some files accordingly, and makes a PR with the changes:
https://github.com/kuelumbus/rdkit-pypi/blob/09b99c2886c41d8da303140a925d12c5f41e7882/.github/workflows/check_rdkit_version.yml#L20-L48

[Yakov Pechersky]

Ah, I see, your action is inlining a third-party action in a workflow step

[Yakov Pechersky]

So, in that case, I have to say that run: lake update needs a warning -- that it should only be that for those that are dependent on Mathlib, not Mathlib forks/clones

[Yakov Pechersky]

Additionally, if the action, on fail, makes an issue -- and it is on cron, you'd need it to be aware of already existing issues so that you don't get daily fail issues created

[Oliver Butterley]

Yakov Pechersky said:

Additionally, if the action, on fail, makes an issue -- and it is on cron, you'd need it to be aware of already existing issues so that you don't get daily fail issues created

Yes, this can be done by having the issue with a particular name and not open another if such an issue is still open.

[Oliver Butterley]

Yakov Pechersky said:

So, in that case, I have to say that run: lake update needs a warning -- that it should only be that for those that are dependent on Mathlib, not Mathlib forks/clones

Good point. Actually this could be tested inside the action before running the update.

[Oliver Butterley]

@Austin Letson Will the lean action you are working on have the functionality that it can be asked to check for available updates and then check if the updated version builds?

In which case it might be better just writing documentation which explains how to use that action in a workflow for update tasks with auto committing / opening PRs / opening issues.

[Austin Letson]

The action I am working on currently doesn't currently have this functionality. It is designed to be run on push/ when opening a PR (not run periodically).

I think it is possible to support both use cases (push/PR and periodic) with a single action or a single repository, but I haven't explored in depth.

Either way, I agree we should align the documentation of the different actions available to lean users.

[Oliver Butterley]

@Austin Letson Thanks for the clarification. Also, let me know if I can help with particular tasks for lean-action. Sounds like it is good to complete that to a solid first stage before adding other features.

[Austin Letson]

@Oliver Butterley Thanks! A few things which would be helpful if they interest you:

• I am in the process of creating an alpha release to get feedback from the lean community. If you know of existing lean projects which would be candidates for alpha testing in their CI, please let me know!
• Since you have some experience with GitHub actions, I would appreciate any feedback on the implementation of lean-action, mainly the action.yml, regarding improvements or missing best practices. Feel free to create issues in the repo or message on Zulip and I can create an issue.
• There are a few existing issues already created which may be of interest to you. I wasn't planning to include these in the initial alpha release in order to get feedback more quickly, but I don't have a concrete plan.

[Kim Morrison]

@Austin Letson, your alpha release testing looks great! I think it's time to test this in production.

We're initially restricted to projects that already have lake test set up (but this is something that I'm hoping will expand quickly in the near term), I think.

Batteries may well be a candidate as soon as batteries#787 is merged.

[Kim Morrison]

https://github.com/leanprover-community/import-graph is now set up for lake test, so is another candidate for using lean-action.

[Kim Morrison]

Similarly Aesop is now using lake test, and could also try out lean-action.

[Austin Letson]

Yay! @Kim Morrison one thing I will note here is that projects which don't use lake test can still use lean-action as long as they set test: false (see this example)

[Austin Letson]

Created PRs for import-graph and Aesop.

[Austin Letson]

I believe we need to add a few more features to lean-action before it can fully support the current CI in batteries. batteries calls lake build with-Kwerror(link) which is configured here in lakefile.lean.

Currently lean-action doesn't support passing options to lake through -K. I have created an issue for it here.

[Kim Morrison]

I merged the import-graph PR.

[Ruben Van de Velde]

That will also be an issue for projects depending on docgen only in ci, until the setup for that changes (which I believe is planned, but I don't know the timeline)

[Kim Morrison]

If there's no sign of trouble from that in the next day or two (hopefully we can think of some stress tests?) we can proceed with aesop.

[Kim Morrison]

I think we're hoping for lake install in v4.9.0-rc1 (June 1?), but there's a decent chance we don't get it right first time to actually remove the meta ifs.

[Kim Morrison]

I've merged https://github.com/leanprover-community/aesop/pull/136, bringing lean-action to Aesop.