Repository navigation
Conversation
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
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.
Saved analysis now uses the same strict semantic-span contract as live decoding, and session-fatal errors propagate through analysis. The writer exclusively owns stdin, cleanup reports each worker’s final state, and workspace helpers preserve open overlays with scoped document cleanup.
The Manual bridge delegates occurrence IDs and definition URLs to Verso, so repeated inclusions and cross-page links work. Logical request keys use collision-free pairs, requests compile through quotation, and the renderer converts overlay coordinates once. Bundle revision 2 removes duplicated authored diagnostic locations and adds caller-owned context provenance. Regenerate saved bundles; migration instructions describe the API changes and exact-request replay limits.
Validation: core tests on Lean 4.35.0 and 4.36.0-rc2; bridge tests and fresh Git-consumer isolation. VBP integration acceptance covers Rust/Rocq, offline HTML/TeX, repeated inclusions, multi-page navigation, nested-page hovers, and unchanged Blueprint queries. Five repeated analyses completed all fifteen session cleanups. The earlier intermittent cleanup failure’s exact cause was not reproduced; EOF ownership and stale completion sampling have explicit fixes, and cleanup failures remain strict.
Used by leanprover/verso-blueprint#502.