chore: add tests for TeX output

.gitignore

@@ -7,4 +7,4 @@
 _out
 *.olean
 /.verso/
-/src/tests/parser/*/*.output
+/src/tests/integration/**/output

src/tests/TestMain.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: David Thrane Christiansen
 -/
 
+import Verso
+import VersoManual
 import VersoSearch.PorterStemmer
 import Tests
 
@@ -29,8 +31,34 @@ def testStemmer (_ : Config) : IO Unit := do
       IO.eprintln s!"{x} --> {s} (wanted '{y}')"
     throw <| IO.userError "Stemmer tests failed"
 
+/--
+Tests manual-genre TeX generation. `dir` is a subdirectory specific to a particular test document,
+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.Part Verso.Genre.Manual) :
+    Config →  IO Unit := fun config =>
+  let versoConfig : Verso.Genre.Manual.Config := {
+    destination := "src/tests/integration" / dir / "output",
+    emitTeX := true,
+    emitHtmlMulti := false
+  }
+
+  let runTest : IO Unit  :=
+    open Verso Genre Manual in do
+    let logError (msg : String) := IO.eprintln msg
+    ReaderT.run (emitTeX logError versoConfig doc) extension_impls%
+
+  Verso.Integration.runTests {
+    testDir := "src/tests/integration" / dir,
+    updateExpected := config.updateExpected,
+    runTest
+  }
+
+open Verso.Integration in
 def tests := [
-  testStemmer
+  testStemmer,
+  testTexOutput "sample-doc" SampleDoc.doc
 ]
 
 def getConfig (config : Config) : List String → IO Config

src/tests/Tests.lean

@@ -4,4 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: David Thrane Christiansen
 -/
 import Tests.Golden
+import Tests.Integration
+import Tests.Integration.SampleDoc
 import Tests.ParserRegression
+import Tests.TexUnit

src/tests/Tests/Integration.lean

@@ -0,0 +1,90 @@
+/-
+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 Lean.Util.Diff
+
+namespace Verso.Integration
+
+/-- Configuration for the test runner -/
+structure Config where
+  /-- Where are expected files located? We expect a subdirectory
+  `expected` and `runTest` should produce files into a subdirectory
+  `output`. -/
+  testDir : System.FilePath
+  /-- Should the expected output be replaced with the actual output? -/
+  updateExpected : Bool := false
+  /-- How to run the test -/
+  runTest : IO Unit
+
+/--
+Returns all non-directory filepaths that are children of `root`, which
+must be a directory. Returns these as paths relative to `root`.
+
+This differs from `System.FilePath.walkRoot`, in that the latter returns
+absolute paths, and includes subdirectories.
+-/
+partial def filesBelow (root : System.FilePath) :
+    IO (Array System.FilePath) := Prod.snd <$> StateT.run (go ".") #[]
+where
+  go (p : System.FilePath) := do
+    for d in (← (root / p).readDir) do
+      if ← d.path.isDir then
+        go (p / d.fileName)
+      else
+        modify (·.push (p / d.fileName))
+
+/--
+Given an array of pairs `(src, tgt)` of absolute paths, copy every
+`src` to every `tgt`, creating directories as necessary.
+-/
+partial def copyFiles (pairs : Array (System.FilePath × System.FilePath)) :
+    IO Unit := do
+  for (src, tgt) in pairs do
+    if let .some parent := tgt.parent then
+      IO.FS.createDirAll parent
+    IO.FS.writeBinFile tgt (← IO.FS.readBinFile src)
+
+/-- Main test runner -/
+def runTests (config : Config) : IO Unit := do
+  unless ← System.FilePath.pathExists config.testDir do
+    throw <| .userError s!"Test directory not found: {config.testDir}"
+
+  let outputRoot := config.testDir / "output"
+  let expectedRoot := config.testDir / "expected"
+
+  if config.updateExpected then
+    let outputFiles := (← filesBelow outputRoot)
+    IO.println s!"Updating expected outputs in {config.testDir}..."
+    if ← System.FilePath.pathExists expectedRoot then do
+      IO.FS.removeDirAll expectedRoot
+    copyFiles (outputFiles.map (fun p => (outputRoot / p, expectedRoot / p)))
+  else
+    unless ← System.FilePath.pathExists expectedRoot do
+      throw <| .userError s!"Expected output directory not found: {expectedRoot}"
+    let expectedFiles := (← filesBelow expectedRoot)
+
+    IO.println s!"Running test in {config.testDir}..."
+    if ← outputRoot.pathExists then
+      IO.FS.removeDirAll outputRoot
+    config.runTest
+    let outputFiles := (← filesBelow outputRoot)
+
+    if expectedFiles != outputFiles then
+      IO.println s!"✗ Expected files differ from actual files"
+      IO.println s!"Expected files in {expectedRoot}:\n  {expectedFiles}"
+      IO.println s!"Actual files in {outputRoot}:\n  {outputFiles}"
+      throw <| .userError s!"Test in {config.testDir} failed"
+
+    for file in expectedFiles do
+      let expected ← IO.FS.readFile (expectedRoot / file)
+      let actual ← IO.FS.readFile (outputRoot / file)
+      if expected != actual then
+        let d := Lean.Diff.diff (expected.split (· == '\n') |>.toArray) (actual.split (· == '\n') |>.toArray)
+        IO.println s!"✗ In test {config.testDir}, output file {file}"
+        IO.println s!"  Expected output differs from actual output"
+        IO.println (Lean.Diff.linesToString d)
+        throw <| .userError s!"Test in {config.testDir} failed"
+
+  return

src/tests/Tests/Integration/SampleDoc.lean

@@ -0,0 +1,37 @@
+/-
+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.SampleDoc
+
+open Verso Genre Manual
+
+--------------------
+
+/-- This is a docstring.
+
+Here's some more text with a `code inline` in it.
+Here's when a `code inline`
+occurs right before a line break.
+
+And then here's a paragraph break.
+-/
+def sample_constant := Unit
+
+#docs (Manual) doc "Title of the Doc" :=
+:::::::
+
+%%%
+shortTitle := "ShortTitle"
+authors := ["Harry Q. Bovik"]
+%%%
+
+{docstring sample_constant}
+
+:::::::
+
+end Verso.Integration.SampleDoc

src/tests/Tests/TexUnit.lean

@@ -0,0 +1,39 @@
+/-
+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 Tests.TexUtil
+
+/-!
+Unit tests covering TeX output given given concrete Verso structures.
+-/
+
+open Verso Genre.Manual
+
+/--
+info: before\Verb|verb|
+after
+-/
+#guard_msgs in
+#eval do
+  let b : Doc.Block Genre.Manual := .concat #[
+    .para #[
+      .text "before",
+      .other (Inline.leanFromMarkdown default) #[.code "verb"],
+      .text "after"
+    ]
+  ]
+  IO.println (← toTex b).asString
+
+/-- info: before\Verb|verb|after -/
+#guard_msgs in
+#eval do
+  let b : Doc.Block Genre.Manual := .concat #[
+    .para #[
+      .text "before",
+      .code "verb",
+      .text "after"
+    ]
+  ]
+  IO.println (← toTex b).asString

src/tests/Tests/TexUtil.lean

@@ -0,0 +1,43 @@
+/-
+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 Lean.Elab.Command
+import VersoManual
+
+/-!
+Support for writing unit tests covering TeX output.
+-/
+
+open Verso Genre.Manual
+
+/--
+Render a Verso block in Manual Genre to TeX in isolation
+
+This requires the `IO` monad because `TraverseM` does.
+-/
+def toTex (block : Doc.Block Genre.Manual) : IO Output.TeX := do
+  let extension_impls := extension_impls%
+
+  -- Traversal monadic data
+  let traverseContext : TraverseContext := {
+    logError msg := IO.println msg,
+  }
+  let traverseState : TraverseState := {
+    remoteContent := {},
+  }
+
+  -- Traverse the block. This shadows both `block` and `traverseState`.
+  -- This is where we engage with the IO at the bottom of TraverseM.
+  let ⟨block, traverseState⟩ ← Doc.Genre.traverse.block Genre.Manual block
+    |>.run extension_impls traverseContext traverseState
+
+  -- Options for TeX
+  let options : Doc.TeX.Options Genre.Manual (ReaderT ExtensionImpls IO) := {
+    headerLevel := none,
+    logError msg := IO.println msg,
+  }
+
+  -- Convert the block to TeX
+  block.toTeX.run ⟨options, traverseContext, traverseState⟩ |>.run extension_impls

src/tests/integration/sample-doc/expected/tex/main.tex

@@ -0,0 +1,59 @@
+
+\documentclass{memoir}
+
+\usepackage{sourcecodepro}
+\usepackage{sourcesanspro}
+\usepackage{sourceserifpro}
+
+\usepackage{fancyvrb}
+\usepackage{fvextra}
+
+
+\makechapterstyle{lean}{%
+\renewcommand*{\chaptitlefont}{\sffamily\HUGE}
+\renewcommand*{\chapnumfont}{\chaptitlefont}
+% allow for 99 chapters!
+\settowidth{\chapindent}{\chapnumfont 999}
+\renewcommand*{\printchaptername}{}
+\renewcommand*{\chapternamenum}{}
+\renewcommand*{\chapnumfont}{\chaptitlefont}
+\renewcommand*{\printchapternum}{%
+\noindent\llap{\makebox[\chapindent][l]{%
+\chapnumfont \thechapter}}}
+\renewcommand*{\afterchapternum}{}
+}
+
+\chapterstyle{lean}
+
+\setsecheadstyle{\sffamily\bfseries\Large}
+\setsubsecheadstyle{\sffamily\bfseries\large}
+\setsubsubsecheadstyle{\sffamily\bfseries}
+
+\renewcommand{\cftchapterfont}{\normalfont\sffamily}
+\renewcommand{\cftsectionfont}{\normalfont\sffamily}
+\renewcommand{\cftchapterpagefont}{\normalfont\sffamily}
+\renewcommand{\cftsectionpagefont}{\normalfont\sffamily}
+
+\title{\sffamily Title of the Doc}
+\author{\sffamily Harry Q. Bovik}
+\date{\sffamily }
+
+\begin{document}
+
+\frontmatter
+
+\begin{titlingpage}
+\maketitle
+\end{titlingpage}
+
+\tableofcontents
+
+\mainmatter
+
+\chapter*{Introduction}
+This is a docstring.Here's some more text with a \Verb|code inline|
+ in it.
+Here's when a \Verb|code inline|
+
+occurs right before a line break.And then here's a paragraph break.
+\end{document}