rodbourn/lean-assumptions audit
Audit the assumption surface of a Lean 4 module in CI. Requires the consumer project to `require lean-assumptions` in its lakefile; this action installs the toolchain pinned by the project's lean-toolchain, builds the CLI on demand via `lake exe`, runs the audit, and fails on policy findings unless told otherwise. It audits elaborated declaration types only; it does not validate proof axioms, sandbox execution, or prove theorem-statement equivalence.
View on GitHubTrust Signals
- Scorecard Score
- not yet scored
- Maintenance Recency
- Stale
- License
- None
Inputs
| name | description | required | default |
|---|---|---|---|
| module | Fully qualified Lean module to import and scan (e.g. MyProject.Theorems). | yes | — |
| preset | Base policy preset, `strict` or `hidden`. Empty uses the CLI default (strict). | no | "" |
| policy | Path to a policy-v1 JSON file, relative to the working directory. | no | "" |
| transparency | Alias-transparency mode, `none`, `reducible`, or `recursive_normalization`. | no | "" |
| baseline | Path to a checked-in v1 batch JSON baseline. When set, the audit runs in baseline mode and fails only on finding identities absent from the baseline. | no | "" |
| extra-args | Extra CLI arguments appended verbatim (e.g. allow flags). | no | "" |
| artifact-path | Where to write the JSON audit artifact. | no | lean-assumptions-report.json |
| fail-on-findings | Fail the step when the audit exits nonzero. Set `false` to only record outputs. | no | true |
| allow-empty-scan | A scan that matches 0 declarations fails by default, because a misconfigured module name would otherwise pass silently (a pure re-export root module declares no constants of its own). Set `true` to permit empty scans. | no | false |
| working-directory | Directory of the Lake package to audit. | no | . |
Outputs
| name | description |
|---|---|
| result | `pass` (exit 0), `findings` (exit 1), `empty-scan` (0 declarations matched), or `error` (exit 2 or other). |
| exit-code | Raw CLI exit code (0 pass/warn, 1 policy failure or audit error, 2 usage/import errors). |
| artifact | Path to the JSON audit artifact (empty when the CLI could not produce one). |