feat: report unavailable docstring metadata

[ejgallego]

When using Lean's module system, a plain import can leave docstrings unavailable in batch builds. Downstream consumers, such as Verso and SubVerso, thus cannot tell from a failed lookup whether a constant has no docstring or its documentation was not imported.

We add a staging API, SubVerso.findDocString, which returns .found, .absent, or .unavailable moduleName. Eventually this API should move upstream to Lean. This lets clients suggest import all M when documentation metadata is unavailable. It does not establish that the declaration actually has a docstring.

The implementation has three parts, which can be read in this order:

1. Look up documentation — DocString.lean. Successful lookups delegate to Lean, preserving its rendering, builtin documentation, tactic aliases, and inherited documentation. When lookup fails, we follow tactic aliases and loaded inherit_doc references and inspect the defining module's effective import mode. This includes transitive imports. A local declaration can therefore report an unavailable imported module if it inherits documentation from it. .absent means no documentation was found and no known unavailable metadata blocks the lookup.

2. Collect diagnostics for the chosen hover — Highlighting/Code.lean. The warning's contract is to report unavailable metadata when it may prevent documentation from appearing in an output hover. Lean's elaboration information can associate several expressions or declarations with the same source span. SubVerso classifies each matching entry into a possible token kind (a “candidate”), then uses its existing priorities to choose the identifier's hover.

   A concrete example is a documented DSL keyword, combineWarnings, whose elaborator returns the imported function SubVerso.Highlighting.Diagnostics.append. Classification finds that function, but the output uses a keyword token with the syntax's own documentation, “Combine warning summaries.” A plain import leaves the function's docstring unavailable; adding import all SubVerso.Highlighting.Diagnostics restores it without changing the keyword's hover. Warning about that module here would therefore give the user an import suggestion that does not improve the displayed documentation. An explicit reference to Diagnostics.append does warn under a plain import, and gains its documentation with import all.

   To implement this distinction, tokenWithDocString returns the lookup information with the candidate instead of immediately adding a warning to the summary. The existing KindWithPPSig tuple gains a third field: some M if metadata was unavailable, or none otherwise. identCandidate selects a candidate without changing the summary; retainKind adds its optional module to HighlightState.missingDocStringModules when that candidate supplies an output token's hover. Lookup still happens during classification, in the environment appropriate to each candidate; only recording the module waits for that choice. The extra tuple field is temporary and is not serialized to clients.

   “Discarded” refers to unused candidate information for a token. Both source branches of an if are highlighted and can contribute diagnostics. “Format-only annotations” are the colour and binding information attached to names in pretty-printed signatures and types; they do not include documentation hovers for those names. cleanFormatTags reuses classification to build these annotations without calling retainKind. Pretty-printer output rendered as tokens with documentation hovers still contributes diagnostics. Regression tests check that discarded candidates and these annotations add no warnings, while output hovers with unavailable metadata do identify their modules.

3. Return a summary to clients — Highlighting/Diagnostics.lean. Each highlighting entrypoint now returns (highlighted, diagnostics). Diagnostics.missingDocStringModules is a NameSet, and callers merge summaries with ++ when combining results. The changes in helpers, module extraction, signatures, and saved examples carry this summary through to their consumers, separately from Lean messages. JSON encodes the set as a sorted array; decoding restores uniqueness and accepts older payloads that omit the diagnostics field.

This is an intentional result-level design: clients can render one import all warning per module; individual token lookup statuses and source locations are not retained. A summary covers the whole returned result. Slicing highlighted output does not narrow it, so an excerpt-specific warning needs diagnostics collected at that excerpt's boundary.

We also need an upstream API to query whether a module's server metadata is available in an environment. Until then, we use declaration ranges from the whole module as evidence that server metadata was loaded. Checking the whole module also covers generated declarations with no range of their own. A module with no recorded ranges may still be reported as unavailable even when its metadata is loaded. Older Lean versions without the module system return only .found or .absent.

InternalTests.lean covers plain imports, import all, server-loaded metadata, local and inherited documentation, discarded candidates, retained hovers, and diagnostic serialization. Existing internal tests already execute during lake build through #eval and assertion commands. The new import-mode tests run from the executable's main, so CI also invokes lake exe subverso-internal-tests. The pinned toolchain is updated to Lean 4.34.0-rc2.

Validation: the clean local build and runtime regressions passed, and the full CI run for this revision passed.

[ejgallego]

We could introduce a record for the result type, but IMHO that's premature.

[david-christiansen]

I think this may not be as useful as we'd want it to be.

The use case we talked about was putting a yellow squiggly on a name that could benefit from import all, and I don't think this really gives us a non-roundabout way to do it. I'd expect to at least have this be a NameMap Name, with keys being the names whose lookup failed and the values being the module that needs to be import all'd. Then, a quick traverse of the infotree is enough to emit the warnings in Verso.

[ejgallego]

Just saw this comment: I was blocked on making this better due to not finding the right Lean upstream API to get the info we need.