From a67fbe79174d5704921a946b376353e33839dbf6 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 4 Sep 2026 08:12:44 +0000 Subject: [PATCH] fix: subverso lost definition sites in extracted modules MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- subverso/src/SubVerso/Highlighting/Code.lean | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/subverso/src/SubVerso/Highlighting/Code.lean b/subverso/src/SubVerso/Highlighting/Code.lean index 460fa58db..156cd2509 100644 --- a/subverso/src/SubVerso/Highlighting/Code.lean +++ b/subverso/src/SubVerso/Highlighting/Code.lean @@ -839,7 +839,12 @@ def termInfoKind let k ← exprKind ci termInfo.lctx termInfo.stx termInfo.expr (allowUnknownTyped := allowUnknownTyped) if (← read).definitionsPossible then if let some (.const name sig docs _isDef pp?, prettySig) := k then - let isDef ← withEnv (constEnv ci.env (← getEnv) name) <| isDefinition name termInfo.stx + -- Unlike `constEnv`, the command's environment is preferred here: declaration ranges are + -- registered as the command finishes, so they are missing from a node's environment even + -- when it already contains the constant, and `isDefinition` would then see no definition. + let cmdEnv ← getEnv + let env := if cmdEnv.contains name then cmdEnv else ci.env + let isDef ← withEnv env <| isDefinition name termInfo.stx return some (.const name sig docs isDef pp?, prettySig) return k