fix: Lean blocks/inlines in TeX (#706)

Fixes inline Lean blocks/inlines, esp. the display of the | character.

Adds tests to keep this working, and updates the integration tests to
run lualatex on the output if requested.

Author: david-christiansen

.github/workflows/ci.yml

@@ -64,32 +64,6 @@ jobs:
               run: |
                   lake build
 
-            - name: Run tests
-              run: |
-                  lake test
-
-            - name: Generate the test website
-              run: |
-                  lake exe demosite --output _out/test-projects/demosite
-
-            - name: Generate the test genre's document
-              run: |
-                  lake exe simplepage
-
-            - name: Generate some source HTML
-              run: |
-                  lake build Verso.Hover:literate
-                  lake exe verso-html .lake/build/literate htmlout
-
-            - name: Check internal links on the test website
-              uses: lycheeverse/[email protected]
-              with:
-                  format: markdown
-                  jobSummary: true
-                  args:
-                      --base './_out/test-projects/demosite' --no-progress --offline
-                      './_out/test-projects/demosite/**/*.html'
-
             - name: Install PDF Dependencies
               uses: zauguin/install-texlive@v4
               with:
@@ -136,6 +110,32 @@ jobs:
             - name: Check `tlmgr` version
               run: tlmgr --version
 
+            - name: Run tests
+              run: |
+                  lake test -- --verbose --check-tex
+
+            - name: Generate the test website
+              run: |
+                  lake exe demosite --output _out/test-projects/demosite
+
+            - name: Generate the test genre's document
+              run: |
+                  lake exe simplepage
+
+            - name: Generate some source HTML
+              run: |
+                  lake build Verso.Hover:literate
+                  lake exe verso-html .lake/build/literate htmlout
+
+            - name: Check internal links on the test website
+              uses: lycheeverse/[email protected]
+              with:
+                  format: markdown
+                  jobSummary: true
+                  args:
+                      --base './_out/test-projects/demosite' --no-progress --offline
+                      './_out/test-projects/demosite/**/*.html'
+
             - name: Generate the manual
               run: |
                   ./generate.sh

.gitignore

@@ -12,3 +12,9 @@ _out
 *.hash
 profile.json
 profile.json.gz
+/src/tests/integration/**/*.log
+/src/tests/integration/**/*.aux
+/src/tests/integration/**/*.out
+/src/tests/integration/**/*.pdf
+/src/tests/integration/**/*.toc
+

src/tests/TestMain.lean

@@ -11,7 +11,9 @@ import VersoUtil.LzCompress
 import Tests
 
 structure Config where
+  verbose : Bool := false
   updateExpected : Bool := false
+  checkTeX : Bool := false
 
 open Verso.Search.Stemmer.Porter in
 def testStemmer (_ : Config) : IO Unit := do
@@ -37,8 +39,10 @@ Tests manual-genre TeX generation. `dir` is a subdirectory specific to a particu
 which is where actual output should go, and which contains the expected output directory.
 `doc` is the document to be rendered.
 -/
-def testTexOutput (dir : System.FilePath) (doc : Verso.Doc.VersoDoc Verso.Genre.Manual) :
-    Config →  IO Unit := fun config =>
+def testTexOutput
+    (dir : System.FilePath)
+    (doc : Verso.Doc.VersoDoc Verso.Genre.Manual)
+    (config : Config) : IO Unit := do
   let versoConfig : Verso.Genre.Manual.Config := {
     destination := "src/tests/integration" / dir / "output",
     emitTeX := true,
@@ -50,13 +54,13 @@ def testTexOutput (dir : System.FilePath) (doc : Verso.Doc.VersoDoc Verso.Genre.
     let logError (msg : String) := IO.eprintln msg
     ReaderT.run (emitTeX logError versoConfig doc.toPart) extension_impls%
 
-  Verso.Integration.runTests {
+  Verso.Integration.runTests { config with
     testDir := "src/tests/integration" / dir,
     updateExpected := config.updateExpected,
     runTest
   }
 
-def testZip (_ : Config) : IO Unit := do
+def testZip (cfg : Config) : IO Unit := do
   IO.println "Running zip tests with fixed files..."
   testExtract #[] .store
   testExtract #[] .deflate
@@ -74,16 +78,21 @@ def testZip (_ : Config) : IO Unit := do
     testExtract #[("T2.lean", me), ("other", bwd)] .store
     testExtract #[("T2.lean", me), ("other", bwd)] .deflate
   for _ in (0 : Nat)...10 do
-    IO.setRandSeed (← IO.monoNanosNow)
+    let seedValue ← IO.monoNanosNow
+    if cfg.verbose then IO.println s!"Seed is {seedValue}"
+    IO.setRandSeed seedValue
     let mut randFiles := #[]
     for _ in 0...(← IO.rand 0 15) do
       let name ← randName
       let size ← IO.rand 0 50000
       let content ← IO.getRandomBytes <| .ofNat size
       randFiles := randFiles.push (name, content)
-    IO.println s!"Running random zip test with {randFiles.size} files, sizes:"
-    for (x, y) in randFiles do
-      IO.println s!" * {x}: {y.size} bytes"
+    if cfg.verbose then
+      IO.println s!"Running random zip test with {randFiles.size} files, sizes:"
+      for (x, y) in randFiles do
+        IO.println s!" * {x}: {y.size} bytes"
+    else
+      IO.println s!"Running random zip test with {randFiles.size} files"
     testExtract randFiles .store
     testExtract randFiles .deflate
 
@@ -147,12 +156,15 @@ def tests := [
   testStemmer,
   testTexOutput "sample-doc" SampleDoc.doc,
   testTexOutput "inheritance-doc" InheritanceDoc.doc,
+  testTexOutput "code-content-doc" CodeContent.doc,
   testZip
 ]
 
 def getConfig (config : Config) : List String → IO Config
   | [] => pure config
   | "--update-expected" :: args => getConfig { config with updateExpected := true } args
+  | "--verbose" :: args | "-v" :: args => getConfig { config with verbose := true } args
+  | "--check-tex" :: args => getConfig { config with checkTeX := true } args
   | other :: _ => throw <| .userError s!"Didn't understand {other}"
 
 def main (args : List String) : IO UInt32 := do

src/tests/Tests.lean

@@ -12,6 +12,7 @@ import Tests.HighlightedToTeX
 import Tests.HtmlEntities
 import Tests.Integration
 import Tests.Integration.SampleDoc
+import Tests.Integration.CodeContent
 import Tests.LeanCode
 import Tests.Integration.InheritanceDoc
 import Tests.ParserRegression

src/tests/Tests/Integration.lean

@@ -17,6 +17,8 @@ structure Config where
   updateExpected : Bool := false
   /-- How to run the test -/
   runTest : IO Unit
+  /-- Whether to see if lualatex builds the file -/
+  checkTeX : Bool
 
 /--
 Returns all non-directory filepaths that are children of `root`, which
@@ -87,4 +89,11 @@ def runTests (config : Config) : IO Unit := do
         IO.println (Lean.Diff.linesToString d)
         throw <| .userError s!"Test in {config.testDir} failed"
 
+    if config.checkTeX then
+      discard <| IO.Process.run {
+        cwd := outputRoot / "tex",
+        cmd := "lualatex",
+        args := #["-halt-on-error", "-interaction=nonstopmode", "main.tex"]
+      }
+
   return

src/tests/Tests/Integration/CodeContent.lean

@@ -0,0 +1,89 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Jason Reed
+-/
+import Verso
+import VersoManual
+
+namespace Verso.Integration.CodeContent
+
+open Verso Genre Manual InlineLean
+
+--------------------
+
+#docs (Manual) doc "Title of the Doc" :=
+:::::::
+
+%%%
+authors := ["Harry Q. Bovik"]
+%%%
+
+Here is some code with vertical bars:
+```lean
+def or := (· || ·)
+```
+
+Here is some with a variety of interesting Unicode, including characters where UTF-16 is funky:
+```lean
+def Set (α : Type u) : Type u := α → Prop
+
+instance : EmptyCollection (Set α) where
+  emptyCollection := fun _ => False
+
+instance : Union (Set α) where
+  union a b := fun x => a x ∨ b x
+
+instance : Inter (Set α) where
+  inter a b := fun x => a x ∧ b x
+
+instance : Membership α (Set α) where
+  mem a x := a x
+
+@[ext]
+theorem Set.ext {a b : Set α} :
+    (∀ x, x ∈ a ↔ x ∈ b) → a = b := by
+  intro h
+  funext x
+  exact propext (h x)
+
+instance : HasSubset (Set α) where
+  Subset a b := ∀ x, x ∈ a → x ∈ b
+
+@[simp, grind .]
+theorem Set.subset_refl {a : Set α} : a ⊆ a := by
+  simp [(· ⊆ ·)]
+
+@[grind ←]
+theorem Set.subset_union {a b c : Set α} :
+    a ⊆ b → a ⊆ b ∪ c := by
+  simp [(· ⊆ ·), (· ∪ ·), (· ∈ ·)]
+  intro h
+  solve_by_elim
+
+def Set.powerset (a : Set α) : Set (Set α) :=
+  fun (x : Set α) => x ⊆ a
+
+notation "𝒫 " x => Set.powerset x
+
+theorem Set.powerset_empty_nonempty :
+    ∃ (a : Set α), a ∈ 𝒫 {} := by
+  constructor
+  case w => exact {}
+  simp [(· ∈ ·), powerset]
+
+@[grind? →]
+theorem Set.powerset_empty_unique (x y : Set α) :
+    x ∈ (𝒫 {}) → y ∈ (𝒫 {}) → x = y := by
+  intro hx hy
+  ext x'
+  exact (iff_false_right (hy x')).mpr (hx x')
+```
+
+And now some inline code:
+
+ * {lean}`∀x y : Set _, x ∈ ((𝒫 x) ∪ (𝒫 y))`
+ * {lean}`true || false`
+ * {lean}`False → True`
+
+:::::::