add: Table of Contents to each chapter (2-12) using mdbook-toc

.github/workflows/deploy.yml

@@ -11,17 +11,27 @@ jobs:
     steps:
     - name: Checkout
       uses: actions/checkout@v3
-    - name: Download mdbook for Lean
+    - name: Download mdbook and dependencies for Lean
       shell: bash
       run: |
+        mkdir -p $HOME/.local/bin
+        echo "$HOME/.local/bin" >> $GITHUB_PATH
+
         curl -O --location https://github.com/leanprover/mdBook/releases/download/v0.4.6/mdbook-linux.tar.gz
         tar xvf mdbook-linux.tar.gz
-        ./mdbook-linux/mdbook --help
+        cp ./mdbook-linux/mdbook $HOME/.local/bin/
         ldd ./mdbook-linux/mdbook
+        mdbook --help
+
+        curl -O --location https://github.com/badboy/mdbook-toc/releases/download/0.14.2/mdbook-toc-0.14.2-x86_64-unknown-linux-gnu.tar.gz
+        tar xvf mdbook-toc-0.14.2-x86_64-unknown-linux-gnu.tar.gz
+        cp ./mdbook-toc $HOME/.local/bin/
+        ldd ./mdbook-toc
+        mdbook-toc --help
     - name: Run mdbook build
       shell: bash
       run: |
-        ./mdbook-linux/mdbook build
+        mdbook build
         rm -rf ./out/.git
         rm -rf ./out/.github
     - name: Deploy 🚀

.github/workflows/netlify-deploy.yml

@@ -14,17 +14,27 @@ jobs:
     steps:
     - name: Checkout
       uses: actions/checkout@v3
-    - name: Download mdbook for Lean
+    - name: Download mdbook and dependencies for Lean
       shell: bash
       run: |
+        mkdir -p $HOME/.local/bin
+        echo "$HOME/.local/bin" >> $GITHUB_PATH
+
         curl -O --location https://github.com/leanprover/mdBook/releases/download/v0.4.6/mdbook-linux.tar.gz
         tar xvf mdbook-linux.tar.gz
-        ./mdbook-linux/mdbook --help
+        cp ./mdbook-linux/mdbook $HOME/.local/bin/
         ldd ./mdbook-linux/mdbook
+        mdbook --help
+
+        curl -O --location https://github.com/badboy/mdbook-toc/releases/download/0.14.2/mdbook-toc-0.14.2-x86_64-unknown-linux-gnu.tar.gz
+        tar xvf mdbook-toc-0.14.2-x86_64-unknown-linux-gnu.tar.gz
+        cp ./mdbook-toc $HOME/.local/bin/
+        ldd ./mdbook-toc
+        mdbook-toc --help
     - name: Run mdbook build
       shell: bash
       run: |
-        ./mdbook-linux/mdbook build
+        mdbook build
         rm -rf ./out/.git
         rm -rf ./out/.github
     - name: Deploy to Netlify hosting

axioms_and_computation.md

@@ -64,6 +64,10 @@ compatible with bytecode evaluation, whereas the third is not amenable
 to computational interpretation. We will spell out the details more
 precisely below.
 
+### Contents
+
+<!-- toc -->
+
 Historical and Philosophical Context
 ------------------------------------
 

book.toml

@@ -13,3 +13,7 @@ git-repository-url = "https://github.com/leanprover/theorem_proving_in_lean4"
 
 [output.html.playground.boring-prefixes]
 lean = "# "
+
+[preprocessor.toc]
+command = "mdbook-toc"
+renderer = ["html"]

conv.md

@@ -6,6 +6,10 @@ Inside a tactic block, one can use the keyword `conv` to enter
 goals, even inside function abstractions and dependent arrows, to apply rewriting or
 simplifying steps.
 
+### Contents
+
+<!-- toc -->
+
 Basic navigation and rewriting
 -------
 

dependent_type_theory.md

@@ -9,6 +9,10 @@ theory known as the *Calculus of Constructions*, with a countable
 hierarchy of non-cumulative universes and inductive types. By the end
 of this chapter, you will understand much of what this means.
 
+### Contents
+
+<!-- toc -->
+
 ## Simple Type Theory
 
 "Type theory" gets its name from the fact that every expression has an

induction_and_recursion.md

@@ -17,6 +17,10 @@ refer to as the "equation compiler." The equation compiler is not part
 of the trusted code base; its output consists of terms that are
 checked independently by the kernel.
 
+### Contents
+
+<!-- toc -->
+
 Pattern Matching
 ----------------
 

inductive_types.md

@@ -62,6 +62,10 @@ to start with a low-level, hands-on understanding. We will start with
 some basic examples of inductive types, and work our way up to more
 elaborate and complex examples.
 
+### Contents
+
+<!-- toc -->
+
 Enumerated Types
 ----------------
 

interacting_with_lean.md

@@ -13,6 +13,10 @@ Not all of the information found here will be useful to you right
 away. We recommend skimming this section to get a sense of Lean's
 features, and then returning to it as necessary.
 
+### Contents
+
+<!-- toc -->
+
 Importing Files
 ---------------
 

propositions_and_proofs.md

@@ -6,6 +6,10 @@ Lean. In this chapter, we will begin to explain how to write
 mathematical assertions and proofs in the language of dependent type
 theory as well.
 
+### Contents
+
+<!-- toc -->
+
 Propositions as Types
 ---------------------
 

quantifiers_and_equality.md

@@ -6,6 +6,10 @@ statements involving the propositional connectives. In this chapter,
 we extend the repertoire of logical constructions to include the
 universal and existential quantifiers, and the equality relation.
 
+### Contents
+
+<!-- toc -->
+
 The Universal Quantifier
 ------------------------
 
@@ -363,7 +367,7 @@ We can also use `_` in the first relation (right after ``<expr>_0``)
 which is useful to align the sequence of relation/proof pairs:
 
 ```
-calc <expr>_0 
+calc <expr>_0
     '_' 'op_1' <expr>_1 ':=' <proof>_1
     '_' 'op_2' <expr>_2 ':=' <proof>_2
     ...

structures_and_records.md

@@ -27,6 +27,10 @@ automatically generates all the projection functions. The
 previously defined ones. Moreover, Lean provides convenient notation
 for defining instances of a given structure.
 
+### Contents
+
+<!-- toc -->
+
 Declaring Structures
 --------------------
 

tactics.md

@@ -22,6 +22,10 @@ instruction. But they can also be shorter and easier to
 write. Moreover, tactics offer a gateway to using Lean's automation,
 since automated procedures are themselves tactics.
 
+### Contents
+
+<!-- toc -->
+
 Entering Tactic Mode
 --------------------
 

type_classes.md

@@ -1,5 +1,9 @@
 # Type Classes
 
+### Contents
+
+<!-- toc -->
+
 Type classes were introduced as a principled way of enabling
 ad-hoc polymorphism in functional programming languages. We first observe that it
 would be easy to implement an ad-hoc polymorphic function (such as addition) if the