feat: metadata blocks

There is now an analogue of YAML metadata blocks in Pandoc, used in
the manual genre for authorship and in the blog genre for authorship
and dates.

doc/UsersGuide/Basic.lean

@@ -5,7 +5,11 @@ open LeanDoc.Genre Manual
 
 set_option pp.rawOnError true
 
-#doc (Manual) "Documentation in Lean" =>
+#doc (Manual) "Writing Documentation in Lean" =>
+
+%%%
+authors := ["David Thrane Christiansen"]
+%%%
 
 Documentation can take many forms:
 

generate.sh

@@ -0,0 +1,14 @@
+#!/bin/bash
+
+echo "Building the user's guide as TeX"
+lake exe usersguide
+
+echo "Building the user's guide as PDF"
+pushd _out/tex
+lualatex main
+lualatex main
+lualatex main
+popd
+
+echo "User's guide PDF is at:"
+readlink -f _out/tex/main.pdf

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

@@ -73,35 +73,82 @@ structure TraverseContext where
   path : List String := {}
   config : Config
 
-end Blog
-
 
 deriving instance Ord for List -- TODO - upstream?
 
-structure Blog.TraverseState where
+structure TraverseState where
   usedIds : Lean.RBMap (List String) (Lean.HashSet String) compare := {}
   targets : Lean.NameMap Blog.Info.Target := {}
   refs : Lean.NameMap Blog.Info.Ref := {}
   pageIds : Lean.NameMap (List String) := {}
   scripts : Lean.HashSet String := {}
   stylesheets : Lean.HashSet String := {}
+  errors : Lean.HashSet String := {}
 
 
-def Blog : Genre where
+def Page : Genre where
   PartMetadata := Empty
   Block := Blog.BlockExt
   Inline := Blog.InlineExt
   TraverseContext := Blog.TraverseContext
   TraverseState := Blog.TraverseState
 
-namespace Blog
-
-structure Post where
-  date : Date
+structure Post.Meta where
+  date : Blog.Date
   authors : List String
-  content : Part Blog
-  draft : Bool
-deriving TypeName, Inhabited
+  draft : Bool := false
+deriving TypeName
+
+def Post : Genre where
+  PartMetadata := Post.Meta
+  Block := Blog.BlockExt
+  Inline := Blog.InlineExt
+  TraverseContext := Blog.TraverseContext
+  TraverseState := Blog.TraverseState
+
+instance : TypeName Post.PartMetadata := inferInstanceAs (TypeName Post.Meta)
+
+structure BlogPost where
+  id : Name
+  contents : Part Post
+deriving TypeName
+
+class BlogGenre (genre : Genre) where
+  traverseContextEq : genre.TraverseContext = Blog.TraverseContext := by rfl
+  traverseStateEq : genre.TraverseState = Blog.TraverseState := by rfl
+
+instance : BlogGenre Post where
+
+instance : BlogGenre Page where
+
+
+defmethod Part.postName [Monad m] [MonadConfig m] [MonadState TraverseState m]
+    (post : Part Post) : m String := do
+  let date ←
+    match post.metadata with
+    | none =>
+      modify fun st => { st with errors := st.errors.insert s!"Missing metadata block in post \"{post.titleString}\""}
+      pure {year := 1900, month := 1, day := 1}
+    | some ⟨date, _authors, _draft⟩ =>
+      pure date
+  pure <| (← currentConfig).postName date post.titleString
+
+defmethod Part.postName' [Monad m] [MonadConfig m]
+    (post : Part Post) : m String := do
+  let date : Date :=
+    match post.metadata with
+    | none =>
+      {year := 1900, month := 1, day := 1}
+    | some ⟨date, _authors, _draft⟩ =>
+      date
+  pure <| (← currentConfig).postName date post.titleString
+
+defmethod BlogPost.postName [Monad m] [MonadConfig m] [MonadState TraverseState m]
+    (post : BlogPost) : m String :=
+  post.contents.postName
+
+defmethod BlogPost.postName' [Monad m] [MonadConfig m] (post : BlogPost) : m String :=
+  post.contents.postName'
 
 partial def TraverseState.freshId (state : Blog.TraverseState) (path : List String) (hint : Lean.Name) : String := Id.run do
   let mut idStr := mangle (toString hint)
@@ -139,21 +186,24 @@ where
 
 instance : BEq TraverseState where
   beq
-    | ⟨u1, t1, r1, p1, s1, s1'⟩, ⟨u2, t2, r2, p2, s2, s2'⟩ =>
+    | ⟨u1, t1, r1, p1, s1, s1', err1⟩, ⟨u2, t2, r2, p2, s2, s2', err2⟩ =>
       u1.toList.map (fun p => {p with snd := p.snd.toList}) == u2.toList.map (fun p => {p with snd := p.snd.toList}) &&
       t1.toList == t2.toList &&
       r1.toList == r2.toList &&
       p1.toList == p2.toList &&
       s1.toList == s2.toList &&
-      s1'.toList == s2'.toList
+      s1'.toList == s2'.toList &&
+      err1.toList == err2.toList
 
+abbrev TraverseM := ReaderT Blog.TraverseContext (StateT Blog.TraverseState IO)
+
+instance : MonadConfig TraverseM where
+  currentConfig := do pure (← read).config
 
 namespace Traverse
 
 open Doc
 
-@[reducible]
-defmethod Blog.TraverseM := ReaderT Blog.TraverseContext (StateT Blog.TraverseState IO)
 
 -- TODO CSS variables, and document it
 def highlightingStyle : String := "
@@ -303,20 +353,16 @@ def renderMathJs : String :=
     }
 });"
 
-instance : Traverse Blog Blog.TraverseM where
-  part _ := pure ()
-  block _ := pure ()
-  inline _ := pure ()
-  genrePart _ _ := pure none
-  genreBlock
+def genreBlock (g : Genre) : Blog.BlockExt → Array (Block g) → Blog.TraverseM (Option (Block g))
     | .highlightedCode .., _contents => do
       modify fun st => {st with
         stylesheets := st.stylesheets.insert highlightingStyle,
         scripts := st.scripts.insert highlightingJs
       }
       pure none
     | _, _ => pure none
-  genreInline
+
+def genreInline (g : Genre) : Blog.InlineExt → Array (Inline g) → Blog.TraverseM (Option (Inline g))
     | .label x, _contents => do
       -- Add as target if not already present
       if let none := (← get).targets.find? x then
@@ -331,4 +377,17 @@ instance : Traverse Blog Blog.TraverseM where
       -- TODO backreference
       pure none
     | .htmlSpan .., _ | .blob .., _ => pure none
+
+def traverser (g : Genre) (block : g.Block = Blog.BlockExt) (inline : g.Inline = Blog.InlineExt) : Traverse g Blog.TraverseM where
+  part _ := pure ()
+  block _ := pure ()
+  inline _ := pure ()
+  genrePart _ _ := pure none
+  genreBlock := block ▸ genreBlock g
+  genreInline := inline ▸ genreInline g
+
+instance : Traverse Page Blog.TraverseM := traverser Page rfl rfl
+
+instance : Traverse Post Blog.TraverseM := traverser Post rfl rfl
+
 end Traverse

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

@@ -6,7 +6,12 @@ open LeanDoc Doc Output Html HtmlT
 
 namespace LeanDoc.Genre.Blog
 
-instance [Monad m] : MonadConfig (HtmlT Blog m) where
+instance [Monad m] : MonadConfig (HtmlT Post m) where
+  currentConfig := do
+    let (_, ctxt, _) ← read
+    pure ctxt.config
+
+instance [Monad m] : MonadConfig (HtmlT Page m) where
   currentConfig := do
     let (_, ctxt, _) ← read
     pure ctxt.config
@@ -35,17 +40,21 @@ instance : MonadPath GenerateM where
 instance : MonadConfig GenerateM where
   currentConfig := do return (← read).config
 
-def GenerateM.toHtml [ToHtml Blog IO α] (x : α) : GenerateM Html := do
+open BlogGenre in
+def GenerateM.toHtml (g : Genre) [BlogGenre g] [ToHtml g IO α] (x : α) : GenerateM Html := do
   let {ctxt := ctxt, xref := state, ..} ← read
-  Blog.toHtml (m := IO) {logError := fun x => ctxt.config.logError x, headerLevel := 2} ctxt state x
+  g.toHtml (m := IO) {logError := fun x => ctxt.config.logError x, headerLevel := 2}
+    (BlogGenre.traverseContextEq (genre := g) ▸ ctxt)
+    (traverseStateEq (genre := g) ▸ state)
+    x
 
 namespace Template
 
 namespace Params
-def forPart (txt : Part Blog) : GenerateM Params := do
-  let titleHtml := {{ <h1> {{ ← txt.title.mapM GenerateM.toHtml }} </h1>}}
-  let preamble ← txt.content.mapM GenerateM.toHtml
-  let subParts ← txt.subParts.mapM GenerateM.toHtml
+def forPart [BlogGenre g] [GenreHtml g IO] [ToHtml g IO (Part g)] (txt : Part g) : GenerateM Params := do
+  let titleHtml := {{ <h1> {{ ← txt.title.mapM (GenerateM.toHtml g) }} </h1>}}
+  let preamble ← txt.content.mapM (GenerateM.toHtml g)
+  let subParts ← txt.subParts.mapM (GenerateM.toHtml g)
   return ofList [
     ("title", ⟨.mk txt.titleString, #[.mk titleHtml]⟩),
     ("content", preamble ++ subParts)
@@ -87,13 +96,12 @@ def ensureDir (dir : System.FilePath) : IO Unit := do
   if !(← dir.isDir) then
     throw (↑ s!"Not a directory: {dir}")
 
-def inPage (here : Page) (act : GenerateM α) : GenerateM α :=
+def inDir (here : Dir) (act : GenerateM α) : GenerateM α :=
   withReader (fun c => {c with ctxt.path := c.ctxt.path ++ [here.name]}) act
 
-def inPost (here : Post) (act : GenerateM α) : GenerateM α :=
-  withReader (fun c => {c with ctxt.path := c.ctxt.path ++ [c.ctxt.config.postName here.date here.content.titleString ]}) act
-
-
+def inPost (here : BlogPost) (act : GenerateM α) : GenerateM α := do
+  let name ← here.postName'
+  withReader (fun c => {c with ctxt.path := c.ctxt.path ++ [name]}) act
 
 end Generate
 
@@ -116,60 +124,56 @@ partial def copyRecursively (src tgt : System.FilePath) : IO Unit := do
           buf ← h.read 1024
 
 open Template.Params (forPart)
+
+def writePage (theme : Theme) (params : Template.Params) (template : Template := theme.pageTemplate) : GenerateM Unit := do
+  ensureDir <| (← currentDir)
+  let ⟨baseTemplate, modParams⟩ := theme.adHocTemplates (Array.mk (← currentPath)) |>.getD ⟨template, id⟩
+  let output ← Template.renderMany [baseTemplate, theme.primaryTemplate] <| modParams <| params
+  IO.FS.withFile ((← currentDir).join "index.html") .write fun h => do
+    h.putStrLn "<!DOCTYPE html>"
+    h.putStrLn output.asString
+
+def writeBlog (theme : Theme) (txt : Part Page) (posts : Array BlogPost) : GenerateM Unit := do
+  let postList ← posts.mapM fun p =>
+      theme.archiveEntryTemplate.render (.ofList [("post", ⟨.mk p, #[]⟩)])
+  let pageParams : Template.Params := (← forPart txt).insert "posts" ⟨.mk (Html.seq postList), #[]⟩
+  writePage theme pageParams
+  for post in posts do
+    if post.contents.metadata.map (·.draft) == some true && !(← showDrafts) then continue
+    inPost post do
+      IO.println s!"Generating post {← currentDir}"
+      let postParams : Template.Params ← match post.contents.metadata with
+        | none => forPart post.contents
+        | some md => (·.insert "metadata" ⟨.mk md, #[]⟩) <$> forPart post.contents
+      writePage theme postParams (template := theme.postTemplate)
+
 mutual
-  partial def Dir.generate (theme : Theme) : Dir Page → GenerateM Unit
-    | .pages content => do
-      for page in content do
-        inPage page <|
-          page.generate theme
-    | .blog posts => do
-      for post in posts do
-          if post.draft && !(← showDrafts) then continue
-          inPost post <| do
-            let ⟨baseTemplate, modParams⟩ := theme.adHocTemplates (Array.mk (← currentPath)) |>.getD ⟨theme.postTemplate, id⟩
-            let output ← Template.renderMany [baseTemplate, theme.primaryTemplate] <| modParams <| ← forPart post.content
-            ensureDir (← currentDir)
-            IO.println s!"Generating post {← currentDir}"
-            IO.FS.withFile ((← currentDir).join "index.html") .write fun h => do
-              h.putStrLn "<!DOCTYPE html>"
-              h.putStrLn output.asString
-
-  partial def Page.generate (theme : Theme) : Page → GenerateM Unit
+  partial def Dir.generate (theme : Theme) (dir : Dir) : GenerateM Unit :=
+    inDir dir <|
+    match dir with
     | .page _ _ txt subPages => do
       IO.println s!"Generating page {← currentDir}"
-      ensureDir <| (← currentDir)
       -- TODO more configurable template context
-      let postList ←
-        if let .blog ps := subPages then
-          some <$> ps.mapM fun p =>
-            theme.archiveEntryTemplate.render (.ofList [("post", ⟨.mk p, #[]⟩)])
-        else pure none
-      let pageParams : Template.Params ← forPart txt
-      let ⟨baseTemplate, modParams⟩ := theme.adHocTemplates (Array.mk (← currentPath)) |>.getD ⟨theme.pageTemplate, id⟩
-      let output ← Template.renderMany [baseTemplate, theme.primaryTemplate] <| modParams <|
-        match postList with
-        | none => pageParams
-        | some ps => pageParams.insert "posts" ⟨.mk (Html.seq ps), #[]⟩
-
-      IO.FS.withFile ((← currentDir).join "index.html") .write fun h => do
-        h.putStrLn "<!DOCTYPE html>"
-        h.putStrLn output.asString
-      subPages.generate theme
+      writePage theme (← forPart txt)
+      for p in subPages do
+        p.generate theme
+    | .blog _ _ txt posts => do
+      IO.println s!"Generating blog section {← currentDir}"
+      writeBlog theme txt posts
     | .static _ file => do
       IO.println s!"Copying from {file} to {(← currentDir)}"
       if ← (← currentDir).pathExists then
         IO.FS.removeDirAll (← currentDir)
       copyRecursively file (← currentDir)
+
+
 end
 
 def Site.generate (theme : Theme) (site : Site): GenerateM Unit := do
-  let root ← currentDir
-  ensureDir root
-  let ⟨baseTemplate, modParams⟩ := theme.adHocTemplates (Array.mk (← currentPath)) |>.getD ⟨theme.pageTemplate, id⟩
-  let output ← Template.renderMany [baseTemplate, theme.primaryTemplate] <| modParams <| ← forPart site.frontPage
-  let filename := root.join "index.html"
-  IO.FS.withFile filename .write fun h => do
-    h.putStrLn "<!DOCTYPE html>"
-    h.putStrLn output.asString
-
-  site.contents.generate theme
+  match site with
+  | .page _ txt subPages =>
+    writePage theme (← forPart txt)
+    for p in subPages do
+      p.generate theme
+  | .blog _ txt posts =>
+    writeBlog theme txt posts