Leverage Lake's API to determine if a package is downstream of Mathlib

Currently, lean-action uses grep to determine if a package is downstream of Mathlib. This is brittle. Instead, we should leverage Lake's API to determine if a package is downstream of Mathlib.

Add input to support passing parameters to `lake build`

Some existing lean projects use -K to pass parameters to lake when running lake build etc (see this line in the batteries workflow).

Supporting this will require some thinking about how these parameters should be passed into lean-action.

Mathlib detection prints unnecessary error when lakefile.toml not present

From https://github.com/leanprover-community/batteries/actions/runs/9181778942/job/25249274199?pr=805:

Mathlib Detection
  Trying to detect if project is downstream of Mathlib.
  grep: lakefile.toml: No such file or directory

Update `RELEASING.md` based on improvements to release process

Now that lean-action contains an automated functional test suite, revisit RELEASING.md to make sure it aligns with the new process
Add a template for release issues based on #66

Leverage output parameters for `lake build` and `lake test` steps to to verify the expected steps ran during a test

Currently, the tests in .github/functional_tests do not verify the expected steps ran during the test run of lean-action. We can leverage workflow commands and output parameters to verify the correct steps ran.

In the future, we may expose these outputs to lean-action users so they can use the results of lean-action in later workflow steps.

Parameterize functional tests by lean version.

Currently functional tests use 4.8.0.
We want a way to run the functional test suite with any version of lean:

to make updating lean-action between lean versions easier (ideally there would be nothing to update in the lean-action repo when an new version of lean is released).
to support multiple versions of lean with confidence.

Problem about caching strategy for Lean

Note: This is based on my assumptions and might not be entirely accurate.

This issue occurs when we update our project from v4.9.0-rc1 to v4.9.0-rc2. FormalizedFormalLogic/Foundation#85
And it seems to be happens same problem branch in the nightly branch of the import-graph.

In our project, we set the GitHub Action cache strategy as follows

path: .lake
key: lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}-${{ github.ref }}
restore-keys: |
    lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}-${{ github.ref }}
    lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}
    lake-${{ runner.os }}

The problem we encountered was with the restore-keys we specified. The issue is that when updating the Lean version itself, the previous version's cache also becomes a fallback candidate. In our project, it seems we referenced the v4.9.0-rc1 cache, which caused the build to fail.

Solution is remove fallbacks of restore-keys to lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}-${{ github.ref }} only.

Currently, the cache strategy of this action is similar (i.e., it doesn't avoid using the cache when the Lean version itself is updated).

lean-action/action.yml

Lines 93 to 99 in 52906d4

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

This seems to be why the nightly branch of the import-graph is broken.
As a solution, specifying ${{ hashFiles('lean-toolchain') }} as the key should work.

Improve log readability by grouping log lines inside of steps

The logging produced by each step of lean-action is not properly grouped. This make it is difficult to tell which logs are generated by which steps when reading the output of lean-action (see example form aesop here).

GitHub provides ::group:: and ::endgroup:: workflow commands which allow us to group the logs of each step into a collapsible group.

bug: run `lake update` and `lean-action` gets an error

This workflow raise an error: https://github.com/lean-ja/lean-by-example/actions/runs/9530357340/workflow
The workflow content is simple: Just install elan, run lake update and then lean-action.

jobs:
  build:
    runs-on: ubuntu-latest
    steps:
      - name: checkout
        uses: actions/checkout@v4

      # - name: update lean-toolchain
      #   run: |
      #     LATEST_LEAN=$(gh release list --repo leanprover/lean4 --limit 1 | awk '{print $1}')
      #     echo "The latest release/prerelase is: $LATEST_LEAN"
      #     echo "leanprover/lean4:$LATEST_LEAN" > lean-toolchain
      #   env:
      #     GH_TOKEN: ${{ github.token }}
      #   shell: bash

      - name: Install elan
        run: |
          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
          echo "$HOME/.elan/bin" >> $GITHUB_PATH
        shell: bash

      - name: Update dependencies of ${{ github.repository }}
        run: lake update
        shell: bash

      - name: build lean
        uses: leanprover/lean-action@main
        with:
          test: false

You can see error details: https://github.com/lean-ja/lean-by-example/actions/runs/9530357340/job/26270125659

error message:

▼ Run : Get Mathlib Cache
  : Get Mathlib Cache
  echo "::group::Mathlib Cache"
  lake exe cache get
  echo "::endgroup::"
  echo
  shell: /usr/bin/bash --noprofile --norc -e -o pipefail {0}
▼ Mathlib Cache
  info: mdgen: updating repository '././.lake/packages/mdgen' to revision '6a6a412465e82572f6e30385592eac52ab055c83'
  info: mathlib: updating repository '././.lake/packages/mathlib' to revision '03092720f68254315c95a5bf2[49](https://github.com/lean-ja/tactic-cheatsheet/actions/runs/9530357340/job/26270125659#step:5:55)c5f2cdef717d6'
  error: external command 'git' exited with code 1
  Error: Process completed with exit code 1.

I have no idea what caused it.

Use `lake check-test` to detect absence of a test runner

lake check-test will return exit code 1 if no test runner is available.

When lean-action tries to run tests, we should check this first, and provide a helpful error message. (For now, as the test framework is changing quickly, it doesn't need to be particularly helpful! Later we can point to some proper documentation on how to set up test runners.)

detect_mathlib assumes a lakefile.lean; should also support lakefile.toml

We don't necessarily actually need to parse the TOML (although there is a TOML parser baked into core lean now!) and can probably get away with grepping for now. We'd be looking for:

[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4"

Enhance version information logging

Add a step to lean-action (ideally after detect mathlib) to log:

Lean version
Lake version
Whether the project is downstream of mathlib

This aligns with logging practices in existing Lean CI workflows (e.g., import-graph).

(DRAFT RFC) Add support for building leanblueprint to lean-action

Some projects rebuild the leanblueprint site when a new PR is merged into the main branch to keep the blueprint updated with the latest progress, e.g., this workflow from carleson.

I imagine there are a range of workflows for this CI step, so this may be difficult to support. But this seems like a nice feature to add to lean-action.

Redundant mathlib caching

One area for improvement is that currently the action caches the mathlib cache generated by lake exe cache get which seems redundant and takes up significant space in the GitHub cache.

One potential fix for this would be to exclude certain subfolders of .lake from the cache. This behavior of the cache action may be relevant.

Add support for `lean4checker`

Add an input for users to enable lean4checker and a corresponding step which runs lean4checker

Document use cases where additional Lean CI steps are taken after `lean-action`

In many cases, Lean developers will want to run additional Lean related CI steps after lean-action runs which take advantage of the features of lean-action. For instance in import-graph, there is a step to verify lake exe graph which uses the elan setup and .lake caching features from lean-action (see leanprover-community/import-graph#9).

The lean-action README.md should document where this is possible and give examples.

Automatically check if test runner is available

Automatically checks if test_driver or test_runner is defined in lakefile.lean and executes lake test if it is defined, otherwise does not.

It would be tedious to have the user manually enter whether or not to run lake test each time. default input should be auto.

Add option to disable `lake build`

I sometimes want just to install elan and not to run lake build

v1-beta release

Create a release/v1-beta branch for the release candidate.
Run functional_tests.yml workflow on release/v1-beta.
Test release/v1-beta on existing test projects.
Create a release of release/v1-beta with a v1-beta tag.
- Copy the release notes from the ## Unreleased section of CHANGELOG.md.
Verify action with uses: leanprover/lean-action@v1-beta.
Create a PR to update README.md and CHANGELOG.md.

Automatically detect module for `lake exe runLinter`

Instead of users manually providing a module to lint with the lint-module input, automatically detect which module to lint.

Depending on how this automatic detection works, we may still want to allow users to manually specify which module to lint.

Create `auto-config` input

Create auto-config input to allow users to specify if lean-action should use the Lake workspace (or grep in some cases) to determine a configuration for lean-action.

Related: #30, #46, #53

This feature still needs to be fleshed out.

Support repositories with subdirectory Lean packages

Some projects contain Lean packages within a subdirectory of the GitHub repository (e.g. cedar-spec).

Two ways to potentially support this case:

Document how users can leverage the working-directory feature of GitHub workflows to achieve this behavior (this seems preferable if it works properly)
Add input to specify the directory which lean-action should run

v1-beta.1 release

Inconsistency with `mathlib-cache` input

The current situation is:

mathlib-cache:
    description: |
      Run "lake exe cache get" before build.
      Project must be downstream of Mathlib.
      Allowed values: "true" or "false".
      If mathlib-cache input is not provided, the action will attempt to automatically detect if the project is downstream of Mathlib.
    required: false
    default: ""

    - name: detect mathlib
      # only detect Mathlib if the user did not provide the mathlib-cache input
      if: ${{ inputs.mathlib-cache == '' }}
      # etc...

An input here of either "true" or "false" will have the same effect. Possible solutions:

the description of the input is changed,
or, set required: true and default: false for this input and change the conditional to ${{ inputs.mathlib-cache == 'false' }}

Style note: could be clearer for the input name to be "get-mathlib-cache" or "use-mathlib-cache". (At the moment "mathlib-cache: true" could be understood to mean that the action can expect mathlib-cache to have already been obtained in a step prior to lean-action.)

Add an option to disable GitHub caching

It is useful to have an option to disable GitHub caching because GitHub caching doesn't work well with automated testing of lean-action

Save cache even if a build fails

We should be able to save the cache even if a build fails similar to this example.

For reference, here is the initial discussion where we explored the now unsupported save-always flag.

build args default should be 'quiet'

output messages are usually unnecessary.

Add existing usage examples to README.md

Add examples to README.md of lean projects which use lean-action

v1-alpha release

Align on features to include in `leanprover/lean-action@v1-alpha
Create release/v1-alpha branch for release candidate
Test release/v1-alpha on existing test projects
Create release of release/v1-alpha with v1-alpha tag
Verify action with uses: leanprover/lean-action@v1-alpha

install elan on windows

I have created a workflow running on Windows.

see: https://github.com/lean-ja/lean-by-example/blob/edc6f5e9d023b0f4c4beb26474e1b678b8e9ba5e/.github/workflows/ci.yml#L29

Almost always building on Windows is not necessary, but I sometimes need this. (For example, when trying to provide an environment which reproduce a lean bug on Windows machine...)

v1.0.0 release

Std is renamed Batteries

    # Run "lake exe runLinter" on the specified module.
    # Project must be downstream of Std.
    # Allowed values: name of module to lint.
    # If lint-module input is not provided, linter will not run.
    lint-module: ""

Fix GitHub cache keys to reduce problems with the cache when updating Lean version

The GitHub cache can cause problems when updating Lean version. To fix this and improve the overall caching strategy, we can add hashes of the lean-toolchain and lake-manifest.json files to the cache keys to narrow cache hits to runs of lean-action with the same toolchain and lake manifest.

In action.yml,

update the - uses: actions/cache@v4 step to use the following key and restore-key inputs:

key: lake-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
restore-keys: lake-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}

update the - uses: actions/cache/save@v4 step to use the following key input:

key: lake-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}

See #62 and #64 for original bug reports

Update the lint step to use the more flexible `lake lint`

leanprover/lean4#4261 adds support for a new lake lint command. We should refactor the lint step to use this more flexible linting command. We should still test that the batteries linting framework works when wrapped with lake lint.

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

leanprover / lean-action Goto Github PK

lean-action's People

Contributors

Stargazers

Watchers

Forkers

lean-action's Issues

v1.0.0 release

Recommend Projects

Recommend Topics

Recommend Org