From 6b389f91703e18a5d233518507d777ab155ac1cc Mon Sep 17 00:00:00 2001
From: Joshua Potter <jrpotter2112@gmail.com>
Date: Wed, 10 May 2023 15:30:35 -0600
Subject: [PATCH] Explain color/symbol code.

---
 README.md          | 17 ++++++++++++++---
 lake-manifest.json |  4 ++--
 lakefile.lean      |  2 +-
 3 files changed, 17 insertions(+), 6 deletions(-)

diff --git a/README.md b/README.md
index 4af16d6..02c15a8 100644
--- a/README.md
+++ b/README.md
@@ -1,7 +1,7 @@
 # bookshelf
 
-A collection on the study of the books listed below. I aim to use [Lean](https://leanprover.github.io/)
-when possible and fallback to LaTeX when not.
+A study of the books listed below. Most proofs are conducted in LaTeX. Where
+feasible, theorems are also formally proven in [Lean](https://leanprover.github.io/).
 
 - [ ] Apostol, Tom M. Calculus, Vol. 1: One-Variable Calculus, with an Introduction to Linear Algebra. 2nd ed. Vol. 1. 2 vols. Wiley, 1991.
 - [x] Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.
@@ -15,7 +15,7 @@ when possible and fallback to LaTeX when not.
 
 ## Documentation
 
-To generate Lean documentation, we use [bookshelf-docgen](https://github.com/jrpotter/bookshelf-docgen).
+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:
 
@@ -27,3 +27,14 @@ serve files locally:
 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/symbol code is used on generated PDF headers to indicate their status:
+
+* Teal coloring (with a checkmark) indicates the corresponding proof is
+  complete. That is, the proof has been written in TeX and also formally
+  verified in Lean.
+* Magenta coloring (with a spinner) indicates the corresponding proof is in
+  progress. That is, a proof in both TeX and Lean have not yet been finished,
+  but is actively being worked on.
+* Red coloring (with a warning) indicates the formal Lean proof has not yet been
+  started. It may or may not also indicate the TeX proof has been written.
diff --git a/lake-manifest.json b/lake-manifest.json
index 1bf0f30..05cbe49 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -16,9 +16,9 @@
   {"git":
    {"url": "https://github.com/jrpotter/bookshelf-docgen.git",
     "subDir?": null,
-    "rev": "93aa96a2b6318d78cc505e45f6538d507ce0834c",
+    "rev": "291f71e6c520751d52832c95f47cbc059c77bfa7",
     "name": "doc-gen4",
-    "inputRev?": "93aa96a2b6318d78cc505e45f6538d507ce0834c"}},
+    "inputRev?": "291f71e6c520751d52832c95f47cbc059c77bfa7"}},
   {"git":
    {"url": "https://github.com/mhuisi/lean4-cli",
     "subDir?": null,
diff --git a/lakefile.lean b/lakefile.lean
index 1ff5e09..1d2e9d9 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -12,7 +12,7 @@ require std4 from git
     "6006307d2ceb8743fea7e00ba0036af8654d0347"
 require «doc-gen4» from git
   "https://github.com/jrpotter/bookshelf-docgen.git" @
-    "93aa96a2b6318d78cc505e45f6538d507ce0834c"
+    "291f71e6c520751d52832c95f47cbc059c77bfa7"
 
 @[default_target]
 lean_lib «Bookshelf» {