fix: parser errors getting silently lost - #476
Merged
Merged
Conversation
Collaborator
Author
|
This still needs testing on the big corpus of Verso documents out there before a merge |
david-christiansen
added a commit
that referenced
this pull request
Jul 28, 2025
* feat: structured messages (#479) Lean's messages are now showed as structured information, rather than strings, which enables hovers and interactive traces. * fix: mobile Safari rendering issue (#478) * fix: parser errors getting silently lost (#476) * feat: allow customising blog header (#472) Currently, any page generated by the blog genre starts with the magic string `<!DOCTYPE html>`. This PR modifies that to, by default, use `Html.doctype` (as used by the manual genre). It also allows customising that string to something else, which is useful to replace it with a Jekyll-friendly front-matter. The default behaviour is left unchanged. * chore: bump to latest nightly --------- Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
kim-em
added a commit
that referenced
this pull request
Aug 14, 2025
* feat: components in blog genre (#385) Components bundle together HTML, JS, and CSS. * chore: bump dependencies for nightly-2025-05-08 (#386) * feat: upstream table from reference manual (#387) * feat: generate directives for block components (#388) * chore: document and partially enforce new procedures (#381) * chore: bump to latest SubVerso and Lean nightly (#390) * fix: use correct internal name for table block (#391) * fix: allow list item contents to be on new line (#392) * fix: behavior of SVG tags inside the HTML (#393) * feat: manual genre can display Lean code from external projects (#394) * feat: allow namespace suppression when extracting external code (#395) * chore: remove redundant error mods (#397) SubVerso now retains the fact that they were errors. * feat: use upstream hints infrastructure in errors (#398) * chore: bump to nightly-2025-05-19 (#399) * feat: alternative approach to incrementality (#400) Replaces the Lean command parser with a new one that takes a block at a time, rather than parsing Verso as one giant command and implementing incrementality "by hand". Each Verso block is elaborated to a top-level definition, which makes the checking for `sorry` and errors work the way it should. Without this, the `sorry` warning was emitted in the presence of errors, which was inconsistent with the rest of Lean. This is also a step towards elaborating Verso directly, which will probably improve performance in the future. A diff threshold was added to `leanOutput` in the manual genre to account for differences in IR shown in examples in the reference manual as a result of compiling blocks to separate defs. * feat: generalize external Lean code display (#401) It can now work in many genres, with only an instance declaration needed. In particular, it works in blogs. * fix: also generate document when text is empty (#402) * feat: bundle KaTeX and include by default in manual genre (#403) * fix: external code rebuilds and hints (#404) Prevents spurious rebuilds from subprocesses and repairs broken hint formatting. * feat: suggest code samples based on string contents (#405) * feat: document elaboration hooks (#406) This allows Verso extensions to register things like cleanup functions for internal state that they can't otherwise control (e.g. temporary directories). * chore: bump toolchain to nightly-2025-05-27 * fix: default anchor suggestions to false (#407) * fix: more reliable external module extraction (#408) * fix: incorporate SubVerso improvements to error/tactic spans (#409) * chore: bump to 2025-06-01 (#413) * chore: bump to 2025-06-05 (#423) * feat: show hovers on closing delimiters (#428) Closes #427 * chore: bump to 2025-06-09 * chore: bump nightly-testing to 2025 06 20 and merge main (#447) * feat: show hovers on closing delimiters (#428) Closes #427 * feat: linter for Unicode typography (#430) * chore: adapt to upstream SubVerso improvements (#432) In particular, this fixes highlighting for sorts and improves the display of tactic states. * feat: LinkTargets for Blog Genre and definitions (#431) * fix: parse ` ` correctly (#433) * doc: update README for nightly procedures (#424) * fix: hover for imax had flipped args (#434) * fix: remove obsolete z-index customization for tactic states (#435) * chore: bump SubVerso version (#438) * fix: demo textbook would delete files (#439) It seems that a relative path became absolute. Now it's relative again. * chore: bump SubVerso for bug fixes (#440) * Fix port number for accessing demosite in README.md (#442) * feat: allow parts to disable showing inline HTML ToC (#444) * feat: cross-references between documents (#441) This is a feature inspired by InterSphinx, to allow documents to reference one another. The idea is that the internal cross-references database is placed at a well-known URL, and documents can download and cache it, using it to resolve links. * chore: bump to nightly-2025-06-19 --------- Co-authored-by: Pim Otte <otte.pim@gmail.com> Co-authored-by: Hanson Char <hanson.char@gmail.com> Co-authored-by: jrr6 <7482866+jrr6@users.noreply.github.com> * chore: bump to nightly-2025-06-23 and merge `main` (#452) Contained: * feat: show hovers on closing delimiters (#428) Closes #427 * feat: linter for Unicode typography (#430) * chore: adapt to upstream SubVerso improvements (#432) In particular, this fixes highlighting for sorts and improves the display of tactic states. * feat: LinkTargets for Blog Genre and definitions (#431) * fix: parse ` ` correctly (#433) * doc: update README for nightly procedures (#424) * fix: hover for imax had flipped args (#434) * fix: remove obsolete z-index customization for tactic states (#435) * chore: bump SubVerso version (#438) * fix: demo textbook would delete files (#439) It seems that a relative path became absolute. Now it's relative again. * chore: bump SubVerso for bug fixes (#440) * Fix port number for accessing demosite in README.md (#442) * feat: allow parts to disable showing inline HTML ToC (#444) * feat: cross-references between documents (#441) This is a feature inspired by InterSphinx, to allow documents to reference one another. The idea is that the internal cross-references database is placed at a well-known URL, and documents can download and cache it, using it to resolve links. * feat: add linters for extra markup (#448) In particular, this will help users not get caught on the fact that `*` is different from Markdown. * fix: display multiple authors correctly (#449) * feat: add part generation and info-string checking in Markdown elab (#445) This PR adds the Markdown elaboration features required for error explanations, namely the ability to create `Part`s from Markdown headers, the ability to access infostrings in code-block elaborators, and a "strict" inline code elaboration mode. * feat: linter for missing section tags in manual genre (#450) * fix: respect `none` for section tags in manual genre (#451) * chore: bump to nightly-2025-06-23 --------- Co-authored-by: Pim Otte <otte.pim@gmail.com> Co-authored-by: Hanson Char <hanson.char@gmail.com> Co-authored-by: jrr6 <7482866+jrr6@users.noreply.github.com> * chore: bump nightly testing to 2025-06-24 and merge main (#455) * chore: bump to nightly nightly-2025-06-26 * chore: bump to nightly nightly-2025-06-27 * chore: bump to nightly nightly-2025-06-28 * chore: bump to nightly nightly-2025-06-29 * chore: delete file that shouldn't have been committed * chore: bump to nightly nightly-2025-06-30 * chore: bump to nightly-2025-07-04 (#468) * chore: bump to nightly nightly-2025-07-05 * chore: bump to nightly nightly-2025-07-06 * chore: bump to nightly nightly-2025-07-07 * chore: bump to nightly nightly-2025-07-08 * chore: bump to nightly nightly-2025-07-09 * chore: bump to nightly nightly-2025-07-10 * chore: bump to nightly nightly-2025-07-11 * chore: bump to nightly nightly-2025-07-12 * chore: bump to nightly nightly-2025-07-13 * chore: bump to nightly-2025-07-19 (#470) * chore: bump to nightly nightly-2025-07-21 * chore: bump to nightly-2025-07-22 (#473) * chore: bump to nightly nightly-2025-07-24 * chore: bump to nightly nightly-2025-07-25 * chore: bump to nightly-2025-07-27 (#481) * feat: structured messages (#479) Lean's messages are now showed as structured information, rather than strings, which enables hovers and interactive traces. * fix: mobile Safari rendering issue (#478) * fix: parser errors getting silently lost (#476) * feat: allow customising blog header (#472) Currently, any page generated by the blog genre starts with the magic string `<!DOCTYPE html>`. This PR modifies that to, by default, use `Html.doctype` (as used by the manual genre). It also allows customising that string to something else, which is useful to replace it with a Jekyll-friendly front-matter. The default behaviour is left unchanged. * chore: bump to latest nightly --------- Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com> * chore: bump to nightly nightly-2025-07-28 * chore: merge main into nightly-testing * chore: bump to nightly nightly-2025-07-29 * fix: make go-to-def work with latest nightly (#483) * chore: bump to nightly nightly-2025-07-30 * chore: bump to nightly nightly-2025-07-31 * chore: merge main into nightly-testing * chore: bump to nightly-2025-08-04 (#491) * chore: bump to nightly nightly-2025-08-05 * chore: bump to nightly-2025-08-07 (#496) * chore: switch back to main md4lean (#497) * chore: bump to nightly nightly-2025-08-08 * chore: bump to nightly nightly-2025-08-10 * chore: bump to nightly nightly-2025-08-11 * chore: bump to nightly nightly-2025-08-12 * chore: bump to nightly nightly-2025-08-13 * chore: bump toolchain to v4.23.0-rc1 --------- Co-authored-by: David Thrane Christiansen <david@lean-fro.org> Co-authored-by: Sofia Rodrigues <algebraic.sofia+github@gmail.com> Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk> Co-authored-by: Pim Otte <otte.pim@gmail.com> Co-authored-by: Hanson Char <hanson.char@gmail.com> Co-authored-by: jrr6 <7482866+jrr6@users.noreply.github.com> Co-authored-by: github-actions[bot] <github-actions[bot]@users.noreply.github.com> Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
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.
No description provided.