Lean Update

A GitHub Action that attempts to update Lean and dependencies of a Lean project. This is basically a fork of oliver-butterley/lean-update but more feature-rich.

Quick Setup

Create a file named update.yml in the .github/workflows directory.

If you want to keep dependencies always up-to-date

To keep dependencies always up-to-date, you might want to configure as follows:

name: Update Lean Projecton:
schedule:
- cron: "0 0 * * *"# every dayworkflow_dispatch: # allows workflow to be triggered manuallyjobs:
update_lean:
# The default GITHUB_TOKEN is read-only, so the write scopes have to be asked for.# Opening the pull request also needs `Allow GitHub Actions to create and approve pull# requests` under Settings > Actions > General > Workflow permissions.permissions:
contents: writepull-requests: writeissues: writeruns-on: ubuntu-lateststeps:
- name: Checkout codeuses: actions/checkout@v6
- name: Update Lean projectuses: leanprover-community/lean-update@main

When you only want to update when there is a new Lean version

If you want to skip updates unless there is a change to the lean-toolchain file, you might want to configure as follows:

name: Update Lean Projecton:
schedule:
- cron: "0 0 * * *"# every dayworkflow_dispatch: # allows workflow to be triggered manuallyjobs:
update_lean:
# The default GITHUB_TOKEN is read-only, so the write scopes have to be asked for.# Opening the pull request also needs `Allow GitHub Actions to create and approve pull# requests` under Settings > Actions > General > Workflow permissions.permissions:
contents: writepull-requests: writeissues: writeruns-on: ubuntu-lateststeps:
- name: Checkout codeuses: actions/checkout@v6
- name: Update Lean projectuses: leanprover-community/lean-update@mainwith:
update_if_modified: lean-toolchain

If you want to receive notifications on Zulip when the update fails

1. First, create a bot in Zulip and note its API key. Be careful not to create a new account - Zulip has a dedicated feature for "creating a bot".
2. Next, register the bot's API key as a secret named ZULIP_API_KEY in your repository. You can set up secrets from the repository's "Settings".
3. Prepare a workflow file like the following:

name: Update Lean Projecton:
schedule:
- cron: "0 0 * * *"# every dayworkflow_dispatch: # allows workflow to be triggered manuallyjobs:
update_lean:
# The default GITHUB_TOKEN is read-only, so the write scopes have to be asked for.# Opening the pull request also needs `Allow GitHub Actions to create and approve pull# requests` under Settings > Actions > General > Workflow permissions.permissions:
contents: writepull-requests: writeissues: writeruns-on: ubuntu-lateststeps:
- name: Checkout codeuses: actions/checkout@v6
- name: Update Lean projectid: lean-updateuses: leanprover-community/lean-update@mainwith:
on_update_fails: "silent"
- name: Notificationif: steps.lean-update.outputs.result == 'update-fail' # only send a message when the update failsuses: zulip/github-actions-zulip/send-message@v1with:
api-key: ${{ secrets.ZULIP_API_KEY }} # Zulip API key of your botemail: "***-bot@leanprover.zulipchat.com"# your Zulip bot's emailorganization-url: 'https://leanprover.zulipchat.com'to: "123456"# user_idtype: "private"# private messagecontent: | ❌ The update of ${{ github.repository }} has failed - [See Action Run](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}) - [See Commit](https://github.com/${{ github.repository }}/commit/${{ github.sha }})

Description of Functionality

1. This Action first installs elan and runs lake update. This fetches the latest Lean release and updates all dependent packages to their latest versions.

2. If lake update determines that all dependencies are already up to date, this Action does nothing further.

3. Subsequently, this GitHub Action validates the updated code. This performs the build process, runs tests if a test driver is configured, and executes lint checks if a lint driver is set up. You can configure what build arguments are passed to lake build using the build_args option.

4. This Action classifies the post-update validation results into two categories: success or failure.

   1. If successful, it behaves according to the setting specified in the on_update_succeeds option. By default, this is set to pr, which submits the updated code as a pull request. However, if the update_if_modified option is set to lean-toolchain, the Action does nothing unless the Lean version has been updated.
   2. If it fails, it behaves according to the setting specified in the on_update_fails option. By default, this is set to issue, which submits an issue indicating that the update failed.

Details of Option

See action.yml for details.