[jiro-by-nori]

What this fixes

Issue #41: "where is Sorbet" was written down twice, and the two copies
disagreed. books/scripts/srb_sigs.py's find_sorbet() returned $SORBET
unconditionally, so a stale or misspelled value reached subprocess and failed
later in the corpus stage; scripts/check-prereqs.sh only accepted $SORBET if
it existed and otherwise repeated the RubyGems lookup. Since the binary decides
which programs reach the validator, the wrong one moves every verdict without an
error naming the cause.

The issue also names three find ... sorbet-static copies in
.github/workflows/ci.yml; those were removed by an earlier refactor, so the
duplication left was the two sites above. (srb_sigs.py has also moved from
ruby-lean/scripts/ to books/scripts/ since the issue was filed.)

The change

• find_sorbet() is now the single definition, and it validates what it
  returns:
  • $SORBET, when set, must resolve to an executable file (a bare name is
    looked up on PATH, which is what it meant before). A path that does not
    exist, or a file without the execute bit, is an error naming the value
    instead of a silent fallback to a different Sorbet.
  • the sorbet-static gem binary is used only when executable, then srb on
    PATH; when none is found the message names the cause and make deps
    instead of returning a bare srb that cannot run.
• scripts/check-prereqs.sh calls the new srb_sigs.py --which-sorbet and
  reports that path, so make prereqs and the gate cannot name different
  binaries. The Python check moves above it because the lookup runs through it.
• srb_sigs.py already records the chosen binary in each manifest's "sorbet"
  field, so a run still records which Sorbet produced its signatures.

Tests

New books/scripts/test/test_srb_sigs.rb (6 tests, runs under
make emitter-unit) pins the contract:

• the gem binary is named when $SORBET is unset, and it is executable;
• an executable $SORBET is honoured, and a bare name resolves through PATH;
• a $SORBET that does not exist, and one without the execute bit, are errors
  that name the value and print nothing on stdout;
• scripts/check-prereqs.sh reports exactly the path --which-sorbet prints,
  which is the drift Sorbet-location logic is duplicated in four places and can drift (follow-up to #32) #41 describes.

Validation

Run locally on the branch from a cold toolchain (Lean v4.32.2, CRuby 4.0.5):

make check              -> make check: ALL CHECKS PASSED
make check-not-weakened -> CHECKS NOT WEAKENED

• make prereqs — prints the gem's Sorbet; SORBET=/nope/sorbet scripts/check-prereqs.sh reports sorbet MISSING — $SORBET is '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/nope/sorbet', which is not an executable file and exits 1;
  srb_sigs.py --which-sorbet agrees with the script's line.
• make conformance — ran 1287, agree 1087, sut_unsupported 194, disagree 0,
  exactly the recorded baseline.
• make emitter-unit — 373 runs, 444 assertions, 0 failures; coverage holds
  (line 98.17%, branch 82.33%).
• make lint — ruff (format + check), RuboCop, shellcheck and actionlint all
  clean; make gen-check, make docs, make books, make soundness,
  make comparator all pass as part of make check.
• No recorded result moved, and no check, theorem, test or lint suppression was
  added.

---

Authored by Jiro, an autonomous coding agent: both the code and this
description.