From f9cd7ebb7cca0085f498a834be8dae360e46270a Mon Sep 17 00:00:00 2001 From: Adam Dingle Date: Thu, 9 Jul 2026 16:24:56 -0400 Subject: [PATCH 1/3] fix: preserve paragraphs in docstring boxes in TeX output (#918) --- src/verso-manual/VersoManual/Docstring.lean | 7 ++++--- src/verso-manual/VersoManual/TeX.lean | 1 + 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/src/verso-manual/VersoManual/Docstring.lean b/src/verso-manual/VersoManual/Docstring.lean index a9e6a5305..4fa682d88 100644 --- a/src/verso-manual/VersoManual/Docstring.lean +++ b/src/verso-manual/VersoManual/Docstring.lean @@ -567,7 +567,7 @@ def internalSignature.descr : BlockDescr where if let some sig := signature then pure \TeX{ " : " \Lean{ (← sig.toTeX) } } else pure .empty - pure \TeX{\par " " \Lean{← name.toTeX} \Lean{signatureTeX} \Lean{.seq (← contents.mapM goB)}} + pure \TeX{\par\noindent " " \Lean{← name.toTeX} \Lean{signatureTeX} \Lean{.seq (← contents.mapM goB)}} toHtml := some fun _goI goB _id info contents => open Verso.Doc.Html HtmlT in open Verso.Output Html in do @@ -629,7 +629,7 @@ def fieldSignature.descr : BlockDescr where | .public => .empty | .private => \TeX{ \textbf{"private"} } | .protected => .empty - let desc := \TeX{ \par " " \Lean{visibility} \Lean{← name.toTeX} " : " \Lean{← signature.toTeX} \par " " \Lean{.seq (← contents.mapM goB)}} + let desc := \TeX{ \par\noindent " " \Lean{visibility} \Lean{← name.toTeX} " : " \Lean{← signature.toTeX} \par " " \Lean{.seq (← contents.mapM goB)}} let parentsTeX := (← parents.toList.mapM (·.toTeX)).intersperse (.raw ", ") let inheritedExtra : Output.TeX := match inheritedFrom with | .none => "" @@ -843,7 +843,8 @@ def docstring.descr : BlockDescr := withHighlighting { let label := customLabel.getD declType.label if label == "" then reportError s!"Missing label for '{name}': supply one with 'label := \"LABEL\"'" - pure \TeX{\begin{docstringBox}{\Lean{label}} \Lean{← signature.toTeX} \tcblower " " \Lean{← contents.mapM goB} \end{docstringBox}} + pure \TeX{\begin{docstringBox}{\Lean{label}} \Lean{← signature.toTeX} \tcblower " " + \Lean{← contents.mapM (fun b => do pure <| seq #[← goB b, .paragraphBreak])} \end{docstringBox}} extraCss := [docstringStyle] } diff --git a/src/verso-manual/VersoManual/TeX.lean b/src/verso-manual/VersoManual/TeX.lean index 96ff529b9..1fb30e9ab 100644 --- a/src/verso-manual/VersoManual/TeX.lean +++ b/src/verso-manual/VersoManual/TeX.lean @@ -97,6 +97,7 @@ r##" \definecolor{bordercolor}{HTML}{98B2C0} \definecolor{medgray}{HTML}{555555} \newtcolorbox{docstringBox}[2][]{colback=white, +before lower={\parindent15pt\noindent}, % indent all paragraphs after first within lower part of box breakable, colframe=bordercolor, colbacktitle=white, From ab1997f1fca36f5bd285ebb61313008a82f9ce4a Mon Sep 17 00:00:00 2001 From: Adam Dingle Date: Tue, 28 Jul 2026 17:47:30 +0100 Subject: [PATCH 2/3] chore: fix integration tests --- .../code-content-doc/expected/tex/main.tex | 1 + .../diagram-doc/expected/tex/main.tex | 1 + .../escape-doc/expected/tex/main.tex | 1 + .../extra-files-doc/expected/tex/main.tex | 1 + .../front-matter-doc/expected/tex/main.tex | 1 + .../inheritance-doc/expected/tex/main.tex | 11 +- .../sample-doc/expected/tex/main.tex | 11 +- .../literate-config/lake-manifest.json | 119 +++++++------- .../literate-multi-root/lake-manifest.json | 119 +++++++------- test.out | 145 ++++++++++++++++++ 10 files changed, 275 insertions(+), 135 deletions(-) create mode 100644 test.out diff --git a/src/tests/integration/code-content-doc/expected/tex/main.tex b/src/tests/integration/code-content-doc/expected/tex/main.tex index 4d245fe9d..dc5c4add1 100644 --- a/src/tests/integration/code-content-doc/expected/tex/main.tex +++ b/src/tests/integration/code-content-doc/expected/tex/main.tex @@ -88,6 +88,7 @@ \definecolor{bordercolor}{HTML}{98B2C0} \definecolor{medgray}{HTML}{555555} \newtcolorbox{docstringBox}[2][]{colback=white, +before lower={\parindent15pt\noindent}, % indent all paragraphs after first within lower part of box breakable, colframe=bordercolor, colbacktitle=white, diff --git a/src/tests/integration/diagram-doc/expected/tex/main.tex b/src/tests/integration/diagram-doc/expected/tex/main.tex index 47d521914..cae367de9 100644 --- a/src/tests/integration/diagram-doc/expected/tex/main.tex +++ b/src/tests/integration/diagram-doc/expected/tex/main.tex @@ -88,6 +88,7 @@ \definecolor{bordercolor}{HTML}{98B2C0} \definecolor{medgray}{HTML}{555555} \newtcolorbox{docstringBox}[2][]{colback=white, +before lower={\parindent15pt\noindent}, % indent all paragraphs after first within lower part of box breakable, colframe=bordercolor, colbacktitle=white, diff --git a/src/tests/integration/escape-doc/expected/tex/main.tex b/src/tests/integration/escape-doc/expected/tex/main.tex index 643e68e0e..ad10c55ff 100644 --- a/src/tests/integration/escape-doc/expected/tex/main.tex +++ b/src/tests/integration/escape-doc/expected/tex/main.tex @@ -88,6 +88,7 @@ \definecolor{bordercolor}{HTML}{98B2C0} \definecolor{medgray}{HTML}{555555} \newtcolorbox{docstringBox}[2][]{colback=white, +before lower={\parindent15pt\noindent}, % indent all paragraphs after first within lower part of box breakable, colframe=bordercolor, colbacktitle=white, diff --git a/src/tests/integration/extra-files-doc/expected/tex/main.tex b/src/tests/integration/extra-files-doc/expected/tex/main.tex index c9aa89ea8..0e510661d 100644 --- a/src/tests/integration/extra-files-doc/expected/tex/main.tex +++ b/src/tests/integration/extra-files-doc/expected/tex/main.tex @@ -88,6 +88,7 @@ \definecolor{bordercolor}{HTML}{98B2C0} \definecolor{medgray}{HTML}{555555} \newtcolorbox{docstringBox}[2][]{colback=white, +before lower={\parindent15pt\noindent}, % indent all paragraphs after first within lower part of box breakable, colframe=bordercolor, colbacktitle=white, diff --git a/src/tests/integration/front-matter-doc/expected/tex/main.tex b/src/tests/integration/front-matter-doc/expected/tex/main.tex index 371a84f8e..7da5a0b40 100644 --- a/src/tests/integration/front-matter-doc/expected/tex/main.tex +++ b/src/tests/integration/front-matter-doc/expected/tex/main.tex @@ -88,6 +88,7 @@ \definecolor{bordercolor}{HTML}{98B2C0} \definecolor{medgray}{HTML}{555555} \newtcolorbox{docstringBox}[2][]{colback=white, +before lower={\parindent15pt\noindent}, % indent all paragraphs after first within lower part of box breakable, colframe=bordercolor, colbacktitle=white, diff --git a/src/tests/integration/inheritance-doc/expected/tex/main.tex b/src/tests/integration/inheritance-doc/expected/tex/main.tex index 0600aab1b..1a8eba05f 100644 --- a/src/tests/integration/inheritance-doc/expected/tex/main.tex +++ b/src/tests/integration/inheritance-doc/expected/tex/main.tex @@ -88,6 +88,7 @@ \definecolor{bordercolor}{HTML}{98B2C0} \definecolor{medgray}{HTML}{555555} \newtcolorbox{docstringBox}[2][]{colback=white, +before lower={\parindent15pt\noindent}, % indent all paragraphs after first within lower part of box breakable, colframe=bordercolor, colbacktitle=white, @@ -143,7 +144,15 @@ \cleardoublepage \begin{docstringBox}{structure} -\LeanVerb|Verso.\allowbreak{}Integration.\allowbreak{}Inheritance\-Doc.\allowbreak{}Foo\-Extends : Type|\tcblower Documentation for FooExtends\par\noindent\textbf{Constructor}\par \par \LeanVerb|Verso.\allowbreak{}Integration.\allowbreak{}Inheritance\-Doc.\allowbreak{}Foo\-Extends.\allowbreak{}mk|\par\noindent\textbf{Extends}\par Verso.Integration.InheritanceDoc.FooExtends\par\noindent\textbf{Fields}\par \par \LeanVerb|bar\-Field1| : \LeanVerb|Bool|\par Inherited from \LeanVerb|Bar\-Extended|\par \LeanVerb|bar\-Field2| : \LeanVerb|Unit|\par Inherited from \LeanVerb|Bar\-Extended|\par \LeanVerb|foo\-Field1| : \LeanVerb|Nat|\par Documentation for fooField1\par \LeanVerb|foo\-Field2| : \LeanVerb|String|\par Documentation for fooField2 +\LeanVerb|Verso.\allowbreak{}Integration.\allowbreak{}Inheritance\-Doc.\allowbreak{}Foo\-Extends : Type|\tcblower Documentation for FooExtends + +\par\noindent\textbf{Constructor}\par \par\noindent \LeanVerb|Verso.\allowbreak{}Integration.\allowbreak{}Inheritance\-Doc.\allowbreak{}Foo\-Extends.\allowbreak{}mk| + +\par\noindent\textbf{Extends}\par Verso.Integration.InheritanceDoc.FooExtends + +\par\noindent\textbf{Fields}\par \par\noindent \LeanVerb|bar\-Field1| : \LeanVerb|Bool|\par Inherited from \LeanVerb|Bar\-Extended|\par\noindent \LeanVerb|bar\-Field2| : \LeanVerb|Unit|\par Inherited from \LeanVerb|Bar\-Extended|\par\noindent \LeanVerb|foo\-Field1| : \LeanVerb|Nat|\par Documentation for fooField1\par\noindent \LeanVerb|foo\-Field2| : \LeanVerb|String|\par Documentation for fooField2 + + \end{docstringBox} diff --git a/src/tests/integration/sample-doc/expected/tex/main.tex b/src/tests/integration/sample-doc/expected/tex/main.tex index 7d0f48a24..5dcb18dd7 100644 --- a/src/tests/integration/sample-doc/expected/tex/main.tex +++ b/src/tests/integration/sample-doc/expected/tex/main.tex @@ -88,6 +88,7 @@ \definecolor{bordercolor}{HTML}{98B2C0} \definecolor{medgray}{HTML}{555555} \newtcolorbox{docstringBox}[2][]{colback=white, +before lower={\parindent15pt\noindent}, % indent all paragraphs after first within lower part of box breakable, colframe=bordercolor, colbacktitle=white, @@ -143,9 +144,15 @@ \cleardoublepage \begin{docstringBox}{def} -\LeanVerb|Verso.\allowbreak{}Integration.\allowbreak{}Sample\-Doc.\allowbreak{}sample_constant : Type|\tcblower This is a docstring.Here's some more text with a \LeanVerb|code inline| in it. +\LeanVerb|Verso.\allowbreak{}Integration.\allowbreak{}Sample\-Doc.\allowbreak{}sample_constant : Type|\tcblower This is a docstring. + +Here's some more text with a \LeanVerb|code inline| in it. Here's when a \LeanVerb|code inline| -occurs right before a line break.And then here's a paragraph break. +occurs right before a line break. + +And then here's a paragraph break. + + \end{docstringBox} Here is a test of \LeanVerb|escaping of things like \symbol{92}TeX in code inlines| diff --git a/test-projects/literate-config/lake-manifest.json b/test-projects/literate-config/lake-manifest.json index 1df319f58..599d1b9fd 100644 --- a/test-projects/literate-config/lake-manifest.json +++ b/test-projects/literate-config/lake-manifest.json @@ -1,66 +1,53 @@ -{ - "version": "1.2.0", - "packagesDir": ".lake/packages", - "packages": [ - { - "type": "path", - "scope": "", - "name": "verso", - "manifestFile": "lake-manifest.json", - "inherited": false, - "dir": "../..", - "configFile": "lakefile.lean" - }, - { - "url": "https://github.com/leanprover/illuminate", - "type": "git", - "subDir": null, - "scope": "", - "rev": "b3debfe6b629192033ef87257e1c60201881646f", - "name": "illuminate", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean" - }, - { - "url": "https://github.com/leanprover-community/plausible", - "type": "git", - "subDir": null, - "scope": "", - "rev": "e12c1910fe855cbfc38803cd4e55543906d5fa62", - "name": "plausible", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml" - }, - { - "url": "https://github.com/acmepjz/md4lean", - "type": "git", - "subDir": null, - "scope": "", - "rev": "31907cc18f48a95384f99cee5582c00fb39e0f67", - "name": "MD4Lean", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean" - }, - { - "url": "https://github.com/leanprover/subverso", - "type": "git", - "subDir": null, - "scope": "", - "rev": "4db22f2caed235317d21945d1b51fba0fdb69e89", - "name": "subverso", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean" - } - ], - "name": "«literate-config-test»", - "lakeDir": ".lake", - "fixedToolchain": false -} +{"version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": + [{"type": "path", + "scope": "", + "name": "verso", + "manifestFile": "lake-manifest.json", + "inherited": false, + "dir": "../..", + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover/illuminate", + "type": "git", + "subDir": null, + "scope": "", + "rev": "56958b3901ca108830de34fbce6cecd4b5757c1f", + "name": "illuminate", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "", + "rev": "b1c4a69a7e247ab7df20460212001673d74f08c0", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/acmepjz/md4lean", + "type": "git", + "subDir": null, + "scope": "", + "rev": "31907cc18f48a95384f99cee5582c00fb39e0f67", + "name": "MD4Lean", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover/subverso", + "type": "git", + "subDir": null, + "scope": "", + "rev": "4db22f2caed235317d21945d1b51fba0fdb69e89", + "name": "subverso", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}], + "name": "«literate-config-test»", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/test-projects/literate-multi-root/lake-manifest.json b/test-projects/literate-multi-root/lake-manifest.json index d3c6b734f..ba23ee257 100644 --- a/test-projects/literate-multi-root/lake-manifest.json +++ b/test-projects/literate-multi-root/lake-manifest.json @@ -1,66 +1,53 @@ -{ - "version": "1.2.0", - "packagesDir": ".lake/packages", - "packages": [ - { - "type": "path", - "scope": "", - "name": "verso", - "manifestFile": "lake-manifest.json", - "inherited": false, - "dir": "../..", - "configFile": "lakefile.lean" - }, - { - "url": "https://github.com/leanprover/illuminate", - "type": "git", - "subDir": null, - "scope": "", - "rev": "b3debfe6b629192033ef87257e1c60201881646f", - "name": "illuminate", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean" - }, - { - "url": "https://github.com/leanprover-community/plausible", - "type": "git", - "subDir": null, - "scope": "", - "rev": "e12c1910fe855cbfc38803cd4e55543906d5fa62", - "name": "plausible", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml" - }, - { - "url": "https://github.com/acmepjz/md4lean", - "type": "git", - "subDir": null, - "scope": "", - "rev": "31907cc18f48a95384f99cee5582c00fb39e0f67", - "name": "MD4Lean", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean" - }, - { - "url": "https://github.com/leanprover/subverso", - "type": "git", - "subDir": null, - "scope": "", - "rev": "4db22f2caed235317d21945d1b51fba0fdb69e89", - "name": "subverso", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean" - } - ], - "name": "«literate-multi-root-test»", - "lakeDir": ".lake", - "fixedToolchain": false -} +{"version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": + [{"type": "path", + "scope": "", + "name": "verso", + "manifestFile": "lake-manifest.json", + "inherited": false, + "dir": "../..", + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover/illuminate", + "type": "git", + "subDir": null, + "scope": "", + "rev": "56958b3901ca108830de34fbce6cecd4b5757c1f", + "name": "illuminate", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "", + "rev": "b1c4a69a7e247ab7df20460212001673d74f08c0", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/acmepjz/md4lean", + "type": "git", + "subDir": null, + "scope": "", + "rev": "31907cc18f48a95384f99cee5582c00fb39e0f67", + "name": "MD4Lean", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover/subverso", + "type": "git", + "subDir": null, + "scope": "", + "rev": "4db22f2caed235317d21945d1b51fba0fdb69e89", + "name": "subverso", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}], + "name": "«literate-multi-root-test»", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/test.out b/test.out new file mode 100644 index 000000000..163d3212d --- /dev/null +++ b/test.out @@ -0,0 +1,145 @@ +Running build-log tests... + All build-log tests passed. +Running serialization tests with Plausible... +testInternalId: success (no proof) +testObject: success (no proof) +testDomain: success (no proof) +testRefDomain: success (no proof) +testRefObject: success (no proof) +testRemoteInfo: success (no proof) +testAllRemotes: success (no proof) +testTraverseState: success (no proof) +testHtml: success (no proof) +testDataFile: success (no proof) +testNumbering: success (no proof) +testXrefSource: success (no proof) +testRemote: success (no proof) +testSearchPriorities: success (no proof) +testPriorityMapJson: success (no proof) +Running search JS wire-format tests... +testMapperToJs: passed +testMappersToJs: passed +testMappersToJsDefaults: passed +testPriorityMap: passed +Running blog tests with Plausible... +freshIdOk: success (no proof) +freshId_first_is_hint: success (no proof) +freshId_second_is_hint_with_1: success (no proof) +Running test in src/tests/integration/sample-doc... +Running test in src/tests/integration/inheritance-doc... +Running test in src/tests/integration/code-content-doc... +Running test in src/tests/integration/extra-files-doc... +Running test in src/tests/integration/escape-doc... +Running test in src/tests/integration/front-matter-doc... +Running test in src/tests/integration/diagram-doc... +Running zip tests with fixed files... +Running random zip test with 5 files +Running random zip test with 0 files +Running random zip test with 15 files +Running random zip test with 11 files +Running random zip test with 0 files +Running random zip test with 9 files +Running random zip test with 7 files +Running random zip test with 2 files +Running random zip test with 13 files +Running random zip test with 10 files +Running interactive (LSP) tests... +current dir: /home/adam/src/verso +------------------------------------------------ + Starting Verso Interactive Test Suite: Tue Jul 28 05:45:43 PM WEST 2026 +------------------------------------------------ +Running test: completion_inline.lean... ✅ PASS +Running test: folding_verso.lean... ✅ PASS +Running test: folding_verso_term_doc.lean... ✅ PASS +Running test: infoview_verso.lean... ✅ PASS +Running test: inline_goals.lean... ✅ PASS +Running test: math_hover.lean... ✅ PASS +Running test: symbols_verso.lean... ✅ PASS +Running test: symbols_verso_term_doc.lean... ✅ PASS +Running test: title_escape_hover.lean... ✅ PASS +Running test: title_unicode_escape_hover.lean... ✅ PASS +----------------------------------------------- +Test Summary: + Total: 10 + Passed: 10 + Failed: 0 +All tests passed successfully! +----------------------------------------------- +Running literate config unit tests... + missing file: passed + empty file: passed + whitespace file: passed + exclude: passed + order: passed + landing_page: passed + order_children: passed + targets: passed + combined: passed + invalid TOML: passed + hide_commands: passed + metadata: passed + extra_css/js: passed + show_docstrings: passed + show_docstrings_for: passed + hide_docstrings_for: passed + show_output: passed + show_output default: passed + show_imports: passed + show_imports default: passed + combined new: passed + theme light: passed + theme dark: passed + theme empty: passed + modules config: passed + resolve no match: passed + resolve prefix match: passed + resolve overrides global: passed + All literate config tests passed. +Running literate HTML tests... + Building literate JSON for test modules... + default behavior... passed + exclude... passed + navbar order... passed + landing page... passed + HTML landing_page not found... passed + recursive exclusion... passed + order_children... passed + xref.json generated... passed + plan file content... passed + targets filtering... passed + targets library... passed + targets library nonexistent... passed + targets library + module... passed + hide_commands... passed + metadata title... passed + extra CSS... passed + show_docstrings = false... passed + hide_docstrings_for... passed + show_imports = false... passed + show_imports default... passed + show_output... passed + show_output = []... passed + favicon... passed + extra JS... passed + targets + exclude... passed + show_docstrings_for exceptions... passed + metadata description... passed + current page highlighting... passed + plan targets + exclude... passed + plan landing_page not in set... passed + plan empty module set... passed + plan order warning... passed + HTML invalid docstring_for... passed + theme CSS... passed + theme CSS empty... passed + per-module hide_commands... passed + per-module title... passed + per-module title breadcrumbs... passed + per-module url... passed + per-module url inheritance... passed + plan duplicate url... passed + plan duplicate url trailing slash... passed + plan duplicate url case... passed + accessibility focus-visible... passed + accessibility reduced-motion... passed + accessibility ARIA... \ No newline at end of file From 3cbc3ac9bd99fd5d53735afa8149c82cdc3ea210 Mon Sep 17 00:00:00 2001 From: Adam Dingle Date: Tue, 28 Jul 2026 17:54:56 +0100 Subject: [PATCH 3/3] chore: revert several files committed by mistake --- .../literate-config/lake-manifest.json | 119 +++++++------- .../literate-multi-root/lake-manifest.json | 119 +++++++------- test.out | 145 ------------------ 3 files changed, 132 insertions(+), 251 deletions(-) delete mode 100644 test.out diff --git a/test-projects/literate-config/lake-manifest.json b/test-projects/literate-config/lake-manifest.json index 599d1b9fd..1df319f58 100644 --- a/test-projects/literate-config/lake-manifest.json +++ b/test-projects/literate-config/lake-manifest.json @@ -1,53 +1,66 @@ -{"version": "1.2.0", - "packagesDir": ".lake/packages", - "packages": - [{"type": "path", - "scope": "", - "name": "verso", - "manifestFile": "lake-manifest.json", - "inherited": false, - "dir": "../..", - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/illuminate", - "type": "git", - "subDir": null, - "scope": "", - "rev": "56958b3901ca108830de34fbce6cecd4b5757c1f", - "name": "illuminate", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/plausible", - "type": "git", - "subDir": null, - "scope": "", - "rev": "b1c4a69a7e247ab7df20460212001673d74f08c0", - "name": "plausible", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/acmepjz/md4lean", - "type": "git", - "subDir": null, - "scope": "", - "rev": "31907cc18f48a95384f99cee5582c00fb39e0f67", - "name": "MD4Lean", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/subverso", - "type": "git", - "subDir": null, - "scope": "", - "rev": "4db22f2caed235317d21945d1b51fba0fdb69e89", - "name": "subverso", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}], - "name": "«literate-config-test»", - "lakeDir": ".lake", - "fixedToolchain": false} +{ + "version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": [ + { + "type": "path", + "scope": "", + "name": "verso", + "manifestFile": "lake-manifest.json", + "inherited": false, + "dir": "../..", + "configFile": "lakefile.lean" + }, + { + "url": "https://github.com/leanprover/illuminate", + "type": "git", + "subDir": null, + "scope": "", + "rev": "b3debfe6b629192033ef87257e1c60201881646f", + "name": "illuminate", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean" + }, + { + "url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "", + "rev": "e12c1910fe855cbfc38803cd4e55543906d5fa62", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/acmepjz/md4lean", + "type": "git", + "subDir": null, + "scope": "", + "rev": "31907cc18f48a95384f99cee5582c00fb39e0f67", + "name": "MD4Lean", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean" + }, + { + "url": "https://github.com/leanprover/subverso", + "type": "git", + "subDir": null, + "scope": "", + "rev": "4db22f2caed235317d21945d1b51fba0fdb69e89", + "name": "subverso", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean" + } + ], + "name": "«literate-config-test»", + "lakeDir": ".lake", + "fixedToolchain": false +} diff --git a/test-projects/literate-multi-root/lake-manifest.json b/test-projects/literate-multi-root/lake-manifest.json index ba23ee257..d3c6b734f 100644 --- a/test-projects/literate-multi-root/lake-manifest.json +++ b/test-projects/literate-multi-root/lake-manifest.json @@ -1,53 +1,66 @@ -{"version": "1.2.0", - "packagesDir": ".lake/packages", - "packages": - [{"type": "path", - "scope": "", - "name": "verso", - "manifestFile": "lake-manifest.json", - "inherited": false, - "dir": "../..", - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/illuminate", - "type": "git", - "subDir": null, - "scope": "", - "rev": "56958b3901ca108830de34fbce6cecd4b5757c1f", - "name": "illuminate", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/plausible", - "type": "git", - "subDir": null, - "scope": "", - "rev": "b1c4a69a7e247ab7df20460212001673d74f08c0", - "name": "plausible", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/acmepjz/md4lean", - "type": "git", - "subDir": null, - "scope": "", - "rev": "31907cc18f48a95384f99cee5582c00fb39e0f67", - "name": "MD4Lean", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/subverso", - "type": "git", - "subDir": null, - "scope": "", - "rev": "4db22f2caed235317d21945d1b51fba0fdb69e89", - "name": "subverso", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}], - "name": "«literate-multi-root-test»", - "lakeDir": ".lake", - "fixedToolchain": false} +{ + "version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": [ + { + "type": "path", + "scope": "", + "name": "verso", + "manifestFile": "lake-manifest.json", + "inherited": false, + "dir": "../..", + "configFile": "lakefile.lean" + }, + { + "url": "https://github.com/leanprover/illuminate", + "type": "git", + "subDir": null, + "scope": "", + "rev": "b3debfe6b629192033ef87257e1c60201881646f", + "name": "illuminate", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean" + }, + { + "url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "", + "rev": "e12c1910fe855cbfc38803cd4e55543906d5fa62", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/acmepjz/md4lean", + "type": "git", + "subDir": null, + "scope": "", + "rev": "31907cc18f48a95384f99cee5582c00fb39e0f67", + "name": "MD4Lean", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean" + }, + { + "url": "https://github.com/leanprover/subverso", + "type": "git", + "subDir": null, + "scope": "", + "rev": "4db22f2caed235317d21945d1b51fba0fdb69e89", + "name": "subverso", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean" + } + ], + "name": "«literate-multi-root-test»", + "lakeDir": ".lake", + "fixedToolchain": false +} diff --git a/test.out b/test.out deleted file mode 100644 index 163d3212d..000000000 --- a/test.out +++ /dev/null @@ -1,145 +0,0 @@ -Running build-log tests... - All build-log tests passed. -Running serialization tests with Plausible... -testInternalId: success (no proof) -testObject: success (no proof) -testDomain: success (no proof) -testRefDomain: success (no proof) -testRefObject: success (no proof) -testRemoteInfo: success (no proof) -testAllRemotes: success (no proof) -testTraverseState: success (no proof) -testHtml: success (no proof) -testDataFile: success (no proof) -testNumbering: success (no proof) -testXrefSource: success (no proof) -testRemote: success (no proof) -testSearchPriorities: success (no proof) -testPriorityMapJson: success (no proof) -Running search JS wire-format tests... -testMapperToJs: passed -testMappersToJs: passed -testMappersToJsDefaults: passed -testPriorityMap: passed -Running blog tests with Plausible... -freshIdOk: success (no proof) -freshId_first_is_hint: success (no proof) -freshId_second_is_hint_with_1: success (no proof) -Running test in src/tests/integration/sample-doc... -Running test in src/tests/integration/inheritance-doc... -Running test in src/tests/integration/code-content-doc... -Running test in src/tests/integration/extra-files-doc... -Running test in src/tests/integration/escape-doc... -Running test in src/tests/integration/front-matter-doc... -Running test in src/tests/integration/diagram-doc... -Running zip tests with fixed files... -Running random zip test with 5 files -Running random zip test with 0 files -Running random zip test with 15 files -Running random zip test with 11 files -Running random zip test with 0 files -Running random zip test with 9 files -Running random zip test with 7 files -Running random zip test with 2 files -Running random zip test with 13 files -Running random zip test with 10 files -Running interactive (LSP) tests... -current dir: /home/adam/src/verso ------------------------------------------------- - Starting Verso Interactive Test Suite: Tue Jul 28 05:45:43 PM WEST 2026 ------------------------------------------------- -Running test: completion_inline.lean... ✅ PASS -Running test: folding_verso.lean... ✅ PASS -Running test: folding_verso_term_doc.lean... ✅ PASS -Running test: infoview_verso.lean... ✅ PASS -Running test: inline_goals.lean... ✅ PASS -Running test: math_hover.lean... ✅ PASS -Running test: symbols_verso.lean... ✅ PASS -Running test: symbols_verso_term_doc.lean... ✅ PASS -Running test: title_escape_hover.lean... ✅ PASS -Running test: title_unicode_escape_hover.lean... ✅ PASS ------------------------------------------------ -Test Summary: - Total: 10 - Passed: 10 - Failed: 0 -All tests passed successfully! ------------------------------------------------ -Running literate config unit tests... - missing file: passed - empty file: passed - whitespace file: passed - exclude: passed - order: passed - landing_page: passed - order_children: passed - targets: passed - combined: passed - invalid TOML: passed - hide_commands: passed - metadata: passed - extra_css/js: passed - show_docstrings: passed - show_docstrings_for: passed - hide_docstrings_for: passed - show_output: passed - show_output default: passed - show_imports: passed - show_imports default: passed - combined new: passed - theme light: passed - theme dark: passed - theme empty: passed - modules config: passed - resolve no match: passed - resolve prefix match: passed - resolve overrides global: passed - All literate config tests passed. -Running literate HTML tests... - Building literate JSON for test modules... - default behavior... passed - exclude... passed - navbar order... passed - landing page... passed - HTML landing_page not found... passed - recursive exclusion... passed - order_children... passed - xref.json generated... passed - plan file content... passed - targets filtering... passed - targets library... passed - targets library nonexistent... passed - targets library + module... passed - hide_commands... passed - metadata title... passed - extra CSS... passed - show_docstrings = false... passed - hide_docstrings_for... passed - show_imports = false... passed - show_imports default... passed - show_output... passed - show_output = []... passed - favicon... passed - extra JS... passed - targets + exclude... passed - show_docstrings_for exceptions... passed - metadata description... passed - current page highlighting... passed - plan targets + exclude... passed - plan landing_page not in set... passed - plan empty module set... passed - plan order warning... passed - HTML invalid docstring_for... passed - theme CSS... passed - theme CSS empty... passed - per-module hide_commands... passed - per-module title... passed - per-module title breadcrumbs... passed - per-module url... passed - per-module url inheritance... passed - plan duplicate url... passed - plan duplicate url trailing slash... passed - plan duplicate url case... passed - accessibility focus-visible... passed - accessibility reduced-motion... passed - accessibility ARIA... \ No newline at end of file