Verso migration

.github/workflows/workflows/build_book.yml

@@ -0,0 +1,84 @@
+name: Build book
+
+on:
+  push:
+    branches:
+    - main
+  pull_request:
+  workflow_dispatch:
+
+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
+
+      - name: Get Mathlib cache
+        run: ~/.elan/bin/lake exe cache get || true
+        working-directory: ./analysis
+
+      - name: Cache mathlib API docs
+        uses: actions/cache@v4
+        with:
+          path: |
+            ./analysis/.lake/build/doc/Init
+            ./analysis/.lake/build/doc/Lake
+            ./analysis/.lake/build/doc/Lean
+            ./analysis/.lake/build/doc/Std
+            ./analysis/.lake/build/doc/Mathlib
+            ./analysis/.lake/build/doc/declarations
+            ./analysis/.lake/build/doc/find
+            ./analysis/.lake/build/doc/*.*
+            !./analysis/.lake/build/doc/declarations/declaration-data-Analysis*
+          key: MathlibDoc-${{ hashFiles('lake-manifest.json') }}
+          restore-keys: MathlibDoc-
+
+      - name: Build doc-gen
+        run: ~/.elan/bin/lake -R -Kenv=dev build Analysis:docs
+        working-directory: ./analysis
+
+      - name: Build book
+        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`
+        run: |
+          find _site/docs -name "*.trace" -delete
+          find _site/docs -name "*.hash" -delete
+      - name: Upload website
+        uses: actions/upload-pages-artifact@v3
+        with:
+          path: './book/_site'
+  deploy:
+    # Add a dependency to the build job
+    needs: build
+
+    # Grant GITHUB_TOKEN the permissions required to make a Pages deployment
+    permissions:
+      pages: write      # to deploy to Pages
+      id-token: write   # to verify the deployment originates from an appropriate source
+
+    # Deploy to the github-pages environment
+    environment:
+      name: github-pages
+      url: ${{ steps.deployment.outputs.page_url }}
+
+    # Specify runner + deployment step
+    runs-on: ubuntu-latest
+    if: github.ref == 'refs/heads/main'
+    steps:
+      - name: Deploy to GitHub Pages
+        id: deployment
+        uses: actions/deploy-pages@v4

.gitignore

@@ -2,6 +2,7 @@
 # Compiled files and directories
 .lake/
 build/
+_site/
 
 # IDE files
 .vscode/

CONTRIBUTING.md

@@ -0,0 +1,23 @@
+# Contributing
+
+I would be interested in having volunteers “playtest” the companion to see if this can actually be done (and if the helper lemmas or “API” provided in the Lean files are sufficient to fill in the sorries in a conceptually straightforward manner without having to rely on more esoteric Lean programming techniques). Any other feedback will of course also be welcome.
+
+# Building the book locally
+
+Change directory to `analysis`
+Build the doc-gen
+```
+lake exe Analysis:docs
+```
+
+Change the working directory to `./book/`
+Build:
+```
+lake exe analysis-book
+```
+
+View the book:
+```
+python3 serve.py
+```
+then visit `http://localhost:8000`

README.md

@@ -14,18 +14,18 @@ In order to align the formalization with Mathlib conventions, a small number of
 
 Currently formalized sections:
 
-- [Section 2.1: The Peano axioms](https://teorth.github.io/analysis/docs/Analysis/Section_2_1.html)
-- [Section 2.2: Addition](https://teorth.github.io/analysis/docs/Analysis/Section_2_2.html)
-- [Section 2.3: Multiplication](https://teorth.github.io/analysis/docs/Analysis/Section_2_3.html)
-- [Chapter 2 epilogue: Isomorphism with the Mathlib natural numbers](https://teorth.github.io/analysis/docs/Analysis/Section_2_epilogue.html)
-- [Section 3.1: Set theory fundamentals](https://teorth.github.io/analysis/docs/Analysis/Section_3_1.html)
-- [Section 4.1: The integers](https://teorth.github.io/analysis/docs/Analysis/Section_4_1.html)
-- [Section 4.2: The rationals](https://teorth.github.io/analysis/docs/Analysis/Section_4_2.html)
-- [Section 4.3: Absolute value and exponentiation](https://teorth.github.io/analysis/docs/Analysis/Section_4_3.html)
-- [Section 5.1: Cauchy sequences of rationals](https://teorth.github.io/analysis/docs/Analysis/Section_5_1.html)
-- [Section 5.2: Equivalent Cauchy sequences](https://teorth.github.io/analysis/docs/Analysis/Section_5_2.html)
-- [Section 5.3: Construction of the real numbers](https://teorth.github.io/analysis/docs/Analysis/Section_5_3.html)
-- [Section 5.4: Ordering the reals](https://teorth.github.io/analysis/docs/Analysis/Section_5_4.html)
+- [Section 2.1: The Peano axioms](https://teorth.github.io/analysis/sec21/)
+- [Section 2.2: Addition](https://teorth.github.io/analysis/sec22/)
+- [Section 2.3: Multiplication](https://teorth.github.io/analysis/sec23/)
+- [Chapter 2 epilogue: Isomorphism with the Mathlib natural numbers](https://teorth.github.io/analysis/sec2e/)
+- [Section 3.1: Set theory fundamentals](https://teorth.github.io/analysis/sec31/)
+- [Section 4.1: The integers](https://teorth.github.io/analysis/sec41/)
+- [Section 4.2: The rationals](https://teorth.github.io/analysis/sec42/)
+- [Section 4.3: Absolute value and exponentiation](https://teorth.github.io/analysis/sec43/)
+- [Section 5.1: Cauchy sequences of rationals](https://teorth.github.io/analysis/sec51/)
+- [Section 5.2: Equivalent Cauchy sequences](https://teorth.github.io/analysis/sec52/)
+- [Section 5.3: Construction of the real numbers](https://teorth.github.io/analysis/sec53/)
+- [Section 5.4: Ordering the reals](https://teorth.github.io/analysis/sec54/)
 
 
 Other resources:
@@ -34,6 +34,7 @@ Other resources:
   - [Springer edition](https://link.springer.com/book/10.1007/978-981-19-7261-4)
 - [Blog post announcing this project](https://terrytao.wordpress.com/2025/05/31/a-lean-companion-to-analysis-i/), Terence Tao, May 31 2025.
 - [Lean Zulip discussion about this project](https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Lean.20companion.20to.20.22Analysis.20I.22.20-.20discussion/with/521458888)
+- [Notes for contributors](./CONTRIBUTING.md)
 
 General Lean resources:
 - [The Lean community](https://leanprover-community.github.io/)

Analysis.lean → analysis/Analysis.lean

@@ -1,5 +1,3 @@
--- This module serves as the root of the `Analysis` library.
--- Import modules here that should be built as part of the library.
 import Analysis.Section_2_1
 import Analysis.Section_2_2
 import Analysis.Section_2_3
@@ -11,3 +9,4 @@ import Analysis.Section_4_3
 import Analysis.Section_5_1
 import Analysis.Section_5_2
 import Analysis.Section_5_3
+import Analysis.Section_5_4