leanprover-community/Lean update

Attempts to update lean and dependencies of a lean project

Trust Signals

Scorecard Score: not yet scored
Maintenance Recency: Activelast commit Jun 24, 2026
License: MIT

Pinned Snippet

workflow.ymlSHA-pinned

uses: leanprover-community/lean-update@6f7b598c3255645e06f5d31f9f77b7440fc16451 # v0.12.0

tags can be moved; commit SHAs can't. why a SHA?

Inputs

name	description	required	default
lake_package_directory	The directory containing the Lake package to update. This parameter is passed to the lake-package-directory argument of leanprover/lean-action.	no	.
update_lean_toolchain	Controls whether to update the lean-toolchain file for projects with no dependencies. Allowed values: * `auto`: Update the lean-toolchain file to the latest release (default behavior) * `never`: Do not update the lean-toolchain file Default: `auto`	no	auto
release_kind_to_fetch	The kind of the latest Lean release to fetch. This parameter is used only for Lean, not used for fetching other lake dependencies. Allowed values: * `nightly`: fetch the latest nightly release * `tagged`: fetch the latest tagged release (including both stable and pre-releases)	no	tagged
legacy_update	If set to `true`, executes `lake -R -Kenv=dev update` instead of `lake update`. Allowed values: * `true`: Execute `lake -R -Kenv=dev update` * `false`: Execute `lake update` Default: `false`	no	false
build_args	Build arguments to pass to `lake build` during post-update validation.	no	--log-level=warning
on_update_succeeds	What to do when an update is available and post-update validation is successful. Allowed values: * `silent`: Do nothing * `commit`: directly commit the updated files * `issue`: notify the user by creating an issue. No new issue will be created if one already exists. * `pr`: notify the user by creating a pull request. No new PR will be created if one already exists. Default: `pr`.	no	pr
on_update_fails	What to do when an update is available and post-update validation fails. Allowed values: * `silent`: Do nothing * `issue`: notify the user by creating an issue. No new issue will be created if one already exists. * `fail`: fail the action. Default: `issue`.	no	issue
update_if_modified	Specifies which files, when updated during `lake update`, will cause the action to update code or notify the user. This option does not affect the behavior when post-update validation fails after `lake update`. Allowed values: * `lean-toolchain`: If `lean-toolchain` is specified, this GitHub Action will skip updates unless the Lean version is updated. Here, "skipping updates" means "not attempting to update code or send notifications when post-update validation succeeds after lake update". * `lake-manifest.json`: if `lake-manifest.json` is specified, this GitHub Action will perform an update if any dependent package is updated. Default: `lake-manifest.json`	no	lake-manifest.json
token	A Github token to be used for committing	no	${{ github.token }}

Outputs

name	description
has_dependency	This value is `true` or `false` depending on whether the lake package has dependencies.
result	The action outputs `no-update`, `update-success` or `update-fail` depending on the three possible scenarios. Description of each value: * `no-update`: No update was available. * `update-success`: An update was available and post-update validation was successful. * `update-fail`: An update was available but post-update validation failed.
latest_lean	The latest Lean release version, including both stable and pre-release versions. This value could be also nightly. ## Note * This is not necessarily matching to the updated content of the lean-toolchain file of the lake package. * This value is fetched according to the `release_kind_to_fetch` option.
notify	Indicates whether there is an event worth notifying the user about. Returns `true` in the following cases: * When updates are available and post-update validation succeeds. However, if `update_if_modified` is set to `lean-toolchain`, this is only true when the Lean version has been updated. * When updates are available and post-update validation fails. Returns `false` in all other cases.