Repository navigation
Conversation
sam-xif
force-pushed
the
drop-committed-generated-lean
branch
from
October 15, 2026 12:44
48b8ba7 to
4a5f043
Compare
Every file in ruby-lean/RubyCore/Generated/ and the audited checker modules that books/scripts/generate_audited_checker.py writes into Checker/Audit/ are build outputs: each is derived from in-repo inputs (the prelude and the desugarer, the CRuby-name and Unicode oracles the repository pins a Ruby version for, the checker's Check/ modules). Commit them no longer. BootedHeap.lean was already a build artifact; this extends the same treatment to the rest. Checker/Audit/ also holds hand-written sources (Derive, Erase, Permissions), so it is not ignored as a whole. .gitignore lists the generated modules one by one, and the generator gains --list, which the Makefile uses for `make clean` and `make gen-check`. `make` regenerates each file before any target that compiles the model, the checker or the books reads it. `make gen-check` now fails if a file carrying a generated header is committed, or if .gitignore's list of generated audit modules differs from the generator's. A README in each directory, AGENTS.md and the contributing guide say which files are generated. A bare `lake build` in a fresh checkout, with no prior `make`, will not find these files; run `make gen` once first (needs Ruby and Python). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
sam-xif
force-pushed
the
drop-committed-generated-lean
branch
from
November 5, 2026 02:45
4a5f043 to
8b284a1
Compare
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
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.
Summary
Generated Lean sources are build outputs, not source. This stops committing them and has
makeregenerate each one before anything that reads it, extending what42801a8calready does forGenerated/BootedHeap.leanto the rest:ruby-lean/RubyCore/Generated/—PreludeJson,Prelude,CRubyNames,Unicode(andBootedHeap, already uncommitted);books/scripts/generate_audited_checker.pywrites intobooks/Books/TypeSoundness/Checker/Audit/.Checker/Audit/also holds hand-written sources —Derive.lean,Erase.lean,Permissions.lean— which stay committed. (The first version of this PR un-committed the whole directory, deleting those three; that is what CI failed on.)What changed
.gitignorecoversGenerated/*.leanand lists the 13 audit modules one by one (plus transient*.lean.tmp).generate_audited_checker.py --listprints the paths it writes; the Makefile reads it (AUDIT_OUT), so the generated set is defined once, in itsMODULES.CRubyNames.leanandUnicode.lean; an audit stamp;lean-exesdepends on the tables,BootedHeapand the audit stamp (the checker imports audit modules, sovalidate-oneneeds them);soundnesslikewise;books/metatheory/comparatorthroughlean-exes.BootedHeap's inputs include the regenerated tables, since generating it compiles the model.gen-check(still amake checktarget, soci-syncis unchanged) fails if a committed file underGenerated/orAudit/carries a generated header, or if.gitignore's audit list differs from--list. Exercised locally: passes as-is; fails, naming the file, with a generated module staged; fails, showing the diff, with one module missing from.gitignore.genalso writesBootedHeap.lean.cleanremovesGenerated/*.leanandAUDIT_OUTonly — not the hand-written audit sources.docs/contributing.mdanddocs/semantics/index.mdno longer say these files are committed.The CRuby-name and Unicode tables are oracle snapshots, so regenerating them assumes the Ruby the repository pins. #74 makes
CRubyNames.leanindependent of the oracle's startup load state, which this relies on: land this after #74. They touch different files.Consequence: a bare
lake buildin a fresh checkout with no priormakewill not find these files; runmake genonce (needs Ruby and Python). Everymaketarget that builds the model, checker or books does it already.Verification
make checkwas not run locally; CI runs it on the pinned Ruby. Locally:make gen-check(and its two failure modes, above);generate_audited_checker.py --check; andlake build validate-oneagainst the restored hand-written sources plus regenerated audit modules, the step CI failed on. ruff format and check pass on the generator.Authored by Claude (an agent). A human should review before merging.
🤖 Generated with Claude Code