Download only the Mathlib files the project uses

.devcontainer/devcontainer.json

@@ -6,15 +6,22 @@
 
   // Runs when the codespace is created, and again whenever a prebuild is refreshed,
   // so prebuilds pick up changes such as a new linglib version. Same script a local
-  // agent runs; about 10 minutes from scratch, seconds when nothing changed.
+  // agent runs; about 5 minutes from scratch, seconds when nothing changed.
   "updateContentCommand": "bash scripts/setup.sh",
 
-  // Make lean and lake available in every terminal and to the agent.
+  // Python runs scripts/get_mathlib.py, which downloads only the Mathlib files the project uses.
+  "features": {
+    "ghcr.io/devcontainers/features/python:1": { "version": "os-provided", "installTools": false }
+  },
+
+  // Make lean and lake available in every terminal and to the agent, and keep `lake update`
+  // from downloading all of Mathlib (about 7 GB); scripts/build.sh fetches what is needed.
   "remoteEnv": {
-    "PATH": "/home/vscode/.elan/bin:${containerEnv:PATH}"
+    "PATH": "/home/vscode/.elan/bin:${containerEnv:PATH}",
+    "MATHLIB_NO_CACHE_ON_UPDATE": "1"
   },
 
-  // Lean needs some memory; storage is mostly the prebuilt Mathlib files (about 12 GB).
+  // Lean needs some memory; Lean and the prebuilt files take about 5 GB of storage.
   "hostRequirements": {
     "memory": "8gb",
     "storage": "32gb"

.github/workflows/ci.yml

@@ -1,6 +1,10 @@
 # Builds the starter weekly and on every change, so the template does not
 # quietly break when linglib or Mathlib move on. Tests both ways in:
 # the setup script a local agent runs, and the Codespaces dev container.
+#
+# Setup downloads only the Mathlib files the project uses. Each job fails if Lean
+# compiled a file that should have been downloaded, since on a user's machine that
+# is a build that runs for hours.
 name: Build starter
 
 on:
@@ -10,13 +14,63 @@ on:
     - cron: "17 6 * * 1"
   workflow_dispatch:
 
+defaults:
+  run:
+    shell: bash
+
 jobs:
+  script-tests:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - name: Test the download script (needs neither Lean nor a network)
+        run: python3 -m unittest discover -s scripts -p 'test_*.py' -v
+
   setup-script:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v4
       - name: Run the setup script a new user's agent would run
         run: bash scripts/setup.sh
+      - name: Check that nothing from Mathlib or linglib was compiled
+        run: |
+          if grep -rEn 'Buil(t|ding) (Mathlib|Linglib|Eval)\.' .lake/setup-logs/; then
+            echo "Setup compiled files that should have been downloaded."
+            exit 1
+          fi
+      - name: Show how much disk space the setup uses
+        if: always()
+        run: du -sh .lake ~/.elan
+
+  new-import:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - name: Run the setup script
+        run: bash scripts/setup.sh
+      - name: Import another part of linglib and build it through scripts/build.sh
+        run: |
+          count() { find .lake/packages/mathlib/.lake/build/lib/lean -name '*.olean' | wc -l; }
+          # A part of linglib that needs Mathlib files the worked example does not use. If a
+          # newer linglib renames this module, pick another one that brings in extra files.
+          printf 'import Linglib.Semantics.Exhaustification.Finite\n' > MyProject/CiProbe.lean
+          before=$(count)
+          if python3 scripts/get_mathlib.py --check MyProject/CiProbe.lean; then
+            echo "--check passed although the new import needs files that are not there."
+            exit 1
+          fi
+          bash scripts/build.sh MyProject.CiProbe 2>&1 | tee build.log
+          after=$(count)
+          echo "Prebuilt Mathlib files: $before before, $after after."
+          if [ "$after" -le "$before" ]; then
+            echo "The new import did not bring in any more Mathlib files."
+            exit 1
+          fi
+          python3 scripts/get_mathlib.py --check MyProject/CiProbe.lean
+          if grep -En 'Buil(t|ding) (Mathlib|Linglib|Eval)\.' build.log; then
+            echo "The build compiled files that should have been downloaded."
+            exit 1
+          fi
 
   devcontainer:
     runs-on: ubuntu-latest
@@ -26,4 +80,11 @@ jobs:
         uses: devcontainers/ci@v0.3
         with:
           push: never
-          runCmd: lake build MyProject.Example
+          runCmd: |
+            set -e
+            lake build MyProject.Example
+            if grep -rEn 'Buil(t|ding) (Mathlib|Linglib|Eval)\.' .lake/setup-logs/; then
+              echo "Setup compiled files that should have been downloaded."
+              exit 1
+            fi
+            du -sh .lake "$HOME/.elan"

.gitignore

@@ -1,2 +1,3 @@
 .lake/
 .DS_Store
+__pycache__/

AGENTS.md

@@ -23,22 +23,25 @@ Setup is complete when `.lake/build/lib/lean/MyProject/Example.olean` exists. If
 and the user has asked you to set up the project, do the following.
 
 1. Tell the user, in two or three sentences, what will happen: you will install Lean (into
-   `~/.elan`, no administrator rights needed), download linglib and the prebuilt Mathlib library,
-   and build a worked example. It needs about 15 GB of disk space and takes about 10 minutes on a
-   fast connection, and up to 30 on a slow one, mostly downloading. Ask for their go-ahead once.
+   `~/.elan`, no administrator rights needed), download linglib and the parts of the Mathlib
+   library this project uses, and build a worked example. It needs about 6 GB of disk space
+   (3 GB for Lean in the home folder, 3 GB in this folder) and takes about 5 minutes on a fast
+   connection, and up to 15 on a slow one, mostly downloading. Ask for their go-ahead once.
 2. Run `bash scripts/setup.sh` from the project root. It prints one line per step and writes full
-   logs to `.lake/setup-logs/`. Let it run. Steps 1 to 3 take about a minute; steps 4 and 5
-   are the slow ones. Give the user a short update when step 4 finishes and when step 5 finishes.
+   logs to `.lake/setup-logs/`. Let it run. Steps 1 to 3 take about a minute; step 4 is the slow
+   one. Give the user a short update when step 4 finishes and when step 5 finishes.
 3. If it ends with `SETUP OK`, go to "After setup" below.
 4. If it ends with `SETUP FAILED`, read the log it names and use the table below. Fix the cause,
    then run the script again; it skips finished steps.
 
 | Symptom in the log | What to do |
 |---|---|
 | `lake: command not found` after elan installed | Use `~/.elan/bin/lake`, or run `source ~/.elan/env` first. Tell the user a new terminal will pick it up automatically. |
-| Disk space error | Tell the user how much is free and that about 15 GB is needed. Do not delete anything to make room without asking. |
+| Disk space error | Tell the user how much is free and that about 6 GB is needed (3 GB in this folder, 3 GB in the home folder). Do not delete anything to make room without asking. |
+| `python3 is not installed` | Python 3 runs the script that downloads only the Mathlib files the project uses. Ask the user before installing it (on macOS, `xcode-select --install`; on Ubuntu or Debian, `sudo apt install python3`), then run the setup again. |
 | Network errors in step 4 (timeouts, TLS, 403) | Retry once. If it fails again, tell the user the setup needs access to `github.com` and `cache.mathlib.org`, which some university or company networks block. Suggest trying another network. |
-| Step 4 reports that cache files are missing, or Lean starts compiling Mathlib files | Stop the build. Do not let it compile Mathlib from source: that takes hours. Report the problem to the user and suggest they open an issue on linglib. |
+| Step 4 says Mathlib files could not be downloaded | Do not go on to build: Lean would compile the missing files, which takes hours. Run `python3 scripts/get_mathlib.py --verbose` once more. If files are still missing, report the problem to the user and suggest they open an issue on linglib. |
+| Lean starts compiling Mathlib files (`Building Mathlib...` or `Built Mathlib...` lines) | Stop the build at once. Run `python3 scripts/get_mathlib.py`, then build again with `bash scripts/build.sh`. See "Building" below. |
 | A toolchain or version mismatch error | Do not edit `lean-toolchain` or the linglib version in `lakefile.toml` to make the error go away. These must match linglib's. Report the exact error to the user. |
 | `building from source; failed to fetch GitHub release` in step 5 | Lake could not download linglib's prebuilt files, so it is compiling the parts it needs instead. This is slower (a few minutes) but works. If it happens on every run, check that `rev` in `lakefile.toml` is a release tag. |
 | Warnings (not errors) in the logs, for example from elan's self-update check or linter warnings in linglib files | Ignore them. Only errors, or a `SETUP FAILED` line, need attention. |
@@ -70,16 +73,29 @@ missing, setup may still be running or may have failed: check `.lake/setup-logs/
 user they can also see progress with the command "Codespaces: View Creation Log". If it failed,
 run `bash scripts/setup.sh` and continue as above.
 
-Codespaces use the user's free monthly allowance, and this one takes about 12 GB of storage.
+Codespaces use the user's free monthly allowance, and this one takes about 5 GB of storage.
 Remind the user to stop the codespace when they finish a session, and to delete it from
 github.com/codespaces once they no longer need it (after committing anything they want to keep).
 
 ### Windows
 
-`scripts/setup.sh` needs a Unix shell. On Windows, prefer WSL if it is installed. Otherwise, do the
-same steps by hand in PowerShell: install elan with the Windows installer from
-https://github.com/leanprover/elan, then run `lake --version`, `lake exe cache get` and
-`lake build MyProject.Example` from the project root. The table above still applies.
+`scripts/setup.sh` and `scripts/build.sh` need a Unix shell. On Windows, prefer WSL if it is
+installed. Otherwise, do the same steps by hand in PowerShell, from the project root. Install elan
+with the Windows installer from https://github.com/leanprover/elan, and Python 3 if it is missing
+(ask first). Then:
+
+```
+$env:MATHLIB_NO_CACHE_ON_UPDATE = "1"
+lake --version
+lake env lean --version
+py scripts\get_mathlib.py
+lake build MyProject.Example
+```
+
+The third command downloads linglib and the other packages and builds nothing. Use `python` in
+place of `py` if `py` is not found. Later, wherever these instructions say
+`bash scripts/build.sh <target>`, run `py scripts\get_mathlib.py <target>` and then
+`lake build <target>`, with the variable above set. The table above still applies.
 
 ## After setup
 
@@ -121,15 +137,36 @@ Then offer two or three things to try next, for example:
 
 ### Building
 
+This project downloads only the parts of Mathlib it uses (about 0.7 GB instead of 7 GB). A file
+that imports something new may need Mathlib files that are not there yet. If they are missing
+when a build starts, Lean compiles them instead, and that takes hours. So:
+
+- **Always build with `bash scripts/build.sh <target>`**, for example
+  `bash scripts/build.sh MyProject.Example`. It downloads any missing Mathlib files for the
+  target (`python3 scripts/get_mathlib.py <target>`) and then runs `lake build <target>`. After
+  adding or changing any `import` line, build through the script again before anything else.
+  Do not call `lake build` or `lake env lean` on a file until the script has run for it.
+- **If a build ever starts compiling Mathlib** (lines such as `Building Mathlib...` or
+  `Built Mathlib...`), stop it at once. Run `python3 scripts/get_mathlib.py`, then build again
+  through the script.
+- **The Lean extension in VS Code builds a file's imports as soon as the file is opened.** After
+  changing imports, run `python3 scripts/get_mathlib.py` before opening or reloading that file
+  in the editor.
+
+Also:
+
 - `lake` lives in `~/.elan/bin`. Setup adds it to the user's shell profile, but a shell you
   start may not read that file. If `lake` is not found, run
   `export PATH="$HOME/.elan/bin:$PATH"` first, or call `~/.elan/bin/lake` directly.
-- Check one file at a time: `lake env lean MyProject/<File>.lean`, or
-  `lake build MyProject.<File>`. Avoid building all of linglib; it is large and almost never
-  needed.
+  `scripts/build.sh` does this itself.
+- Check one file at a time: `bash scripts/build.sh MyProject.<File>`. Avoid building all of
+  linglib; it is large and almost never needed.
 - After a change, rebuild before you tell the user something works.
-- The first build of a file that imports a new part of linglib can take several minutes,
-  because that part of linglib is compiled then. Tell the user when this happens.
+- A file that imports a new part of linglib does not compile linglib: linglib's prebuilt files
+  are unpacked the first time they are used, which takes seconds. Downloading more Mathlib
+  files for it usually takes under a minute.
+- If the user's work comes to import much of linglib, `bash scripts/setup.sh --full` downloads
+  all of Mathlib once (about 11 GB of disk space in total). Ask before running it.
 
 ### Formalizing a claim
 
@@ -169,8 +206,9 @@ To update, which you should do only when the user asks:
    release tag, not a branch or commit: only releases have prebuilt files.
 2. Set `rev` in `lakefile.toml` to that tag, and copy linglib's `lean-toolchain` from that tag
    if it changed.
-3. Run `lake update`, then `lake build MyProject.Example`, and check that the user's own files
-   still build. Tell the user if a change in linglib broke any of their files.
+3. Run `MATHLIB_NO_CACHE_ON_UPDATE=1 lake update` (without the variable, Lake downloads all of
+   Mathlib, about 7 GB), then `bash scripts/build.sh MyProject.Example`, and check that the
+   user's own files still build. Tell the user if a change in linglib broke any of their files.
 
 ## Saving work to GitHub
 

README.md

@@ -24,8 +24,9 @@ need a paid plan, and long sessions use credits.
    > Set up the linglib starter: clone https://github.com/linglib-community/starter, read
    > AGENTS.md, and follow its setup instructions. Then walk me through the worked example.
 
-3. The agent tells you what it will install and asks you to confirm. Setup takes about 10
-   minutes on a fast connection, and up to 30 on a slow one. Then it explains the worked example and suggests what to try next.
+3. The agent tells you what it will install and asks you to confirm. Setup takes about 5
+   minutes on a fast connection, and up to 15 on a slow one. Then it explains the worked example
+   and suggests what to try next.
 
 Saving your work: at the end of a session, ask the agent to save it. It can push your changes to
 your copy on GitHub, save the files to a folder on your computer if your app is connected to one,
@@ -38,7 +39,7 @@ Use this if you want everything to stay on your machine. You need:
 
 - An AI agent that can edit files and run commands on your computer, such as the Claude app
   connected to a folder, Claude Code, OpenAI's Codex, or Cursor.
-- About 15 GB of free disk space, and a network connection that allows access to `github.com` and
+- About 6 GB of free disk space, and a network connection that allows access to `github.com` and
   `cache.mathlib.org`.
 - macOS or Linux works best. Windows works through WSL or with a few manual steps.
 
@@ -47,7 +48,7 @@ Give your agent this prompt:
 > Clone https://github.com/linglib-community/starter into a new folder called my-linglib, then
 > read AGENTS.md in that folder and follow its setup instructions.
 
-Setup takes about 10 minutes on a fast connection, and up to 30 on a slow one, mostly
+Setup takes about 5 minutes on a fast connection, and up to 15 on a slow one, mostly
 downloading. To keep your work on GitHub as well as your computer, make your own copy first
 ("Use this template", as in Option 1) and give the agent its address instead.
 
@@ -60,7 +61,7 @@ Code panel in the sidebar. It suits workshops, where everyone needs the same env
 people who are comfortable with code editors.
 
 - Codespaces are paid for by your GitHub account, which includes a free monthly allowance, or by
-  the linglib-community organization for its members. This project uses about 12 GB of storage,
+  the linglib-community organization for its members. This project uses about 5 GB of storage,
   so stop the codespace when you finish a session and delete it from github.com/codespaces when
   you no longer need it.
 - Claude Code requires a paid Claude plan.
@@ -87,13 +88,21 @@ statement together, so you can compare them. Only you should mark a claim as che
 
 ## Setting up without an agent
 
-If you are comfortable with a terminal, run `bash scripts/setup.sh` from this folder.
+If you are comfortable with a terminal, run `bash scripts/setup.sh` from this folder. It
+downloads only the parts of the Mathlib library the project uses. If you expect to import much
+of linglib, `bash scripts/setup.sh --full` downloads all of Mathlib instead, which brings the
+total to about 11 GB.
+
+After changing an `import` line, build with `bash scripts/build.sh MyProject.<File>` rather than
+`lake build`: it first downloads any Mathlib files the new import needs.
 
 ## Files
 
 - `AGENTS.md`: instructions the agent reads (`CLAUDE.md` points to it).
 - `MyProject/`: your work. `Example.lean` is the worked example; `MyFirstStudy.lean` is a
   template for formalizing a claim.
 - `scripts/setup.sh`: the setup steps, which the agent (or the codespace) runs for you.
-- `.devcontainer/`: the configuration for Option 1.
+- `scripts/build.sh` and `scripts/get_mathlib.py`: build a file after downloading the Mathlib
+  files it needs.
+- `.devcontainer/`: the configuration for Option 3.
 - `lakefile.toml` and `lean-toolchain`: which versions of linglib and Lean this project uses.

scripts/build.sh

@@ -0,0 +1,21 @@
+#!/usr/bin/env bash
+# Build the safe way: first download any prebuilt Mathlib files the target needs, then build it.
+#
+#   bash scripts/build.sh MyProject.Example     # a module, or a path such as MyProject/Example.lean
+#   bash scripts/build.sh                       # the whole project
+#
+# This project downloads only the parts of Mathlib it uses. If a file needs a Mathlib file
+# that was never downloaded, Lean compiles it instead, which takes hours. This script stops
+# before that can happen, so build through it rather than calling `lake build` directly.
+#
+# macOS and Linux. On Windows, see AGENTS.md ("Windows").
+
+set -euo pipefail
+cd "$(dirname "$0")/.."
+export PATH="$HOME/.elan/bin:$PATH"
+export MATHLIB_NO_CACHE_ON_UPDATE=1
+
+command -v python3 >/dev/null 2>&1 || { echo "python3 is not installed; scripts/get_mathlib.py needs it."; exit 1; }
+
+python3 scripts/get_mathlib.py "$@"
+exec lake build "$@"