From aa25e084d2b5ad667ba29d62b70d9a8ee6ab67d5 Mon Sep 17 00:00:00 2001
From: Joshua Potter <jrpotter2112@gmail.com>
Date: Thu, 14 Dec 2023 15:27:12 -0700
Subject: [PATCH] Update index and add pdflatex generation script.

---
 DocGen4/Output/Index.lean | 65 +++++++++++++++++++++++++++++++++++++--
 lakefile.lean             |  9 ++++++
 run_pdflatex.sh           | 19 ++++++++++++
 3 files changed, 90 insertions(+), 3 deletions(-)
 create mode 100755 run_pdflatex.sh

diff --git a/DocGen4/Output/Index.lean b/DocGen4/Output/Index.lean
index afa4eb5..f12b0fa 100644
--- a/DocGen4/Output/Index.lean
+++ b/DocGen4/Output/Index.lean
@@ -15,9 +15,68 @@ def index : BaseHtmlM Html := do templateExtends (baseHtml "Index") <|
   pure <|
     <main>
       <a id="top"></a>
-      <h1> Welcome to the documentation page </h1>
-      -- Temporary comment until the lake issue is resolved
-      -- for commit <a href={s!"{← getProjectGithubUrl}/tree/{← getProjectCommit}"}>{s!"{← getProjectCommit} "}</a>
+      <h1>Bookshelf</h1>
+      <p>
+        A study of the books listed below. Most proofs are conducted in LaTeX.
+        Where feasible, theorems are also formally proven in
+        <a target="_blank" href="https://leanprover.github.io/">Lean</a>.
+      </p>
+
+      <h2>In Progress</h2>
+      <ul>
+        <li><a href={s!"{← getRoot}Bookshelf/Apostol.html"}>Apostol, Tom M. Calculus, Vol. 1: One-Variable Calculus, with an Introduction to Linear Algebra. 2nd ed. Vol. 1. 2 vols. Wiley, 1991.</a></li>
+        <li><a href={s!"{← getRoot}Bookshelf/Enderton/Logic.html"}>Enderton, Herbert B. A Mathematical Introduction to Logic. 2nd ed. San Diego: Harcourt/Academic Press, 2001.</a></li>
+        <li><a href={s!"{← getRoot}Bookshelf/Enderton/Set.html"}>Enderton, Herbert B. Elements of Set Theory. New York: Academic Press, 1977.</a></li>
+        <li><a href={s!"{← getRoot}Bookshelf/Fraleigh.html"}>Fraleigh, John B. A First Course in Abstract Algebra, n.d.</a></li>
+      </ul>
+
+      <h2>Complete</h2>
+      <ul>
+        <li><a href={s!"{← getRoot}Bookshelf/Avigad.html"}>Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.</a></li>
+      </ul>
+
+      <h2>Pending</h2>
+      <ul>
+        <li>Axler, Sheldon. Linear Algebra Done Right. Undergraduate Texts in Mathematics. Cham: Springer International Publishing, 2015.</li>
+        <li>Cormen, Thomas H., Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. Introduction to Algorithms. 3rd ed. Cambridge, Mass: MIT Press, 2009.</li>
+        <li>Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.</li>
+        <li>Gustedt, Jens. Modern C. Shelter Island, NY: Manning Publications Co, 2020.</li>
+        <li>Ross, Sheldon. A First Course in Probability Theory. 8th ed. Pearson Prentice Hall, n.d.</li>
+        <li>Smullyan, Raymond M. To Mock a Mockingbird: And Other Logic Puzzles Including an Amazing Adventure in Combinatory Logic. Oxford: Oxford university press, 2000.</li>
+      </ul>
+
+      <h2>Legend</h2>
+      <p>
+        A color/symbol code is used on generated PDF headers to indicate their
+        status:
+        <ul>
+          <li>
+            <span style="color:darkgray">Dark gray statements </span> are
+            reserved for definitions and axioms that have been encoded in LaTeX.
+            A reference to a definition in Lean may also be provided.
+          </li>
+          <li>
+            <span style="color:teal">Teal statements </span> are reserved for
+            statements, theorems, lemmas, etc. that have been proven in LaTeX
+            and have a corresponding proof in Lean.
+          </li>
+          <li>
+            <span style="color:olive">Olive statements </span> are reserved for
+            statements, theorems, lemmas, etc. that have been proven in LaTeX.
+            A reference to a statement in Lean may also be provided.
+          </li>
+          <li>
+            <span style="color:fuchsia">Fuchsia statements </span> are reserved
+            for statements, theorems, lemmas, etc. that have been proven in
+            LaTeX and <i>will </i> have a corresponding proof in Lean.
+          </li>
+          <li>
+            <span style="color:maroon">Maroon </span> serves as a catch-all for
+            statements that don't fit the above categorizations. Incomplete
+            definitions, statements without proof, etc. belong here.
+          </li>
+        </ul>
+      </p>
       <p>This was built using Lean 4 at commit <a href={s!"https://github.com/leanprover/lean4/tree/{Lean.githash}"}>{Lean.githash}</a></p>
     </main>
 
diff --git a/lakefile.lean b/lakefile.lean
index a062dcc..9366362 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -160,6 +160,15 @@ library_facet docs (lib) : FilePath := do
   coreJob.bindAsync fun _ coreInputTrace => do
     exeJob.bindAsync fun exeFile exeTrace => do
       moduleJobs.bindSync fun _ inputTrace => do
+        logInfo "Converting TeX to PDF"
+        let some docGen4 ← findPackage? `«doc-gen4»
+          | error "no doc-gen4 package found in workspace"
+        let pdfLatex := docGen4.srcDir / "run_pdflatex.sh"
+        let buildDir := (←getWorkspace).root.buildDir
+        proc {
+          cmd := pdfLatex.toString
+          args := #[buildDir.toString]
+        }
         let depTrace := mixTraceArray #[inputTrace, exeTrace, coreInputTrace]
         let trace ← buildFileUnlessUpToDate dataFile depTrace do
           logInfo "Documentation indexing"
diff --git a/run_pdflatex.sh b/run_pdflatex.sh
new file mode 100755
index 0000000..b46f9cf
--- /dev/null
+++ b/run_pdflatex.sh
@@ -0,0 +1,19 @@
+#!/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"
+
+# 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
+TEX_FILES=$(find . -name ".tex" -not -path "*preamble.tex")
+for _ in {1..2}; do
+  for f in $TEX_FILES; do
+    REL_DIR=$(dirname "$f")
+    REL_BASE=$(basename -s ".tex" "$1")
+    cp "$REL_DIR/$REL_BASE.pdf" "$BUILD_DIR/doc/$REL_DIR/"
+  done
+done