feat: TeX math

doc/UsersGuide/Markup.lean

@@ -33,8 +33,14 @@ Like Markdown, Lean's markup has three primary syntactic categories:
 
 ## Description
 
+TODO build an extension to test the parsing here
+
 ### Inline Syntax
 
+
+
+TeX math can be included using a single or double dollar sign followed by code. Two dollar signs results in display-mode math, so `` $`\sum_{i=0}^{10} i` `` results in $`\sum_{i=0}^{10} i` while `` $$`\sum_{i=0}^{10} i` `` results in: $$`\sum_{i=0}^{10} i`
+
 ### Block Syntax
 
 ### Document Structure

src/leanblog/LeanDoc/Genre/Blog/Basic.lean

@@ -278,14 +278,27 @@ def highlightingJs : String :=
 }
 "
 
+def renderMathJs : String :=
+"document.addEventListener(\"DOMContentLoaded\", () => {
+    for (const m of document.querySelectorAll(\".math.inline\")) {
+        katex.render(m.textContent, m, {throwOnError: false, displayMode: false});
+    }
+    for (const m of document.querySelectorAll(\".math.display\")) {
+        katex.render(m.textContent, m, {throwOnError: false, displayMode: true});
+    }
+});"
+
 instance : Traverse Blog Blog.TraverseM where
   part _ := pure ()
   block _ := pure ()
   inline _ := pure ()
   genrePart _ _ := pure none
   genreBlock
     | .highlightedCode .., _contents => do
-      modify fun st => {st with stylesheets := st.stylesheets.insert highlightingStyle, scripts := st.scripts.insert highlightingJs}
+      modify fun st => {st with
+        stylesheets := st.stylesheets.insert highlightingStyle,
+        scripts := st.scripts.insert highlightingJs
+      }
       pure none
     | _, _ => pure none
   genreInline

src/leanblog/LeanDoc/Genre/Blog/Generate.lean

@@ -25,7 +25,7 @@ def Generate.Context.templateContext (ctxt : Generate.Context) (params : Templat
   params := params
   path := ctxt.ctxt.path
   builtInStyles := ctxt.xref.stylesheets
-  builtInScripts := ctxt.xref.scripts
+  builtInScripts := ctxt.xref.scripts.insert Traverse.renderMathJs
 
 abbrev GenerateM := ReaderT Generate.Context IO
 

src/leanblog/LeanDoc/Genre/Blog/Template.lean

@@ -205,6 +205,11 @@ def builtinHeader : TemplateM Html := do
     out := out ++ {{<style>"\n"{{.text false style}}"\n"</style>"\n"}}
   for script in (← read).builtInScripts do
     out := out ++ {{<script>"\n"{{.text false script}}"\n"</script>"\n"}}
+  out := out ++ {{
+    <link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/[email protected]/dist/katex.min.css" integrity="sha384-n8MVd4RsNIU0tAv4ct0nTaAbDJwPJzDEaqSD1odI+WdtXRGWt2kTvGFasHpSy3SV" crossorigin="anonymous"/>
+    <script defer="defer" src="https://cdn.jsdelivr.net/npm/[email protected]/dist/katex.min.js" integrity="sha384-XjKyOOlGwcjNTAIQHIpgOno0Hl1YQqzUOEleOLALmuqehneUG+vnGctmUb0ZY0l8" crossorigin="anonymous"></script>
+  }}
+
   pure out
 
 namespace Params

src/leandoc/LeanDoc/Doc.lean

@@ -41,12 +41,16 @@ instance : Repr Genre.none.Inline where
 instance : Repr Genre.none.PartMetadata where
   reprPrec e _ := nomatch e
 
+inductive MathMode where | inline | display
+deriving Repr, BEq
 
 inductive Inline (genre : Genre) : Type where
   | text (string : String)
   | emph (content : Array (Inline genre))
   | bold (content : Array (Inline genre))
   | code (string : String)
+  /-- Embedded blobs of TeX math -/
+  | math (mode : MathMode) (string : String)
   | linebreak (string : String)
   | link (content : Array (Inline genre)) (url : String)
   | footnote (name : String) (content : Array (Inline genre))
@@ -75,6 +79,7 @@ partial def Inline.reprPrec [Repr g.Inline] (inline : Inline g) (prec : Nat) : S
         | .emph content => reprCtor ``Inline.emph [reprArray go content]
         | .bold content => reprCtor ``Inline.bold [reprArray go content]
         | .code str => reprCtor ``Inline.code [reprArg str]
+        | .math mode str => reprCtor ``Inline.math [reprArg mode, reprArg str]
         | .linebreak str => reprCtor ``Inline.linebreak [reprArg str]
         | .link content dest => reprCtor ``Inline.link [
             reprArray go content,
@@ -207,7 +212,7 @@ where
       match ← Traverse.genreInline container content with
       | .none => .other container <$> content.mapM inline
       | .some i' => inline i'
-    | .text .. | .linebreak .. | .code .. => pure i
+    | .text .. | .linebreak .. | .code .. | .math .. => pure i
 
   block (b : Doc.Block g) : m (Doc.Block g) := do
     Traverse.block b

src/leandoc/LeanDoc/Doc/Elab.lean

@@ -153,6 +153,20 @@ def _root_.LeanDoc.Syntax.code.expand : InlineExpander
     ``(Inline.code $s)
   | _ => throwUnsupportedSyntax
 
+
+@[inline_expander LeanDoc.Syntax.inline_math]
+def _root_.LeanDoc.Syntax.inline_math.expand : InlineExpander
+  |  `(inline| ${ code{ $s } }) =>
+    ``(Inline.math MathMode.inline $s)
+  | _ => throwUnsupportedSyntax
+
+@[inline_expander LeanDoc.Syntax.display_math]
+def _root_.LeanDoc.Syntax.display_math.expand : InlineExpander
+  |  `(inline| $${ code{ $s } }) =>
+    ``(Inline.math MathMode.display $s)
+  | _ => throwUnsupportedSyntax
+
+
 def elabBlock (block : Syntax) : DocElabM (TSyntax `term) :=
   withRef block <| withFreshMacroScope <| withIncRecDepth <| do
   match block with

src/leandoc/LeanDoc/Doc/Html.lean

@@ -82,6 +82,9 @@ partial def Inline.toHtml [Monad m] [GenreHtml g m] : Inline g → HtmlT g m Htm
   | .bold content => do
     pure {{ <strong> {{← content.mapM toHtml}} </strong> }}
   | .code str => pure {{ <code> {{str}} </code> }}
+  | .math mode str => do
+     let classes := "math " ++ match mode with | .inline => "inline" | .display => "display"
+     pure {{ <code class={{classes}}>{{str}}</code> }}
   | .concat inlines => inlines.mapM toHtml
   | .other container content => GenreHtml.inline Inline.toHtml container content
 

src/leandoc/LeanDoc/Doc/TeX.lean

@@ -28,7 +28,7 @@ def logError [Monad m] (message : String) : TeXT g m Unit := do
 def header [Monad m] (name : TeX) : TeXT g m TeX := do
   let opts ← options
   let some i := opts.headerLevel
-    | logError "No more header nesting available"; return \TeX{\textbf{\Lean{name}}}
+    | logError s!"No more header nesting available at {name.asString}"; return \TeX{\textbf{\Lean{name}}}
   let header := opts.headerLevels[i]
   pure <| .raw (s!"\\{header}" ++ "{") ++ name ++ .raw "}"
 
@@ -62,6 +62,8 @@ partial defmethod Inline.toTeX [Monad m] [GenreTeX g m] : Inline g → TeXT g m
     pure \TeX{\textbf{\Lean{← content.mapM toTeX}}}
   | .code str => do
     pure \TeX{s!"\\verb|{str}|"} --- TODO choose delimiter automatically
+  | .math .inline str => pure <| .raw s!"${str}$"
+  | .math .display str => pure <| .raw s!"\\[{str}\\]"
   | .concat inlines => inlines.mapM toTeX
   | .other container content => GenreTeX.inline Inline.toTeX container content
 

src/leandoc/LeanDoc/Output/Html.lean

@@ -145,7 +145,11 @@ partial def asString : Html → String
   | .text true str => str.replace "<" "&lt;" |>.replace ">" "&gt;"
   | .text false str => str
   | .tag name attrs (.seq #[]) =>
-    "<" ++ name ++ attrsAsString attrs ++ "/>"
+    -- TODO make this more elegant
+    if name == "script" then
+      "<" ++ name ++ attrsAsString attrs ++ "></script>"
+    else
+      "<" ++ name ++ attrsAsString attrs ++ "/>"
   | .tag name attrs (.seq #[subElem]) =>
     "<" ++ name ++ attrsAsString attrs ++ ">" ++ asString subElem ++ s!"</{name}>"
   | .tag "pre" attrs body =>

src/leandoc/LeanDoc/Parser.lean

@@ -304,6 +304,11 @@ Remaining:
 #guard_msgs in
 #eval nl.test! "\n "
 
+def fakeAtom (str : String) : ParserFn := fun _c s =>
+  let atom := mkAtom SourceInfo.none str
+  s.pushSyntax atom
+
+
 def strFn (str : String) : ParserFn := asStringFn <| fun c s =>
   let rec go (iter : String.Iterator) (s : ParserState) :=
     if iter.atEnd then s
@@ -396,6 +401,22 @@ def inlineTextChar : ParserFn := fun c s =>
       else if c.input.get' i' h == '['
       then s.mkUnexpectedErrorAt "![" i
       else s
+    | '$' =>
+      let s := s.next' c.input i h
+      let i' := s.pos
+      if h : c.input.atEnd i' then
+        s
+      else if c.input.get' i' h == '`' then
+        s.mkUnexpectedErrorAt "$`" i
+      else if c.input.get' i' h == '$' then
+        let s := s.next' c.input i' h
+        let i' := s.pos
+        if h : c.input.atEnd i' then
+          s
+        else if c.input.get' i' h == '`' then
+          s.mkUnexpectedErrorAt "$$`" i
+        else s
+      else s
     | _ => s.next' c.input i h
 
 /-- Return some inline text up to the next inline opener or the end of
@@ -820,6 +841,9 @@ mutual
         else if ch == '\n' then s.mkUnexpectedError "newline"
         else takeContentsFn maxCount c (s.next' c.input i h)
 
+  partial def math : ParserFn :=
+    atomicFn (nodeFn ``display_math <| strFn "$$" >> code >> fakeAtom "`") <|>
+    atomicFn (nodeFn ``inline_math <| strFn "$" >> code >> fakeAtom "`")
 
   -- Read a prefix of a line of text, stopping at a text-mode special character
   partial def text :=
@@ -873,7 +897,7 @@ mutual
       s.pushSyntax fakeClose
 
 
-  partial def delimitedInline (ctxt : InlineCtxt) : ParserFn := emph ctxt <|> bold ctxt <|> code <|> role ctxt <|> image <|> link ctxt <|> footnote ctxt
+  partial def delimitedInline (ctxt : InlineCtxt) : ParserFn := emph ctxt <|> bold ctxt <|> code <|> math <|> role ctxt <|> image <|> link ctxt <|> footnote ctxt
 
   partial def inline (ctxt : InlineCtxt) : ParserFn :=
     text <|> linebreak ctxt <|> delimitedInline ctxt
@@ -1215,6 +1239,60 @@ All input consumed.
 #guard_msgs in
 #eval inline {} |>.test! "[^1]"
 
+/--
+info: Success! Final stack:
+  (LeanDoc.Syntax.inline_math
+   "$"
+   (LeanDoc.Syntax.code
+    "`"
+    (str "\"\\\\frac{x}{4}\"")
+    "`")
+   "`")
+All input consumed.
+-/
+#guard_msgs in
+#eval inline {} |>.test! "$`\\frac{x}{4}`"
+
+/--
+info: Success! Final stack:
+  (LeanDoc.Syntax.display_math
+   "$$"
+   (LeanDoc.Syntax.code
+    "`"
+    (str "\"\\\\frac{x}{4}\"")
+    "`")
+   "`")
+All input consumed.
+-/
+#guard_msgs in
+#eval inline {} |>.test! "$$`\\frac{x}{4}`"
+
+/--
+info: Success! Final stack:
+  (LeanDoc.Syntax.text (str "\"$35.23\""))
+All input consumed.
+-/
+#guard_msgs in
+#eval inline {} |>.test! "$35.23"
+
+/--
+info: Success! Final stack:
+  (LeanDoc.Syntax.text (str "\"$\""))
+Remaining:
+"`code`"
+-/
+#guard_msgs in
+#eval inline {} |>.test! "\\$`code`"
+
+/--
+info: Success! Final stack:
+  (LeanDoc.Syntax.text (str "\"$$$\""))
+All input consumed.
+-/
+#guard_msgs in
+#eval inline {} |>.test! "$$$"
+
+
 structure InList where
   indentation : Nat
   type : OrderedListType ⊕ UnorderedListType
@@ -1226,10 +1304,6 @@ structure BlockCtxt where
   inLists : List InList := []
 deriving Inhabited, Repr
 
-def fakeAtom (str : String) : ParserFn := fun _c s =>
-  let atom := mkAtom SourceInfo.none str
-  s.pushSyntax atom
-
 def lookaheadOrderedListIndicator (ctxt : BlockCtxt) (p : OrderedListType → Int → ParserFn) : ParserFn := fun c s =>
     let iniPos := s.pos
     let iniSz := s.stxStack.size
@@ -1772,7 +1846,7 @@ All input consumed.
   #eval blocks {} |>.test! "* foo\n  * bar\n* more outer"
 
 /--
-info: Failure: unexpected end of input; expected ![, [, [^ or expected beginning of line at ⟨2, 15⟩
+info: Failure: unexpected end of input; expected ![, $, $$, [, [^ or expected beginning of line at ⟨2, 15⟩
 Final stack:
   [(LeanDoc.Syntax.dl
     [(LeanDoc.Syntax.desc

src/leandoc/LeanDoc/Syntax.lean

@@ -38,6 +38,8 @@ syntax (name:=linebreak) "line!" : inline
 /-- Literal characters-/
 syntax (name:=code) "code{" str "}" : inline
 syntax (name:=role) "role{" ident argument* "}" "[" inline "]"  : inline
+syntax (name:=inline_math) "${" inline "}" : inline
+syntax (name:=display_math) "$${" inline "}" : inline
 
 declare_syntax_cat list_item
 /-- List item -/

src/manual/LeanDoc/Genre/Manual.lean

@@ -60,12 +60,16 @@ def ensureDir (dir : System.FilePath) : IO Unit := do
 open IO.FS in
 def emitTeX (logError : String → IO Unit) (config : Config) (text : Part Manual) : IO Unit := do
   let opts : TeX.Options Manual IO := {headerLevels := #["chapter", "section", "subsection", "subsubsection", "paragraph"], headerLevel := some ⟨0, by simp_arith [Array.size, List.length]⟩, logError := logError}
-  let rendered ← text.toTeX (opts, (), ())
+  let frontMatter ← text.content.mapM (·.toTeX (opts, (), ()))
+  let chapters ← text.subParts.mapM (·.toTeX (opts, (), ()))
   let dir := config.destination.join "tex"
   ensureDir dir
   withFile (dir.join "main.tex") .write fun h => do
     h.putStrLn (preamble text.titleString ["author 1", "author 2"])
-    h.putStrLn rendered.asString
+    for b in frontMatter do
+      h.putStrLn b.asString
+    for c in chapters do
+      h.putStrLn c.asString
     h.putStrLn postamble
 
 def manualMain (text : Part Manual) (options : List String) : IO UInt32 := do