Create a standard GitHub action for Lean projects

[kim-em]

We should create a GitHub action that users can add to their .github/workflows/ci.yml file (and indeed, lake init can create such).

It should automatically:

• setup elan
• if downstream of Mathlib, run lake exe cache get
• lake build
• lake test
• if downstream of Std, run Std's linter framework

Probably also, but certainly with an easy mechanism to opt-out (that is explained on failure)

• check if the project is eligible for inclusion in Reservoir
• run lean4checker on the project (make it easy to run in a cron job, as this can slow down CI)

It could also:

• provide a cron job that tries lake update && lake build, and reports (either via emails, notifications, or opening PRs) the result.

[austinletson]

Based on these requirements, GitHub recommends we put the custom action in it's own repository. This would allow lean projects to use the action by adding,

- uses: leanprovercommunity/lean-action@{version-number-tag}

to their continuous integration workflow config.

To give an idea, here is an action with elan -> cache -> build -> test -> lint capabilities. Currently the action is configured by three inputs:

• test : Bool (defaults to true)
  • when test = true, include step to run lake test (this only works on versions of lean after lake test was introduced)
• mathlib-cache : Bool (defaults to false)
  • when mathlib-cache = true, run lake exe cache get before other build steps
• lint-module: String (defaults to empty string)
  • if the lint-module input is a non empty string, include step to run lake exe runLinter {lint-module}

Here are two repos to demonstrate usage:

• A package with a Mathlib dependency with mathlib-cache and lint-module inputs and test = false
  • link to ci.yml
  • link to ci run which uses the action
• A package with no dependencies using nightly toolchain (required for lake test) which runs tests but doesn't use mathlib cache or linting. This is the default configuration if you don't provide any inputs to the action
  • link to ci.yml
  • link to ci run which uses the action

Does this seems like the right approach?

If so I can expand this to,

• optionally include Reservoir and lean4checker
• automatically choosing the right input parameters (currently you need to manually set the mathlib-cache and lint-module inputs)

[kim-em]

Yes, this is the right approach, and I'm really happy to see this!

It would be fantastic if we could provide a good default for mathlib-cache, that just tries to check for Mathlib in the dependencies (a very simple test is "does .lake/packages/mathlib exist", although perhaps that doesn't exist in a fresh repository until some lake command has run).

[Seasawher]

I thought it would be nice to include caching the .lake directory in the CI. Would this not contribute to increased speeds?

[austinletson]

I thought it would be nice to include caching the .lake directory in the CI. Would this not contribute to increased speeds?

@Seasawher We could potentially cache some of the build files using the cache action. It takes a list of paths to cache and a key to match caches on, usually a hash of a lock file. Potentially we could use .lake for the directories and hash lake-manifest.json for the key?

[austinletson]

It would be fantastic if we could provide a good default for mathlib-cache, that just tries to check for Mathlib in the dependencies (a very simple test is "does .lake/packages/mathlib exist", although perhaps that doesn't exist in a fresh repository until some lake command has run).

@semorrison I think you are right that the existence of .lake would be an issue

How about greping the lakefile.lean? I updated the action with a grep "require mathlib" lakefile.lean step.

Updated usage examples:

• Now we get the cache without setting the mathlib-cache input in the mathlib test repo (link to pipeline)
• The other test package without a Mathlib dependency logs "Mathlib dependency not found. Skipping Mathlib cache." and proceeds (link to pipeline).

The grep solution is still somewhat brittle if the dependency is not declared in lakefile.lean. For instance, if a package uses a lakefile.toml or if Mathlib is a transitive dependency.

Does lake have something similar to cargo tree which would give a more reliable graph of the dependencies? If not, grep "require mathlib" could be good for now as long as users can manually set the action to use the Mathlib cache through setting the mathlib-cache input in edge cases.

[Kha]

hash lake-manifest.json for the key?

That would mean new build results are not cached as long as that file is unchanged. You should instead make sure that each unique build generates a unique key but also can fall back to previous caches using restore-keys, see e.g. https://github.com/leanprover/lean4/blob/master/.github/workflows/ci.yml#L303-L310

[austinletson]

Ah, okay. Thanks for the tip @Kha.

I have added the cache action before running any lake commands with the following configuration:

    - uses: actions/cache@v4
      with:
        path: .lake
        key: ${{ runner.os }}-lake-${{ github.sha }}
        # if no cache hit, fall back to the (latest) previous cache
        restore-keys: ${{ runner.os }}-lake-

One area for improvement is that the github cache will cache the Mathlib cache generated by lake exe cache get which seems redundant and takes up significant space in the github cache. I will look into improving this after implementing the rest of the requirements listed in the initial issue.

[austinletson]

The action now includes an optional step to check reservoir eligibility using the inclusion criteria. It verifies the repository,

• is not private
• contains a lake-manifest.json file
• contains a GitHub-recognized OSI-approved license
• has two or more stars

[nomeata]

Nice! Another possibility useful tweak is to save the cache even upon build or test failures:
https://stackoverflow.com/a/75961093/946226

This way when you fix a build failure, the build will continue from there. Very useful if otherwise you'd be watching it compile std over and over again :-)

[austinletson]

Thanks for the suggestion, @nomeata. I've added a step to preserve the cache after lake build but before lake test. This ensures that even if any tests fail and halt the CI pipeline, the cache remains intact. Currently, I haven't found a way to save the cache using actions/cache if lake build fails. The save-always parameter seemed like a potential solution, but it's currently not functioning as expected. However, as long as lake build was successfully cached in a different commit, the restore-keys should restore that cache and you wouldn't have to wait for dependencies to compile.

[austinletson]

Regarding lean4checker and lake update && lake build: Integrating tasks which should be scheduled with a cron job while maintaining user-friendly defaults presents a challenge. It appears that users would need to invoke the action twice: once for pushes/PRs and another with a cron job.

To support both use cases, we could modify the inputs to resemble action-python, where users specify the exact steps to run. However, this may complicate the user interface more than it adds value.

As an alternative, we could create a separate action in the same repo for these tasks, perhaps named lean-periodic or lean-cron, specifically designed to be scheduled with a cron job, rather than being triggered by pushes/PRs.

[nomeata]

Maybe a cron-based job isn't great for the fits-80%-solution anyways? It is annoying with forks, and with low activity repositories GitHub after a while sends annoying mails about disabling the cron job. Maybe to keep it simple make running lean4checker optional and leave it at that?

[kim-em]

Yes, thinking about it again let's keep lean4checker as a push-triggered event. For small repositories it runs fast enough it shouldn't be a problem.

[kim-em]

I'm really excited to see this work: don't hesitate to ping me if I can help with next steps. I would suggest we create a repository under the leanprover organization to host this action, maybe even just leanprover/action. If that sounds good, I can create it.

[austinletson]

@semorrison A repository under leanprover sounds great! For naming, what about leanprover/lean-action? Forks will be more clear: austinletson/lean-action instead of austinletson/action.

I an create a README.md and make an initial PR so development can continue in that repository.

[kim-em]

@austinletson, I have created leanprover/lean-action, and added you as a maintainer.

[oliver-butterley]

Great to see this functionality being made more accessible as an action.

I worry that lean-action is very generic as a name, particularly when it is likely there will be other lean actions. How about a name that describes what it does? lean-check-action? lean-test-action? This leaves the possibility for lean-update-action and many other things.

[Seasawher]

Why not include lean update actions in this as well? Actions that automatically update Lean and mathlib versions should be in demand, as Lean is frequently updated.

[oliver-butterley]

I believe standard use would be that some workflow tasks need to run on commits and PRs whilst others need to be run periodically. Consequently they must be separate actions. Also separate actions allow more per repo customization and better feedback when something fails.

[oliver-butterley]

I was exaggerating when I wrote "must be separate actions", the comment above explains a style of having one action with multiple functionality where different functionality is selected using input variables. I believe above it was decided to opt for the style of separate actions.

In this use case I believe separate actions will be more comfortable for the majority of people who use it. However my experience of lean is much less than my experience with github actions so it is for others with more lean experience to decide!

[austinletson]

@austinletson, I have created leanprover/lean-action, and added you as a maintainer.

Thanks! I will move over the current version and update documentation to reflect the change.

[austinletson]

I worry that lean-action is very generic as a name, particularly when it is likely there will be other lean actions. How about a name that describes what it does? lean-check-action? lean-test-action? This leaves the possibility for lean-update-action and many other things.

@oliver-butterley this is a good point. If the vision is to have multiple action repos for the periodic and push/PR actions, lean-action is probably not specific enough.

I had originally thought that it may make sense to have two actions in one repository, but it seems like GitHub doesn't recommend this. This is actually a requirement for publishing the action on GitHub Marketplace. Note, we don't have to publish the action on GitHub marketplace in order for Lean projects to use it.

lean-check-action seems reasonable to me, but I would defer to those with more knowledge of the Lean community and the leanprover GitHub organization for the naming scheme.

[digama0]

My understanding is that leanprover/lean-action will just be the main repository for holding all leanprover github actions, and the actual different behaviors will either be exposed as subfolders or options in a single multi-personality action. It's a bit annoying to have to write the framework code in five separate repos if we go that route.

[austinletson]

Alright, thanks for the context.

@semorrison I have moved the work which was done for this issue to leanprover/lean-action and created a few initial issues there from todos in this issue, including one to track an initial beta release.

Additionally, I did an initial test of uses: leanprover/lean-action@main on my fork of lean4-cli (link to job) which worked as expected.

[Kha]

Given that lean-action has had a v1 release, I think we can close this! Thank you very much, @austinletson!