From d567828ea33db3a9cc5ffa4a3b6b16d4eb468306 Mon Sep 17 00:00:00 2001 From: Jason Reed Date: Tue, 30 Sep 2025 17:16:34 -0400 Subject: [PATCH 1/4] Add TeX integration test --- .gitignore | 2 +- src/tests/TestMain.lean | 31 ++++++- src/tests/Tests.lean | 2 + src/tests/Tests/Integration.lean | 90 +++++++++++++++++++ src/tests/Tests/Integration/SampleDoc.lean | 37 ++++++++ .../sample-doc/expected/tex/main.tex | 59 ++++++++++++ 6 files changed, 219 insertions(+), 2 deletions(-) create mode 100644 src/tests/Tests/Integration.lean create mode 100644 src/tests/Tests/Integration/SampleDoc.lean create mode 100644 src/tests/integration/sample-doc/expected/tex/main.tex diff --git a/.gitignore b/.gitignore index 98d45bb4c..6cf6e1144 100644 --- a/.gitignore +++ b/.gitignore @@ -7,4 +7,4 @@ _out *.olean /.verso/ -/src/tests/parser/*/*.output +/src/tests/integration/**/output diff --git a/src/tests/TestMain.lean b/src/tests/TestMain.lean index 86056bf61..cbeb34a71 100644 --- a/src/tests/TestMain.lean +++ b/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,35 @@ 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. +`doc` is the document itself. +-/ +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 Lean.Parser in +open Verso.Parser in +open Verso.Integration in def tests := [ - testStemmer + testStemmer, + testTexOutput "sample-doc" SampleDoc.doc ] def getConfig (config : Config) : List String → IO Config diff --git a/src/tests/Tests.lean b/src/tests/Tests.lean index 406cd6bf7..1309a65dd 100644 --- a/src/tests/Tests.lean +++ b/src/tests/Tests.lean @@ -4,4 +4,6 @@ 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 diff --git a/src/tests/Tests/Integration.lean b/src/tests/Tests/Integration.lean new file mode 100644 index 000000000..2e77d0457 --- /dev/null +++ b/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 diff --git a/src/tests/Tests/Integration/SampleDoc.lean b/src/tests/Tests/Integration/SampleDoc.lean new file mode 100644 index 000000000..101a69df5 --- /dev/null +++ b/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 diff --git a/src/tests/integration/sample-doc/expected/tex/main.tex b/src/tests/integration/sample-doc/expected/tex/main.tex new file mode 100644 index 000000000..2a930fc73 --- /dev/null +++ b/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} From 21c7167e67a8fcecbc978f857c266d1f8b13afce Mon Sep 17 00:00:00 2001 From: Jason Reed Date: Wed, 1 Oct 2025 09:39:31 -0400 Subject: [PATCH 2/4] Slightly better docstring --- src/tests/TestMain.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/tests/TestMain.lean b/src/tests/TestMain.lean index cbeb34a71..f09c90825 100644 --- a/src/tests/TestMain.lean +++ b/src/tests/TestMain.lean @@ -32,8 +32,9 @@ def testStemmer (_ : Config) : IO Unit := do throw <| IO.userError "Stemmer tests failed" /-- -Tests manual-genre TeX generation. `dir` is a subdirectory specific to a particular test document. -`doc` is the document itself. +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 => From e721099d92a74e95d09ca53833b0749b15201737 Mon Sep 17 00:00:00 2001 From: Jason Reed Date: Wed, 1 Oct 2025 09:39:58 -0400 Subject: [PATCH 3/4] Remove unnecessary opens --- src/tests/TestMain.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/tests/TestMain.lean b/src/tests/TestMain.lean index f09c90825..eb1f90e4c 100644 --- a/src/tests/TestMain.lean +++ b/src/tests/TestMain.lean @@ -55,8 +55,6 @@ def testTexOutput (dir : System.FilePath) (doc : Verso.Doc.Part Verso.Genre.Manu runTest } -open Lean.Parser in -open Verso.Parser in open Verso.Integration in def tests := [ testStemmer, From 35955a7b38d195f1d635b314beb1d5628d6d4bc6 Mon Sep 17 00:00:00 2001 From: Jason Reed Date: Thu, 2 Oct 2025 16:54:15 -0400 Subject: [PATCH 4/4] Add a couple of unit tests also --- src/tests/Tests.lean | 1 + src/tests/Tests/TexUnit.lean | 39 ++++++++++++++++++++++++++++++++ src/tests/Tests/TexUtil.lean | 43 ++++++++++++++++++++++++++++++++++++ 3 files changed, 83 insertions(+) create mode 100644 src/tests/Tests/TexUnit.lean create mode 100644 src/tests/Tests/TexUtil.lean diff --git a/src/tests/Tests.lean b/src/tests/Tests.lean index 1309a65dd..ca68f8459 100644 --- a/src/tests/Tests.lean +++ b/src/tests/Tests.lean @@ -7,3 +7,4 @@ import Tests.Golden import Tests.Integration import Tests.Integration.SampleDoc import Tests.ParserRegression +import Tests.TexUnit diff --git a/src/tests/Tests/TexUnit.lean b/src/tests/Tests/TexUnit.lean new file mode 100644 index 000000000..234405b8e --- /dev/null +++ b/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 diff --git a/src/tests/Tests/TexUtil.lean b/src/tests/Tests/TexUtil.lean new file mode 100644 index 000000000..69c41259e --- /dev/null +++ b/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