lambdaclass / lambdaclass/trust-lean
Enable --wfail axiom-guard gate once warnings are clean
Nobody has claimed this yet.
- Dominant language
- Lean
- Stars
- 3
- Forks
- 3
- PR merge metrics
- No merged PRs in 30d
Description
The lean_extensions axiom-guard plugin is now wired into the lakefile and active during lake build. CI currently runs a plain lake build rather than lake build --wfail, because the axiom guard reports pre-existing declarations that depend on non-standard axioms. These all come from native_decide-style proofs and pull in two axioms: Lean.ofReduceBool and Lean.trustCompiler.
Once these are resolved (e.g. replaced with decide or kernel-checkable proofs, or explicitly allowlisted via linter.axiomGuard.allowedAxioms), switch the CI workflow (.github/workflows/ci.yml) to build-args: "--wfail" so the axiom guard is enforced as a gate.
Affected declarations (22 total, each depends on both Lean.ofReduceBool and Lean.trustCompiler):
TrustLean/Backend/Common.lean:244TrustLean.countChar_joinCodeTrustLean/Backend/Common.lean:452TrustLean.sanitizeIdentifierRust_idempotentTrustLean/MicroC/Int64.lean:54TrustLean.wrapInt64_zeroTrustLean/MicroC/Int64.lean:55TrustLean.wrapInt64_oneTrustLean/MicroC/Int64.lean:56TrustLean.wrapInt64_neg_oneTrustLean/MicroC/Int64.lean:57TrustLean.wrapInt64_maxInt64TrustLean/MicroC/Int64.lean:58TrustLean.wrapInt64_minInt64TrustLean/MicroC/Int64.lean:60TrustLean.wrapInt64_overflowTrustLean/MicroC/Int64.lean:63TrustLean.wrapInt64_underflowTrustLean/MicroC/Roundtrip.lean:179TrustLean.char_ofNat_toNat_digitTrustLean/MicroC/Roundtrip.lean:187TrustLean.char_ofNat_isDigitTrustLean/MicroC/Roundtrip.lean:202TrustLean.natToChars_all_digitsTrustLean/MicroC/Roundtrip.lean:223TrustLean.natToChars_roundtripTrustLean/MicroC/Roundtrip.lean:265TrustLean.pNat_natToCharsTrustLean/MicroC/Roundtrip.lean:365TrustLean.binOp_roundtrip_allTrustLean/MicroC/Roundtrip.lean:371TrustLean.unaryOp_roundtrip_allTrustLean/MicroC/Roundtrip.lean:377TrustLean.litBool_roundtripTrustLean/MicroC/Roundtrip.lean:421TrustLean.stmt_skip_roundtripTrustLean/MicroC/Roundtrip.lean:424TrustLean.stmt_break_roundtripTrustLean/MicroC/Roundtrip.lean:427TrustLean.stmt_continue_roundtripTrustLean/MicroC/Roundtrip.lean:430TrustLean.stmt_return_none_roundtripTrustLean/MicroC/Simulation.lean:539TrustLean.sanitizeIdentifier_mem
Representative warning output:
warning: TrustLean/Backend/Common.lean:244:0: `TrustLean.countChar_joinCode` depends on non-standard axiom `Lean.ofReduceBool`
Allow it via `linter.axiomGuard.allowedAxioms`, or silence with `set_option linter.axiomGuard false`.
warning: TrustLean/Backend/Common.lean:244:0: `TrustLean.countChar_joinCode` depends on non-standard axiom `Lean.trustCompiler`
Allow it via `linter.axiomGuard.allowedAxioms`, or silence with `set_option linter.axiomGuard false`.
(There are also unrelated linter.unusedSimpArgs warnings in TrustLean/Backend/Common.lean that would independently block --wfail.)
Contributor guide
No contributing guide indexed for this repository
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Research direction
Start with the axiom-guard warnings at the listed declarations in TrustLean/Backend/Common.lean, TrustLean/MicroC/Int64.lean, TrustLean/MicroC/Roundtrip.lean, and TrustLean/MicroC/Simulation.lean, then inspect .github/workflows/ci.yml and the lakefile. Done means the reported warnings and unrelated unusedSimpArgs warnings are resolved or intentionally allowed, and CI uses build-args: "--wfail".
Written by the indexing model from the issue text.
Assessment
- Domain
- build-system, ci-cd
- Issue type
- Feature
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Activity status
- Quiet
- Clarity
- Mostly clear
- Newbie friendliness
- 45/100