fix: restore subverso definition sites, unbreaking verso-slides - #41
Open
Kha wants to merge 1 commit into
Open
Conversation
subverso#237 made the definition-site check in `termInfoKind` run in the environment `constEnv` picks, which is the info node's own environment whenever that environment already contains the constant. Declaration ranges are only registered as the command finishes, so a node's environment holds the constant but not its ranges, and `isDefinition` consequently reported every top-level declaration as a plain occurrence. `ModuleItem.defines` collapsed to the names whose info nodes predate their addition to the environment — `where` helpers and constructors — which broke `verso-slides`' `leanLibCode … (decl := …)` blocks with "No declaration named `Verso.Code.External.withNl` in module." Prefer the command's environment for that check, falling back to the node's for constants the former does not contain. Verified: `Verso.Code.External` goes from 9 back to 56 `defines`; subverso builds and `subverso-internal-tests` passes; verso-slides builds and tests.
Contributor
Build report for fix: subverso lost definition sites in extracted modulesStayed red
Stayed green
|
This was referenced Sep 5, 2026
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.
masteris red onnightly-2026-09-03(run33849693560):
versofails to build andverso-web-components,verso-slidesand the criticalreference-manualare skipped behind it. There are two independent causes; this PR fixesone of them, so it will not by itself make the run green.
subverso— fixedNot visible in the run, because
verso-slidesnever got to build. With the dependency fixupbelow undone locally,
verso-slidesfails withleanLibCode … (decl := …)looks the declaration up inModuleItem.defines, whichsubverso-extract-modfills from the tokens the highlighter marked as definition sites. ForVerso.Code.Externalthat set had collapsed from 56 names to 9 — onlywherehelpers andconstructors survived, no top-level declaration did.
The monorepo's
subversois exactly one commit ahead of thefda188f7thatversoandverso-slidespin, so this arrived whensubversowas added as a subrepo: leanprover/subverso#237(the fix for the
InternalTestsbreakage from lean4#14834) made the definition-site check intermInfoKindrun in the environmentconstEnvselects, which is the info node's ownenvironment whenever that already contains the constant. Declaration ranges are registered as
the command finishes, so a node's environment holds the constant but not its ranges, and
isDefinitionthen reports the declaration as a plain occurrence. The names that still workedare exactly those whose info nodes predate their addition to the environment, where
constEnvfalls back to the command environment anyway.
The check now prefers the command's environment and falls back to the node's for constants that
environment does not contain. Worth reporting upstream:
subverso's own CI pinsv4.29.0-rc7and does not exercise
defines, so it will not catch this.Verified:
Verso.Code.Externalback to 56defines;lake buildclean (56 jobs) andsubverso-internal-testspasses.subversodefines no test or lint driver, solake buildisits full phase set in CI.
The dependency fixup — still broken, needs a
.downstream/changedownstream: fixup repo versowritessubversointo the.lake/package-overrides.jsonofverso's nested test projects
test-projects/{anchor-examples,documented-package,website-examples,website-literate}.Those four pin
leanprover/lean4:v4.31.0in their ownlean-toolchain, so verso's build runselan run --install leanprover/lean4:v4.31.0 lake buildover the in-treesubversoandrewrites
subverso/.lake/buildwith v4.31.0.oleans. Every verso module importing subversothen fails with
and where the nightly outputs are still read-only the nested build fails first with a bogus
permission denied (error code: 13).Updater.fixup_subrepo_toolchainalready skips nestedlean-toolchainfiles whose contentsdiffer from the subrepo's;
fixup_subrepo_dependenciesappliesfixup_manifest_dependenciestoevery
**/lake-manifest.jsonwith no such check and needs the same guard. That is a.downstream/change, which this run may not make, so it is not in this PR. Hand-editing thefour override files is not a fix either:
fixup_subrepo_and_commitregenerates them on everydownstream: update repo verso, which lands daily.Verified with the four override entries emptied locally
Everything behind the fixup is clean on this nightly once
subversois fixed, so the guard plusthe commit here should be all
masterneeds:versoverso-slides--no-playwright, as in CI)verso-web-componentsreference-manualAlso: #39 can be closed. Its
subverso/InternalTests.leancommit is superseded byleanprover/subverso#237, which reached the monorepo in
downstream: update repo subverso(3558e9b) and made
subversogreen in this run.🤖 Generated with Claude Code