Auto update

[Seasawher]

@oliver-butterley @austinletson

Please do not merge this PR

This was implemented in an attempt to integrate lean-update actions into lean-action.

Summary of code

• The update action is only set to be performed when executed as schedule and when debugging options are passed.
• There is a part of the lean-update action that calls lean-action, but how to implement that part is difficult. A naive approach is likely to lead to more repetition of code, and commonisation would make it more complex.

My Opinion

I would suggest that the GitHub Action for automatic updates should be managed as a separate Action.Why not clone lean-update and create a repository under leanprover?

Reasons:

1. There is overlapping processing between lean-update and lean-action. (Run build and test on update, download mathlib cache, etc.) But this could be solved by calling lean-action from the lean-update side.
2. Combining lean-update and lean-action would complicate the management of if-conditions, make debugging difficult, and increase the scope of influence when changes are made.

Thanks. Please tell me your opinion.

[austinletson]

@Seasawher, thank you for exploring this!

Your reasoning makes sense to me, especially regarding the maintainability of a complex action.yml. I have encountered maintainability issues as the action.yml of lean-action has become more complicated.

I like your recommendation to keep lean-action and lean-update separated but reuse as much functionality from lean-action as is practical within lean-update to avoid duplicated functionality. (This is already the case to some extent.)

@oliver-butterley what do you think?

[oliver-butterley]

Merge the existing version of lean-update into lean-action❓ No

• Would be unpleasant from the code maintainability side, would create a very complex action.yml 😱. Also, currently lean-update uses lean-action in order to test if an update attempt works.
• Currently lean-update isn't sufficiently tested for us to consider it v1 release material, confusing to the user if one functionality of the action were considered alpha whilst the rest is relatively solid.

I agree with @Seasawher's opinion on the current versions of the actions:

Combining lean-update and lean-action would complicate the management of if-conditions, make debugging difficult, and increase the scope of influence when changes are made.

Eventually merge lean-update into lean-action❓

Keep separate because:

• The tasks performed by lean-action and lean-update fit into different categories in the sense that the first is stuff that would run on a CI workflow, typically to confirm a PR works correctly, whereas the latter would run on cron and is likely to open a PR, open an issue or commit directly.
• Reducing the functionality of each for easier maintainability of the code.

Merge because:

• One action to rule them all, fits the pattern already established in lean-action to have a single action with multiple functionality selected by options.
• There is functionality that can be shared by the two actions.

Next steps for lean-update❓

• Test lean-update in more places. @Seasawher has already been doing this for a while. @pitmonticone has just started testing it in various projects and getting valuable feedback.
• Make sure that users can have it running on cron in their repo with minimal problems even if rather unaware of git and github technicalities. This includes making sure that it is hard to create a huge mess by accident and that feedback to the user is clear.
• Convert lean-update to a typescript/javascript action to better deal with the logic, improve the feedback to the user (particularly when problems occur) and improve the way that PR and issues are opened/closed without relying on other actions.
• Massively improve the feedback to the user when problems are detected.
• Move development to a repo within lean-prover?
• Prepare a roadmap to eventually merge with 'lean-action'?

[Seasawher]

@austinletson

Test lean-update in more places. @Seasawher has already been doing this for a while. @pitmonticone has just started testing it in various projects and getting valuable feedback.

I agree that lean-update should be introduced and tested in more repositories. What do you think?

[austinletson]

@austinletson

Test lean-update in more places. @Seasawher has already been doing this for a while. @pitmonticone has just started testing it in various projects and getting valuable feedback.

I agree that lean-update should be introduced and tested in more repositories. What do you think?

I agree with the next steps for lean-update outlined above. To automatically add lean-update cron workflows to lake new, it should be tested on various projects as well as iron out the user experience and feedback, with a special focus on this point that Oliver made:

Make sure that users can have it running on cron in their repo with minimal problems even if rather unaware of git and github technicalities. This includes making sure that it is hard to create a huge mess by accident and that feedback to the user is clear.

Should we post in Zulip that we recommend keeping the actions separated for now and ask Kim if we can move the lean-update repo to lean-prover to prepare for a v1 release and then subsequently add a lean-update workflow when a new lean project is create with lake new?

[pitmonticone]

oliver-butterley/lean-update#39

[pitmonticone]

Solved.

[Seasawher]

Should we post in Zulip that we recommend keeping the actions separated for now and ask Kim if we can move the lean-update repo to lean-prover to prepare for a v1 release and then subsequently add a lean-update workflow when a new lean project is create with lake new?

nice!