fix: subverso breakage from lean4#14834

[Kha]

master went red on nightly-2026-09-03 when subverso was added to the monorepo
(run 33771303779):
subverso failed to build, and verso, verso-web-components, verso-slides and the
critical reference-manual were all skipped behind it.

subverso — fixed

InternalTests failed with Unknown constant Foo.bar / S.x / C.f. Since lean4#14834 a
structure/class field declaration carries term info for its projection, recorded while the
structure is still being elaborated. The highlighter falls back to the ambient environment for
constants that an occurrence's ContextInfo does not know yet, and in InternalTests that
fallback was this test module's own environment, which knows nothing the snippet declared — so
neither environment had the projection and looking up its signature threw. The three
highlighting harnesses now run in the environment that processing the snippet produced, the way
subverso-extract-mod highlights a module in the environment its elaboration ended in.

subverso pins v4.29.0-rc7 upstream, so this only surfaces here; upstream tracks the same
failure in leanprover/subverso#205.

Verified: lake build clean from an empty .lake (56 jobs). subverso defines no test or
lint driver, so that is its full phase set.

verso, verso-web-components, verso-slides, reference-manual — not fixed, blocked on the dependency fixup

None of them needs a source adaptation for this nightly, but they cannot build in the monorepo
as it currently stands, so this PR alone will not make the run green.

downstream: fixup repo verso (e4d5605) added subverso to the .lake/package-overrides.json
of verso's nested test projects test-projects/{anchor-examples,documented-package,website-examples,website-literate}.
Those four pin leanprover/lean4:v4.31.0 in their own lean-toolchain, so verso's build now
runs elan run --install leanprover/lean4:v4.31.0 lake build over the in-tree subverso and
rewrites subverso/.lake/build with v4.31.0 .oleans. Every verso module that imports subverso
then fails with

error: src/tests/Tests/Linters.lean:6:0: failed to read file
'.../subverso/.lake/build/lib/lean/SubVerso/Highlighting.olean', incompatible header

and where the nightly outputs are still read-only the nested build fails first with a bogus
permission denied (error code: 13) on one of them.

Reproduced in isolation: after a clean nightly build of subverso, running
elan run --install leanprover/lean4:v4.31.0 lake build :examples in
verso/test-projects/website-examples replaced 18 of subverso's 25 .oleans with v4.31.0 ones.

Updater.fixup_subrepo_toolchain already skips nested lean-toolchain files whose contents
differ from the subrepo's; fixup_subrepo_dependencies applies fixup_manifest_dependencies to
every **/lake-manifest.json with no such check, so it needs the same guard. That is a
.downstream/ change and is therefore left out of this PR.

With those four override entries emptied locally, everything behind subverso is clean on this
nightly:

repo	build	test
verso	✅ 1114 jobs	✅ all tests passed
verso-web-components	✅ 400 jobs	no driver
reference-manual	✅ 1180 jobs	no driver
verso-slides	✅	✅ (--no-playwright, as in CI)

so once the dependency fixup is corrected, the subverso commit here should be all that
master needs.

🤖 Generated with Claude Code

[downstream-lean4]

Build report for fix: subverso breakage from lean4#14834

Turned green:

Repo	Critical	Build	Test	Lint
subverso		✅ in 12s	⏭️	⏭️

Stayed red

Repo	Critical	Build	Test	Lint
reference-manual	✅	⏭️	⏭️	⏭️
verso		🟥 in 65s	⏭️	⏭️
verso-slides		⏭️	⏭️	⏭️
verso-web-components		⏭️	⏭️	⏭️

Stayed green

Repo	Critical	Build	Test	Lint
aesop	✅	✅ in 7s	✅ in 5s	⏭️
batteries	✅	✅ in 5s	✅ in 4s	✅ in 2s
import-graph	✅	✅ in 2s	✅ in 3s	⏭️
lean4-cli	✅	✅ in 1s	✅ in 0s	⏭️
mathlib4	✅	✅ in 216s	✅ in 47s	✅ in 91s
plausible	✅	✅ in 1s	✅ in 2s	⏭️
ProofWidgets4	✅	✅ in 3s	✅ in 1s	⏭️
quote4	✅	✅ in 2s	✅ in 1s	⏭️
BibtexQuery		✅ in 1s	⏭️	⏭️
comparator		✅ in 2s	⏭️	⏭️
cslib		✅ in 5s	✅ in 8s	✅ in 3s
doc-gen4		✅ in 12s	⏭️	⏭️
illuminate		✅ in 3s	✅ in 10s	⏭️
lean4-unicode-basic		✅ in 2s	⏭️	⏭️
lean4export		✅ in 0s	✅ in 7s	⏭️
LeanSearchClient		✅ in 1s	✅ in 0s	⏭️
leansqlite		✅ in 4s	✅ in 16s	⏭️
nerodia		✅ in 2s	✅ in 21s	⏭️
repl		✅ in 1s	✅ in 57s	⏭️

View run