-
{file.getString!}
+def moduleListFile (file : NameExt) : BaseHtmlM Html := do
+ return
/--
@@ -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