chore: use Verso's new lightweight literate programming support

.github/workflows/build_book.yml

@@ -11,73 +11,56 @@ concurrency:
   group: ${{ github.ref }}  # Group runs by the ref (branch or PR)
   cancel-in-progress: true  # Cancel any ongoing runs in the same group
 
-defaults:
-  run:
-    working-directory: ./book
-
 jobs:
   build:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v4
-      - name: Install elan
-        run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
-      # The build directories for analysis/ and book/ are cached separately, because they
-      # use disjoint sets of build dependencies. There's no need to rebuild both completely
-      # when only one has a version bump.
-      - name: Restore cache if available
-        uses: actions/cache/restore@v4
+
+      - uses: leanprover/lean-action@v1
         with:
-          path: |
-            ./analysis/.lake
-          key: lake-${{ runner.os }}-${{ runner.arch}}-${{ hashFiles('analysis/lean-toolchain') }}-${{ hashFiles('analysis/lake-manifest.json') }}-${{ github.sha }}
-          restore-keys: lake-${{ runner.os }}-${{ runner.arch}}-${{ hashFiles('analysis/lean-toolchain') }}-${{ hashFiles('analysis/lake-manifest.json') }}
-      - name: Restore book cache if available
+          build: false
+          test: false
+          use-mathlib-cache: true
+          use-github-cache: false
+      # We manage the Lake cache ourselves rather than using
+      # lean-action's built-in caching because lean-action saves the
+      # cache before we generate the site. As a result, Verso and its
+      # HTML artifacts would never be cached.
+      - name: Restore Lake cache
         uses: actions/cache/restore@v4
         with:
-          path: |
-            ./book/.lake
-          key: lake-${{ runner.os }}-${{ runner.arch}}-${{ hashFiles('book/lean-toolchain') }}-${{ hashFiles('book/lake-manifest.json') }}-${{ github.sha }}
-          restore-keys: lake-${{ runner.os }}-${{ runner.arch}}-${{ hashFiles('book/lean-toolchain') }}-${{ hashFiles('book/lake-manifest.json') }}
-
-      # Getting the mathlib cache is only useful when mathlib gets updated, but will save a lot of time in that case.
-      - name: Get Mathlib cache
-        run: ~/.elan/bin/lake exe cache get || true
-        working-directory: ./analysis
+          path: .lake
+          key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
+          restore-keys: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}
+      - name: Build project
+        run: lake build
       - name: Build doc-gen
-        run: ~/.elan/bin/lake -R -Kenv=dev build Analysis:docs
-        working-directory: ./analysis
-      - name: Build metadata of project
-        run: ~/.elan/bin/lake build
-        working-directory: ./analysis
+        run: lake -R -Kenv=dev build Analysis:docs
       - name: Build book
+        id: build-site
         run: |
-          ~/.elan/bin/lake exe analysis-book 
-      - name: Copy docs to analysis-book
-        run: |
-          cp -r ../analysis/.lake/build/doc _site/docs
-      - name: Remove unnecessary lake files from documentation in `_site/docs`
+          SITE_PATH="$(lake query :literateHtml)"
+          echo "Generated site at: $SITE_PATH"
+          echo "path=$SITE_PATH" >> "$GITHUB_OUTPUT"
+          mkdir -p _site
+          cp -r "$SITE_PATH/." _site
+      - name: Copy docs to site
+        run: cp -r .lake/build/doc _site/docs
+      - name: Remove unnecessary Lake files from docs
         run: |
           find _site/docs -name "*.trace" -delete
           find _site/docs -name "*.hash" -delete
-      # The cache for analysis/ is saved here, rather than before building the book, because
-      # building the book generates JSON files full of literate program artifacts in analysis/.lake
-      - name: Save cache
-        uses: actions/cache/save@v4
-        with:
-          path: |
-            ./analysis/.lake
-          key: lake-${{ runner.os }}-${{ runner.arch}}-${{ hashFiles('analysis/lean-toolchain') }}-${{ hashFiles('analysis/lake-manifest.json') }}-${{ github.sha }}
-      - name: Save book cache
+      - name: Save Lake cache
+        if: always()
         uses: actions/cache/save@v4
         with:
-          path: |
-            ./book/.lake
-          key: lake-${{ runner.os }}-${{ runner.arch}}-${{ hashFiles('book/lean-toolchain') }}-${{ hashFiles('book/lake-manifest.json') }}-${{ github.sha }}
+          path: .lake
+          key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
       - name: Upload website
         uses: actions/upload-pages-artifact@v3
         with:
-          path: './book/_site'
+          path: _site
   deploy:
     # Add a dependency to the build job
     needs: build

.gitignore

@@ -16,7 +16,7 @@ _site/
 .claude/
 .cursor/
 Claude.md
-analysis/.repair
+.repair
 **/.env
 **/.aider.conf.yml
 **/.formalize

analysis/Analysis.lean → Analysis.lean

@@ -97,3 +97,21 @@ import Analysis.MeasureTheory.Section_1_3_2
 import Analysis.MeasureTheory.Section_1_3_3
 import Analysis.MeasureTheory.Section_1_3_4
 import Analysis.MeasureTheory.Section_1_3_5
+
+/-!
+ The files in this directory contain a formalization of selected portions of my text [Analysis I](https://terrytao.wordpress.com/books/analysis-i/) into [Lean](https://lean-lang.org/). The formalization is intended to be as faithful a paraphrasing as possible to the original text, while also showcasing Lean's features and syntax. In particular, the formalization is not optimized for efficiency, and in some cases may deviate from idiomatic Lean usage.
+
+Portions of the text that were left as exercises to the reader are rendered in this translation as sorrys. Readers are welcome to fork the repository here to try their hand at these exercises, but I do not intend to place solutions in this repository directly.
+
+While the arrangement of definitions, theorems, and proofs here are closely paraphrasing the textbook, I am refraining from directly quoting material from the textbook, instead providing references to the original text where appropriate. As such, this formalization should be viewed as an annotated companion to the primary text, rather than a replacement for it.
+
+Much of the material in this text is duplicated in Lean's standard math library [Mathlib](https://leanprover-community.github.io/mathlib4_docs/), though with slightly different definitions. To reconcile these discrepancies, this formalization will gradually transition from the textbook-provided definitions to the Mathlib-provided definitions as one progresses further into the text, thus sacrificing the self-containedness of the formalization in favor of compatibility with Mathlib. For instance, Chapter 2 develops a theory of the natural numbers independent of Mathlib, but all subsequent chapters will use the Mathlib natural numbers instead. (An epilogue to Chapter 2 is provided to show that the two notions of the natural numbers are isomorphic.) As such, this formalization can also be used as an introduction to various portions of Mathlib.
+
+In order to align the formalization with Mathlib conventions, a small number of technical changes have been made to some of the definitions as compared with the textbook version. Most notably:
+
+    Sequences are indexed to start from zero rather than from one, as Mathlib has much more support for the 0-based natural numbers ℕ than the 1-based natural numbers.
+
+    Many operations that are left undefined in the text, such as division by zero, or taking the formal limit of a non-Cauchy sequence, are instead assigned a "junk" value (e.g., 0) to make the operation totally defined. This is because Lean has better support for total functions than partial functions (indiscriminate use of the latter can lead into "dependent type hell" in which even very basic manipulations require quite subtle and delicate proofs). See for instance [this blog post](https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/) by Kevin Buzzard for more discussion.
+
+[*Generated documentation*](docs/) is available for the project and its dependencies.
+-/

analysis/Analysis/Appendix_A_1.lean → Analysis/Appendix_A_1.lean

@@ -186,14 +186,14 @@ example {X Y Z:Prop} (hXY: X ↔ Y) (hXZ: X ↔ Z) : [X,Y,Z].TFAE := by
   tfae_have 1 ↔ 3 := by exact hXZ  -- This line is optional
   tfae_finish
 
-/-- Note for the `.out` method that one indexes starting from 0, in contrast to the `tfae_have` tactic. -/
+/-- Note for the {name (full := List.TFAE.out)}`out` method that one indexes starting from 0, in contrast to the {tactic}`tfae_have` tactic. -/
 example {X Y Z:Prop} (h: [X,Y,Z].TFAE) : X ↔ Y := by
   exact h.out 0 1
 
-/-- Exercise A.1.1.  Fill in the first `sorry` with something reasonable. -/
+/-- Exercise A.1.1.  Fill in the first {syntax term}`sorry` with something reasonable. -/
 example {X Y:Prop} : ¬ ((X ∨ Y) ∧ ¬ (X ∧ Y)) ↔ sorry := by sorry
 
-/-- Exercise A.1.2.  Fill in the first `sorry` with something reasonable. -/
+/-- Exercise A.1.2.  Fill in the first {syntax term}`sorry` with something reasonable. -/
 example {X Y:Prop} : ¬ (X ↔ Y) ↔ sorry := by sorry
 
 /-- Exercise A.1.3. -/

analysis/Analysis/Appendix_B_1.lean → Analysis/Appendix_B_1.lean

@@ -3,9 +3,9 @@ import Mathlib.Tactic
 /-!
 # Analysis I, Appendix B.1: The decimal representation of natural numbers
 
-Am implementation of the decimal representation of Mathlib's natural numbers `ℕ`.
+Am implementation of the decimal representation of Mathlib's natural numbers {lean}`ℕ`.
 
-This is separate from the way decimal numerals are already represenated in Mathlib via the `OfNat` typeclass.
+This is separate from the way decimal numerals are already represenated in Mathlib via the {name}`OfNat` typeclass.
 -/
 
 namespace AppendixB
@@ -154,7 +154,7 @@ theorem PosintDecimal.pos (p:PosintDecimal) : 0 < (p:ℕ) := by
 abbrev PosintDecimal.append (p:PosintDecimal) (d:Digit) : PosintDecimal :=
   mk' p.head (p.digits.tail ++ [d]) p.head_ne_zero
 
-/-- `toNat` equals Horner (left-fold) evaluation of the digit list. -/
+/-- {name}`toNat` equals Horner (left-fold) evaluation of the digit list. -/
 theorem PosintDecimal.toNat_eq_foldl (q : PosintDecimal) :
     q.toNat = q.digits.foldl (fun acc (d : Digit) => acc * 10 + d.toNat) 0 := by
   suffices h : ∀ (L : List Digit) (acc : ℕ),

analysis/Analysis/Appendix_B_2.lean → Analysis/Appendix_B_2.lean

@@ -4,10 +4,10 @@ import Analysis.Appendix_B_1
 /-!
 # Analysis I, Appendix B.2: The decimal representation of real numbers
 
-An implementation of the decimal representation of Mathlib's real numbers `ℝ`.
+An implementation of the decimal representation of Mathlib's real numbers {lean}`ℝ`.
 
-This is separate from the way decimal numerals are already represented in Mathlib.  We also represent the integer part of the natural numbers just by `ℕ`, avoiding using the decimal representation from the
-previous section, although we still retain the `Digit` class.
+This is separate from the way decimal numerals are already represented in Mathlib.  We also represent the integer part of the natural numbers just by {lean}`ℕ`, avoiding using the decimal representation from the
+previous section, although we still retain the {name}`AppendixB.Digit` class.
 -/
 
 namespace AppendixB

analysis/Analysis/MeasureTheory/Notation.lean → Analysis/MeasureTheory/Notation.lean

@@ -5,12 +5,12 @@ import Mathlib.Tactic
 
 A companion to Chapter 0 of the book "An introduction to Measure Theory".
 
-We use existing Mathlib constructions, such as `Set.indicator`, `EuclideanSpace`, `ENNReal`,
-and `tsum` to describe the concepts defined in Chapter 0.
+We use existing Mathlib constructions, such as {name}`Set.indicator`, {name}`EuclideanSpace`, {name}`ENNReal`,
+and {name}`tsum` to describe the concepts defined in Chapter 0.
 
 -/
 
-/-- A version of `Set.indicator` suitable for this text. -/
+/-- A version of {name}`Set.indicator` suitable for this text. -/
 noncomputable abbrev Set.indicator' {X: Type*} (E: Set X) := indicator E (fun _ ↦ (1:ℝ))
 
 theorem Set.indicator'_apply {X: Type*} (E: Set X) (x: X) [Decidable (x ∈ E)] : indicator' E x = if x ∈ E then 1 else 0 := indicator_apply _ _ _
@@ -21,7 +21,7 @@ theorem Set.indicator'_of_mem {X: Type*} {E:Set X} {x:X} (h: x ∈ E) : indicato
 theorem Set.indicator'_of_notMem {X: Type*} {E:Set X} {x:X} (h: x ∉ E) : indicator' E x = 0 :=
   indicator_of_notMem h _
 
-/-- A version of `EuclideanSpace` suitable for this text. -/
+/-- A version of {name}`EuclideanSpace` suitable for this text. -/
 noncomputable abbrev EuclideanSpace' (n: ℕ) := EuclideanSpace ℝ (Fin n)
 
 abbrev EuclideanSpace'.equiv_Real : EuclideanSpace' 1 ≃ ℝ where