leanprover/Lean Action - CI for Lean Projects

Standard CI for Lean projects. Steps: - install elan - get Mathlib cache (optional, must be downstream of Mathlib) - lake build - lake test (optional) - lake exe runLinter (optional, must be downstream of Batteries) - check reservoir eligibility (optional) - check environment with leanchecker (optional)

View on GitHub

Trust Signals

Scorecard Score: not yet scored
Maintenance Recency: Activelast commit Apr 22, 2026
License: Apache 2.0

Pinned Snippet

workflow.ymlSHA-pinned

uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1.5.0

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

Inputs

name	description	required	default
auto-config	Automatically configure `lean-action` based on the Lake workspace. When set to "true", `lean-action` will use the Lake workspace to determine the set of features to run on the repository, such as `lake build` and `lake test`. Even when set to "true", the user can still override the auto configuration with the `build` and `test` inputs. Allowed values: "true" or "false".	no	true
build	Run `lake build`. Note, this input takes precedence over `auto-config`. Allowed values: "true" \| "false" \| "default".	no	default
test	Run `lake test`. Note, this input takes precedence over `auto-config`. Allowed values: "true" \| "false" \| "default".	no	default
lint	Run `lake lint`. Note, this input takes precedence over `auto-config`. Allowed values: "true" \| "false" \| "default".	no	default
mk_all-check	Check all files are imported with `lake exe mk_all --check`. Allowed values: "true" \| "false"	no	false
build-args	Build arguments to pass to `lake build {build-args}`. For example, `build-args: "--quiet"` will run `lake build --quiet`. By default, `lean-action` calls `lake build` with no arguments.	no	""
test-args	Test arguments to pass to `lake test {test-args}`. For example, `test-args: "--quiet"` will run `lake test --quiet`. By default, `lean-action` calls `lake test` with no arguments.	no	""
use-mathlib-cache	By default, `lean-action` attempts to automatically detect a Mathlib dependency and run `lake exe cache get` accordingly. Setting `use-mathlib-cache` will override automatic detection and run (or not run) `lake exe cache get`. Project must be downstream of Mathlib to use the Mathlib cache. Allowed values: "true" \| "false" \| "auto".	no	auto
check-reservoir-eligibility	Check if the repository is eligible for the Reservoir. Allowed values: "true" \| "false".	no	false
leanchecker	Check environment with leanchecker. Uses the bundled `leanchecker` binary on Lean `nightly-2026-01-09` / `v4.28.0-rc1` and newer. Falls back to building the external `lean4checker` repository on older Lean versions. Allowed values: "true" \| "false".	no	false
lean4checker	Deprecated alias for `leanchecker`. Uses the bundled `leanchecker` binary on Lean `nightly-2026-01-09` / `v4.28.0-rc1` and newer. Falls back to building the external `lean4checker` repository on older Lean versions. Allowed values: "true" \| "false".	no	false
nanoda	Check environment with nanoda external type checker. nanoda is an independent Lean 4 type checker written in Rust. Requires Rust toolchain (will be installed automatically if not present). Allowed values: "true" \| "false".	no	false
nanoda-allow-sorry	When running nanoda, permit the sorryAx axiom. Set to "false" if your project should have no sorry placeholders. Allowed values: "true" \| "false".	no	true
use-github-cache	Enable GitHub caching. Allowed values: "true" or "false". If use-github-cache input is not provided, `lean-action` will use GitHub caching by default.	no	true
lake-package-directory	The directory where `lean-action` will look for a Lake package and run `lake build`, etc. Allowed values: a valid directory containing a Lake package. If lake-package-directory is not provided, `lean-action` will use the root directory of the repository by default.	no	.
reinstall-transient-toolchain	When the `lean-toolchain` file specifies a `lean-pr-release` toolchain, uninstall it before running any `lake` commands. This ensures the latest build of the toolchain will be downloaded and used to run CI steps. Allowed values: "true" \| "false".	no	false

Outputs

name	description
build-status	The status of the `lake build` step. Allowed values: "SUCCESS" \| "FAILURE" \| "".
test-status	The status of the `lake test` step. Allowed values: "SUCCESS" \| "FAILURE" \| "".
lint-status	The status of the `lake lint` step. Allowed values: "SUCCESS" \| "FAILURE" \| "".
mk_all-status	The status of the `lake exe mk_all --check` step. Allowed values: "SUCCESS" \| "FAILURE" \| "".
detected-mathlib	If lean-action detected a mathlib dependency equals "true" otherwise equals "false".
nanoda-status	The status of the nanoda check step. Allowed values: "SUCCESS" \| "FAILURE" \| "".