chore: merge main into nightly-testing and bump to 2026-06-22 - #886
Merged
Conversation
This PR adds a simple literate programming system. To use it, just add a Verso dependency and run `lake build :literateHtml`. The file `literate.toml` can be used to configure some aspects of the presentation, including the order of modules in the navigation tree, the default landing page, custom titles or URLS for modules, and which commands have their output included in the page. Details are available in the Verso user's guide.
Bumps requests from 2.32.5 to 2.33.0. https://github.com/psf/requests/releases Signed-off-by: dependabot[bot] <support@github.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
Bumps marocchino/sticky-pull-request-comment from 2 to 3. https://github.com/marocchino/sticky-pull-request-comment/releases Signed-off-by: dependabot[bot] <support@github.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
Bumps dawidd6/action-download-artifact from 17 to 19. https://github.com/dawidd6/action-download-artifact/releases Signed-off-by: dependabot[bot] <support@github.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
Bumps pygments from 2.19.2 to 2.20.0. https://github.com/pygments/pygments/releases Signed-off-by: dependabot[bot] <support@github.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
This stops upgrades from breaking our CI unexpectedly.
`finishDoc` was installing constants relative to the ambient namespace, but when we have a module `Foo.Bar.Baz`, the name of the doc should be `Foo.Bar.Baz.«the canonical document object name»` irrespective of the ambient modules. If we were using a more low level `addAndCompileDecl` approach, this wouldn't be an issue, but while we're still heavily in the "generate Lean `Syntax` and elaborate it" regime, the easy solution is just to prepend `_root_` to the identifier.
No-number sections have a `null` as the `sectionNum`, but we don't want those to show up as `null` in search results. Old (current deployed) <img width="923" height="291" alt="image" src="https://github.com/user-attachments/assets/d241ed2d-0fd2-4ea5-bda6-89394714663e" /> With this fix <img width="923" height="291" alt="image" src="https://github.com/user-attachments/assets/13d2030d-284e-4eb6-90ab-b74a1b045065" />
Actionlint now runs only in CI, and not as part of lake test.
Co-authored-by: github-actions[bot] <github-actions[bot]@users.noreply.github.com> Co-authored-by: jcreedcmu <jcreed@gmail.com> Co-authored-by: Robert J. Simmons <442315+robsimmons@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: Jonathan Merritt <jmerritt@canva.com>
Bumps actions/setup-node from 4 to 6. https://github.com/actions/setup-node/releases Signed-off-by: dependabot[bot] <support@github.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
Bumps dawidd6/action-download-artifact from 19 to 20. https://github.com/dawidd6/action-download-artifact/releases Signed-off-by: dependabot[bot] <support@github.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
In some very long documents with lots of subsections, this prevents an elaboration error on the metadata blocks.
This gets a fix to a cache issue where mvars in proofs would sometimes not be instantiated. Also adds Lake manifests to the prettier exclude list.
This gets a fix for extremely slow elaboration due to mistaking pretty printer synthetic positions for byte indices.
Bumps pytest from 8.4.2 to 9.0.3. https://github.com/pytest-dev/pytest/releases Signed-off-by: dependabot[bot] <support@github.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
Bumps actions/github-script from 8 to 9. https://github.com/actions/github-script/releases Signed-off-by: dependabot[bot] <support@github.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
The typography linters were accidentally enabled if _either_ option was enabled. This PR fixes that. Additionally, internal changes had rendered the Manual linter that warns about missing tags inoperative. It's reactivated and tested.
Allows the search box to get custom priorities. Priorities may be assigned as follows: * Semantic vs full-text results * Semantic domains may be weighted, e.g. to boost all technical terms * Within a domain, items may be prioritized, e.g. to lower release notes relative to other text. This is done in JS in the domain mapper. * A genre may weight full-text results for parts based on part metadata. In the Manual genre, sections can be assigned search priority values, which affects their full-text and semantic results.
…825) When the test-project `lean-toolchain` files drift from the root `lean-toolchain`, the consistency check now points the reader at a new comment-triggered workflow: commenting `!consistent` on the PR runs `cp lean-toolchain test-projects/*/lean-toolchain` and pushes the fix back to the PR branch, matching the existing `!prettier` pattern. --------- Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Bumps actions/github-script from 8 to 9. https://github.com/actions/github-script/releases Signed-off-by: dependabot[bot] <support@github.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
The Python code in the test and deployment systems is now formatted via `ruff`, a lightweight Python formatter, as we use Prettier for other dependencies.
The action can't work due to branch protection anyway.
Bumps dawidd6/action-download-artifact from 20 to 21. https://github.com/dawidd6/action-download-artifact/releases Signed-off-by: dependabot[bot] <support@github.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
Adds a drag handle on the right edge of the ToC in HTML manual output so readers can set its width, with the choice persisted in localStorage. Pointer and keyboard resizing are both supported, and the handle is exposed as an ARIA separator. The layout is entirely CSS-driven. The JavaScript (static-web/toc-resize.js) only records the user's preferred width in the --verso-toc-user-width custom property and in localStorage. There are two scripts on purpose: - toc-resize-preload.js runs inline in the <head> and applies the saved width before first paint, so returning readers don't see the default width flash to their saved width. - toc-resize.js is deferred, re-applies the width defensively, and wires up the interactive resizing. Both must agree on the localStorage key, since the preload primes the value the main script reads. A CI step enforces that the keys match. The content area's width depends on the ToC width, not just the viewport. This means that some media queries became container queries, and some thresholds were adjusted (for an equivalent result of the old thresholds). Closes #845 --------- Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk> Co-authored-by: David Thrane Christiansen <david@lean-fro.org>
This PR improves diagnostics for Verso document extension resolution, starting from inline role resolution and now sharing the same diagnostic machinery with code blocks, directives, and block commands where appropriate. It reports explicit extension-resolution failures for: - a declaration that can be used as an expander but is not registered for the requested extension syntax - a declaration that exists but is not registered for the requested extension syntax - an unknown extension name, with edit-distance-ranked clickable hints when there are close matches and no broad fallback list when the name is not close enough The PR also: - preserves existing block-command fallback to ordinary declarations when the name resolves but is not registered as a block command - exposes registered extension names for diagnostics across roles, code blocks, directives, and block commands - uses shadowing-aware display names for suggestions - factors shared extension expander execution in `Verso.Doc.Elab` - keeps the new `VersoManual.Index` role imports scoped to the public meta inline elaboration dependency - registers legacy inline APIs as explicit roles for compatibility (`today`, `date`, `sectionRef`, `index`, `see`, `seeAlso`) - adds `Tests.ExtensionResolution`, including explicit distance-matching and no-match cutoff coverage - updates the current release notes Follow-up work remains appropriate for role/directive/command completion. This PR was prepared with help from Codex (model: GPT 5.5) --------- Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
Verso Blueprint exposed very large `.olean` files. For example, a file that imports all test blueprints produced an `.olean` above 10 GiB. The cause was that doc expander and signature environment extension state were re-exported. Importer modules therefore serialized transitive expander entries again, which can compound across import chains. This patch introduces `LocalPersistentEnvExtension`, a small Verso-side helper for persistent extensions that keep complete imported lookup state alongside a separate local export delta. It then uses the helper to store doc expander and signature extension state as separate local and complete maps. Only local entries are exported, while lookup still uses the complete imported state. This prevents importer modules from reserializing every transitive expander entry. The patch adds transitive-import regressions covering role, code block, directive, and block-command expanders, plus a direct regression for the local-persistent-extension failure mode. ## Measurements For blueprints, the size reduction is substantial, on the order of 100x or more. Additional benchmarks: Reference manual at `8ae381a3`, Lean `v4.30.0-rc2`, command `lake --no-cache build Manual`, baseline Verso `ba73c230`: | Build | Elapsed | Max RSS | | --- | ---: | ---: | | baseline run 1 | 157.13s | 2,518,464 KB | | baseline run 2 | 155.61s | 2,525,236 KB | | patched | 144.25s | 2,537,208 KB | Compared reference-manual artifacts: - total artifacts: `637,348,589 B -> 599,759,959 B`, `-37,588,630 B` / about `-35.8 MiB` - `.olean` total: `546,283,272 B -> 508,649,832 B`, `-37,633,440 B` Synthetic importer test, `Manual.PerfImportPair` importing `Manual.Terms` and `Manual.Tactics.Reference`: - Lake-built `.olean`: `375,456 B -> 17,072 B`, `-95.5%` - direct Lean `.olean`: `375,392 B -> 17,008 B` - direct compile time stayed flat: `1.66s -> 1.65s` UsersGuide comparison: - elapsed time effectively flat: `56.59s -> 56.84s` - compared `.olean` artifacts dropped by about `432 KiB`
This fixes a bug where tutorial header IDs had each component doubled, because inPart was called both by the framework and internally.
Bumps nwtgck/actions-netlify from 3.0 to 4.0. https://github.com/nwtgck/actions-netlify/releases Signed-off-by: dependabot[bot] <support@github.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
This PR adds GitHub Deployment reporting to the pull-request manual preview workflow. After PR CI builds and uploads the manual artifact, the follow-up deploy workflow publishes that artifact to Netlify and records the resulting preview URL as a transient GitHub Deployment for the PR preview environment. The deployment is attached to the PR workflow target SHA, with the PR head SHA as a fallback. During rollout, the workflow also posts the familiar PR preview link as a new PR conversation comment. This keeps the existing reviewer experience in place while we verify that GitHub surfaces the deployment link reliably on PRs. Once that is confirmed, the comment step and its `issues: write` permission can be removed. The workflow records the deployment explicitly because it runs under `workflow_run`. In that context, `nwtgck/actions-netlify` sees the default-branch workflow SHA as `context.sha` and does not expose a deployment ref/SHA override. The Netlify action is still used for the Netlify upload itself, but GitHub deployment metadata is recorded by a separate first-party `actions/github-script` step. Supply-chain changes in the secret-bearing deploy workflow: - PR metadata lookup no longer uses `potiuk/get-workflow-origin`; it now uses `actions/github-script@v9`. - Artifact download no longer uses `dawidd6/action-download-artifact`; it now uses `actions/download-artifact@v7`. - PR commenting no longer uses `marocchino/sticky-pull-request-comment`; it now uses `actions/github-script@v9`. - The Netlify upload still uses `nwtgck/actions-netlify`, pinned to a full commit SHA, because that action receives `NETLIFY_AUTH_TOKEN`. - The workflow no longer passes `GITHUB_TOKEN` to the Netlify action. The deploy job runs after PR CI succeeds and deploys the uploaded artifact without checking out or executing PR code. A malicious PR can control the preview HTML content, as expected for a preview, but this workflow does not expose deploy secrets to the PR CI job. Prepared with Codex (GPT-5.5)
This PR fixes Verso's LSP document-symbol and folding ranges for document command syntax and term-position Verso documents. Previously, root document parts did not preserve distinct syntax anchors for the full document range and the visible title selection. This could make a top-level document symbol start at the wrong position, merge unrelated Lean declarations under the document symbol, or produce a `selectionRange` outside its enclosing `range`. LSP clients such as VS Code reject the whole document-symbol response when that containment invariant is violated, which makes VSCode not to display the outline. The fix stores separate syntax anchors for each part: `rangeSyntax` for the full document-symbol and folding range, and `selectionSyntax` for the symbol selection range. Root document elaboration captures the current elaborator reference before title elaboration as the range anchor while keeping the title literal as the selection anchor. TOC construction now validates the syntax anchors before they reach the LSP handlers. This validation only checks the metadata that Verso is about to store: both anchors must have ranges recoverable by Lean's syntax APIs, and the selection anchor must be contained in the full part span from the range anchor start to the part end. The LSP layer then calls Lean's standard `FileMap.lspRangeOfStx?` helper directly, rather than carrying a Verso-specific range fallback or normalization path; TOC LSP conversion now panics if that previously-checked invariant is violated. Explicit `PointOfInterest` selection syntax is also validated when the metadata is saved, so document-symbol construction consumes already-checked selection ranges instead of re-checking containment in the LSP handler. For direct syntax, the important case is header synthetic nodes. Header wrapper syntax can have synthetic or missing source information even when its children retain recoverable positions; if Verso stores such a wrapper as the TOC range anchor without preserving a recoverable full span, document-symbol and folding extraction can later produce invalid or missing ranges. This PR keeps that provenance check at TOC creation, and `#docs` also uses the final token's tail position for document ends. Finally, the term-position `#doc` elaborator now matches `elabDoc`'s `VersoDoc` result instead of expecting `Part`, and a small `Tests.DocTerm` smoke test covers direct term-`#doc` elaboration outside the LSP harness. Prepared with Codex (GPT-5.5)
) Now, we warn instead of error on missing handlers. This PR also adds missing builtin handlers for code blocks and fixes a bug where the lookup for user handlers occurred in the wrong table. In particular, `getBlockToLiterateUnsafe` was looking in the inline handler table instead of the block handler table. --------- Co-authored-by: Robert J. Simmons <442315+robsimmons@users.noreply.github.com>
) This fixes an issue where syntax resulting from parsed string literals would have bogus position information, which got in the way of some LSP features. Even worse, if this syntax was used in a point of interest, it panicked (after the merge of #771).
This fixes a panic in some clients of the Markdown support that used it to add blocks to a document after #771.
This PR allows doc highlighting information to be be provided from a different source, instead of just a hardcoded `-verso-docs.json` resource file. It also incidentally turns the get-highlighting-json operation from a chained promise to an await-ed one. The reason for this change is to eventually allow the lean4web app to generate a single-file page that only refers to external static assets — the main per-document assets for a single-page HTML development are index.html, the highlighting information file, and search data (which can be omitted from a single-page HTML development). (Hint: the diff is quite small if you preview with whitespace changes off.)
Bumps actions/checkout from 6 to 7. https://github.com/actions/checkout/releases Signed-off-by: dependabot[bot] <support@github.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
Bumps actions/download-artifact from 7 to 8. https://github.com/actions/download-artifact/releases Signed-off-by: dependabot[bot] <support@github.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
david-christiansen
force-pushed
the
modules-again
branch
from
June 22, 2026 15:39
ff9bb84 to
d674e93
Compare
ahmedtadde
pushed a commit
to metroncorp/lean4-verso
that referenced
this pull request
Jul 16, 2026
this got added in leanprover#886 just to nightly-testing, adding it to main
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
7 participants
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.
No description provided.