chore: Fix warnings - #5
Open
samuelburnham wants to merge 4 commits into
Open
Conversation
Mechanical cleanup of the 785 linter warnings the build logged under the v4.33 toolchain, all behaviour-preserving; the full build and the sorry frontier audit are unchanged afterwards. - 574 unused simp arguments: dropped from their lists, which are rewrapped. Where every argument in a list was unused, `simp only [..]` becomes `simp only []` -- the structural/matcher reduction is still load-bearing, and deleting the tactic outright fails -- and plain `simp [..]` becomes `simp`. - 117 `def`s of a proposition, flagged by v4.33's `linter.defProp`, are now `theorem`s. - 56 unreferenced binders: pattern binders become `_`, declaration binders gain a `_` prefix. Five implicits (`result`, `argIdx`, `recursiveStarted`, `independent` and the `removed` it was the sole use of) were dead but passed by name, so the binders and those named arguments are gone. The unused `hU` on `Verify`'s `TrProj.instL` is dropped as well, matching the `Theory` lemma of the same name, which never took it. - 19 `simpa` calls whose goal simp already closed, along with the redundant `using` terms and one `have` left orphaned by them. - 12 unused section variables. `omit S in` is not available for the eleven in `InductiveLemmas`: the enclosing `include S` exists so the lemmas are reachable as `S.lemma`, and omitting it breaks four to six dot-notation call sites each, so the linter is scoped off beside each `include S`. - 4 `tac1 <;> tac2` that leave one goal, plus a `<;> omega` that could never run; 2 surplus `extract_lets` names, which named more lets than the tactic extracted; and an `open VEnv` that silently resolved to two namespaces other than the one it reads as, now spelled out.
The 16 allowlisted declarations that carry a `sorry` were the last thing keeping `lake build --wfail` from passing, which downstream consumers need. Each one now sets `warn.sorry false` at its definition. This costs no safety, because the warning was never the gate: `Lean4Lean.Audit.SorryFrontier` reads `sorryAx` out of the compiled environment, so a sorry that is new, moved, or renamed still fails the build. A sorry added without the annotation also still fails `--wfail`. Per declaration rather than per module or via `leanOptions`, so the suppression never covers more than the declaration it is attached to.
The default-target surface is warning-free now, so hold it there: a new warning anywhere in `Lean4Lean`, `Theory`, `Verify` or `Tests` fails the build instead of scrolling past. The frontier check gets `--wfail` too. `Lean4Lean.Experimental` stays without it. That library is parked proof work outside the audited surface, so its `sorry`s are deliberately unannotated and it also trips non-sorry warnings; it is not a default target, so a bare `lake build --wfail` never reaches it.
Bumps `lean4-nix` c41a770 -> 4026c65, which grew `cleanLakeSource`: the same idea as the hand-rolled fileset here, so drop ours for it. Its filter keeps `.lean`/`.toml`/FFI sources plus `lake-manifest.json` and `lean-toolchain`, and excludes any `.lake`, which covers what the union covered, `nix/fixtures` included. Only the `lean4-nix` node moves: `nixpkgs` and `flake-parts` follow it and are unchanged. The `nix flake check --no-build` caveat survives the switch -- a filtered source is still left unrealized, now as `…-lake-source` -- so the note stays. `mkLakeCheck` takes its targets as a list and builds them in one `lake build` rather than taking a shell snippet. `nix flake check` passes: proofs (frontier OK, 22 known sorries), tests, the downstream consumer, and the three CLI checks.
samuelburnham
enabled auto-merge (squash)
August 17, 2026 21:46
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.
No description provided.