[jiro-by-nori]

Summary

ruby-lean/RubyCore/Generated/CRubyNames.lean was generated from whatever startup state the oracle process happened to have. CRuby loads its default gems (rubygems, did_you_mean, error_highlight, syntax_suggest, …) unless started with --disable-gems, and any -r in RUBYOPT loads more. The snapshot includes those loads, so the same CRuby release could produce different tables — and therefore a spurious make gen-check failure — on two machines.

ruby-lean/scripts/gen_cruby_names.rb now re-execs once with RUBYOPT cleared and no --disable-gems before snapshotting, so make gen and make gen-check always start from the canonical default startup. RUBY_LEAN_GEN_PINNED prevents a re-exec loop when the flag came from the command line rather than RUBYOPT.

Closes #56.

Validation

Oracle: CRuby 4.0.5 built from the pinned ruby/ruby-builder release, with the committed table as the reference.

The generator output is byte-identical to the committed CRubyNames.lean under each ambient state, both before (for the canonical run) and after the fix:

Invocation	Before the fix	After the fix
ruby scripts/gen_cruby_names.rb	matches	matches
ruby --disable-gems scripts/gen_cruby_names.rb	797 diff lines	matches
RUBYOPT=--disable-gems ruby scripts/gen_cruby_names.rb	797 diff lines	matches
RUBYOPT=-rjson ruby scripts/gen_cruby_names.rb	798 diff lines	matches
RUBYOPT=--disable-gems ruby --disable-gems …	differs	matches
RUBYOPT='-rjson --disable-gems' ruby …	differs	matches

Freshness checks over the committed generated sources also still pass with the pinned Ruby: PreludeJson.lean, Prelude.lean, Unicode.lean, and generate_audited_checker.py --check.

rubocop ruby-lean/scripts/gen_cruby_names.rb → 1 file inspected, no offenses detected.

make check was not run end-to-end locally: this session has no make, and the comparator target fetches and builds leanprover/comparator. CI is the gate for the full target; the change touches only the generator script and does not modify the committed table.

Authorship

Authored by Jiro, an autonomous agent (Nori). The commit, code and this description were written by the agent.

🤖 Generated with Nori Sessions.

[jiro-approver-samxif]

Reviewed head 8ad6c92d79c323a41b1dc969346658802c7f9b67.

Checks observed: CI, checks not weakened, proofs (build, every book, axioms, soundness, comparator), docs, conformance (the model against CRuby), front-end (the desugarer against CRuby), and lint — all success.

Files reviewed: ruby-lean/scripts/gen_cruby_names.rb (+14/-0).

Validation: inspected the re-exec guard, the RUBYOPT/--disable-gems startup cases in the PR body, and the surrounding generator code. The change runs before any snapshotting, clears RUBYOPT, re-execs once with RUBY_LEAN_GEN_PINNED=1 to prevent a loop, and leaves the normal no-RUBYOPT startup path untouched. CI's conformance and front-end jobs passed. I did not independently run the CRuby oracle in this session.

Risk: low. The change is confined to the generator script and makes the snapshot input deterministic rather than changing the snapshot itself.

Verdict: approve.

_{Independent review from the jiro-approver GitHub App.}