lean-action

Stream: general

[Bolton Bailey]

@Kim Morrison recently recommended to me that I use lean-action to CI my lean project. This seems to be working well, kudos to @Austin Letson for making it. I have a few questions:

• Who pays for the compute to run this action? Is there a limit to how many times I can run it per month?
• Is there an example of a repo with testing set up, so that I can get testing to work?

Thanks!

[Utensil Song]

You may check out leanprover-community/aesop#135 and leanprover-community/aesop#136 .

Your own Github account pays for the compute, which is free for public repo.

[Austin Letson]

• Is there an example of a repo with testing set up, so that I can get testing to work?

In addition to aesop, import-graph also uses lean-action to run lake test. I just created a PR to add these examples to the README.md.

[Austin Letson]

@Bolton Bailey As lean users start to use the alpha version, we want to collect feedback to improve. If you experience issues or have recommendations for how we could improve docs/setup/usage let us know! You can create an issue or message on Zulip.

[Utensil Song]

@Austin Letson My personal feedback is it would be nice to support specifying the directory of the Lean project, https://github.com/cedar-policy/cedar-spec/tree/main/cedar-lean is one such example.

This would also support multiple Lean projects in one repo, via multiple lean-action steps.

[Austin Letson]

@Utensil Song Thanks for pointing this out. I created an issue to support this use case.

[Kim Morrison]

Bolton Bailey said:

• Is there an example of a repo with testing set up, so that I can get testing to work?

Batteries now uses lake test, and #12943 is the Mathlib PR (awaiting-review for 4 days, hint hint) that will enable lake test in Mathlib.

We need to make a few changes in Lake that will not land until at least v4.9.0-rc1, but we are hoping that lake test (and lean-action) will be viable for everyone soon, and indeed that lake new will set up your project to use lean-action.

[Utensil Song]

Austin Letson said:

Utensil Song Thanks for pointing this out. I created an issue to support this use case.

Thanks for the issue, per my test with lean-action, working-directory doesn't work with use, it only works with run etc.

[Austin Letson]

Utensil Song said:

Austin Letson said:

Utensil Song Thanks for pointing this out. I created an issue to support this use case.

Thanks for the issue, per my test with lean-action, working-directory doesn't work with use, it only works with run etc.

Ah okay. In that case we can definitely create an input that allows users to specify a Lean directory directly.

[Austin Letson]

For those who are already trying out lean-action, v1-beta is now available :tada:

v1-beta includes usability improvements and a new build-args input to support additional use cases, such as batteries lake build -Kwerror.

The release notes are on GitHub.

[Austin Letson]

Related, I just opened a PR to use lean-action in batteries.

[Austin Letson]

Also, thank you to @Oliver Butterley for driving many of the improvements in this version!

[Kim Morrison]

Thanks for doing this!

For me the main regression is that the CI output is less easily interpretable.

Can we achieve separate top level items for build, test, etc? I'm not sure how that would be done, at this point.

[Kim Morrison]

Further, could you run some tests in which you break the build, break a test, and break the linter, and them link from the PR description to the build outputs, so we can see what they each look like?

[Kim Morrison]

(i.e. do these just by pushing commits to the PR itself; we squash merge in the end, so once they are reverted after CI has run, these commits can harmlessly stay in the PR history)

[Oliver Butterley]

@Kim Morrison design the desired user interface that is best for those who will use the tooling and we can make it happen! Not everything is possible but most things are. What exact details should be seen and where should they be seen?

Actions can output information in three ways: logs, annotations and summaries.

• The log unavoidably contains a lot of lines of info and so is not useful as an overview.
• Annotations are displayed on the job summary page and are of type (notice | warning | error). (This is the place where all the "Node.js 16 actions are deprecated" messages are written.) Annotations can have links to files and lines within those files. Creating the action we have total control on exactly what the annotations are.
• Summaries give the most flexibility. This is markdown formatted, appears on the job summary page and we have total control on what is written there. Possibly a table displaying the steps and concise (and colourful) info on the results from each?

Additionally the action could produce a markdown formatted summary which is then used by another action to be sent as a message some place if that happens to be useful for the particular PR / reviewing setup.

[Kim Morrison]

Okay! :-)

My basic complaint is that pre-lean-action, we can easily see whether a PR failed at build, test, or lint, as soon as we click through to the build output, e.g.

Screenshot-2024-05-22-at-5.01.07PM.png

from https://github.com/leanprover-community/batteries/actions/runs/9143437388/job/25140072702?pr=782

vs

Screenshot-2024-05-22-at-5.01.25PM.png

from https://github.com/leanprover-community/batteries/actions/runs/9181778942/job/25249274199?pr=805 where all the good stuff is hidden in the lean-action step, and even when we open that we only get

Screenshot-2024-05-22-at-5.01.36PM.png

where it is not at all obvious where the build / test /lint segments of the output start and stop.

[Kim Morrison]

It's true that "The log unavoidably contains a lot of lines of info", but I don't think it's true that "and so is not useful as an overview". Just plain text section headings separating things would help.

But really we want separate sections on the build output screen, which I think can only be achieved by having separate steps.

[Sebastian Ullrich]

Is there something fundamental that the step sections can do that the nested groups can't? If the output was cleaned up into

> Lake Build
> Lake Test
> Lint

would that be sufficient?

[Utensil Song]

One way is to make it to have more action steps like https://github.com/quarto-dev/quarto-actions, so the user can choose to run all step or organize the steps as how they would like it.

[Sebastian Ullrich]

There is also one clear limitation of having separate steps: they are run in order. Really for the highest possible throughput, all (expensive) CI actions would have to be modeled as Lake build targets that are scheduled in parallel as determined by Lake. If the output of such an approach that does not allow for linear section names is not sufficiently clear, we should look at how to improve it.

[Utensil Song]

Another choice may be using Reusable workflows to have all these steps run in one go but logged as separate steps.

image.png

[Kim Morrison]

Nesting is I think fine.

[Utensil Song]

There seems to be actions/toolkit#1001 regarding nested groups.

[Oliver Butterley]

Utensil Song said:

Another choice may be using Reusable workflows to have all these steps run in one go but logged as separate steps.

:thinking: that would give the separate steps and currently lean-action is a composite action so adapting one to the other is straight forward. I'm not aware of possible downsides except that it couldn't be listed on Github Marketplace and couldn't later become a fully fledged javascript or docker action.

[Oliver Butterley]

Utensil Song said:

There seems to be actions/toolkit#1001 regarding nested groups.

Nesting a grouping in the github actions log is a bit primitive. It would be possible to just add blank lines and headers to separate the text a bit. But doesn't seem the perfect solution.

[Oliver Butterley]

Utensil Song said:

One way is to make it to have more action steps like https://github.com/quarto-dev/quarto-actions, so the user can choose to run all step or organize the steps as how they would like it.

Structuring the workflow like this or, more or less equivalently, like action-python does have the benefit of all the steps being separate and the use totally customizable.

Then again, could more functionality be built into lake and so each desired step is already very concise?

[Kim Morrison]

Oliver Butterley said:

except that it couldn't be listed on Github Marketplace

I'd prefer we avoid that.

[Kim Morrison]

Let's not add too much technology here. I think just plain text headers and blank lines is a great start, and we can iteratively ask for changes in lake output too, if needed.

[Austin Letson]

One thing to note is that when there is a failure, the log group where the failure occurred is automatically expanded. I added links to examples on the batteries pr. This isn't as clear as the multi-step workflow, but it is better than manually expanding the log groups.

I agree with @Oliver Butterley that summaries and annotations could complement the logs. To give an idea of what this would look like, here is the lean-action PR for adding lake check-test where we used a summary to surface the reason for the workflow failure to the user.

[Austin Letson]

I have created a PR to improve the log group headers and add blank lines here.

This is what the log output looks like now:
2024-05-22-090841-screenshot.png

There is still room for improvement. I haven't figured out how to control the log output of the actions/cache steps, but there may be a workaround. I used a workaround I found here to change some of the log group names.

[François G. Dorais]

@Austin Letson Thanks for doing this! I've updated most of my active repos to use lean-actions today and it works totally fine so far.

[Austin Letson]

Yay! I am glad it is working well :smile:

[Kim Morrison]

Thanks for the links to the failure mode logs. They look good. I added a suggestion for a name for the build step (users reading the log care what it is doing, not what the action is called).

If that looks good, I propose we merge!

[Austin Letson]

Good point. The new name looks good to me! I have updated the PR.

[Kim Morrison]

Merged. Let's keep an eye on it!

[François G. Dorais]

How can I use lean-actions to do lake update but not lake build?

[Austin Letson]

Currently lean-action always runs lake build. We are currently working on supporting use cases which don't include lake build. This functionality will likely be available in the next couple of weeks.

[Austin Letson]

v1-beta.1 Release of lean-action :rocket:

v1-beta.1 adds new features and improvements to lean-action:

• new lake-package-directory input to specify the directory to run Lake commands.
  This input will enable users to use lean-action when Lake packages are contained in repository subdirectories.

• new use-github-cache input to specify if lean-action should use actions/cache to cache the .lake folder (useful for debugging and testing)

• build-status and test-status output parameters to use in subsequent workflow steps

Additionally, lean-action now supports a fully automated functional test suite to ensure that future improvements and changes don't break existing functionality.

You can view the full release notes here.

Upgrading to v1-beta.1

All workflows with- uses: leanprover/lean-action@v1-beta will automatically start using v1-beta.1 instead of v1-beta.0, so no action is required to upgrade to v1-beta.1.

If you have any questions or encounter any issues, you can post in this Zulip thread or create an issue on GitLab.

Thank you to @Asei Inoue, @Kim Morrison, and @Utensil Song for feedback and help with this release.

[Kim Morrison]

@Austin Letson, thanks so much for this great work on a foundational tool for the ecosystem!

[Kim Morrison]

A milestone I'm really excited about is getting lake new to include a Github workflow running lean-action.

Do we still have technical blockers for this? Or is it a matter of writing the PR that adds to the lake new templates?

[Austin Letson]

Kim Morrison said:

A milestone I'm really excited about is getting lake new to include a Github workflow running lean-action.

Do we still have technical blockers for this? Or is it a matter of writing the PR that adds to the lake new templates?

I am excited about this milestone as well! I recommend waiting until the v1 release of lean-action to ship it with lake new/init. v1 will likely not be backward compatible with the beta versions. There are a few outstanding issues that I would like to complete for v1 (link to the filtered list on GitHub). One issue already has a PR. This PR will impact the user experience, so I have added you as a reviewer.

All this being said, I estimate v1 will be ready in 2-3 weeks, and I see no reason why we couldn't work on adding the functionality to Lake in parallel. Should I create an issue on leanprover/lean4 to add a lake new template?

[Austin Letson]

Another related note: When writing the functional tests for lean-action, my primary focus has been testing lean-actionon packages created with lake new/init. For example, in the test run for v1-beta.1 the lake-init-success matrix runs lean-action on packages created with lake init standalone, lake init mathdep math, and lake init tomltest .toml. Other tests run lake init and then introduce a change to the Lake file, e.g., adding a @[test_driver] or an obvious syntax error and confirming lean-action behaves correctly.

Expanding our functional tests with more scenarios shouldn't take much effort and will allow us to identify issues users may encounter when using lean-action out of the box with lake new. I welcome any suggestions for additional test cases. Also tagging @Mac Malone for his input.

[Austin Letson]

I created an issue and corresponding draft PR to add a lean-action workflow on lake new/init.

[Kim Morrison]

Mac is on vacation this week, but looking forward to discussing this when he is back!

[Austin Letson]

Sounds good!

[Austin Letson]

Quick question: now that Lake supports @[lint_driver] and lake lint I was planning on removing the direct integration of lean-action and the Batteries linting framework in favor of a more general option to run lake lint as part of lean-action. This seems more flexible and users can still run the Batteries linting framework from the lint driver. Does this seem like the right approach to others?

[Kim Morrison]

Yes, thanks!

[Austin Letson]

v1.0.0 Release of lean-action :rocket:

v1.0.0 is the first non-beta release of lean-action :tada: . You can read the full release notes here. As always, if you have any feedback or issues, don't hesitate to respond in the lean-action Zulip topic or create an issue on the lean-action repo.
Thank you to everyone for the feedback on the beta releases, specifically @Asei Inoue, @Oliver Butterley, @SnO2WMaN, and @Kim Morrison.

New features

• lake lint support. lean-action can now run lake lint in your CI pipeline, either automatically (see bellow) or by using the new lint input.
• Automatic CI feature detection using the Lake workspace. lean-action now uses the Lake workspace to automatically determine which CI features to run, i.e., lake build, lake test, lake lint. Users can still specify exactly which steps should run with build, test, and lint inputs as well as disabling automatic configuration with auto-config: false.
• Improved testing of lean-action itself. Maintainers of lean-action can now run the functional test suite on a specific Lean toolchain. This means we can easily run tests with each new Lean core release candidate and identify/fix issues early to avoid disrupting users' workflows.

Upgrading to v1

If you have been using a previous release of lean-action in your repo, you will need to manually upgrade to v1 by updating your yaml workflow to:

- uses: leanprover/lean-action@v1

Breaking changes

• The direct integration with the Batteries linting framework was removed. Users should now use a @[lint_driver] in their lean file in combination with lake lint to run the Batteries linting framework.

[Austin Letson]

v1.0.1 Release of lean-action :rocket:

Improvements

• lean-action now supports macOS runners :apple:
• lean-action now uses the lake-manifest.json instead of the lakefile.{lean, toml} to detect mathlib dependency, which is more robust and easier to maintain. Specifically, this fixes an issue when using the new reservoir require Lake file syntax introduced in Lean 4.10.

Upgrading to v1.0.1

v1.0.1 is a minor release of lean-action, so you don't need to do anything to upgrade if your workflow uses - uses: leanprover/lean-action@v1. If you have specified a more specific version in your workflow (e.g. - uses: leanprover/lean-action@v1.0.0), you will need the specific version or use the major version tag.

You can read the full release notes here.

[Kim Morrison]

Fantastic, thanks for this!

[Kim Morrison]

I can open an issue about this, but maybe some first discussion is warranted.

I still find the CI workflow output from lean-action pretty confusing, and hard to locate where the failure is. Just to take an example, here's the latest failure on the current PR list: https://github.com/leanprover-community/batteries/actions/runs/10436378305/job/28901375546?pr=925

Run leanprover/lean-action@v1
Run : Install Elan
Elan Installation Output

Run : Configure Lean Action
Configure lean-action
Run actions/cache@v4
Cache Size: ~44 MB (46612293 B)
/usr/bin/tar -xf /home/runner/work/_temp/697e5926-a3ea-4e6b-87d6-8ffd033214a8/cache.tzst -P -C /home/runner/work/batteries/batteries --use-compress-program unzstd
Cache restored successfully
Cache restored from key: lake-Linux-35bbb9cdd70d826478d2df7bbf453c1aeb7b32f970cc509538c2e946395c254e-e503a2d63ec7774f5baf6891f61ee3154b09e948bf29ec62baae194489642e73-328eaed87117a8608f10e51432a2f84d3fe3eef0
Run : Detect Mathlib
Detect Mathlib Output

Run : Lake Build
Lake Build Output

Run actions/cache/save@v4
/usr/bin/tar --posix -cf cache.tzst --exclude cache.tzst -P -C /home/runner/work/batteries/batteries --files-from manifest.txt --use-compress-program zstdmt
Cache Size: ~44 MB (46650665 B)
Cache saved successfully
Cache saved with key: lake-Linux-35bbb9cdd70d826478d2df7bbf453c1aeb7b32f970cc509538c2e946395c254e-e503a2d63ec7774f5baf6891f61ee3154b09e948bf29ec62baae194489642e73-d9faee2ee14144d5bca60fa9ff7ad59361621bf6
Run : Lake Test
Lake Test Output

Run : Lake Lint
Lake Lint Output

Error: Process completed with exit code 1.
Run : Set Output Parameters
Set Output Parameters

It's not terrible: the Error line is written in red, so at least my eye jumps pretty quickly there. However the error line itself is not at all informative. I've learnt to read up a few lines the find the previous "Run" statement, but it's not as intuitive as it could be. (And definitely not as helpful as the CI output at Mathlib, where everything is a separate step, so the Github interface itself shows a big red cross at the failing step --- indeed even before the output the unfolds automatically.)

I don't have a concrete suggestion here, but I would love to see the UX around "understand where the problem is asap" improved. No one enjoys spending time reading workflow output. :-)

[Yakov Pechersky]

GitHub workflows have annotation support: https://docs.github.com/en/actions/writing-workflows/choosing-what-your-workflow-does/workflow-commands-for-github-actions#setting-an-error-message

[Austin Letson]

Thanks for sharing this, @Kim Morrison ! UX is an area where there is room for improvement.

First, I am sad that GitHub isn't automatically expanding the log group containing a failure. This seems like a regression because I thought an earlier version of lean action had this working. I might have broken it when consolidating some of the scripts. I want to get this working because I know it is frustrating not to know which log to expand.

Beyond expanding the logs, there are some other options:

As Yakov mentioned, we could improve the error annotations. This would have the most significant impact if we also fix the log group expansion issue, because otherwise, the errors get lost within the groups. I believe these annotations allow you to give a link to the line that caused the problem, which could be great for improving UX.

Additionally, we could use the job summary feature, which essentially allows you to display an arbitrary markdown document at the summary level. Especially for common issues, this would be a quick way for users to understand the issue without diving into the logs at all. Here is a screenshot of what that might look like for lake lint. Obviously, we would want a more detailed description based on the actual issue:

2024-08-21-114756-screenshot.png

Another option would be to allow users to split lean-action usage across multiple steps, bringing it closer to the Mathlib CI. This is already possible to some extent by using the auto-config: false option, however, we would want to make sure that caching and elan installation play nice with this usage if we are going to recommend it. Something like:

  - uses: leanprover/lean-action@v1
    with:
      auto-config: false
      build: true
 - uses: leanprover/lean-action@v1
    with:
      auto-config: false
      test: true
 - uses: leanprover/lean-action@v1
    with:
      auto-config: false
      lint: true

For advanced projects, I am not convinced that this usage of lean action is better than having users use lean-action to set up their CI and environment and then create their own steps that run lake build, lake test, etc..

I can play around with these options and come back with more concrete demos, but I am also open to other ideas.

[Kim Morrison]

Yes, I agree we should aim for "most users have a single step, that just does the best possible", and "for users who need lots of configuration, lean-action will only to the initial setup".

[Eric Wieser]

for users who need lots of configuration, lean-action will only to the initial setup".

Should we have a separate setup-lean action for this, to match setup-python etc?

[Austin Letson]

Eric Wieser said:

for users who need lots of configuration, lean-action will only to the initial setup".

Should we have a separate setup-lean action for this, to match setup-python etc?

This is a good point, considering the setup-* pattern is so common. This wouldn't be hard to pull out into its own action.

Alternatively, we could make the input API of lean-action more obvious, having a setup-only: true input instead of auto-config: false. Or even having users opt in to lean-action running lake build, lake test, etc... Note we could opt in automatically when generating a CI yml with lake initso that users would get the benefits of the "does the best possible functionality".

There is a risk right now of users building/testing/linting their project twice, by adding lean-action at the top of their CI and then running the same CI in subsequent steps. I ran into this when working with the maintainers of LNSym to add lean-action to their workflow.

[Eric Wieser]

I think mixing setup-only and setup-plus-do-stuff in the same package name probably just increases the risk of things being run twice. If you put things in a lean-setup action, then lean-action can use that as its first step, right?

[Austin Letson]

Eric Wieser said:

I think mixing setup-only and setup-plus-do-stuff in the same package name probably just increases the risk of things being run twice. If you put things in a lean-setup action, then lean-action can use that as its first step, right?

I agree. It seems more straightforward to separate the setup-only from the setup-plus-do-stuff. That adheres to the setup-* pattern and if someone simply needs Lean setup in their workflow, they don't have to worry about lean-action doing something unexpected.

[Austin Letson]

@Julian Berman is this in use: https://github.com/Julian/setup-lean

[Austin Letson]

It seems close to what we are discussing :eyes:

[Julian Berman]

Kind of. It's used by lean.nvim but no one else, likely because I 1) didn't advertise it, 2) it doesn't do much! It's like 4 lines. I'm very happy for it to disappear or get taken over or to do whatever with it.

[Julian Berman]

I agree though that I would generally expect any language to have some action called setup-<language> which does not much more than "install the language for me" typically.

[Austin Letson]

v1.0.2 Release of lean-action :rocket:

This is a minor release motivated by the fix for the log expansion issue flagged by @Kim Morrison. Moving forward, when a Lake command fails, GitHub should automatically expand the log group corresponding to the failing step. This means users will hopefully spend less time reading workflow output :)

If anyone encounters other log group issues or UX annoyances, please message here or create an issue on GitHub. There is still room for improvement in this area.

No action is needed to upgrade to this release as long as you are using the leanprover/lean-action@v1. You can read the release notes here.

[Austin Letson]

v1.1.0 Release of lean-action :rocket:

Thank you @Jon Eugster and @Asei Inoue, for the help with adding Windows runner support!

Improvements

• lean-action now supports Windows runners :window:
• removed redundant cache checks

You can view the full release notes here.

[Julian Berman]

It would be useful to have an action which can be set to run on a schedule in GitHub actions which sends an automated PR running lake update if doing so produces changes, i.e. if there's a dependency to update (perhaps even configurably automerging the PR if CI passes, though this could be done by the user of the action). This effectively reimplements dependabot for Lean project dependencies (hoping for new dependabot-supported languages usually isn't fruitful as we've discussed previously).

I think ages ago there used to be an action that did this specifically for Mathlib in Lean 3 -- has this kind of functionality been discussed anywhere recently, either within the scope of lean-action or otherwise in general?

[Bryan Gin-ge Chen]

In case it's helpful, in the mathlib4 repo, we have the update_dependencies.yml workflow for this; it relies a bit on the details of our labeling scheme though.

[Asei Inoue]

@Julian Berman

We have already such an github action!
Do you know lean-update action? https://github.com/oliver-butterley/lean-update

[Julian Berman]

I did not! I was only aware of the Mathlib workflow. That does look exactly like what I want, thanks. The description in GitHub says "update Lean and mathlib", but hopefully it means any dependencies of a project, right?

[Asei Inoue]

@Julian Berman This action update any lean libraries including mathlib.

[Kim Morrison]

@Oliver Butterley, @Austin Letson, what are the prospects for rolling this into lean-action (and possibly even turning it on by default)? It would be great if merely typing lake new gave you this functionality!

[Kim Morrison]

Separately, can we replace the Mathlib workflow with this?

[Austin Letson]

Kim Morrison said:

Oliver Butterley, Austin Letson, what are the prospects for rolling this into lean-action (and possibly even turning it on by default)? It would be great if merely typing lake new gave you this functionality!

We discussed combining them a few months ago but I believe we decided then to wait until both were more fleshed out. Now that it is easier to separate the functionality of lean-action into separate workflows triggered by PRs and cron jobs, I think we could combine them without too much difficulty.

What do you think @Oliver Butterley?

[Asei Inoue]

@Austin Letson @Kim Morrison

what are the prospects for rolling this into lean-action (and possibly even turning it on by default)? It would be great if merely typing lake new gave you this functionality!

I think it's nice idea!

[Oliver Butterley]

Austin Letson said:

We discussed combining them a few months ago but I believe we decided then to wait until both were more fleshed out. Now that it is easier to separate the functionality of lean-action into separate workflows triggered by PRs and cron jobs, I think we could combine them without too much difficulty.

What do you think Oliver Butterley?

lean-update is now rather fleshed out although I would say it is still short of the quality of a v1 release. It covers the use cases we could think about and it has been tested in various places but not very extensively used as yet.

I had planned to substantially improve the reporting of problems when they happen and improve the way that commits/PRs/issues are done by the action if such is selected by the user. Also functionality like updating deprecations. However in the last months I had zero spare time for any of this. I also planned to rewrite it as a javascript action since it was getting more complicated and that would make the code more maintainable.

Within a month I should again have time to polish the parts that need it to get it up to release quality. Or if anyone else wants to take it over and/or incorporate such functionality in lean-action that would be great!

[Asei Inoue]

Within a month I should again have time to polish the parts that need it to get it up to release quality. Or if anyone else wants to take it over and/or incorporate such functionality in lean-action that would be great!

Although lean-update is incomplete at the moment, it still implements key features and could be incorporated into lean-action. I can help with the work.

[Austin Letson]

Asei Inoue said:

Within a month I should again have time to polish the parts that need it to get it up to release quality. Or if anyone else wants to take it over and/or incorporate such functionality in lean-action that would be great!

Although lean-update is incomplete at the moment, it still implements key features and could be incorporated into lean-action. I can help with the work.

@Asei Inoue, given that you have experience working on both lean-action and lean-update, would you be willing to write an issue on the lean-action repo outlining a high-level plan on how we would incorporate lean-update into lean-action?

Specifically, it would be great if you could address:

1. Architectural updates needed in lean-action to support this new use case
2. Recommendations for integrating the new lake update feature into lean-action's existing user interface

This would serve as an excellent starting point and help us determine if we need additional input from the community before implementing the lake update functionality.

[Asei Inoue]

@Austin Letson

Thank you. Review work was carried out.
My opinion is here: https://github.com/leanprover/lean-action/pull/105

[Austin Letson]

v1.1.1 Release of lean-action :rocket:

Thank you, @Asei Inoue and @Abdalrhman M Mohamed, for filing bug reports!

Fixed

• fix bug with passing multiple arguments to lake build via build-args input
• fix false feature flag logic when using auto-config: true

This is a bug-fix release. No action is needed to update. You can view the full release notes here.

[Yury G. Kudryashov]

Hi, should lean action catch warning: [file]: declaration uses 'sorry' and mark the "build" action as failed?

[Austin Letson]

Yury G. Kudryashov said:

Hi, should lean action catch warning: [file]: declaration uses 'sorry' and mark the "build" action as failed?

By default, lean-action runs lake buildwithout any parameters, which does not result in a failure for any warnings. You can configure Lake as you would through the command line with the build-args input. For example, to run lean-action with lake build --fail-level=warning:

- uses: leanprover/lean-action@v1
  with:
    build-args: "--fail-level=warning"

This is what batteries does.

This would cause lean-action to fail on all warnings, not just declaration uses 'sorry'. I don't know if there is a lake option to specify specific warnings that should cause failure.

[Asei Inoue]

@Austin Letson

by the way what happened to the lean-update action?

[Yury G. Kudryashov]

Is there a way to keep building but still report an error, or should I add a step to grep the output?

[Oliver Butterley]

Asei Inoue said:

Austin Letson

by the way what happened to the lean-update action?

I promised to do a complete overhaul of lean-update, both improving reporting and code structure. However I started only recently because of various other commitments. I expect to get it done soon!

[Asei Inoue]

@Oliver Butterley @Austin Letson Thank you! Sorry I've been so forgetful.

[Austin Letson]

Yury G. Kudryashov said:

Is there a way to keep building but still report an error, or should I add a step to grep the output?

Without --fail-level=warning, the error is still reported in the workflow log files. Here is an example run where lake build found sorrys but continued.

However, this information is buried in the log file and isn't particularly helpful, for instance, if you want to be notified on a PR that the proposed changes contain a sorry but still finish the build. What is the use case you're looking to address?

[Austin Letson]

Grepping the output may currently be the best solution. In the past, we have discussed creating a better integration between Lake warnings/errors and the GitHub actions messaging API. Maybe it is time to add this feature.

[Asei Inoue]

@Austin Letson @Oliver Butterley

Hello,
I have taken over the work from the busy Oliver and refactored the lean-update( https://github.com/Seasawher/lean-update ) action. I rewrote some Bash scripts in PowerShell, added several features, and improved some messages.

In my opinion, I am ready to hand over the work to you, Austin! This is something that Oliver and I have built together, but we are prepared to transfer ownership to leanprover organization if it helps more people use this GitHub Action. This GitHub Action is really useful and has become an essential part of my development life. I believe the same is true for quite a few Lean users as well!

I would love to hear Austin's thoughts!

[Kim Morrison]

Does the fact that it is uses PowerShell mean that it only works on Windows runners?

[Kim Morrison]

Can one configure whether to run lake build + lake test + lake lint to determine success of the update? What about configuring other scripts to run to validate?

[Kim Morrison]

Could you clarify the meaning of https://github.com/Seasawher/lean-update/blob/main/action.yml#L21, it is not obviously to me what this setting does?

[Kim Morrison]

The README needs to show how to configure it.

[Kim Morrison]

Can we decide an active repo to try this out in? Any volunteers (Carleson, infinity-cosmos, FLT??)

[Asei Inoue]

Does the fact that it is uses PowerShell mean that it only works on Windows runners?

No. PowerShell Core runs on Ubuntu, and pwsh works on popular Ubuntu images used in GitHub Actions.

[Asei Inoue]

Can one configure whether to run lake build + lake test + lake lint to determine success of the update? What about configuring other scripts to run to validate?

You can configure what to pass to the build-args of lean-action. Therefore, it is possible to treat warnings as failures. Whether to run lake test or lake lint is determined by lean-action.

[Asei Inoue]

Could you clarify the meaning of https://github.com/Seasawher/lean-update/blob/main/action.yml#L21, it is not obviously to me what this setting does?

Sorry for the lack of explanation. The README is also lacking details, but I believe the description section of action.yml should be sufficient for understanding. I'll add more details to improve it.

[Asei Inoue]

The README needs to show how to configure it.

I'll add how to setup later.

[Austin Letson]

Kim Morrison said:

Can we decide an active repo to try this out in? Any volunteers (Carleson, infinity-cosmos, FLT??)

lean-update is used in FLT. link to workflow

Here is a link to an automated update PR created by lean-update.

[Asei Inoue]

Can we decide an active repo to try this out in? Any volunteers (Carleson, infinity-cosmos, FLT??)

At the moment, I am testing this GitHub Action in my actively developed repository.
However, it should indeed be tested in many use cases.
Regarding this, I would like to hear @Austin Letson's opinion.

[Austin Letson]

@Asei Inoue could you outline the differences between your fork and Oliver's lean-update?

I agree that the README should show configuration options and usage examples.

[Austin Letson]

Is it possible to reuse parts of the README that Oliver wrote?

[Oliver Butterley]

Hi everyone!

I'm sorry for any inconvenience I might have inadvertently caused, I genuinely thought I would get some time to do the overhaul of lean-update I claimed I would do but then life happened, months passed and I still didn't get the spare time.

I keep no hold on it, if it is useful and someone has time to improve it then that's great. If I should put a notice on my repo about it moving to another place for active development then let me know.

[Asei Inoue]

@Austin Letson @Oliver Butterley @Kim Morrison

could you outline the differences between your fork and Oliver's lean-update?

The differences between Oliver's action and my fork are minor, but there are a few distinctions:

• It does not display todo messages. Instead, when an issue is raised due to a failed update, it notifies which files were updated.
• A new option called what_to_update has been added. This allows the action to trigger notifications or pull requests only when the Lean version changes. This feature was primarily developed for repositories that depend on Mathlib. Such repositories need to frequently check for updates to ensure existing code is not broken, but they do not necessarily want to update the code unless a breakage occurs. This is because updating Mathlib requires rebuilding the environment locally each time.
• A new option called build_args has been added. This allows passing the --fail-level=warning option to lean-action, treating warnings as update failures.

[Asei Inoue]

I agree that the README should show configuration options and usage examples.

OK! wait a minute.

[Asei Inoue]

Is it possible to reuse parts of the README that Oliver wrote?

I think so, maybe

[Austin Letson]

No worries @Oliver Butterley! Thank you for your work on this. As mentioned above FLT is already getting a lot of use out of the tool.

[Austin Letson]

Asei Inoue said:

I agree that the README should show configuration options and usage examples.

OK! wait a minute.

Sorry! haha. I missed your response to this above

[Austin Letson]

@Asei Inoue what do you think about testing your fork in FLT since Kevin and Pietro have already adopted a workflow that includes lean-update? They may also have some useful feedback after using alpha version.

[Asei Inoue]

what do you think about testing your fork in FLT since Kevin and Pietro have already adopted a workflow that includes lean-update? They may also have some useful feedback after using alpha version.

I think it's a good idea. :+1:

[Asei Inoue]

@Austin Letson @Kim Morrison

README has been updated. https://github.com/Seasawher/lean-update

[Asei Inoue]

My goal is to ensure that when lake new is executed, lean-update or its successor action is generated simultaneously. :smile:

[Kim Morrison]

@Pietro Monticone, what do you think about switching to this fork?

[Kim Morrison]

@Asei Inoue, is it necessarily to include

    permissions:
      contents: write
      pull-requests: write
      issues: write

in the config files? What happens if these are omitted?

[Kim Morrison]

Why does the README recommend the line

        id: update-lean-mathlib

This is just a generic thing: if the example setup isn't making use of it, let's leave it out. If we have an example where a later step makes use of the id, let's have that as a later example in the docs.

[Kim Morrison]

The second example is missing the comment # allows workflow to be triggered manually

[Kim Morrison]

Could you clarify in "However, you can configure what build arguments are passed to lean-action using the build_args option." that these arguments are passed direct to lake build, not to anything else in lean-action?

[Kim Morrison]

I think we should rename the what_to_update field. What about update_if_modified? Currently it reads as an instruction: please modify this file, rather than a condition: please take some action if this file is modified by lake update.

[Kim Morrison]

I propose we change the default value of what_to_update to lake-manifest.json, and in the first example, remove this field (i.e. take advantage of the default value).

[Kim Morrison]

I would really like to also see a zulip option for both on_update_succeeds and on_update_fails, configurable with a stream/topic/api key. This would allow us to replace Mathlib's existing automatic update with this action.

[Kim Morrison]

The zulip option should probably be in addition to the current alternative actions, rather than a replacement.

[Sebastian Ullrich]

The choice of Powershell doesn't seem very friendly to other potential contributors. Why not go with the Actions lingua franca, JS?

[Kim Morrison]

Sebastian Ullrich said:

The choice of Powershell doesn't seem very friendly to other potential contributors. Why not go with the Actions lingua franca, JS?

Yes, please. I hesitated to say this above, because I'm happy to see work being done on this and didn't want to discourage, but if this is going to be adopted widely it's really going to have to be JS.

[Kim Morrison]

(https://claude.ai/share/cb6518eb-41a3-4fce-a678-c9d29860f5d1 might suffice :-)

[Kim Morrison]

Actually looking at the code now, I don't see any validation that the field what_to_update is one of the two allowed options. There should be an actionable error message in this case.

[Asei Inoue]

is it necessarily to include ...
in the config files? What happens if these are omitted?

I tested it and it worked without it. It seems unnecessary. done!

Why does the README recommend the line ..
This is just a generic thing: if the example setup isn't making use of it, let's leave it out. If we have an example where a later step makes use of the id, let's have that as a later example in the docs.

Oh, sorry. done!

The second example is missing the comment # allows workflow to be triggered manually

done!

Could you clarify in "However, you can configure what build arguments are passed to lean-action using the build_args option." that these arguments are passed direct to lake build, not to anything else in lean-action?

done!

I think we should rename the what_to_update field. What about update_if_modified? Currently it reads as an instruction: please modify this file, rather than a condition: please take some action if this file is modified by lake update.

nice idea! done!

I propose we change the default value of what_to_update to lake-manifest.json, and in the first example, remove this field (i.e. take advantage of the default value).

That might be more intuitive. done!

I would really like to also see a zulip option for both on_update_succeeds and on_update_fails, configurable with a stream/topic/api key. This would allow us to replace Mathlib's existing automatic update with this action.

wait a minute, please :construction_zone:

The choice of Powershell doesn't seem very friendly to other potential contributors. Why not go with the Actions lingua franca, JS?

wait a minute, please :construction_zone:

[Kim Morrison]

Thanks!!

[Asei Inoue]

The choice of Powershell doesn't seem very friendly to other potential contributors. Why not go with the Actions lingua franca, JS?

done!

[Kim Morrison]

If you're interested in implementing the zulip messaging, there are examples e.g. in mathlib's .github/workflows/nightly_detect_failure.yml.

[Asei Inoue]

@Kim Morrison

If I implement the zulip option in a straightforward way, it might end up being an option exclusive to Mathlib.
What kind of specifications would be suitable to make it a more general-purpose implementation?

[Kim Morrison]

You should be able to specify the stream, topic, and which API key to use.

[Kim Morrison]

The key shouldn't be specified directly in the configuration file, just the name of the GitHub secret containing it.

[Asei Inoue]

@Kim Morrison
Wouldn't it be more natural to make this action return the appropriate output and pass it to zulip/github-actions-zulip/send-message?

[Asei Inoue]

I thought that if I pass the information about whether this action's update process succeeded or failed, zulip/github-actions-zulip/send-message should be able to handle the rest. What do you think?

[Asei Inoue]

I thought it would be a good idea to include an example in this Action's README for notifying Zulip...?

[Asei Inoue]

zulip action test: update succeed!

(this is automatedly sent)

[Asei Inoue]

Here is a sample

      - uses: actions/checkout@v4
      - name: Update Lean project
        id: lean-update
        uses: Seasawher/lean-update@main
        with:
          update_if_modified: lean-toolchain

      - name: Zulip Notifycation
        if: steps.lean-update.outputs.result == 'update-success'
        uses: zulip/github-actions-zulip/send-message@v1
        with:
          api-key: ${{ secrets.ZULIP_API_KEY }}
          email: "tellagoodstory@icloud.com"
          organization-url: 'https://leanprover.zulipchat.com'
          to: "general"
          type: "stream"
          topic: "lean-action"
          content: "zulip action test: update succeed!"

[Asei Inoue]

hmm, it seems to be required to return whether “update if modified” was triggered…
but what will I name the result…?

[Arthur Paulino]

I'm a bit late for the party but I'm passing here just to thank everyone involved in making this :heart:

[Pietro Monticone]

Kim Morrison said:

Pietro Monticone, what do you think about switching to this fork?

Sure, I'll do it on all the projects I (co-)maintain giving higher priority to the LeanProject template.

I assume @Kim Morrison would like to remove the -R -Kenv=dev in lake -R -Kenv=dev update that is run by the lean-update action, right? :sweat_smile:

#Carleson and #FLT don't need it anymore, but others such as #Equational and #Infinity-Cosmos still do. It can be easily resolved with a new release removing the -R -Kenv=dev in such a way that those projects can continue using the older version for a while.

LeanProject must wait for LeanBlueprint to be updated in order to accomodate for such a change though.

[Pietro Monticone]

Done :check:

[Kim Morrison]

Pietro Monticone said:

I assume @Kim Morrison would like to remove the -R -Kenv=dev in lake -R -Kenv=dev update that is run by the lean-update action, right? :sweat_smile:

#Carleson and #FLT don't need it anymore, but others such as #Equational and #Infinity-Cosmos still do. It can be easily resolved with a new release removing the -R -Kenv=dev in such a way that those projects can continue using the older version for a while.

Yes, please! @Asei Inoue, does this make sense?

[Pietro Monticone]

Here is the related PR. Please consider tagging a (0.0.1?) release before merging this PR.

[Pietro Monticone]

@Asei Inoue Could you please use the standard v0.0.1 as the release tag and title?

[Asei Inoue]

done!

[Pietro Monticone]

Thanks. I'll add it to all the projects who requires -R -Kenv=dev now.

[Pietro Monticone]

Done :check:

[Asei Inoue]

@Kim Morrison

Sorry, I forgot something very important.

When running lake update, does lake automatically upgrade from a stable version like v4.16.0 to a pre-release version like v4.17.0-rc1?

[Ruben Van de Velde]

Sure

[Asei Inoue]

When running lake update, does lake automatically upgrade from a stable version like v4.16.0 to a pre-release version like v4.17.0-rc1?

No! If the version of lake is outdated, updates may not work as expected.

[Austin Letson]

@Kim Morrison @Asei Inoue What do you think of lean-update serving as the reminder/automation to create tags for new tool chains. lean-update could tag the first commit after lake update with the corresponding toolchain-tag.

Note, @Pietro Monticone's LeanProject create-release workflow does this already, but it is triggered off of modifications to lean-toolchain.

[Austin Letson]

Asei Inoue said:

When running lake update, does lake automatically upgrade from a stable version like v4.16.0 to a pre-release version like v4.17.0-rc1?

No! If the version of lake is outdated, updates may not work as expected.

From the Lake section of the Reference:

The lake update command checks for changes to dependencies, fetching their sources and updating the manifest accordingly. By default, lake update also attempts to update the root package's toolchain file when a new version of a dependency specifies an updated toolchain. This behavior can be disabled with the --keep-toolchain flag.

I think this means that lake update would only update from v4.16.0 to v4.17.0-rc1, if the root package depends on a package that uses v4.17.0-rc1.

[Asei Inoue]

No! If the version of lake is outdated, updates may not work as expected.

This issue has been resolved. I have used old solution which I used for Oliver's Action...
Get all release of Lean, and sort them, and rewrite lean-toolchain!

[Asei Inoue]

@Austin Letson

What do you think of lean-update serving as the reminder/automation to create tags for new tool chains. lean-update could tag the first commit after lake update with the corresponding toolchain-tag.

I can't imagine what you mean, so please explain more specifically what it will be used for.

[Asei Inoue]

(deleted)

[Asei Inoue]

For example, taking the Qq library as a case, does this mean setting up lean-update for the Qq library so that a release tag is assigned the moment a PR is merged after a notification about the Qq library's lean-toolchain update?

[Asei Inoue]

I see. If that works, then simply merging a PR from GitHub Mobile would automatically complete the release process. That feature would certainly be convenient for me as well.
However, I'm still not sure whether it should be a feature included in lean-update.

[Austin Letson]

Asei Inoue said:

Austin Letson

What do you think of lean-update serving as the reminder/automation to create tags for new tool chains. lean-update could tag the first commit after lake update with the corresponding toolchain-tag.

I can't imagine what you mean, so please explain more specifically what it will be used for.

Lean packages can have tags for each compatible toolchain so that users can use the version of the package that corresponds to a specific toolchain. This is done for several core projects when a new version of Lean is released, however it would be useful for other projects to automatically get toolchain tags. For example, this came up recently when discussing how to use Pantograph with a specific version of Lean to scrape sorry statements from projects across different toolchains (link to zulip thread).

[Austin Letson]

Asei Inoue said:

For example, taking the Qq library as a case, does this mean setting up lean-update for the Qq library so that a release tag is assigned the moment a PR is merged after a notification about the Qq library's lean-toolchain update?

Yes, exactly!

[Austin Letson]

Asei Inoue said:

I see. If that works, then simply merging a PR from GitHub Mobile would automatically complete the release process. That feature would certainly be convenient for me as well.
However, I'm still not sure whether it should be a feature included in lean-update.

Yes, I am not sure if this should be included in Lean update or be a separate tool. It seems very related to lean-update's behavior, however I would defer to others who are actively maintaining larger scale Lean projects.

[Asei Inoue]

I think it's fine to finish lean-update silently and then handle the release process in a later step.
for example:

      - name: Update Lean package
        id: update
        uses: Seasawher/lean-update@main
        with:
          on_update_succeeds: "silent"
          update_if_modified: "lean-toolchain"

      - name: commit with tag, and create release
        if: steps.update.outputs.result == 'update-success'
        run: |
          foo bar baz....

(I think notifications to Zulip can be handled in the same way.)

[Asei Inoue]

@Kim Morrison

update! see: https://github.com/Seasawher/lean-update?tab=readme-ov-file#if-you-want-to-receive-notifications-on-zulip-when-the-update-fails

I've added an example workflow to send zulip notification

[Asei Inoue]

@Austin Letson
I made it possible to obtain the latest Lean release from the output of this action. Wouldn't this allow for the implementation of automatic releases?

[Asei Inoue]

@Kim Morrison @Austin Letson

It must be annoying to have the update workflow running even when you are working at fork repository.
What do you think?
If I fork, GitHub Action will be disabled?

[Kim Morrison]

I agree it is best that lean-update itself doesn't do the zulip notification or toolchain release tagging. But we may want to package these steps as actions, too!

[Asei Inoue]

@Kim Morrison Is it not enough to add an example to the README?

[Kim Morrison]

Because no one should ever have to read the README, or know the repository exists. All this infrastructure needs to be deployed by lake new, and the only configuration required to uncommenting some lines. We don't want to be copy-pasting these configuration blocks into everyone's lake projects if they can be factored out into a centrally updatable action.

[Kim Morrison]

Let's be more helpful in the line about registering your zulip API key. That text should explain or link to:

• how to create/obtain such a key
• the URL https://github.com/<YOUR-ORG>/<YOUR-REPO>/settings/secrets/actions where the secret needs to be installed.
• doesn't need the word SECRETS capitalized?

[Kim Morrison]

The line

      - name: Zulip Notifycation

should be "Notification"

[Kim Morrison]

The example "content" is wrong. It's not that the latest CI failed, but that an update failed.

[Kim Morrison]

I think we also need to add some functionality to avoid creating duplicate issues and/or PRs. If this github action starts spamming multiple issues and PRs, people will hate it.

[Kim Morrison]

We'd need to detect if there is an existing open issue or PR. Then there's a question: do we update that existing one, or just do nothing?

[Kim Morrison]

Let's change the text:

commit: silently commit the updated files

to

commit: directly commit the updated files

(It's confusing to use the work "silently" when there is a separate option called "silent".)

[Kim Morrison]

In the line

Therefore, this option does not affect the behavior when the build/test/lint fail after lake update.

I think "therefore" is the wrong word, and could be confusing. Just remove "therefore"?

[Kim Morrison]

"will not skip updates as long as" has an unnecessary double negative. Just write as "will perform an update if"

[Kim Morrison]

At https://github.com/Seasawher/lean-update/blob/main/scripts/checkChanges.js#L16, the error message refers to UPDATE_IF_MODIFIED, but the option name should not be capitalized.

[Kim Morrison]

What is postMerge.ps1? Again, let's avoid powershell.

[Kim Morrison]

There are several comments in https://github.com/Seasawher/lean-update/blob/main/action.yml#L127 of # bat. Perhaps remove? Or change to # bash script?

[Kim Morrison]

I just realised that lean-update contains the getLatest.js script and is manually updating the lean-toolchain.

I think we should not be doing this unless the repository has no dependencies. Remember that lake update will update the lean-toolchain itself if all upstream repositories have moved to a new toolchain.

[Kim Morrison]

Kim Morrison said:

We'd need to detect if there is an existing open issue or PR. Then there's a question: do we update that existing one, or just do nothing?

I think peter-evans/create-pull-request@v7 supports just updating the existing one. This is what the current Mathlib auto-update action does. See update_dependencies.yml.

[Kim Morrison]

When creating a PR and/or issue, it would be good to include some additional information.

• At least, today's date, so it is easy for humans to dismiss old issues/PRs
• Ideally, either the title or body would state the new toolchain, if that was being modified
• Possibly, the body should include a list of dependencies which were being modified (nice to have, but certainly not essential --- but if we don't want to implement this now, let's create an issue for the future)

[Kim Morrison]

It might be nice (very optional) to allow customizing the github author and email associated with commits (just noticing that the existing Mathlib-specific action does this).

[Kim Morrison]

(Sorry to spam you with requests like this! I'm really happy to see this being implemented. Don't worry about anything you don't have time/inclination for, I can come back later and create issues etc.)

[Asei Inoue]

@Kim Morrison

Thanks for the detailed review. Now I am busy, so if you could make an issue it would be very helpful.

[Asei Inoue]

I'll respond to the ones I can respond to right away.

What is postMerge.ps1? Again, let's avoid powershell.

This is just a development script that runs on my end. I'll make it a bash script.

There are several comments in https://github.com/Seasawher/lean-update/blob/main/action.yml#L127 of # bat. Perhaps remove? Or change to # bash script?

It's a setup to use the extension harrydowning.yaml-embedded-languages. This makes it easier to see bash scripts etc. embedded in yaml scripts.

I just realised that lean-update contains the getLatest.js script and is manually updating the lean-toolchain.

I think we should not be doing this unless the repository has no dependencies. Remember that lake update will update the lean-toolchain itself if all upstream repositories have moved to a new toolchain.

I thought so too, but it seems that if the Lean version of the repository to be updated is older, the update with lake update may not work.

[Asei Inoue]

@Kim Morrison Thanks a lot for your review. But Zulip makes it hard to manage, so next time I want reviews to be submitted to PR or issue

[Asei Inoue]

@Kim Morrison
I would like to continually test the ability to notify zulip, is there a thread I can use as I please?

[Edward van de Meent]

fwiw, you could have a bot send a DM

[Asei Inoue]

@Edward van de Meent Do I prepare a bot and then send the DM from the bot to me?

[Edward van de Meent]

yea

[Edward van de Meent]

i did a similar thing when i was testing how to escape ` in messages to zulip

[Edward van de Meent]

(apparently it's still non-trivial :smiling_face_with_tear: )

[Asei Inoue]

@Edward van de Meent Thank you. your idea works well

[Asei Inoue]

@Pietro Monticone

I have added an option to run lake -R -Kenv=dev update instead of lake update. If possible, please test lean-update action using the latest version!

[Pietro Monticone]

Ok, I'll do it as soon as I find the time. Thanks.

[Asei Inoue]

@Pietro Monticone Thank you!!

[Pietro Monticone]

Done in #Equational and #Infinity-Cosmos.

[Asei Inoue]

https://github.com/Seasawher/lean-update/releases/tag/v0.2.0

I've implemented the feature to avoid creating duplicate issue/PR!

[Asei Inoue]

Added lake build output to the body of the issue. This allows us to know why the update failed to some extent without having to retry.

image.png

[Asei Inoue]

I think I have implemented all of the features I wanted to implement in my use.

[Asei Inoue]

I think v1 release of lean-update would come soon…!

[Kim Morrison]

What's the status of my suggestions starting at #general > lean-action @ 💬 ?

[Asei Inoue]

see issue, please!
some of them are resolved

[Asei Inoue]

(deleted)

[Asei Inoue]

zulip notification

I agree it is best that lean-update itself doesn't do the zulip notification or toolchain release tagging. But we may want to package these steps as actions, too!

As for having this lean-update action have the ability to send messages to Zulip, it is not yet implemented. I am still on the fence about whether this functionality should be implemented. However, I have included a working example in the README and explained it a bit more carefully.

[Asei Inoue]

Notifycation typo

should be "Notification"

fixed!

[Asei Inoue]

avoid creating duplicate issue/PR

I think we also need to add some functionality to avoid creating duplicate issues and/or PRs.

resolved!!

[Asei Inoue]

description of commit option

It's confusing to use the work "silently" when there is a separate option called "silent".

done!

[Asei Inoue]

remove double negative

"will not skip updates as long as" has an unnecessary double negative. Just write as "will perform an update if"

done!

[Asei Inoue]

avoid pwsh

What is postMerge.ps1? Again, let's avoid powershell.

this is for development purpose only. (this is run in my local environment only)

[Asei Inoue]

comment in action.yml

There are several comments in https://github.com/Seasawher/lean-update/blob/main/action.yml#L127 of # bat. Perhaps remove? Or change to # bash script?

these comment is for syntax highlighting. see: https://marketplace.visualstudio.com/items?itemName=harrydowning.yaml-embedded-languages

[Asei Inoue]

manually update lean-toolchain

I just realised that lean-update contains the getLatest.js script and is manually updating the lean-toolchain.

No real harm has been done, so it is left as it is.

[Asei Inoue]

additional info

• At least, today's date, so it is easy for humans to dismiss old issues/PRs

As a feature of GitHub, the creation date of an issue or PR can usually be checked. Do we need to implement it?

• Ideally, either the title or body would state the new toolchain, if that was being modified

not implemented! I agree this is a wanted feature.

• Possibly, the body should include a list of dependencies which were being modified (nice to have, but certainly not essential --- but if we don't want to implement this now, let's create an issue for the future)

not implemented! I agree this is a wanted feature.

t might be nice (very optional) to allow customizing the github author and email associated with commits (just noticing that the existing Mathlib-specific action does this).

not implemented! Do we even want this?

[Asei Inoue]

@Kim Morrison

I have already implemented the minimum functionality I want in lean-update. So I have a question.

I would like to see lean-update incorporated into lake new, but people will be annoyed if I die or lose touch and there is no maintainer. So you would clone it under the leanprover organization, right? When will that be done? Who will be the new maintainer?

[Kim Morrison]

Yes, I'm sure we can adopt this under the leanprover-community organization. Personally, I'd be very happy if you'd continue as a maintainer of the repo, of course. We'll give people access as needed (at least people doing the monthly releases) or requested!

[Kim Morrison]

Asei Inoue said:

It might be nice (very optional) to allow customizing the github author and email associated with commits (just noticing that the existing Mathlib-specific action does this).

not implemented! Do we even want this?

We don't need to do this now. Might not hurt to open an issue about it, perhaps labelled help-wanted, to provide an easy place for someone new to get involved!

[Kim Morrison]

Asei Inoue said:

• Ideally, either the title or body would state the new toolchain, if that was being modified

not implemented! I agree this is a wanted feature.

Could you create an issue for this?

[Kim Morrison]

Asei Inoue said:

• Possibly, the body should include a list of dependencies which were being modified (nice to have, but certainly not essential --- but if we don't want to implement this now, let's create an issue for the future)

not implemented! I agree this is a wanted feature.

Also this.

[Kim Morrison]

Once we at least have the tracking issues up for those, I'm happy if you want to transfer to the leanprover-community organisation. I can click "accept" at the other end and give you maintainer status there.

[Asei Inoue]

@Kim Morrison

Once we at least have the tracking issues up for those, I'm happy if you want to transfer to the leanprover-community organisation. I can click "accept" at the other end and give you maintainer status there.

I tried, but it seems that it is not possible to transfer to a leanprover without the permission to create a public repository in the leanprover.

It would be necessary to create a new repository under leanprover by simply cloning & pushing.

[Kim Morrison]

Can you make me an admin of your existing repo? Then I can transfer it.

[Kim Morrison]

It looks like you only gave me write access. I'd need admin access to transfer it.

[Asei Inoue]

how to add admin access? I cannot edit collaborator access right.

[Kim Morrison]

https://github.com/Seasawher/lean-update/settings/access

[Asei Inoue]

I added you from the page.

[Asei Inoue]

image.png

[Asei Inoue]

image.png

[Kim Morrison]

Hmm, okay, that's different from what I'm used to.

[Kim Morrison]

Did you try transferring it to leanprover-community? Maybe it will ask someone to confirm? Sorry, I've forgotten how to do this, and will have to run in a moment.

[Oliver Butterley]

A github repository owned by a personal account has only two permission levels: repository owner and collaborators.

[Kim Morrison]

Let's just try transferring it then.

[Asei Inoue]

Did you try transferring it to leanprover-community?

I don't have right creating public repository in leanprover-community...

[Kim Morrison]

But does it actually error? I know it says that in the text, but I remember the past that there was a mechanism where the owner initiates the transfer, then we have to accept.

[Kim Morrison]

But I may be misremembering!

[Kim Morrison]

Have to go!

[Asei Inoue]

I can't :(

image.png

[Ruben Van de Velde]

I think you can transfer it to Kim first, and they can transfer to the org

[Asei Inoue]

I think you can transfer it to Kim first, and they can transfer to the org

nice idea! I've tried and succeed!

[Asei Inoue]

@Kim Morrison please accept transfer request

[Ruben Van de Velde]

I think Kim might be out for the weekend, but I expect they'll see it when they get back

[Kim Morrison]

@Asei Inoue, I'm sorry, I was too slow and the transfer has expired. If you'd like to try again I should be able to respond quickly this week.

[Asei Inoue]

I’ve sent invitation again!

[Kim Morrison]

Thanks. I've transferred it on to leanprover-community. I then re-added you with maintenance access, you'll need to check you email inbox to accept that.

[Asei Inoue]

With the release of v4.19.0-rc2, a number of bugs were found in the lean-update, all of which have been fixed! I think the development is going well.

[Pietro Monticone]

This topic might be of interest https://leanprover.zulipchat.com/#narrow/stream/479953-PhysLean/topic/Bumps.20of.20PhysLean.2E