From fe5302581712a714e2f6d40280685dcb1ed765da Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Thu, 11 May 2023 07:55:25 -0600 Subject: [PATCH] Add PDF generation to absorbed doc-gen4 project. --- DocGen4/Output/Base.lean | 17 ++++++--- DocGen4/Output/DocString.lean | 2 +- DocGen4/Output/Index.lean | 45 ++++++++++++++++++++++-- DocGen4/Output/Navbar.lean | 12 +++---- DocGen4/Output/ToJson.lean | 2 +- DocGen4/Process.lean | 1 + DocGen4/Process/Hierarchy.lean | 64 ++++++++++++++++++++-------------- DocGen4/Process/NameExt.lean | 43 +++++++++++++++++++++++ README.md | 25 ++++--------- lakefile.lean | 21 +++++++++++ scripts/run_pdflatex.sh | 26 ++++++++++++++ 11 files changed, 198 insertions(+), 60 deletions(-) create mode 100644 DocGen4/Process/NameExt.lean create mode 100755 scripts/run_pdflatex.sh diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index d02bf99..b45481f 100644 --- a/DocGen4/Output/Base.lean +++ b/DocGen4/Output/Base.lean @@ -107,18 +107,25 @@ def templateExtends {α β} {m} [Bind m] (base : α → m β) (new : m α) : m def templateLiftExtends {α β} {m n} [Bind m] [MonadLift n m] (base : α → n β) (new : m α) : m β := new >>= (monadLift ∘ base) + +/- +Returns the doc-gen4 link to a module `NameExt`. +-/ +def moduleNameExtToLink (n : NameExt) : BaseHtmlM String := do + let parts := n.name.components.map Name.toString + return (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ "." ++ n.ext.toString + /-- Returns the doc-gen4 link to a module name. -/ -def moduleNameToLink (n : Name) : BaseHtmlM String := do - let parts := n.components.map Name.toString - return (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html" +def moduleNameToHtmlLink (n : Name) : BaseHtmlM String := + moduleNameExtToLink ⟨n, .html⟩ /-- Returns the HTML doc-gen4 link to a module name. -/ def moduleToHtmlLink (module : Name) : BaseHtmlM Html := do - return {module.toString} + return {module.toString} /-- Returns the LeanInk link to a module name. @@ -168,7 +175,7 @@ Returns the doc-gen4 link to a declaration name. def declNameToLink (name : Name) : HtmlM String := do let res ← getResult let module := res.moduleNames[res.name2ModIdx.find! name |>.toNat]! - return (← moduleNameToLink module) ++ "#" ++ name.toString + return (← moduleNameToHtmlLink module) ++ "#" ++ name.toString /-- Returns the HTML doc-gen4 link to a declaration name. diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean index ef75d76..33c8503 100644 --- a/DocGen4/Output/DocString.lean +++ b/DocGen4/Output/DocString.lean @@ -76,7 +76,7 @@ def nameToLink? (s : String) : HtmlM (Option String) := do declNameToLink name -- module name else if res.moduleNames.contains name then - moduleNameToLink name + moduleNameToHtmlLink name -- find similar name in the same module else match (← getCurrentName) with diff --git a/DocGen4/Output/Index.lean b/DocGen4/Output/Index.lean index afa4eb5..c87a68c 100644 --- a/DocGen4/Output/Index.lean +++ b/DocGen4/Output/Index.lean @@ -15,9 +15,48 @@ def index : BaseHtmlM Html := do templateExtends (baseHtml "Index") <| pure <|
-

Welcome to the documentation page

- -- Temporary comment until the lake issue is resolved - -- for commit {s!"{← getProjectCommit} "} +

Bookshelf

+

+ A study of the books listed below. Most proofs are conducted in LaTeX. + Where feasible, theorems are also formally proven in + Lean. +

+ +

+ A color/symbol code is used on generated PDF headers to indicate their + status: +

+

This was built using Lean 4 at commit {Lean.githash}

diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean index 4280864..75975b6 100644 --- a/DocGen4/Output/Navbar.lean +++ b/DocGen4/Output/Navbar.lean @@ -13,9 +13,9 @@ namespace Output open Lean open scoped DocGen4.Jsx -def moduleListFile (file : Name) : BaseHtmlM Html := do - return
- {file.getString!} +def moduleListFile (file : NameExt) : BaseHtmlM Html := do + return
+ {file.getString!}
/-- @@ -25,13 +25,13 @@ partial def moduleListDir (h : Hierarchy) : BaseHtmlM Html := do let children := Array.mk (h.getChildren.toList.map Prod.snd) let dirs := children.filter (fun c => c.getChildren.toList.length != 0) let files := children.filter (fun c => Hierarchy.isFile c && c.getChildren.toList.length = 0) - |>.map Hierarchy.getName + |>.map Hierarchy.getNameExt let dirNodes ← dirs.mapM moduleListDir let fileNodes ← files.mapM moduleListFile - let moduleLink ← moduleNameToLink h.getName + let moduleLink ← moduleNameToHtmlLink h.getName let summary := if h.isFile then - {s!"{h.getName.getString!} ({file})"} + {s!"{h.getName.getString!} ({file})"} else {h.getName.getString!} diff --git a/DocGen4/Output/ToJson.lean b/DocGen4/Output/ToJson.lean index a641f67..95e84a0 100644 --- a/DocGen4/Output/ToJson.lean +++ b/DocGen4/Output/ToJson.lean @@ -53,7 +53,7 @@ instance : ToJson JsonIndex where def JsonIndex.addModule (index : JsonIndex) (module : JsonModule) : BaseHtmlM JsonIndex := do let mut index := index - let newModule := (module.name, ← moduleNameToLink (String.toName module.name)) + let newModule := (module.name, ← moduleNameToHtmlLink (String.toName module.name)) let newDecls := module.declarations.map (fun d => (d.name, d)) index := { index with modules := newModule :: index.modules diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean index 0c1d9e6..dd6a317 100644 --- a/DocGen4/Process.lean +++ b/DocGen4/Process.lean @@ -14,6 +14,7 @@ import DocGen4.Process.DocInfo import DocGen4.Process.Hierarchy import DocGen4.Process.InductiveInfo import DocGen4.Process.InstanceInfo +import DocGen4.Process.NameExt import DocGen4.Process.NameInfo import DocGen4.Process.OpaqueInfo import DocGen4.Process.StructureInfo diff --git a/DocGen4/Process/Hierarchy.lean b/DocGen4/Process/Hierarchy.lean index 86d2be0..2667f89 100644 --- a/DocGen4/Process/Hierarchy.lean +++ b/DocGen4/Process/Hierarchy.lean @@ -6,6 +6,8 @@ Authors: Henrik Böving import Lean import Lean.Data.HashMap +import DocGen4.Process.NameExt + def Lean.HashSet.fromArray [BEq α] [Hashable α] (xs : Array α) : Lean.HashSet α := xs.foldr (flip .insert) .empty @@ -18,35 +20,38 @@ def getNLevels (name : Name) (levels: Nat) : Name := (components.drop (components.length - levels)).reverse.foldl (· ++ ·) Name.anonymous inductive Hierarchy where -| node (name : Name) (isFile : Bool) (children : RBNode Name (fun _ => Hierarchy)) : Hierarchy +| node (name : NameExt) (isFile : Bool) (children : RBNode NameExt (fun _ => Hierarchy)) : Hierarchy -instance : Inhabited Hierarchy := ⟨Hierarchy.node Name.anonymous false RBNode.leaf⟩ +instance : Inhabited Hierarchy := ⟨Hierarchy.node ⟨.anonymous, .html⟩ false RBNode.leaf⟩ -abbrev HierarchyMap := RBNode Name (fun _ => Hierarchy) +abbrev HierarchyMap := RBNode NameExt (fun _ => Hierarchy) -- Everything in this namespace is adapted from stdlib's RBNode namespace HierarchyMap -def toList : HierarchyMap → List (Name × Hierarchy) +def toList : HierarchyMap → List (NameExt × Hierarchy) | t => t.revFold (fun ps k v => (k, v)::ps) [] -def toArray : HierarchyMap → Array (Name × Hierarchy) +def toArray : HierarchyMap → Array (NameExt × Hierarchy) | t => t.fold (fun ps k v => ps ++ #[(k, v)] ) #[] -def hForIn [Monad m] (t : HierarchyMap) (init : σ) (f : (Name × Hierarchy) → σ → m (ForInStep σ)) : m σ := +def hForIn [Monad m] (t : HierarchyMap) (init : σ) (f : (NameExt × Hierarchy) → σ → m (ForInStep σ)) : m σ := t.forIn init (fun a b acc => f (a, b) acc) -instance : ForIn m HierarchyMap (Name × Hierarchy) where +instance : ForIn m HierarchyMap (NameExt × Hierarchy) where forIn := HierarchyMap.hForIn end HierarchyMap namespace Hierarchy -def empty (n : Name) (isFile : Bool) : Hierarchy := +def empty (n : NameExt) (isFile : Bool) : Hierarchy := node n isFile RBNode.leaf def getName : Hierarchy → Name +| node n _ _ => n.name + +def getNameExt : Hierarchy → NameExt | node n _ _ => n def getChildren : Hierarchy → HierarchyMap @@ -55,31 +60,34 @@ def getChildren : Hierarchy → HierarchyMap def isFile : Hierarchy → Bool | node _ f _ => f -partial def insert! (h : Hierarchy) (n : Name) : Hierarchy := Id.run do - let hn := h.getName +partial def insert! (h : Hierarchy) (n : NameExt) : Hierarchy := Id.run do + let hn := h.getNameExt let mut cs := h.getChildren - if getNumParts hn + 1 == getNumParts n then - match cs.find Name.cmp n with + if getNumParts hn.name + 1 == getNumParts n.name then + match cs.find NameExt.cmp n with | none => - node hn h.isFile (cs.insert Name.cmp n <| empty n true) + node hn h.isFile (cs.insert NameExt.cmp n <| empty n true) | some (node _ true _) => h | some (node _ false ccs) => - cs := cs.erase Name.cmp n - node hn h.isFile (cs.insert Name.cmp n <| node n true ccs) + cs := cs.erase NameExt.cmp n + node hn h.isFile (cs.insert NameExt.cmp n <| node n true ccs) else - let leveledName := getNLevels n (getNumParts hn + 1) - match cs.find Name.cmp leveledName with + let leveled := ⟨getNLevels n.name (getNumParts hn.name + 1), .html⟩ + match cs.find NameExt.cmp leveled with | some nextLevel => - cs := cs.erase Name.cmp leveledName + cs := cs.erase NameExt.cmp leveled -- BUG? - node hn h.isFile <| cs.insert Name.cmp leveledName (nextLevel.insert! n) + node hn h.isFile <| cs.insert NameExt.cmp leveled (nextLevel.insert! n) | none => - let child := (insert! (empty leveledName false) n) - node hn h.isFile <| cs.insert Name.cmp leveledName child + let child := (insert! (empty leveled false) n) + node hn h.isFile <| cs.insert NameExt.cmp leveled child partial def fromArray (names : Array Name) : Hierarchy := - names.foldl insert! (empty anonymous false) + (names.map (fun n => NameExt.mk n .html)).foldl insert! (empty ⟨anonymous, .html⟩ false) + +partial def fromArrayExt (names : Array NameExt) : Hierarchy := + names.foldl insert! (empty ⟨anonymous, .html⟩ false) def baseDirBlackList : HashSet String := HashSet.fromArray #[ @@ -99,13 +107,15 @@ def baseDirBlackList : HashSet String := "style.css" ] -partial def fromDirectoryAux (dir : System.FilePath) (previous : Name) : IO (Array Name) := do +partial def fromDirectoryAux (dir : System.FilePath) (previous : Name) : IO (Array NameExt) := do let mut children := #[] for entry in ← System.FilePath.readDir dir do if ← entry.path.isDir then children := children ++ (← fromDirectoryAux entry.path (.str previous entry.fileName)) else if entry.path.extension = some "html" then - children := children.push <| .str previous (entry.fileName.dropRight ".html".length) + children := children.push <| ⟨.str previous (entry.fileName.dropRight ".html".length), .html⟩ + else if entry.path.extension = some "pdf" then + children := children.push <| ⟨.str previous (entry.fileName.dropRight ".pdf".length), .pdf⟩ return children def fromDirectory (dir : System.FilePath) : IO Hierarchy := do @@ -116,8 +126,10 @@ def fromDirectory (dir : System.FilePath) : IO Hierarchy := do else if ← entry.path.isDir then children := children ++ (← fromDirectoryAux entry.path (.mkSimple entry.fileName)) else if entry.path.extension = some "html" then - children := children.push <| .mkSimple (entry.fileName.dropRight ".html".length) - return Hierarchy.fromArray children + children := children.push <| ⟨.mkSimple (entry.fileName.dropRight ".html".length), .html⟩ + else if entry.path.extension = some "pdf" then + children := children.push <| ⟨.mkSimple (entry.fileName.dropRight ".pdf".length), .pdf⟩ + return Hierarchy.fromArrayExt children end Hierarchy end DocGen4 diff --git a/DocGen4/Process/NameExt.lean b/DocGen4/Process/NameExt.lean new file mode 100644 index 0000000..d495cc5 --- /dev/null +++ b/DocGen4/Process/NameExt.lean @@ -0,0 +1,43 @@ +/- +A generalization of `Lean.Name` that includes a file extension. +-/ +import Lean + +open Lean Name + +inductive Extension where +| html +| pdf +deriving Repr + +namespace Extension + +def cmp : Extension → Extension → Ordering + | html, html => Ordering.eq + | html, _ => Ordering.lt + | pdf, pdf => Ordering.eq + | pdf, _ => Ordering.gt + +def toString : Extension → String + | html => "html" + | pdf => "pdf" + +end Extension + +structure NameExt where + name : Name + ext : Extension + +namespace NameExt + +def cmp (n₁ n₂ : NameExt) : Ordering := + match Name.cmp n₁.name n₂.name with + | Ordering.eq => Extension.cmp n₁.ext n₂.ext + | ord => ord + +def getString! : NameExt → String + | ⟨str _ s, .html⟩ => s + | ⟨str _ s, .pdf⟩ => s ++ "_pdf" + | _ => unreachable! + +end NameExt diff --git a/README.md b/README.md index 9a6beb4..1977250 100644 --- a/README.md +++ b/README.md @@ -15,27 +15,16 @@ feasible, theorems are also formally proven in [Lean](https://leanprover.github. ## Documentation -To generate documentation, we use [bookshelf-docgen](https://github.com/jrpotter/bookshelf-docgen). -Refer to this project on prerequisites and then run the following to build and -serve files locally: +This project has absorbed [doc-gen4](https://github.com/leanprover/doc-gen4) to +ease customization. In particular, the `DocGen4` module found in this project +allows generating PDFs and including them into the navbar. To generate +documentation and serve files locally, run the following: ```bash > lake build Bookshelf:docs > lake run server ``` -This assumes you have `python3` available in your `$PATH`. To change how the -server behaves, refer to the `.env` file located in the root directory of this -project. - -A color code is used on generated PDF headers to indicate their status: - -* Cyan statements indicate axioms and definitions. There must exist a - corresponding `axiom` or `def` in Lean. -* Teal statements indicate those with complete proofs in both LaTeX *and* Lean. -* Magenta statements indicate those that have not been completely proven in - either LaTeX or Lean (or both). Progress is currently being made to correct - this though. -* Red coloring is a catch-all for all statements that don't fit the above - categorizations. Incomplete definitions, proofs only conducted in LaTeX, etc. - belong here. +This assumes you have `pdflatex` and `python3` available in your `$PATH`. To +change how the server behaves, refer to the `.env` file located in the root +directory of this project. diff --git a/lakefile.lean b/lakefile.lean index 41676d8..fbee696 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -77,7 +77,28 @@ target coreDocs : FilePath := do } return (dataFile, trace) +/-- +Wrapper for running scripts found in the `script` directory. +-/ +def run_sh (name : String) : IndexBuildM Unit := do + let some bookshelfPkg ← findPackage? `«bookshelf» + | error "no bookshelf package found in workspace" + let proc <- IO.Process.output { + cmd := bookshelfPkg.dir.toString ++ s!"/scripts/{name}.sh", + args := #[(← getWorkspace).root.buildDir.toString] + } + if proc.exitCode == 0 then + let out := proc.stdout.trim + if out.length > 0 then IO.println out + else + let err := proc.stderr.trim + if err.length > 0 then IO.eprintln err + library_facet docs (lib) : FilePath := do + run_sh "run_pdflatex" + -- Ordering is important. The index file is generated by walking through the + -- filesystem directory. Files copied from the shell scripts need to exist + -- prior to this. let some bookshelfPkg ← findPackage? `«bookshelf» | error "no bookshelf package found in workspace" let some docGen4 := bookshelfPkg.findLeanExe? `«doc-gen4» diff --git a/scripts/run_pdflatex.sh b/scripts/run_pdflatex.sh new file mode 100755 index 0000000..5911bf6 --- /dev/null +++ b/scripts/run_pdflatex.sh @@ -0,0 +1,26 @@ +#!/usr/bin/env bash + +if ! command -v pdflatex > /dev/null; then + >&2 echo 'pdflatex was not found in the current $PATH.' + exit 1 +fi + +BUILD_DIR="$1" + +function process_file () { + REL_DIR=$(dirname "$1") + REL_BASE=$(basename -s ".tex" "$1") + mkdir -p "$BUILD_DIR/doc/$REL_DIR" + (cd "$REL_DIR" && pdflatex "$REL_BASE.tex") + cp "$REL_DIR/$REL_BASE.pdf" "$BUILD_DIR/doc/$REL_DIR/" +} + +export BUILD_DIR +export -f process_file + +# We run this command twice to allow any cross-references to resolve correctly. +# https://tex.stackexchange.com/questions/41539/does-hyperref-work-between-two-files +for _ in {1..2}; do + find ./* \( -path build -o -path lake-packages \) -prune -o -name "*.tex" -print0 \ + | xargs -0 -I{} bash -c "process_file {}" +done