Skip to content

Commit 733e479

Browse files
david-christiansendavid-christiansen
authored
fix: bugs in TeX output (#717)
This PR fixes bugs found in PDF output for FPiL: * Internal links are now generated with \autoref instead of \href to the URL of the online version. * The message severity colors are harmonized with Lean, and no longer use red/green distinctions. * Trace messages are rendered. * Some placeholder toTeX implementations have been replaced by real implementations.
1 parent 9137d01 commit 733e479

File tree

19 files changed

+277
-62
lines changed

19 files changed

+277
-62
lines changed

‎lake-manifest.json‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@
2525
"type": "git",
2626
"subDir": null,
2727
"scope": "",
28-
"rev": "1e55697c44a646f8a22e2a91878efc4496aa5743",
28+
"rev": "4539e605ff834c35ecc0bcd0b7daec69163fd9f0",
2929
"name": "subverso",
3030
"manifestFile": "lake-manifest.json",
3131
"inputRev": "main",

‎src/tests/integration/code-content-doc/expected/tex/main.tex‎

Lines changed: 23 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -51,9 +51,9 @@
5151
% Work around missing U+2011 (non-breaking hyphen) in Source Serif Pro
5252
\newunicodechar{‑}{-}
5353

54-
\definecolor{errorColor}{HTML}{ff0000}
55-
\definecolor{infoColor}{HTML}{007f00}
56-
\definecolor{warningColor}{HTML}{0000ff}
54+
\definecolor{errorColor}{HTML}{B91C1C}
55+
\definecolor{infoColor}{HTML}{1E6BB8}
56+
\definecolor{warningColor}{HTML}{D97706}
5757
\newcommand{\errorDecorate}[1]{\coloredwave{errorColor}{#1}}
5858
\newcommand{\infoDecorate}[1]{\coloredwave{infoColor}{#1}}
5959
\newcommand{\warningDecorate}[1]{\coloredwave{warningColor}{#1}}
@@ -65,6 +65,26 @@
6565
\CustomVerbatimCommand{\FileListingVerb}{Verb}
6666
{commandchars=\\\{\},fontsize=\small,frame=single,framesep=2mm, numbers=left}
6767

68+
%%% Trace messages
69+
\newlength{\traceindent}
70+
\setlength{\traceindent}{1.5em}
71+
72+
\newcommand{\expandedIndicator}{$\blacktriangledown$\hspace{2pt}}
73+
\newcommand{\collapsedIndicator}{$\blacktriangleright$\hspace{2pt}}
74+
75+
\newenvironment{expandedtrace}[1]{%
76+
\par\noindent\expandedIndicator #1\par
77+
\advance\leftskip by \traceindent
78+
}{%
79+
}
80+
81+
\newenvironment{collapsedtrace}[1]{%
82+
\par\noindent\collapsedIndicator #1\par
83+
\advance\leftskip by \traceindent
84+
}{%
85+
}
86+
%%% End Trace messages
87+
6888
\definecolor{bordercolor}{HTML}{98B2C0}
6989
\definecolor{medgray}{HTML}{555555}
7090
\newtcolorbox{docstringBox}[2][]{colback=white,

‎src/tests/integration/extra-files-doc/expected/tex/main.tex‎

Lines changed: 24 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -51,9 +51,9 @@
5151
% Work around missing U+2011 (non-breaking hyphen) in Source Serif Pro
5252
\newunicodechar{‑}{-}
5353

54-
\definecolor{errorColor}{HTML}{ff0000}
55-
\definecolor{infoColor}{HTML}{007f00}
56-
\definecolor{warningColor}{HTML}{0000ff}
54+
\definecolor{errorColor}{HTML}{B91C1C}
55+
\definecolor{infoColor}{HTML}{1E6BB8}
56+
\definecolor{warningColor}{HTML}{D97706}
5757
\newcommand{\errorDecorate}[1]{\coloredwave{errorColor}{#1}}
5858
\newcommand{\infoDecorate}[1]{\coloredwave{infoColor}{#1}}
5959
\newcommand{\warningDecorate}[1]{\coloredwave{warningColor}{#1}}
@@ -65,6 +65,26 @@
6565
\CustomVerbatimCommand{\FileListingVerb}{Verb}
6666
{commandchars=\\\{\},fontsize=\small,frame=single,framesep=2mm, numbers=left}
6767

68+
%%% Trace messages
69+
\newlength{\traceindent}
70+
\setlength{\traceindent}{1.5em}
71+
72+
\newcommand{\expandedIndicator}{$\blacktriangledown$\hspace{2pt}}
73+
\newcommand{\collapsedIndicator}{$\blacktriangleright$\hspace{2pt}}
74+
75+
\newenvironment{expandedtrace}[1]{%
76+
\par\noindent\expandedIndicator #1\par
77+
\advance\leftskip by \traceindent
78+
}{%
79+
}
80+
81+
\newenvironment{collapsedtrace}[1]{%
82+
\par\noindent\collapsedIndicator #1\par
83+
\advance\leftskip by \traceindent
84+
}{%
85+
}
86+
%%% End Trace messages
87+
6888
\definecolor{bordercolor}{HTML}{98B2C0}
6989
\definecolor{medgray}{HTML}{555555}
7090
\newtcolorbox{docstringBox}[2][]{colback=white,
@@ -123,7 +143,7 @@
123143

124144

125145
\mainmatter
126-
\chapter{Testing Extra Files}
146+
\chapter{Testing Extra Files}\label{Extra--Files--Test--Document----Testing--Extra--Files}
127147

128148
This document tests the \LeanVerb|extraFiles|, \LeanVerb|extraFilesHtml|, and \LeanVerb|extraFilesTex| functionality.
129149

‎src/tests/integration/front-matter-doc/expected/tex/main.tex‎

Lines changed: 28 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -51,9 +51,9 @@
5151
% Work around missing U+2011 (non-breaking hyphen) in Source Serif Pro
5252
\newunicodechar{‑}{-}
5353

54-
\definecolor{errorColor}{HTML}{ff0000}
55-
\definecolor{infoColor}{HTML}{007f00}
56-
\definecolor{warningColor}{HTML}{0000ff}
54+
\definecolor{errorColor}{HTML}{B91C1C}
55+
\definecolor{infoColor}{HTML}{1E6BB8}
56+
\definecolor{warningColor}{HTML}{D97706}
5757
\newcommand{\errorDecorate}[1]{\coloredwave{errorColor}{#1}}
5858
\newcommand{\infoDecorate}[1]{\coloredwave{infoColor}{#1}}
5959
\newcommand{\warningDecorate}[1]{\coloredwave{warningColor}{#1}}
@@ -65,6 +65,26 @@
6565
\CustomVerbatimCommand{\FileListingVerb}{Verb}
6666
{commandchars=\\\{\},fontsize=\small,frame=single,framesep=2mm, numbers=left}
6767

68+
%%% Trace messages
69+
\newlength{\traceindent}
70+
\setlength{\traceindent}{1.5em}
71+
72+
\newcommand{\expandedIndicator}{$\blacktriangledown$\hspace{2pt}}
73+
\newcommand{\collapsedIndicator}{$\blacktriangleright$\hspace{2pt}}
74+
75+
\newenvironment{expandedtrace}[1]{%
76+
\par\noindent\expandedIndicator #1\par
77+
\advance\leftskip by \traceindent
78+
}{%
79+
}
80+
81+
\newenvironment{collapsedtrace}[1]{%
82+
\par\noindent\collapsedIndicator #1\par
83+
\advance\leftskip by \traceindent
84+
}{%
85+
}
86+
%%% End Trace messages
87+
6888
\definecolor{bordercolor}{HTML}{98B2C0}
6989
\definecolor{medgray}{HTML}{555555}
7090
\newtcolorbox{docstringBox}[2][]{colback=white,
@@ -124,7 +144,7 @@
124144
\cleardoublepage
125145
This is the introduction text that appears before any chapters.
126146
It should be part of the front matter.
127-
\chapter{Preface}
147+
\chapter{Preface}\label{preface}
128148

129149
This is an unnumbered preface section.
130150
It should appear in the front matter, before \LeanVerb|\symbol{92}mainmatter|.
@@ -134,15 +154,15 @@ \chapter{Preface}
134154

135155

136156
\mainmatter
137-
\chapter{Chapter One}
157+
\chapter{Chapter One}\label{ch1}
138158

139159
This is the first numbered chapter.
140160
It should appear after \LeanVerb|\symbol{92}mainmatter|.
141161

142162

143163

144164

145-
\chapter{Chapter Two}
165+
\chapter{Chapter Two}\label{ch2}
146166

147167
This is the second numbered chapter.
148168
It should also appear after \LeanVerb|\symbol{92}mainmatter|.
@@ -152,15 +172,15 @@ \chapter{Chapter Two}
152172

153173

154174
\backmatter
155-
\chapter{Acknowledgments}
175+
\chapter{Acknowledgments}\label{ack}
156176

157177
This is an unnumbered acknowledgments section at the end.
158178
It should appear in the back matter, after \LeanVerb|\symbol{92}backmatter|.
159179

160180

161181

162182

163-
\chapter{Index}
183+
\chapter{Index}\label{index}
164184

165185
This is an unnumbered index section.
166186
It should also appear in the back matter.

‎src/tests/integration/inheritance-doc/expected/tex/main.tex‎

Lines changed: 23 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -51,9 +51,9 @@
5151
% Work around missing U+2011 (non-breaking hyphen) in Source Serif Pro
5252
\newunicodechar{‑}{-}
5353

54-
\definecolor{errorColor}{HTML}{ff0000}
55-
\definecolor{infoColor}{HTML}{007f00}
56-
\definecolor{warningColor}{HTML}{0000ff}
54+
\definecolor{errorColor}{HTML}{B91C1C}
55+
\definecolor{infoColor}{HTML}{1E6BB8}
56+
\definecolor{warningColor}{HTML}{D97706}
5757
\newcommand{\errorDecorate}[1]{\coloredwave{errorColor}{#1}}
5858
\newcommand{\infoDecorate}[1]{\coloredwave{infoColor}{#1}}
5959
\newcommand{\warningDecorate}[1]{\coloredwave{warningColor}{#1}}
@@ -65,6 +65,26 @@
6565
\CustomVerbatimCommand{\FileListingVerb}{Verb}
6666
{commandchars=\\\{\},fontsize=\small,frame=single,framesep=2mm, numbers=left}
6767

68+
%%% Trace messages
69+
\newlength{\traceindent}
70+
\setlength{\traceindent}{1.5em}
71+
72+
\newcommand{\expandedIndicator}{$\blacktriangledown$\hspace{2pt}}
73+
\newcommand{\collapsedIndicator}{$\blacktriangleright$\hspace{2pt}}
74+
75+
\newenvironment{expandedtrace}[1]{%
76+
\par\noindent\expandedIndicator #1\par
77+
\advance\leftskip by \traceindent
78+
}{%
79+
}
80+
81+
\newenvironment{collapsedtrace}[1]{%
82+
\par\noindent\collapsedIndicator #1\par
83+
\advance\leftskip by \traceindent
84+
}{%
85+
}
86+
%%% End Trace messages
87+
6888
\definecolor{bordercolor}{HTML}{98B2C0}
6989
\definecolor{medgray}{HTML}{555555}
7090
\newtcolorbox{docstringBox}[2][]{colback=white,

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

Lines changed: 23 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -51,9 +51,9 @@
5151
% Work around missing U+2011 (non-breaking hyphen) in Source Serif Pro
5252
\newunicodechar{‑}{-}
5353

54-
\definecolor{errorColor}{HTML}{ff0000}
55-
\definecolor{infoColor}{HTML}{007f00}
56-
\definecolor{warningColor}{HTML}{0000ff}
54+
\definecolor{errorColor}{HTML}{B91C1C}
55+
\definecolor{infoColor}{HTML}{1E6BB8}
56+
\definecolor{warningColor}{HTML}{D97706}
5757
\newcommand{\errorDecorate}[1]{\coloredwave{errorColor}{#1}}
5858
\newcommand{\infoDecorate}[1]{\coloredwave{infoColor}{#1}}
5959
\newcommand{\warningDecorate}[1]{\coloredwave{warningColor}{#1}}
@@ -65,6 +65,26 @@
6565
\CustomVerbatimCommand{\FileListingVerb}{Verb}
6666
{commandchars=\\\{\},fontsize=\small,frame=single,framesep=2mm, numbers=left}
6767

68+
%%% Trace messages
69+
\newlength{\traceindent}
70+
\setlength{\traceindent}{1.5em}
71+
72+
\newcommand{\expandedIndicator}{$\blacktriangledown$\hspace{2pt}}
73+
\newcommand{\collapsedIndicator}{$\blacktriangleright$\hspace{2pt}}
74+
75+
\newenvironment{expandedtrace}[1]{%
76+
\par\noindent\expandedIndicator #1\par
77+
\advance\leftskip by \traceindent
78+
}{%
79+
}
80+
81+
\newenvironment{collapsedtrace}[1]{%
82+
\par\noindent\collapsedIndicator #1\par
83+
\advance\leftskip by \traceindent
84+
}{%
85+
}
86+
%%% End Trace messages
87+
6888
\definecolor{bordercolor}{HTML}{98B2C0}
6989
\definecolor{medgray}{HTML}{555555}
7090
\newtcolorbox{docstringBox}[2][]{colback=white,

‎src/verso-manual/VersoManual.lean‎

Lines changed: 18 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -69,13 +69,13 @@ private structure RefInfo where
6969
canonicalName : String
7070
domain : Option Name
7171
remote : Option String
72-
resolvedDestination : Option String := none
72+
resolvedDestination : Option Link := none
7373
deriving BEq, ToJson, FromJson
7474

7575
defmethod Part.htmlToc (part : Part Manual) : Bool :=
7676
part.metadata.map (·.htmlToc) |>.getD true
7777

78-
inline_extension Inline.ref (canonicalName : String) (domain : Option Name) (remote : Option String) (resolvedDestination : Option String := none) where
78+
inline_extension Inline.ref (canonicalName : String) (domain : Option Name) (remote : Option String) (resolvedDestination : Option Link := none) where
7979
data := ToJson.toJson (RefInfo.mk canonicalName domain remote resolvedDestination)
8080
traverse := fun _ info content => do
8181
match FromJson.fromJson? (α := RefInfo) info with
@@ -86,7 +86,7 @@ inline_extension Inline.ref (canonicalName : String) (domain : Option Name) (rem
8686
match (← get).resolveDomainObject domain name with
8787
| .error _ => return none
8888
| .ok dest =>
89-
return some <| .other (Inline.ref name (some domain) none (some dest.link)) content
89+
return some <| .other (Inline.ref name (some domain) none (some dest)) content
9090
| .ok { canonicalName := name, domain := none, remote := some remote, resolvedDestination := none } =>
9191
return some <| .other (Inline.ref name (some sectionDomain) (some remote) none) content
9292
| .ok { resolvedDestination := some _, .. } | .ok { remote := some _, .. } =>
@@ -102,8 +102,15 @@ inline_extension Inline.ref (canonicalName : String) (domain : Option Name) (rem
102102
TeX.logError ("No destination found for tag '" ++ name ++ "' in " ++ toString domain); content.mapM go
103103
| .ok { canonicalName := name, domain, remote := some remote, resolvedDestination := none } =>
104104
TeX.logError ("No destination found for remote '" ++ remote ++ "' tag '" ++ name ++ "' in " ++ toString domain); content.mapM go
105-
| .ok {resolvedDestination := some dest, ..} =>
106-
pure <| makeLink dest (← content.mapM go)
105+
| .ok {resolvedDestination := some dest, remote, ..} =>
106+
if remote.isSome then
107+
-- Inter-document links should be URLs
108+
pure <| makeLink dest.link (← content.mapM go)
109+
else
110+
-- Intra-document links should be page references
111+
let label := labelForTeX dest.htmlId
112+
pure \TeX{\autoref{\Lean{label}}" (p."~\pageref{\Lean{label}} ")"}
113+
107114
toHtml :=
108115
open Verso.Output.Html in
109116
some <| fun go _ info content => do
@@ -131,7 +138,7 @@ inline_extension Inline.ref (canonicalName : String) (domain : Option Name) (rem
131138
-- If any error was logged, just don't emit a link
132139
content.mapM go
133140
| .ok {resolvedDestination := some dest, ..} =>
134-
pure {{<a href={{dest}}>{{← content.mapM go}}</a>}}
141+
pure {{<a href={{dest.link}}>{{← content.mapM go}}</a>}}
135142

136143
section
137144
open Lean
@@ -361,9 +368,11 @@ def emitTeX (logError : String → IO Unit) (config : Config) (text : Part Manua
361368
let texCtxt := {}
362369
let { frontMatter := (frontText, frontParts), mainMatter, backMatter } := DividedDoc.ofPart text
363370
let frontMatter := (← frontText.mapM (·.toTeX (opts, ctxt, state, texCtxt)))
364-
let frontMatter := frontMatter ++ (← frontParts.mapM (·.toTeX (opts, ctxt, state, texCtxt)))
365-
let chapters ← mainMatter.mapM (·.toTeX (opts, ctxt, state, texCtxt))
366-
let appendices ← backMatter.mapM (·.toTeX (opts, ctxt, state, texCtxt))
371+
-- Passing `none` as the label is fine here because traversal has assigned labels already so
372+
-- there's no need for a fallback.
373+
let frontMatter := frontMatter ++ (← frontParts.mapM (·.toTeX none (opts, ctxt, state, texCtxt)))
374+
let chapters ← mainMatter.mapM (·.toTeX none (opts, ctxt, state, texCtxt))
375+
let appendices ← backMatter.mapM (·.toTeX none (opts, ctxt, state, texCtxt))
367376
let dir := config.destination.join "tex"
368377
ensureDir dir
369378
let mut packages : Std.HashSet String := {}

‎src/verso-manual/VersoManual/Basic.lean‎

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1430,7 +1430,13 @@ instance : Traverse Manual TraverseM where
14301430

14311431
open Verso.Output.TeX in
14321432
instance : TeX.GenreTeX Manual (ReaderT ExtensionImpls IO) where
1433-
part go _meta txt := go txt
1433+
part go metadata txt := do
1434+
let st ← TeX.state
1435+
let label? := do
1436+
let id ← metadata.id
1437+
let link ← st.externalTags[id]?
1438+
pure <| labelForTeX link.htmlId
1439+
go txt label?
14341440
block goI goB b content := do
14351441
let some id := b.id
14361442
| panic! s!"Block {b.name} wasn't assigned an ID during traversal"

‎src/verso-manual/VersoManual/ExternalLean.lean‎

Lines changed: 12 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -182,9 +182,17 @@ inline_extension Inline.leanOutput
182182
traverse _ _ _ := do
183183
pure none
184184
toTeX :=
185-
some <| fun go _ _ content => do
186-
pure <| .seq <| ← content.mapM fun b => do
187-
pure <| .seq #[← go b, .raw "\n"]
185+
open Verso.Output.TeX in
186+
some <| fun _ _ data _ => do
187+
match FromJson.fromJson? data with
188+
| .error err =>
189+
TeX.logError <| "Couldn't deserialize Lean code while rendering TeX: " ++ err
190+
pure .empty
191+
| .ok ((txt, plain, expandTraces) : Highlighted.Message × Bool × List Name) =>
192+
if plain then
193+
txt.toTeXInlinePlain expandTraces
194+
else
195+
txt.toTeX expandTraces
188196
toHtml :=
189197
open Verso.Output.Html in
190198
some <| fun _ _ data _ => do
@@ -193,8 +201,7 @@ inline_extension Inline.leanOutput
193201
HtmlT.logError <| "Couldn't deserialize Lean code while rendering HTML: " ++ err
194202
pure .empty
195203
| .ok ((txt, plain, expandTraces) : Highlighted.Message × Bool × List Name) =>
196-
let plainHtml := {{<code>{{txt.toString}}</code>}}
197-
if plain then pure plainHtml
204+
if plain then pure {{<code>{{txt.toString}}</code>}}
198205
else txt.toHtml expandTraces (g := Manual)
199206

200207
open Verso.Code.External

‎src/verso-manual/VersoManual/InlineLean.lean‎

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -578,9 +578,14 @@ block_extension Block.leanOutput via withHighlighting where
578578
traverse _ _ _ := do
579579
pure none
580580
toTeX :=
581-
some <| fun _ go _ _ content => do
582-
pure <| .seq <| ← content.mapM fun b => do
583-
pure <| .seq #[← go b, .raw "\n"]
581+
open Verso.Output.Html in
582+
some <| fun _ _ _ data _ => do
583+
match FromJson.fromJson? data with
584+
| .error err =>
585+
TeX.logError <| "Couldn't deserialize Lean output while rendering TeX: " ++ err ++ "\n" ++ toString data
586+
pure .empty
587+
| .ok ((msg, _summarize, expandTraces) : Highlighted.Message × Bool × List Name) =>
588+
msg.toTeX (expandTraces := expandTraces) (g := Manual)
584589
toHtml :=
585590
open Verso.Output.Html in
586591
some <| fun _ _ _ data _ => do

0 commit comments

Comments
 (0)