Harden the CI check scripts - #32
Merged
Merged
Conversation
The lane modules were read via `mapfile` from a process substitution, whose failure escapes `set -e`: if check_native_optin.py died (or died after partial output), the loop ran over an empty or truncated lane and the check passed vacuously as "core-only (0 modules)". Use command substitution — an assignment's exit status is the command's, so any failure aborts the script — and reject empty output explicitly. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
Port the zcash/ironwood improvements to the shared csimp-census check: - an `attribute [csimp] a b …` command is censused per target, and an unparsable target fails rather than being silently skipped; - census entries count from any file, matched by final name component, with `#guard_msgs`-wrapped entries excluded (they assert that an entry *fails*, so they are the opposite of coverage); - the census lookup uses a herestring rather than piping into `grep -q`, which exits at the first match and would fail a *successful* lookup under `pipefail` via the writer's SIGPIPE; - `MetaCheck/` is excluded from the scan (it holds forged declarations exercising the census macros' rejection paths), and the top-level root modules are included. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
Adapted from zcash/ironwood's check_build_coverage.sh. `lake build` compiles exactly the modules reachable from the default targets, so a module outside that set is never elaborated: its sorries, axiom drift, or failure to compile stay invisible while CI is green. The script mirrors Lake's glob semantics over lakefile.toml and BFS-closes the in-package import graph, flagging any module file no counted target reaches. Differences from the ironwood original: CI here runs a plain `lake build`, so there is no CI-side target list to compare against defaultTargets; the opt-in `FastFieldNative` lane counts as a covered target (its own invariants are enforced by check_native_lane.sh and check_native_optin.py); and the module universe includes all top-level `*.lean` files, so a stray module beside the package roots is caught rather than being invisible to the scan. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
Port zcash/ironwood's guard: no tracked Lean file may contain a bare `import Mathlib` or `import Mathlib.Tactic`. Each umbrella loads a large slice of Mathlib into every elaborating process (measured in ironwood at ~6.5 GB RSS for the full umbrella, +1.3 GB RSS per process for `Mathlib.Tactic`), and nothing fails when one creeps in — builds just quietly get slow. The library is currently clean; this keeps it that way. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
daira
marked this pull request as ready for review
August 19, 2026 01:28
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.
Hardening of the CI check scripts, prompted by a vacuous pass observed while running them locally, plus a port of the script improvements zcash/ironwood has accumulated.
Fail loudly when the lane list cannot be obtained
check_native_lane.shread the lane modules withmapfilefrom a process substitution. A failure there escapesset -e: ifcheck_native_optin.pydied (or died after partial output), the loop ran over an empty or truncated lane and the check passed vacuously as "core-only (0 modules)" — observed locally when the interpreter lackedtomllib. Command substitution propagates the failure, and empty output is rejected explicitly.Ports from zcash/ironwood
attribute [csimp]commands, with an unparsable target failing rather than being skipped; census entries counted from any file (excluding#guard_msgs-wrapped rejection fixtures); a SIGPIPE-safe census lookup;MetaCheck/excluded from the scan and the root modules included.lakefile.tomland closing the in-package import graph. Adaptations: CI here runs a plainlake build, sodefaultTargetsis the single spelling of the surface; the opt-inFastFieldNativelane counts as covered (check_native_lane.shandcheck_native_optin.pypolice it); and, hardening the original, all top-level*.leanfiles are in the scanned universe, so a stray module beside the package roots is caught.import Mathliborimport Mathlib.Tactic; the library is currently clean. Without this check, nothing would fail if an umbrella crept in — builds would just quietly get slow.🤖 Claude Fable 5