feat: add opt-in axiom-audit check#166
Open
kim-em wants to merge 2 commits into
Open
Conversation
This PR add an opt-in `axiom-audit` input that audits a project's axioms with leanprover-community/axiom-audit: it fails CI if any declaration defined under the project's library namespace transitively depends on an axiom outside an allowlist (default propext, Classical.choice, Quot.sound), catching sorry, native_decide, and home-rolled axioms — including ones reaching in through imports. Modeled on the nanoda integration, the tool is cloned and built with the project's own toolchain, then run against the compiled environment via `lake env`, so no per-project dependency is required. Adds `axiom-audit-allow` and `axiom-audit-root` inputs, an `axiom-audit-status` output, and a functional test that verifies success on a clean library and failure once a home-rolled axiom is introduced. Default off. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
- force `lake build` before auditing so a `build: false` or stale checkout can't silently audit the wrong (or missing) oleans - pin the tool by commit SHA (verified after clone), not just the mutable v0.1.2 tag - let the tool auto-detect the library root from the lakefile (it now does), dropping the brittle bash lakefile parsing; pass --root only when axiom-audit-root overrides it - run in a mktemp dir under RUNNER_TEMP instead of a _axiom_audit dir in the package tree - shellcheck polish: set -euo pipefail, quote the exit status, re-exit from the trap - run the functional test on the modern toolchain (the tool builds with the project's toolchain) - fix the axiom-audit-root doc to say "first lean_lib", matching the implementation Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR adds an opt-in
axiom-auditinput that audits a project's axioms with leanprover-community/axiom-audit: it fails CI if any declaration defined under the project's library namespace transitively depends on an axiom outside an allowlist (defaultpropext,Classical.choice,Quot.sound), catchingsorry,native_decide(Lean.ofReduceBool), and home-rolled axioms — including ones reaching in through imports. Because it inspects the compiled kernel environment, it catches what agrepcannot.Modeled on the
nanodaintegration: the tool is cloned (pinned atv0.1.0) and built with the project's own toolchain, then run against the compiled environment vialake env, so no per-project dependency is required. New inputsaxiom-audit-allowandaxiom-audit-root, a newaxiom-audit-statusoutput, and a functional test (.github/functional_tests/axiom_audit) that verifies success on a clean library and failure once a home-rolled axiom is introduced.Default off — like every other check here, it does nothing unless
axiom-audit: trueis set. (axiom-audit builds with the project's toolchain, so it needs a recent enough Lean; the tool's README documents the minimum.)I verified the integration end to end locally: on a clean
lake init … libpackage the check reportsaxiom-audit-status=SUCCESS(exit 0); after appending a home-rolledaxiom, it reports the offending declarations andaxiom-audit-status=FAILURE(exit 1).Context: the tool generalizes an audit from the TauCeti project; its fast shared-cache axiom collection is also being upstreamed to Lean core as leanprover/lean4#14157.
Implemented with assistance from Claude Code (Anthropic).