From d724bfb8f42f5efb1cfd4b80594e6b8ce683041a Mon Sep 17 00:00:00 2001 From: Pim Otte Date: Fri, 6 Jun 2025 16:10:58 +0200 Subject: [PATCH 1/4] Main migration --- .github/workflows/blueprint.yml | 136 --------- .github/workflows/workflows/build_book.yml | 84 +++++ .gitignore | 1 + CONTRIBUTING.md | 23 ++ README.md | 1 + Analysis.lean => analysis/Analysis.lean | 3 +- .../Analysis}/Section_2_1.lean | 0 .../Analysis}/Section_2_2.lean | 0 .../Analysis}/Section_2_3.lean | 0 .../Analysis}/Section_2_epilogue.lean | 0 .../Analysis}/Section_3_1.lean | 0 .../Analysis}/Section_4_1.lean | 0 .../Analysis}/Section_4_2.lean | 0 .../Analysis}/Section_4_3.lean | 0 .../Analysis}/Section_5_1.lean | 0 .../Analysis}/Section_5_2.lean | 0 .../Analysis}/Section_5_3.lean | 0 .../Analysis}/Section_5_4.lean | 0 .../lake-manifest.json | 126 +++----- analysis/lakefile.lean | 27 ++ analysis/lean-toolchain | 1 + blueprint/src/blueprint.sty | 2 - blueprint/src/content.tex | 7 - blueprint/src/extra_styles.css | 25 -- blueprint/src/latexmkrc | 5 - blueprint/src/macros/common.tex | 18 -- blueprint/src/macros/print.tex | 29 -- blueprint/src/macros/web.tex | 5 - blueprint/src/plastex.cfg | 17 -- blueprint/src/print.tex | 33 -- blueprint/src/web.tex | 27 -- book/AnalysisBook.lean | 75 +++++ book/AnalysisBook/Home.lean | 30 ++ book/lake-manifest.json | 35 +++ book/lakefile.lean | 14 + book/lean-toolchain | 1 + book/static_files/style.css | 44 +++ home_page/404.html | 25 -- home_page/Gemfile | 25 -- home_page/Gemfile.lock | 287 ------------------ home_page/_config.yml | 34 --- home_page/_include/mathjax.html | 17 -- home_page/_layouts/default.html | 50 --- home_page/assets/css/style.scss | 9 - home_page/index.md | 15 - lakefile.lean | 51 ---- lean-toolchain | 1 - serve.py | 30 ++ 48 files changed, 410 insertions(+), 903 deletions(-) delete mode 100644 .github/workflows/blueprint.yml create mode 100644 .github/workflows/workflows/build_book.yml create mode 100644 CONTRIBUTING.md rename Analysis.lean => analysis/Analysis.lean (70%) rename {Analysis => analysis/Analysis}/Section_2_1.lean (100%) rename {Analysis => analysis/Analysis}/Section_2_2.lean (100%) rename {Analysis => analysis/Analysis}/Section_2_3.lean (100%) rename {Analysis => analysis/Analysis}/Section_2_epilogue.lean (100%) rename {Analysis => analysis/Analysis}/Section_3_1.lean (100%) rename {Analysis => analysis/Analysis}/Section_4_1.lean (100%) rename {Analysis => analysis/Analysis}/Section_4_2.lean (100%) rename {Analysis => analysis/Analysis}/Section_4_3.lean (100%) rename {Analysis => analysis/Analysis}/Section_5_1.lean (100%) rename {Analysis => analysis/Analysis}/Section_5_2.lean (100%) rename {Analysis => analysis/Analysis}/Section_5_3.lean (100%) rename {Analysis => analysis/Analysis}/Section_5_4.lean (100%) rename lake-manifest.json => analysis/lake-manifest.json (61%) create mode 100644 analysis/lakefile.lean create mode 100644 analysis/lean-toolchain delete mode 100644 blueprint/src/blueprint.sty delete mode 100644 blueprint/src/content.tex delete mode 100644 blueprint/src/extra_styles.css delete mode 100644 blueprint/src/latexmkrc delete mode 100644 blueprint/src/macros/common.tex delete mode 100644 blueprint/src/macros/print.tex delete mode 100644 blueprint/src/macros/web.tex delete mode 100644 blueprint/src/plastex.cfg delete mode 100644 blueprint/src/print.tex delete mode 100644 blueprint/src/web.tex create mode 100644 book/AnalysisBook.lean create mode 100644 book/AnalysisBook/Home.lean create mode 100644 book/lake-manifest.json create mode 100644 book/lakefile.lean create mode 100644 book/lean-toolchain create mode 100644 book/static_files/style.css delete mode 100644 home_page/404.html delete mode 100644 home_page/Gemfile delete mode 100644 home_page/Gemfile.lock delete mode 100644 home_page/_config.yml delete mode 100644 home_page/_include/mathjax.html delete mode 100644 home_page/_layouts/default.html delete mode 100644 home_page/assets/css/style.scss delete mode 100644 home_page/index.md delete mode 100644 lakefile.lean delete mode 100644 lean-toolchain create mode 100644 serve.py diff --git a/.github/workflows/blueprint.yml b/.github/workflows/blueprint.yml deleted file mode 100644 index d0287232..00000000 --- a/.github/workflows/blueprint.yml +++ /dev/null @@ -1,136 +0,0 @@ -name: Compile blueprint - -on: - pull_request: - push: - branches: - - main # Trigger on pushes to the default branch - workflow_dispatch: # Allow manual triggering of the workflow from the GitHub Actions interface - -# Cancel previous runs if a new commit is pushed to the same PR or branch -concurrency: - group: ${{ github.ref }} # Group runs by the ref (branch or PR) - cancel-in-progress: true # Cancel any ongoing runs in the same group - -# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages -permissions: - contents: read # Read access to repository contents - pages: write # Write access to GitHub Pages - id-token: write # Write access to ID tokens - -jobs: - build_project: - runs-on: ubuntu-latest - name: Build project - steps: - - name: Checkout project - uses: actions/checkout@v4 - with: - fetch-depth: 0 # Fetch all history for all branches and tags - - - 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 - - - name: Build project - run: ~/.elan/bin/lake build Analysis - - - name: Cache mathlib API docs - uses: actions/cache@v4 - with: - path: | - .lake/build/doc/Init - .lake/build/doc/Lake - .lake/build/doc/Lean - .lake/build/doc/Std - .lake/build/doc/Mathlib - .lake/build/doc/declarations - .lake/build/doc/find - .lake/build/doc/*.* - !.lake/build/doc/declarations/declaration-data-Analysis* - key: MathlibDoc-${{ hashFiles('lake-manifest.json') }} - restore-keys: MathlibDoc- - - - name: Build project API documentation - run: ~/.elan/bin/lake -R -Kenv=dev build Analysis:docs - - - name: Check for `home_page` folder # this is meant to detect a Jekyll-based website - if: github.event_name != 'pull_request' - id: check_home_page - run: | - if [ -d home_page ]; then - echo "The 'home_page' folder exists in the repository." - echo "HOME_PAGE_EXISTS=true" >> $GITHUB_ENV - else - echo "The 'home_page' folder does not exist in the repository." - echo "HOME_PAGE_EXISTS=false" >> $GITHUB_ENV - fi - - - name: Build blueprint and copy to `home_page/blueprint` - if: github.event_name != 'pull_request' - uses: xu-cheng/texlive-action@v2 - with: - docker_image: ghcr.io/xu-cheng/texlive-full:20250101 - run: | - # Install necessary dependencies and build the blueprint - apk update - apk add --update make py3-pip git pkgconfig graphviz graphviz-dev gcc musl-dev - git config --global --add safe.directory $GITHUB_WORKSPACE - git config --global --add safe.directory `pwd` - python3 -m venv env - source env/bin/activate - pip install --upgrade pip requests wheel - pip install pygraphviz --global-option=build_ext --global-option="-L/usr/lib/graphviz/" --global-option="-R/usr/lib/graphviz/" - pip install leanblueprint - leanblueprint pdf - mkdir -p home_page - cp blueprint/print/print.pdf home_page/blueprint.pdf - leanblueprint web - cp -r blueprint/web home_page/blueprint - - - name: Check declarations mentioned in the blueprint exist in Lean code - if: github.event_name != 'pull_request' - run: | - ~/.elan/bin/lake exe checkdecls blueprint/lean_decls - - - name: Copy API documentation to `home_page/docs` - if: github.event_name != 'pull_request' - run: cp -r .lake/build/doc home_page/docs - - - name: Remove unnecessary lake files from documentation in `home_page/docs` - if: github.event_name != 'pull_request' - run: | - find home_page/docs -name "*.trace" -delete - find home_page/docs -name "*.hash" -delete - - - name: Bundle dependencies - if: github.event_name != 'pull_request' - uses: ruby/setup-ruby@v1 - with: - working-directory: home_page - ruby-version: "3.0" # Specify Ruby version - bundler-cache: true # Enable caching for bundler - - - name: Build website using Jekyll - if: github.event_name != 'pull_request' && env.HOME_PAGE_EXISTS == 'true' - working-directory: home_page - env: - JEKYLL_GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} - run: JEKYLL_ENV=production bundle exec jekyll build # Note this will also copy the blueprint and API doc into home_page/_site - - - name: "Upload website (API documentation, blueprint and any home page)" - if: github.event_name != 'pull_request' - uses: actions/upload-pages-artifact@v3 - with: - path: ${{ env.HOME_PAGE_EXISTS == 'true' && 'home_page/_site' || 'home_page/' }} - - - name: Deploy to GitHub Pages - if: github.event_name != 'pull_request' - id: deployment - uses: actions/deploy-pages@v4 - - - name: Make sure the API documentation cache works - if: github.event_name != 'pull_request' - run: mv home_page/docs .lake/build/doc diff --git a/.github/workflows/workflows/build_book.yml b/.github/workflows/workflows/build_book.yml new file mode 100644 index 00000000..f76a1990 --- /dev/null +++ b/.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 diff --git a/.gitignore b/.gitignore index c93dfd53..f8b2b0d1 100644 --- a/.gitignore +++ b/.gitignore @@ -2,6 +2,7 @@ # Compiled files and directories .lake/ build/ +_site/ # IDE files .vscode/ diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md new file mode 100644 index 00000000..a65ab7ec --- /dev/null +++ b/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` \ No newline at end of file diff --git a/README.md b/README.md index 17a1113c..f4463ee4 100644 --- a/README.md +++ b/README.md @@ -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/) diff --git a/Analysis.lean b/analysis/Analysis.lean similarity index 70% rename from Analysis.lean rename to analysis/Analysis.lean index 3c2b548a..abd4319b 100644 --- a/Analysis.lean +++ b/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 diff --git a/Analysis/Section_2_1.lean b/analysis/Analysis/Section_2_1.lean similarity index 100% rename from Analysis/Section_2_1.lean rename to analysis/Analysis/Section_2_1.lean diff --git a/Analysis/Section_2_2.lean b/analysis/Analysis/Section_2_2.lean similarity index 100% rename from Analysis/Section_2_2.lean rename to analysis/Analysis/Section_2_2.lean diff --git a/Analysis/Section_2_3.lean b/analysis/Analysis/Section_2_3.lean similarity index 100% rename from Analysis/Section_2_3.lean rename to analysis/Analysis/Section_2_3.lean diff --git a/Analysis/Section_2_epilogue.lean b/analysis/Analysis/Section_2_epilogue.lean similarity index 100% rename from Analysis/Section_2_epilogue.lean rename to analysis/Analysis/Section_2_epilogue.lean diff --git a/Analysis/Section_3_1.lean b/analysis/Analysis/Section_3_1.lean similarity index 100% rename from Analysis/Section_3_1.lean rename to analysis/Analysis/Section_3_1.lean diff --git a/Analysis/Section_4_1.lean b/analysis/Analysis/Section_4_1.lean similarity index 100% rename from Analysis/Section_4_1.lean rename to analysis/Analysis/Section_4_1.lean diff --git a/Analysis/Section_4_2.lean b/analysis/Analysis/Section_4_2.lean similarity index 100% rename from Analysis/Section_4_2.lean rename to analysis/Analysis/Section_4_2.lean diff --git a/Analysis/Section_4_3.lean b/analysis/Analysis/Section_4_3.lean similarity index 100% rename from Analysis/Section_4_3.lean rename to analysis/Analysis/Section_4_3.lean diff --git a/Analysis/Section_5_1.lean b/analysis/Analysis/Section_5_1.lean similarity index 100% rename from Analysis/Section_5_1.lean rename to analysis/Analysis/Section_5_1.lean diff --git a/Analysis/Section_5_2.lean b/analysis/Analysis/Section_5_2.lean similarity index 100% rename from Analysis/Section_5_2.lean rename to analysis/Analysis/Section_5_2.lean diff --git a/Analysis/Section_5_3.lean b/analysis/Analysis/Section_5_3.lean similarity index 100% rename from Analysis/Section_5_3.lean rename to analysis/Analysis/Section_5_3.lean diff --git a/Analysis/Section_5_4.lean b/analysis/Analysis/Section_5_4.lean similarity index 100% rename from Analysis/Section_5_4.lean rename to analysis/Analysis/Section_5_4.lean diff --git a/lake-manifest.json b/analysis/lake-manifest.json similarity index 61% rename from lake-manifest.json rename to analysis/lake-manifest.json index 253663f2..c253c106 100644 --- a/lake-manifest.json +++ b/analysis/lake-manifest.json @@ -1,145 +1,105 @@ {"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover/doc-gen4", + [{"url": "https://github.com/leanprover/subverso.git", "type": "git", "subDir": null, "scope": "", - "rev": "efe744c75a6ab384619513b9762db1cfc40b0fe4", - "name": "«doc-gen4»", + "rev": "9ff8c4e0d9912170d5cfc2e5067231d5f6eaac3c", + "name": "subverso", "manifestFile": "lake-manifest.json", - "inputRev": "v4.20.0", - "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/PatrickMassot/checkdecls.git", - "type": "git", - "subDir": null, - "scope": "", - "rev": "3d425859e73fcfbef85b9638c2a91708ef4a22d4", - "name": "checkdecls", - "manifestFile": "lake-manifest.json", - "inputRev": null, + "inputRev": "main", "inherited": false, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/quote4", + {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, "scope": "", - "rev": "2865ea099ab1dd8d6fc93381d77a4ac87a85527a", - "name": "Qq", + "rev": "c211948581bde9846a99e32d97a03f0d5307c31e", + "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "v4.20.0", "inherited": false, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/ProofWidgets4.git", - "type": "git", - "subDir": null, - "scope": "", - "rev": "21e6a0522cd2ae6cf88e9da99a1dd010408ab306", - "name": "proofwidgets", - "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.60", - "inherited": false, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/plausible.git", + {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, - "scope": "", + "scope": "leanprover-community", "rev": "2ac43674e92a695e96caac19f4002b25434636da", "name": "plausible", "manifestFile": "lake-manifest.json", - "inputRev": "v4.20.0", - "inherited": false, + "inputRev": "main", + "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/mathlib4.git", + {"url": "https://github.com/leanprover-community/LeanSearchClient", "type": "git", "subDir": null, - "scope": "", - "rev": "c211948581bde9846a99e32d97a03f0d5307c31e", - "name": "mathlib", + "scope": "leanprover-community", + "rev": "6c62474116f525d2814f0157bb468bf3a4f9f120", + "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", - "inputRev": "v4.20.0", - "inherited": false, - "configFile": "lakefile.lean"}, + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/import-graph", "type": "git", "subDir": null, - "scope": "", + "scope": "leanprover-community", "rev": "a11bcb5238149ae5d8a0aa5e2f8eddf8a3a9b27d", "name": "importGraph", "manifestFile": "lake-manifest.json", - "inputRev": "v4.20.0", - "inherited": false, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/batteries", - "type": "git", - "subDir": null, - "scope": "", - "rev": "7a0d63fbf8fd350e891868a06d9927efa545ac1e", - "name": "batteries", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.20.0", - "inherited": false, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/mhuisi/lean4-cli", - "type": "git", - "subDir": null, - "scope": "", - "rev": "4f22c09e7ded721e6ecd3cf59221c4647ca49664", - "name": "Cli", - "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/fgdorais/lean4-unicode-basic", + {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, - "scope": "", - "rev": "45c426d1cb016fcb4fcbe043f1cd2d97acb2dbc3", - "name": "UnicodeBasic", + "scope": "leanprover-community", + "rev": "21e6a0522cd2ae6cf88e9da99a1dd010408ab306", + "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v0.0.60", "inherited": true, "configFile": "lakefile.lean"}, - {"url": "https://github.com/dupuisf/BibtexQuery", + {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "scope": "", - "rev": "dbfe2b7630c5f7c5c1cf71e7747ffc0a30337f69", - "name": "BibtexQuery", + "scope": "leanprover-community", + "rev": "ddfca7829bf8aa4083cdf9633935dddbb28b7b2a", + "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/acmepjz/md4lean", + {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, - "scope": "", - "rev": "8ba0ef10d178ab95a5d6fe3cfbd586c6ecef2717", - "name": "MD4Lean", + "scope": "leanprover-community", + "rev": "2865ea099ab1dd8d6fc93381d77a4ac87a85527a", + "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "master", "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/LeanSearchClient", + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6c62474116f525d2814f0157bb468bf3a4f9f120", - "name": "LeanSearchClient", + "rev": "7a0d63fbf8fd350e891868a06d9927efa545ac1e", + "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/aesop", + {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, - "scope": "leanprover-community", - "rev": "ddfca7829bf8aa4083cdf9633935dddbb28b7b2a", - "name": "aesop", + "scope": "leanprover", + "rev": "f9e25dcbed001489c53bceeb1f1d50bbaf7451d4", + "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}], - "name": "analysis", + "name": "Analysis", "lakeDir": ".lake"} diff --git a/analysis/lakefile.lean b/analysis/lakefile.lean new file mode 100644 index 00000000..a8ac2eea --- /dev/null +++ b/analysis/lakefile.lean @@ -0,0 +1,27 @@ +import Lake +open Lake DSL + +package «Analysis» where + -- Settings applied to both builds and interactive editing + leanOptions := #[ + ⟨`pp.unicode.fun, true⟩ -- pretty-prints `fun a ↦ b` + ] + -- add any additional package configuration options here + +-- Require Mathlib (the comprehensive library of mathematics in Lean) +require mathlib from git + "https://github.com/leanprover-community/mathlib4.git" @ "v4.20.0" +-- Needed to build book +require subverso from git + "https://github.com/leanprover/subverso.git" @ "main" + + + +@[default_target] +lean_lib «Analysis» where + -- add any library configuration options here + + +meta if get_config? env = some "dev" then +require «doc-gen4» from git + "https://github.com/leanprover/doc-gen4" @ "v4.20.0" diff --git a/analysis/lean-toolchain b/analysis/lean-toolchain new file mode 100644 index 00000000..5e485899 --- /dev/null +++ b/analysis/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.20.0 \ No newline at end of file diff --git a/blueprint/src/blueprint.sty b/blueprint/src/blueprint.sty deleted file mode 100644 index 1353f398..00000000 --- a/blueprint/src/blueprint.sty +++ /dev/null @@ -1,2 +0,0 @@ -\DeclareOption*{} -\ProcessOptions \ No newline at end of file diff --git a/blueprint/src/content.tex b/blueprint/src/content.tex deleted file mode 100644 index b5cd27b9..00000000 --- a/blueprint/src/content.tex +++ /dev/null @@ -1,7 +0,0 @@ -% In this file you should put the actual content of the blueprint. -% It will be used both by the web and the print version. -% It should *not* include the \begin{document} -% -% If you want to split the blueprint content into several files then -% the current file can be a simple sequence of \input. Otherwise It -% can start with a \section or \chapter for instance. \ No newline at end of file diff --git a/blueprint/src/extra_styles.css b/blueprint/src/extra_styles.css deleted file mode 100644 index b96c7767..00000000 --- a/blueprint/src/extra_styles.css +++ /dev/null @@ -1,25 +0,0 @@ -/* This file contains CSS tweaks for this blueprint. - * As an example, we included CSS rules that put - * a vertical line on the left of theorem statements - * and proofs. - * */ - -div.theorem_thmcontent { - border-left: .15rem solid black; -} - -div.proposition_thmcontent { - border-left: .15rem solid black; -} - -div.lemma_thmcontent { - border-left: .1rem solid black; -} - -div.corollary_thmcontent { - border-left: .1rem solid black; -} - -div.proof_content { - border-left: .08rem solid grey; -} diff --git a/blueprint/src/latexmkrc b/blueprint/src/latexmkrc deleted file mode 100644 index 38d59630..00000000 --- a/blueprint/src/latexmkrc +++ /dev/null @@ -1,5 +0,0 @@ -# This file configures the latexmk command you can use to compile -# the pdf version of the blueprint -$pdf_mode = 1; -$pdflatex = 'xelatex -synctex=1'; -@default_files = ('print.tex'); \ No newline at end of file diff --git a/blueprint/src/macros/common.tex b/blueprint/src/macros/common.tex deleted file mode 100644 index 83d71e14..00000000 --- a/blueprint/src/macros/common.tex +++ /dev/null @@ -1,18 +0,0 @@ -% In this file you should put all LaTeX macros and settings to be used both by -% the pdf version and the web version. -% This should be most of your macros. - -% The theorem-like environments defined below are those that appear by default -% in the dependency graph. See the README of leanblueprint if you need help to -% customize this. -% The configuration below use the theorem counter for all those environments -% (this is what the [theorem] arguments mean) and never resets it. -% If you want for instance to number them within chapters then you can add -% [chapter] at the end of the next line. -\newtheorem{theorem}{Theorem} -\newtheorem{proposition}[theorem]{Proposition} -\newtheorem{lemma}[theorem]{Lemma} -\newtheorem{corollary}[theorem]{Corollary} - -\theoremstyle{definition} -\newtheorem{definition}[theorem]{Definition} \ No newline at end of file diff --git a/blueprint/src/macros/print.tex b/blueprint/src/macros/print.tex deleted file mode 100644 index 668fec13..00000000 --- a/blueprint/src/macros/print.tex +++ /dev/null @@ -1,29 +0,0 @@ -% In this file you should put macros to be used only by -% the printed version. Of course they should have a corresponding -% version in macros/web.tex. -% Typically the printed version could have more fancy decorations. -% This should be a very short file. -% -% This file starts with dummy macros that ensure the pdf -% compiler will ignore macros provided by plasTeX that make -% sense only for the web version, such as dependency graph -% macros. - - -% Dummy macros that make sense only for web version. -\newcommand{\lean}[1]{} -\newcommand{\discussion}[1]{} -\newcommand{\leanok}{} -\newcommand{\mathlibok}{} -\newcommand{\notready}{} -% Make sure that arguments of \uses and \proves are real labels, by using invisible refs: -% latex prints a warning if the label is not defined, but nothing is shown in the pdf file. -% It uses LaTeX3 programming, this is why we use the expl3 package. -\ExplSyntaxOn -\NewDocumentCommand{\uses}{m} - {\clist_map_inline:nn{#1}{\vphantom{\ref{##1}}}% - \ignorespaces} -\NewDocumentCommand{\proves}{m} - {\clist_map_inline:nn{#1}{\vphantom{\ref{##1}}}% - \ignorespaces} -\ExplSyntaxOff \ No newline at end of file diff --git a/blueprint/src/macros/web.tex b/blueprint/src/macros/web.tex deleted file mode 100644 index ceee9755..00000000 --- a/blueprint/src/macros/web.tex +++ /dev/null @@ -1,5 +0,0 @@ -% In this file you should put macros to be used only by -% the web version. Of course they should have a corresponding -% version in macros/print.tex. -% Typically the printed version could have more fancy decorations. -% This will probably be a very short file. \ No newline at end of file diff --git a/blueprint/src/plastex.cfg b/blueprint/src/plastex.cfg deleted file mode 100644 index de3dbae2..00000000 --- a/blueprint/src/plastex.cfg +++ /dev/null @@ -1,17 +0,0 @@ -[general] -renderer=HTML5 -copy-theme-extras=yes -plugins=plastexdepgraph plastexshowmore leanblueprint - -[document] -toc-depth=3 -toc-non-files=True - -[files] -directory=../web/ -split-level= 0 - -[html5] -localtoc-level=0 -extra-css=extra_styles.css -mathjax-dollars=False \ No newline at end of file diff --git a/blueprint/src/print.tex b/blueprint/src/print.tex deleted file mode 100644 index f230f867..00000000 --- a/blueprint/src/print.tex +++ /dev/null @@ -1,33 +0,0 @@ -% This file makes a printable version of the blueprint -% It should include all the \usepackage needed for the pdf version. -% The template version assume you want to use a modern TeX compiler -% such as xeLaTeX or luaLaTeX including support for unicode -% and Latin Modern Math font with standard bugfixes applied. -% It also uses expl3 in order to support macros related to the dependency graph. -% It also includes standard AMS packages (and their improved version -% mathtools) as well as support for links with a sober decoration -% (no ugly rectangles around links). -% It is otherwise a very minimal preamble (you should probably at least -% add cleveref and tikz-cd). - -\documentclass[a4paper]{report} - -\usepackage{geometry} - -\usepackage{expl3} - -\usepackage{amssymb, amsthm, mathtools} -\usepackage[unicode,colorlinks=true,linkcolor=blue,urlcolor=magenta, citecolor=blue]{hyperref} - -\usepackage[warnings-off={mathtools-colon,mathtools-overbracket}]{unicode-math} - -\input{macros/common} -\input{macros/print} - -\title{Analysis Lean companion} -\author{Terence Tao} - -\begin{document} -\maketitle -\input{content} -\end{document} \ No newline at end of file diff --git a/blueprint/src/web.tex b/blueprint/src/web.tex deleted file mode 100644 index 7c420dc1..00000000 --- a/blueprint/src/web.tex +++ /dev/null @@ -1,27 +0,0 @@ -% This file makes a web version of the blueprint -% It should include all the \usepackage needed for this version. -% The template includes standard AMS packages. -% It is otherwise a very minimal preamble (you should probably at least -% add cleveref and tikz-cd). - -\documentclass{report} - -\usepackage{amssymb, amsthm, amsmath} -\usepackage{hyperref} -\usepackage[showmore, dep_graph]{blueprint} - - -\input{macros/common} -\input{macros/web} - -\home{https://teorth.github.io/analysis} -\github{https://github.com/teorth/analysis} -\dochome{https://teorth.github.io/analysis/docs} - -\title{Analysis Lean companion} -\author{Terence Tao} - -\begin{document} -\maketitle -\input{content} -\end{document} \ No newline at end of file diff --git a/book/AnalysisBook.lean b/book/AnalysisBook.lean new file mode 100644 index 00000000..79913be9 --- /dev/null +++ b/book/AnalysisBook.lean @@ -0,0 +1,75 @@ + +import VersoBlog +import AnalysisBook.Home + +open Verso Genre Blog Site Syntax + +open Output Html Template Theme in +def theme : Theme := { Theme.default with + primaryTemplate := do + return {{ + + + + {{ (← param (α := String) "title") }} " — Verso " + + + {{← builtinHeader }} + + +
+
+ + +
+
+
+
+ {{ (← param "content") }} +
+
+ + + }} + } + |>.override #[] ⟨do return {{

{{← param "title"}}

{{← param "content"}}
}}, id⟩ + + + +def_literate_page sec21 from Analysis.Section_2_1 in "../analysis" as "The Peano Axioms" + +def_literate_page sec22 from Analysis.Section_2_2 in "../analysis" as "Addition" +def_literate_page sec23 from Analysis.Section_2_3 in "../analysis" as "Multiplication" +def_literate_page sec2e from Analysis.Section_2_epilogue in "../analysis" as "Equivalence of naturals" +def_literate_page sec31 from Analysis.Section_3_1 in "../analysis" as "Fundamentals" +def_literate_page sec41 from Analysis.Section_4_1 in "../analysis" as "The integers" +def_literate_page sec42 from Analysis.Section_4_2 in "../analysis" as "The rationals" +def_literate_page sec43 from Analysis.Section_4_3 in "../analysis" as "Absolute value and exponentiation" +def_literate_page sec51 from Analysis.Section_5_1 in "../analysis" as "Cauchy sequences" +def_literate_page sec52 from Analysis.Section_5_2 in "../analysis" as "Equivalent Cauchy sequences" +def_literate_page sec53 from Analysis.Section_5_3 in "../analysis" as "The construction of the real numbers" +def_literate_page sec54 from Analysis.Section_5_4 in "../analysis" as "Ordering the reals" + +def demoSite : Site := site AnalysisBook.Home / + static "static" ← "./static_files" + "sec21" sec21 + "sec22" sec22 + "sec23" sec23 + "sec2e" sec2e + "sec31" sec31 + "sec41" sec41 + "sec42" sec42 + "sec43" sec43 + "sec51" sec51 + "sec52" sec52 + "sec53" sec53 + "sec54" sec54 + + +def main := blogMain theme demoSite diff --git a/book/AnalysisBook/Home.lean b/book/AnalysisBook/Home.lean new file mode 100644 index 00000000..1af65c6d --- /dev/null +++ b/book/AnalysisBook/Home.lean @@ -0,0 +1,30 @@ +import VersoBlog +open Verso Genre Blog + +#doc (Page) " Partial Lean formalization of Analysis I" => + +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 `sorry`s. 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. + +Currently formalized sections: + +- [Section 2.1: The Peano axioms](./sec21/) +- [Section 2.2: Addition](./sec22/) +- [Section 2.3: Multiplication](./sec23/) +- [Chapter 2 epilogue: Isomorphism with the Mathlib natural numbers](./sec2e) +- [Section 3.1: Set theory fundamentals](./sec31/) +- [Section 4.1: The integers](./sec41/) +- [Section 4.2: The rationals](./sec42/) +- [Section 4.3: Absolute value and exponentiation](./sec43/) +- [Section 5.1: Cauchy sequences of rationals](./sec51) +- [Section 5.2: Equivalent Cauchy sequences](./sec52/) +- [Section 5.3: Construction of the real numbers](./sec53/) diff --git a/book/lake-manifest.json b/book/lake-manifest.json new file mode 100644 index 00000000..b1d90f4f --- /dev/null +++ b/book/lake-manifest.json @@ -0,0 +1,35 @@ +{"version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": + [{"url": "https://github.com/pimotte/verso.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "a71fb6d4153ff528186aef3df20732076f71509f", + "name": "verso", + "manifestFile": "lake-manifest.json", + "inputRev": "analysis", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/acmepjz/md4lean", + "type": "git", + "subDir": null, + "scope": "", + "rev": "8ba0ef10d178ab95a5d6fe3cfbd586c6ecef2717", + "name": "MD4Lean", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover/subverso.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "a3e5c4c50791e536fc7f13a7aadd6236091796f9", + "name": "subverso", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}], + "name": "«analysis-book»", + "lakeDir": ".lake"} diff --git a/book/lakefile.lean b/book/lakefile.lean new file mode 100644 index 00000000..b04ec18b --- /dev/null +++ b/book/lakefile.lean @@ -0,0 +1,14 @@ +import Lake +open Lake DSL + +require verso from git "https://github.com/pimotte/verso.git"@"analysis" + +package "analysis-book" where + version := v!"0.1.0" + +lean_lib «AnalysisBook» where + -- add library configuration options here + +@[default_target] +lean_exe "analysis-book" where + root := `AnalysisBook diff --git a/book/lean-toolchain b/book/lean-toolchain new file mode 100644 index 00000000..cfb5ca96 --- /dev/null +++ b/book/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.20.0-rc2 \ No newline at end of file diff --git a/book/static_files/style.css b/book/static_files/style.css new file mode 100644 index 00000000..8999664e --- /dev/null +++ b/book/static_files/style.css @@ -0,0 +1,44 @@ +nav { + position: fixed; + top: 0; + left: 0; + width: 14em; + height: 100vh; + background: #f7f7fa; + border-right: 1px solid #ddd; + padding: 2em 1em 1em 1em; + box-sizing: border-box; + overflow-y: auto; + z-index: 100; +} + +nav ol { + list-style: none; + padding: 0; + margin: 0; +} + +nav ol li { + margin-bottom: 1em; +} + +nav ol li a { + display: block; + color: #222; + text-decoration: none; + padding: 0.5em 0.75em; + border-radius: 4px; + transition: background 0.2s; +} + +nav ol li a:hover, +nav ol li a:focus { + background: #e0e0f0; + color: #000; +} + +/* Add left margin to main content to avoid overlap */ +header, +div.main { + margin-left: 16em; +} diff --git a/home_page/404.html b/home_page/404.html deleted file mode 100644 index fcebf3fc..00000000 --- a/home_page/404.html +++ /dev/null @@ -1,25 +0,0 @@ ---- -permalink: /404.html -layout: default ---- - - - -
-

404

- -

Page not found :(

-

The requested page could not be found.

-
\ No newline at end of file diff --git a/home_page/Gemfile b/home_page/Gemfile deleted file mode 100644 index 78763738..00000000 --- a/home_page/Gemfile +++ /dev/null @@ -1,25 +0,0 @@ -source "https://rubygems.org" - -# To upgrade, run `bundle update github-pages`. -gem "github-pages", group: :jekyll_plugins -# If you have any plugins, put them here! -group :jekyll_plugins do - #gem "jekyll-feed", "~> 0.12" -end - -# Windows and JRuby does not include zoneinfo files, so bundle the tzinfo-data gem -# and associated library. -platforms :mingw, :x64_mingw, :mswin, :jruby do - gem "tzinfo", "~> 1.2" - gem "tzinfo-data" -end - -# Performance-booster for watching directories on Windows. -gem "wdm", "~> 0.1.1", :platforms => [:mingw, :x64_mingw, :mswin] - -# Lock `http_parser.rb` gem to `v0.6.x` on JRuby builds since newer versions of the gem -# do not have a Java counterpart. -gem "http_parser.rb", "~> 0.6.0", :platforms => [:jruby] - -# Used for locally serving the website. -gem "webrick", "~> 1.7" \ No newline at end of file diff --git a/home_page/Gemfile.lock b/home_page/Gemfile.lock deleted file mode 100644 index 5436ad6b..00000000 --- a/home_page/Gemfile.lock +++ /dev/null @@ -1,287 +0,0 @@ -GEM - remote: https://rubygems.org/ - specs: - activesupport (6.0.5) - concurrent-ruby (~> 1.0, >= 1.0.2) - i18n (>= 0.7, < 2) - minitest (~> 5.1) - tzinfo (~> 1.1) - zeitwerk (~> 2.2, >= 2.2.2) - addressable (2.8.0) - public_suffix (>= 2.0.2, < 5.0) - coffee-script (2.4.1) - coffee-script-source - execjs - coffee-script-source (1.11.1) - colorator (1.1.0) - commonmarker (0.23.4) - concurrent-ruby (1.1.10) - dnsruby (1.61.9) - simpleidn (~> 0.1) - em-websocket (0.5.3) - eventmachine (>= 0.12.9) - http_parser.rb (~> 0) - ethon (0.15.0) - ffi (>= 1.15.0) - eventmachine (1.2.7) - execjs (2.8.1) - faraday (1.10.0) - faraday-em_http (~> 1.0) - faraday-em_synchrony (~> 1.0) - faraday-excon (~> 1.1) - faraday-httpclient (~> 1.0) - faraday-multipart (~> 1.0) - faraday-net_http (~> 1.0) - faraday-net_http_persistent (~> 1.0) - faraday-patron (~> 1.0) - faraday-rack (~> 1.0) - faraday-retry (~> 1.0) - ruby2_keywords (>= 0.0.4) - faraday-em_http (1.0.0) - faraday-em_synchrony (1.0.0) - faraday-excon (1.1.0) - faraday-httpclient (1.0.1) - faraday-multipart (1.0.3) - multipart-post (>= 1.2, < 3) - faraday-net_http (1.0.1) - faraday-net_http_persistent (1.2.0) - faraday-patron (1.0.0) - faraday-rack (1.0.0) - faraday-retry (1.0.3) - ffi (1.15.5) - forwardable-extended (2.6.0) - gemoji (3.0.1) - github-pages (226) - github-pages-health-check (= 1.17.9) - jekyll (= 3.9.2) - jekyll-avatar (= 0.7.0) - jekyll-coffeescript (= 1.1.1) - jekyll-commonmark-ghpages (= 0.2.0) - jekyll-default-layout (= 0.1.4) - jekyll-feed (= 0.15.1) - jekyll-gist (= 1.5.0) - jekyll-github-metadata (= 2.13.0) - jekyll-include-cache (= 0.2.1) - jekyll-mentions (= 1.6.0) - jekyll-optional-front-matter (= 0.3.2) - jekyll-paginate (= 1.1.0) - jekyll-readme-index (= 0.3.0) - jekyll-redirect-from (= 0.16.0) - jekyll-relative-links (= 0.6.1) - jekyll-remote-theme (= 0.4.3) - jekyll-sass-converter (= 1.5.2) - jekyll-seo-tag (= 2.8.0) - jekyll-sitemap (= 1.4.0) - jekyll-swiss (= 1.0.0) - jekyll-theme-architect (= 0.2.0) - jekyll-theme-cayman (= 0.2.0) - jekyll-theme-dinky (= 0.2.0) - jekyll-theme-hacker (= 0.2.0) - jekyll-theme-leap-day (= 0.2.0) - jekyll-theme-merlot (= 0.2.0) - jekyll-theme-midnight (= 0.2.0) - jekyll-theme-minimal (= 0.2.0) - jekyll-theme-modernist (= 0.2.0) - jekyll-theme-primer (= 0.6.0) - jekyll-theme-slate (= 0.2.0) - jekyll-theme-tactile (= 0.2.0) - jekyll-theme-time-machine (= 0.2.0) - jekyll-titles-from-headings (= 0.5.3) - jemoji (= 0.12.0) - kramdown (= 2.3.2) - kramdown-parser-gfm (= 1.1.0) - liquid (= 4.0.3) - mercenary (~> 0.3) - minima (= 2.5.1) - nokogiri (>= 1.13.4, < 2.0) - rouge (= 3.26.0) - terminal-table (~> 1.4) - github-pages-health-check (1.17.9) - addressable (~> 2.3) - dnsruby (~> 1.60) - octokit (~> 4.0) - public_suffix (>= 3.0, < 5.0) - typhoeus (~> 1.3) - html-pipeline (2.14.1) - activesupport (>= 2) - nokogiri (>= 1.4) - http_parser.rb (0.8.0) - i18n (0.9.5) - concurrent-ruby (~> 1.0) - jekyll (3.9.2) - addressable (~> 2.4) - colorator (~> 1.0) - em-websocket (~> 0.5) - i18n (~> 0.7) - jekyll-sass-converter (~> 1.0) - jekyll-watch (~> 2.0) - kramdown (>= 1.17, < 3) - liquid (~> 4.0) - mercenary (~> 0.3.3) - pathutil (~> 0.9) - rouge (>= 1.7, < 4) - safe_yaml (~> 1.0) - jekyll-avatar (0.7.0) - jekyll (>= 3.0, < 5.0) - jekyll-coffeescript (1.1.1) - coffee-script (~> 2.2) - coffee-script-source (~> 1.11.1) - jekyll-commonmark (1.4.0) - commonmarker (~> 0.22) - jekyll-commonmark-ghpages (0.2.0) - commonmarker (~> 0.23.4) - jekyll (~> 3.9.0) - jekyll-commonmark (~> 1.4.0) - rouge (>= 2.0, < 4.0) - jekyll-default-layout (0.1.4) - jekyll (~> 3.0) - jekyll-feed (0.15.1) - jekyll (>= 3.7, < 5.0) - jekyll-gist (1.5.0) - octokit (~> 4.2) - jekyll-github-metadata (2.13.0) - jekyll (>= 3.4, < 5.0) - octokit (~> 4.0, != 4.4.0) - jekyll-include-cache (0.2.1) - jekyll (>= 3.7, < 5.0) - jekyll-mentions (1.6.0) - html-pipeline (~> 2.3) - jekyll (>= 3.7, < 5.0) - jekyll-optional-front-matter (0.3.2) - jekyll (>= 3.0, < 5.0) - jekyll-paginate (1.1.0) - jekyll-readme-index (0.3.0) - jekyll (>= 3.0, < 5.0) - jekyll-redirect-from (0.16.0) - jekyll (>= 3.3, < 5.0) - jekyll-relative-links (0.6.1) - jekyll (>= 3.3, < 5.0) - jekyll-remote-theme (0.4.3) - addressable (~> 2.0) - jekyll (>= 3.5, < 5.0) - jekyll-sass-converter (>= 1.0, <= 3.0.0, != 2.0.0) - rubyzip (>= 1.3.0, < 3.0) - jekyll-sass-converter (1.5.2) - sass (~> 3.4) - jekyll-seo-tag (2.8.0) - jekyll (>= 3.8, < 5.0) - jekyll-sitemap (1.4.0) - jekyll (>= 3.7, < 5.0) - jekyll-swiss (1.0.0) - jekyll-theme-architect (0.2.0) - jekyll (> 3.5, < 5.0) - jekyll-seo-tag (~> 2.0) - jekyll-theme-cayman (0.2.0) - jekyll (> 3.5, < 5.0) - jekyll-seo-tag (~> 2.0) - jekyll-theme-dinky (0.2.0) - jekyll (> 3.5, < 5.0) - jekyll-seo-tag (~> 2.0) - jekyll-theme-hacker (0.2.0) - jekyll (> 3.5, < 5.0) - jekyll-seo-tag (~> 2.0) - jekyll-theme-leap-day (0.2.0) - jekyll (> 3.5, < 5.0) - jekyll-seo-tag (~> 2.0) - jekyll-theme-merlot (0.2.0) - jekyll (> 3.5, < 5.0) - jekyll-seo-tag (~> 2.0) - jekyll-theme-midnight (0.2.0) - jekyll (> 3.5, < 5.0) - jekyll-seo-tag (~> 2.0) - jekyll-theme-minimal (0.2.0) - jekyll (> 3.5, < 5.0) - jekyll-seo-tag (~> 2.0) - jekyll-theme-modernist (0.2.0) - jekyll (> 3.5, < 5.0) - jekyll-seo-tag (~> 2.0) - jekyll-theme-primer (0.6.0) - jekyll (> 3.5, < 5.0) - jekyll-github-metadata (~> 2.9) - jekyll-seo-tag (~> 2.0) - jekyll-theme-slate (0.2.0) - jekyll (> 3.5, < 5.0) - jekyll-seo-tag (~> 2.0) - jekyll-theme-tactile (0.2.0) - jekyll (> 3.5, < 5.0) - jekyll-seo-tag (~> 2.0) - jekyll-theme-time-machine (0.2.0) - jekyll (> 3.5, < 5.0) - jekyll-seo-tag (~> 2.0) - jekyll-titles-from-headings (0.5.3) - jekyll (>= 3.3, < 5.0) - jekyll-watch (2.2.1) - listen (~> 3.0) - jemoji (0.12.0) - gemoji (~> 3.0) - html-pipeline (~> 2.2) - jekyll (>= 3.0, < 5.0) - kramdown (2.3.2) - rexml - kramdown-parser-gfm (1.1.0) - kramdown (~> 2.0) - liquid (4.0.3) - listen (3.7.1) - rb-fsevent (~> 0.10, >= 0.10.3) - rb-inotify (~> 0.9, >= 0.9.10) - mercenary (0.3.6) - minima (2.5.1) - jekyll (>= 3.5, < 5.0) - jekyll-feed (~> 0.9) - jekyll-seo-tag (~> 2.1) - minitest (5.15.0) - multipart-post (2.1.1) - nokogiri (1.13.6-x86_64-linux) - racc (~> 1.4) - octokit (4.22.0) - faraday (>= 0.9) - sawyer (~> 0.8.0, >= 0.5.3) - pathutil (0.16.2) - forwardable-extended (~> 2.6) - public_suffix (4.0.7) - racc (1.6.0) - rb-fsevent (0.11.1) - rb-inotify (0.10.1) - ffi (~> 1.0) - rexml (3.2.5) - rouge (3.26.0) - ruby2_keywords (0.0.5) - rubyzip (2.3.2) - safe_yaml (1.0.5) - sass (3.7.4) - sass-listen (~> 4.0.0) - sass-listen (4.0.0) - rb-fsevent (~> 0.9, >= 0.9.4) - rb-inotify (~> 0.9, >= 0.9.7) - sawyer (0.8.2) - addressable (>= 2.3.5) - faraday (> 0.8, < 2.0) - simpleidn (0.2.1) - unf (~> 0.1.4) - terminal-table (1.8.0) - unicode-display_width (~> 1.1, >= 1.1.1) - thread_safe (0.3.6) - typhoeus (1.4.0) - ethon (>= 0.9.0) - tzinfo (1.2.9) - thread_safe (~> 0.1) - unf (0.1.4) - unf_ext - unf_ext (0.0.8.1) - unicode-display_width (1.8.0) - webrick (1.7.0) - zeitwerk (2.5.4) - -PLATFORMS - x86_64-linux - -DEPENDENCIES - github-pages - http_parser.rb (~> 0.6.0) - tzinfo (~> 1.2) - tzinfo-data - wdm (~> 0.1.1) - webrick (~> 1.7) - -BUNDLED WITH - 2.3.14 \ No newline at end of file diff --git a/home_page/_config.yml b/home_page/_config.yml deleted file mode 100644 index e7352f37..00000000 --- a/home_page/_config.yml +++ /dev/null @@ -1,34 +0,0 @@ -# Welcome to Jekyll! -# -# This config file is meant for settings that affect your whole blog, values -# which you are expected to set up once and rarely edit after that. If you find -# yourself editing this file very often, consider using Jekyll's data files -# feature for the data you need to update frequently. -# -# For technical reasons, this file is *NOT* reloaded automatically when you use -# 'bundle exec jekyll serve'. If you change this file, please restart the server process. -# -# If you need help with YAML syntax, here are some quick references for you: -# https://learn-the-web.algonquindesign.ca/topics/markdown-yaml-cheat-sheet/#yaml -# https://learnxinyminutes.com/docs/yaml/ -# -# Site settings -# These are used to personalize your new site. If you look in the HTML files, -# you will see them accessed via {{ site.title }}, {{ site.email }}, and so on. -# You can create any custom variable you would like, and they will be accessible -# in the templates via {{ site.myvariable }}. - -title: Analysis Lean companion -#email: your-email@example.com -description: by Terence Tao -baseurl: "" # the subpath of your site, e.g. /blog -url: "https://teorth.github.io/analysis" # the base hostname & protocol for your site, e.g. http://example.com -twitter_username: -github_username: teorth -repository: teorth/analysis - -# Build settings -remote_theme: pages-themes/cayman@v0.2.0 -plugins: - - jekyll-remote-theme - - jekyll-github-metadata \ No newline at end of file diff --git a/home_page/_include/mathjax.html b/home_page/_include/mathjax.html deleted file mode 100644 index ab9c0075..00000000 --- a/home_page/_include/mathjax.html +++ /dev/null @@ -1,17 +0,0 @@ - -{% if page.usemathjax %} - - - - -{% endif %} \ No newline at end of file diff --git a/home_page/_layouts/default.html b/home_page/_layouts/default.html deleted file mode 100644 index 2484b944..00000000 --- a/home_page/_layouts/default.html +++ /dev/null @@ -1,50 +0,0 @@ - - - - - - - {% seo %} - - - - - - {% if jekyll.environment == "production" %} - - {% else %} - - {% endif %} - {% include head-custom.html %} - - - - - - - -
- {{ content }} - -
- {% if site.github.is_project_page %} - {{ site.github.repository_name }} - is maintained by Terence Tao. Visit the GitHub repository for more information. - {% endif %} -
-
- - - \ No newline at end of file diff --git a/home_page/assets/css/style.scss b/home_page/assets/css/style.scss deleted file mode 100644 index 312da210..00000000 --- a/home_page/assets/css/style.scss +++ /dev/null @@ -1,9 +0,0 @@ ---- ---- - -/* In this file you can add css rules overriding rules defined by your Jekyll theme. */ - -/* Import the CSS from the specified theme */ -@import "{{ site.theme }}"; - -/* Put your rules below this line */ \ No newline at end of file diff --git a/home_page/index.md b/home_page/index.md deleted file mode 100644 index 2ab3ac6f..00000000 --- a/home_page/index.md +++ /dev/null @@ -1,15 +0,0 @@ ---- -# Feel free to add content and custom Front Matter to this file. -# To modify the layout, see https://jekyllrb.com/docs/themes/#overriding-theme-defaults - -# layout: home -usemathjax: true ---- - -Useful links: - -* [Zulip chat for Lean](https://leanprover.zulipchat.com/) for coordination -* [Blueprint]({{ site.url }}/blueprint/) -* [Blueprint as pdf]({{ site.url }}/blueprint.pdf) -* [Dependency graph]({{ site.url }}/blueprint/dep_graph_document.html) -* [Doc pages for this repository]({{ site.url }}/docs/) \ No newline at end of file diff --git a/lakefile.lean b/lakefile.lean deleted file mode 100644 index aaff2e3f..00000000 --- a/lakefile.lean +++ /dev/null @@ -1,51 +0,0 @@ -import Lake -open Lake DSL - -package «analysis» where - -- Settings applied to both builds and interactive editing - leanOptions := #[ - ⟨`pp.unicode.fun, true⟩ -- pretty-prints `fun a ↦ b` - ] - -- add any additional package configuration options here - - --- Require Batteries (a general-purpose utility library) -require batteries from git - "https://github.com/leanprover-community/batteries" @ "v4.20.0" - --- Require ImportGraph (transitive dep, now made direct to override version) -require importGraph from git - "https://github.com/leanprover-community/import-graph" @ "v4.20.0" - --- Require Mathlib (the comprehensive library of mathematics in Lean) -require mathlib from git - "https://github.com/leanprover-community/mathlib4.git" @ "v4.20.0" - --- Require Pantograph (a library for automated theorem proving) --- require pantograph from git --- "https://github.com/lenianiva/Pantograph.git" @ "v0.3.1" - --- Require Plausible (transitive dep, now made direct to override version) -require plausible from git - "https://github.com/leanprover-community/plausible.git" @ "v4.20.0" - --- Require ProofWidgets4 (for interactive proof widgets) -require proofwidgets from git - "https://github.com/leanprover-community/ProofWidgets4.git" @"v0.0.60" - --- Require quote4 (transitive dep, now made direct to override version) -require Qq from git - "https://github.com/leanprover-community/quote4" @ "v4.20.0" - - - - -@[default_target] -lean_lib «Analysis» where - -- add any library configuration options here - -require checkdecls from git "https://github.com/PatrickMassot/checkdecls.git" - -meta if get_config? env = some "dev" then -require «doc-gen4» from git - "https://github.com/leanprover/doc-gen4" @ "v4.20.0" diff --git a/lean-toolchain b/lean-toolchain deleted file mode 100644 index 52fe7747..00000000 --- a/lean-toolchain +++ /dev/null @@ -1 +0,0 @@ -leanprover/lean4:v4.20.0 diff --git a/serve.py b/serve.py new file mode 100644 index 00000000..df4951d9 --- /dev/null +++ b/serve.py @@ -0,0 +1,30 @@ +import os +from http.server import SimpleHTTPRequestHandler, HTTPServer + +BOOK_SITE = os.path.abspath('./book/_site') +DOCS_SITE = os.path.abspath('./analysis/.lake/build/doc') + +class CustomHTTPRequestHandler(SimpleHTTPRequestHandler): + def translate_path(self, path): + # Serve /analysis-book/docs/* from DOCS_SITE + if path.startswith('/analysis-book/docs/'): + rel_path = path[len('/analysis-book/docs/'):] + return os.path.join(DOCS_SITE, rel_path) + # Serve /analysis-book/* from BOOK_SITE + elif path.startswith('/analysis-book/'): + rel_path = path[len('/analysis-book/'):] + return os.path.join(BOOK_SITE, rel_path) + # Otherwise, serve nothing (could return a non-existent path) + else: + raise FileNotFoundError("File not found") + + +if __name__ == '__main__': + PORT = 8000 + handler = CustomHTTPRequestHandler + with HTTPServer(("", PORT), handler) as httpd: + print(f"Serving at http://localhost:{PORT}/analysis-book") + print(f"/analysis-book: {BOOK_SITE}") + print(f"/analysis-book/docs: {DOCS_SITE}") + httpd.serve_forever() + From bb754055ccf2f2d9d7d98784fd3250cbef3b28bf Mon Sep 17 00:00:00 2001 From: Pim Otte Date: Fri, 6 Jun 2025 16:29:40 +0200 Subject: [PATCH 2/4] Move hosting path from /analysis-book to /analysis --- book/AnalysisBook.lean | 2 +- serve.py | 14 +++++++------- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/book/AnalysisBook.lean b/book/AnalysisBook.lean index 79913be9..82e4398f 100644 --- a/book/AnalysisBook.lean +++ b/book/AnalysisBook.lean @@ -13,7 +13,7 @@ def theme : Theme := { Theme.default with {{ (← param (α := String) "title") }} " — Verso " - + {{← builtinHeader }} diff --git a/serve.py b/serve.py index df4951d9..aa993580 100644 --- a/serve.py +++ b/serve.py @@ -7,12 +7,12 @@ class CustomHTTPRequestHandler(SimpleHTTPRequestHandler): def translate_path(self, path): # Serve /analysis-book/docs/* from DOCS_SITE - if path.startswith('/analysis-book/docs/'): - rel_path = path[len('/analysis-book/docs/'):] + if path.startswith('/analysis/docs/'): + rel_path = path[len('/analysis/docs/'):] return os.path.join(DOCS_SITE, rel_path) # Serve /analysis-book/* from BOOK_SITE - elif path.startswith('/analysis-book/'): - rel_path = path[len('/analysis-book/'):] + elif path.startswith('/analysis/'): + rel_path = path[len('/analysis/'):] return os.path.join(BOOK_SITE, rel_path) # Otherwise, serve nothing (could return a non-existent path) else: @@ -23,8 +23,8 @@ def translate_path(self, path): PORT = 8000 handler = CustomHTTPRequestHandler with HTTPServer(("", PORT), handler) as httpd: - print(f"Serving at http://localhost:{PORT}/analysis-book") - print(f"/analysis-book: {BOOK_SITE}") - print(f"/analysis-book/docs: {DOCS_SITE}") + print(f"Serving at http://localhost:{PORT}/analysis") + print(f"/analysis: {BOOK_SITE}") + print(f"/analysis/docs: {DOCS_SITE}") httpd.serve_forever() From a7ebe95e6952cfb7ce6fbebd245f278652878279 Mon Sep 17 00:00:00 2001 From: Pim Otte Date: Fri, 6 Jun 2025 16:30:07 +0200 Subject: [PATCH 3/4] Use Lean manual fonts, scale up code --- book/static_files/style.css | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/book/static_files/style.css b/book/static_files/style.css index 8999664e..4a4bfc49 100644 --- a/book/static_files/style.css +++ b/book/static_files/style.css @@ -42,3 +42,12 @@ header, div.main { margin-left: 16em; } + +code span { + font-family: "Source Code Pro" "Noto sans mono", monospace; + font-size: 15px; +} + +body { + font-family: "Source Sans 3","Helvetica Neue","Segoe UI","Roboto",Arial,sans-serif; +} \ No newline at end of file From 24b73d0ff0cf80807ce0770086ad1c2a63661388 Mon Sep 17 00:00:00 2001 From: Pim Otte Date: Fri, 6 Jun 2025 16:33:29 +0200 Subject: [PATCH 4/4] Update links in README --- README.md | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/README.md b/README.md index f4463ee4..8d2e19d2 100644 --- a/README.md +++ b/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: