From c193172366a13bc486f123171271a3e558424c89 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Mon, 12 Oct 2026 11:47:46 -0700 Subject: [PATCH] Download only the Mathlib files the project uses --- .devcontainer/devcontainer.json | 15 +- .github/workflows/ci.yml | 63 +++++- .gitignore | 1 + AGENTS.md | 76 +++++-- README.md | 23 +- scripts/build.sh | 21 ++ scripts/get_mathlib.py | 369 ++++++++++++++++++++++++++++++++ scripts/setup.sh | 47 +++- scripts/test_get_mathlib.py | 178 +++++++++++++++ 9 files changed, 755 insertions(+), 38 deletions(-) create mode 100755 scripts/build.sh create mode 100755 scripts/get_mathlib.py create mode 100644 scripts/test_get_mathlib.py diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json index cba5164..7db2ce2 100644 --- a/.devcontainer/devcontainer.json +++ b/.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" diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 8e9176b..ae83150 100644 --- a/.github/workflows/ci.yml +++ b/.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" diff --git a/.gitignore b/.gitignore index d031741..4b7ee8c 100644 --- a/.gitignore +++ b/.gitignore @@ -1,2 +1,3 @@ .lake/ .DS_Store +__pycache__/ diff --git a/AGENTS.md b/AGENTS.md index 99f7590..1d0c63e 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -23,12 +23,13 @@ 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. @@ -36,9 +37,11 @@ and the user has asked you to set up the project, do the following. | 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 `, run `py scripts\get_mathlib.py ` and then +`lake build `, 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 `**, for example + `bash scripts/build.sh MyProject.Example`. It downloads any missing Mathlib files for the + target (`python3 scripts/get_mathlib.py `) and then runs `lake build `. 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/.lean`, or - `lake build MyProject.`. 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.`. 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 diff --git a/README.md b/README.md index 6c314a9..c6ef7b8 100644 --- a/README.md +++ b/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,7 +88,13 @@ 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.` rather than +`lake build`: it first downloads any Mathlib files the new import needs. ## Files @@ -95,5 +102,7 @@ If you are comfortable with a terminal, run `bash scripts/setup.sh` from this fo - `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. diff --git a/scripts/build.sh b/scripts/build.sh new file mode 100755 index 0000000..6bfcffa --- /dev/null +++ b/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 "$@" diff --git a/scripts/get_mathlib.py b/scripts/get_mathlib.py new file mode 100755 index 0000000..fb1ce25 --- /dev/null +++ b/scripts/get_mathlib.py @@ -0,0 +1,369 @@ +#!/usr/bin/env python3 +"""Download the prebuilt Mathlib files this project needs, and no others. + +All of Mathlib's prebuilt files take about 7 GB; a project uses a small part of them. This +script follows the `import` lines from the project's own Lean files (or from the modules or +files named as arguments) through linglib and the other packages in `.lake/packages`, finds the +Mathlib files that are reached, and asks Mathlib's own download tool for exactly those: + + lake exe cache get + +Run it from the project folder before `lake build` whenever an `import` line has changed (in +the linglib starter, `scripts/build.sh` does both). Lean compiles any Mathlib file that is +needed but was not downloaded, and that takes hours. + + python3 get_mathlib.py # all that the project's own files import + python3 get_mathlib.py MyProject.Example # one module, or a path to a .lean file + python3 get_mathlib.py --check # download nothing; exit 1 if any is missing + +Exit status: 0 when every needed file is present, 1 when some are missing or a download failed, +2 when the project is not set up far enough to tell (for example, no packages yet). + +Python 3.8 or later, standard library only. Works on macOS, Linux and Windows. +""" + +from __future__ import annotations + +import argparse +import json +import os +import re +import shutil +import subprocess +import sys +from pathlib import Path +from typing import Dict, Iterable, List, Optional, Set, Tuple + +# --------------------------------------------------------------------------------------------- +# Reading the imports of a Lean file +# --------------------------------------------------------------------------------------------- + +_SKIP = re.compile(r"\s+|--[^\n]*") # whitespace and line comments +_TOKEN = re.compile(r"(?:(?!--|/-)\S)+") # a word, ending where a comment starts +_COMMENT_EDGE = re.compile(r"/-|-/") +_MODIFIERS = {"public", "private", "meta"} + + +def _skip_block_comment(text: str, pos: int) -> int: + """The position just after the block comment that opens at `pos`. Comments nest.""" + depth, pos = 1, pos + 2 + while depth: + edge = _COMMENT_EDGE.search(text, pos) + if edge is None: + return len(text) + depth += 1 if edge.group(0) == "/-" else -1 + pos = edge.end() + return pos + + +def header_imports(text: str) -> List[str]: + """The modules a Lean file imports. + + A Lean file opens with a header: optionally `module`, optionally `prelude`, then its imports, + each of the form `[public] [meta] import [all] Some.Module`. Comments may come before and + between them. The header ends at the first word that is not part of it. + """ + imports: List[str] = [] + pos, expect_name, seen_all = 0, False, False + while pos < len(text): + skipped = _SKIP.match(text, pos) + if skipped: + pos = skipped.end() + continue + if text.startswith("/-", pos): + pos = _skip_block_comment(text, pos) + continue + word = _TOKEN.match(text, pos) + if word is None: + break + token, pos = word.group(0), word.end() + if expect_name: + if token == "all" and not seen_all: + seen_all = True + continue + imports.append(token) + expect_name = False + elif token == "import": + expect_name, seen_all = True, False + elif token in _MODIFIERS: + continue + elif token in ("module", "prelude") and not imports: + continue + else: + break + return imports + + +# --------------------------------------------------------------------------------------------- +# The project and its packages +# --------------------------------------------------------------------------------------------- + +class Problem(Exception): + """Something the user has to fix before this script can do its job.""" + + +def find_project_root(start: Path) -> Path: + """The nearest folder at or above `start` that holds a lakefile.""" + for folder in [start, *start.parents]: + if (folder / "lakefile.toml").is_file() or (folder / "lakefile.lean").is_file(): + return folder + raise Problem(f"No lakefile.toml or lakefile.lean found in {start} or the folders above it.") + + +def _read_json(path: Path) -> dict: + try: + return json.loads(path.read_text(encoding="utf-8")) + except (OSError, ValueError): + return {} + + +class Workspace: + """Where each module's source file is, and which packages Mathlib's download tool serves.""" + + def __init__(self, root: Path): + self.root = root + self.manifest = _read_json(root / "lake-manifest.json") + self.packages_dir = root / self.manifest.get("packagesDir", ".lake/packages") + self.mathlib = self.packages_dir / "mathlib" + if not self.mathlib.is_dir(): + raise Problem( + "Mathlib has not been downloaded into this project yet " + f"({self.mathlib} does not exist). Run the project's setup first.") + packages = sorted(p for p in self.packages_dir.iterdir() if p.is_dir()) + self.source_roots: List[Path] = [root, *packages] + # Mathlib's download tool serves Mathlib and the packages Mathlib itself depends on. + names = {"mathlib"} + for package in _read_json(self.mathlib / "lake-manifest.json").get("packages", []): + names.add(str(package.get("name", "")).strip("«»")) + self.served: Set[Path] = {self.packages_dir / name for name in names} + self._candidates: Dict[str, List[Path]] = {} + + def locate(self, module: str) -> Optional[Tuple[Path, Path]]: + """The source root and file of a module, or None for a module that comes with Lean.""" + parts = module.split(".") + top = parts[0] + if top not in self._candidates: + self._candidates[top] = [ + r for r in self.source_roots + if (r / top).is_dir() or (r / (top + ".lean")).is_file()] + for source_root in self._candidates[top]: + path = source_root.joinpath(*parts[:-1], parts[-1] + ".lean") + if path.is_file(): + return source_root, path + return None + + def olean(self, source_root: Path, module: str) -> Path: + parts = module.split(".") + built = source_root.joinpath(".lake", "build", "lib", "lean") + return built.joinpath(*parts[:-1], parts[-1] + ".olean") + + def mathlib_version(self) -> str: + """What the downloaded files must match: Mathlib's revision and the Lean version.""" + rev = next((p.get("rev", "") for p in self.manifest.get("packages", []) + if str(p.get("name", "")).strip("«»") == "mathlib"), "") + try: + toolchain = (self.root / "lean-toolchain").read_text(encoding="utf-8").strip() + except OSError: + toolchain = "" + return f"{rev} {toolchain}".strip() + + @property + def stamp(self) -> Path: + return self.mathlib / ".lake" / "build" / "get_mathlib.version" + + +def project_modules(root: Path) -> List[str]: + """Every Lean file of the project itself, as module names.""" + modules = [] + for folder, subfolders, files in os.walk(root): + subfolders[:] = sorted(d for d in subfolders if not d.startswith(".")) + for name in sorted(files): + if name.endswith(".lean") and name != "lakefile.lean": + rel = Path(folder, name).relative_to(root).with_suffix("") + modules.append(".".join(rel.parts)) + return modules + + +def as_module(root: Path, target: str) -> str: + """A target given as a module name or as a path to a .lean file, as a module name.""" + if not (target.endswith(".lean") or "/" in target or "\\" in target): + return target + path = Path(target) + path = path if path.is_absolute() else Path.cwd() / path + try: + rel = path.resolve().relative_to(root.resolve()) + except ValueError: + raise Problem(f"{target} is not inside the project folder {root}.") + if not path.is_file(): + raise Problem(f"{target} does not exist.") + return ".".join(rel.with_suffix("").parts) + + +def needed_files(ws: Workspace, targets: Iterable[str]) -> Tuple[Dict[str, Path], Set[str]]: + """Follow imports from the targets. + + Returns the modules reached that Mathlib's download tool serves (with their source roots), + and the ones among them to ask the tool for: those imported directly from outside, since + the tool fetches whatever they import in turn. + """ + needed: Dict[str, Path] = {} + ask: Set[str] = set() + seen: Set[str] = set() + stack = [] + for target in targets: + if ws.locate(target) is None: + raise Problem(f"Cannot find the module {target} in this project or its packages.") + stack.append((target, True)) + while stack: + module, from_outside = stack.pop() + found = ws.locate(module) + if found is None: + continue + source_root, path = found + served = source_root in ws.served + if served: + needed[module] = source_root + if from_outside: + ask.add(module) + if module in seen: + continue + seen.add(module) + try: + text = path.read_text(encoding="utf-8", errors="replace") + except OSError: + continue + for imported in header_imports(text): + if imported not in seen or not served: + stack.append((imported, not served)) + return needed, ask + + +# --------------------------------------------------------------------------------------------- +# Downloading +# --------------------------------------------------------------------------------------------- + +def find_lake() -> str: + lake = shutil.which("lake") + if lake: + return lake + for name in ("lake", "lake.exe"): + candidate = Path.home() / ".elan" / "bin" / name + if candidate.is_file(): + return str(candidate) + raise Problem("Cannot find `lake`. Is Lean installed? (It lives in ~/.elan/bin.)") + + +def batches(modules: List[str], limit: int = 6000) -> Iterable[List[str]]: + """Split a long list so that no command line exceeds what Windows accepts.""" + batch: List[str] = [] + size = 0 + for module in modules: + if batch and size + len(module) + 1 > limit: + yield batch + batch, size = [], 0 + batch.append(module) + size += len(module) + 1 + if batch: + yield batch + + +def say(text: str) -> None: + try: + print(text, flush=True) + except UnicodeEncodeError: + print(text.encode("ascii", "replace").decode("ascii"), flush=True) + + +def download(ws: Workspace, ask: Set[str], verbose: bool) -> bool: + """Run Mathlib's download tool on the given modules. False if it reports a failure.""" + lake = find_lake() + for batch in batches(sorted(ask)): + command = [lake, "exe", "cache", "get", *batch] + if verbose: + say("running: lake exe cache get <%d modules>" % len(batch)) + result = subprocess.run( + command, cwd=str(ws.root), stdout=subprocess.PIPE, stderr=subprocess.STDOUT, + universal_newlines=True, encoding="utf-8", errors="replace") + if verbose or result.returncode != 0: + say(result.stdout.rstrip()[-6000:]) + if result.returncode != 0: + say("Mathlib's download tool failed (exit code %d). This step needs internet access " + "to github.com and cache.mathlib.org." % result.returncode) + return False + return True + + +def main(argv: Optional[List[str]] = None) -> int: + parser = argparse.ArgumentParser( + description="Download the prebuilt Mathlib files this project needs, and no others.") + parser.add_argument("targets", nargs="*", metavar="TARGET", + help="module names or .lean files (default: all of the project's files)") + parser.add_argument("--check", action="store_true", + help="download nothing; exit 1 if a needed file is missing") + parser.add_argument("--dir", metavar="FOLDER", help="the project folder (default: this one)") + parser.add_argument("-v", "--verbose", action="store_true", + help="show the download tool's own output") + args = parser.parse_args(argv) + + try: + root = find_project_root(Path(args.dir).resolve() if args.dir else Path.cwd()) + ws = Workspace(root) + targets = [as_module(root, t) for t in args.targets] or project_modules(root) + needed, ask = needed_files(ws, targets) + + def missing() -> List[str]: + return sorted(m for m, source_root in needed.items() + if not ws.olean(source_root, m).is_file()) + + version = ws.mathlib_version() + try: + downloaded_for = ws.stamp.read_text(encoding="utf-8").strip() + except OSError: + downloaded_for = None + changed = downloaded_for is not None and downloaded_for != version + absent = missing() + from_mathlib = sum(1 for m in needed if needed[m] == ws.mathlib) + what = "%d prebuilt files needed (%d from Mathlib, %d from the packages it uses)" % ( + len(needed), from_mathlib, len(needed) - from_mathlib) + + if args.check: + if changed: + say("Mathlib files: Mathlib or Lean changed version since the files were " + "downloaded. Run this script without --check before building.") + return 1 + if absent: + say("Mathlib files: %d of the %s are missing, for example %s. " + "Run this script without --check before building." + % (len(absent), what, ", ".join(absent[:3]))) + return 1 + say("Mathlib files: all present; %s." % what) + return 0 + + if not absent and not changed and downloaded_for is not None: + say("Mathlib files: all present; %s." % what) + return 0 + if not download(ws, ask, args.verbose): + return 1 + still = missing() + if still: + say("Mathlib files: %d of the %s could not be downloaded, for example %s. " + "Do not build: Lean would compile them, which takes hours." + % (len(still), what, ", ".join(still[:3]))) + return 1 + ws.stamp.parent.mkdir(parents=True, exist_ok=True) + ws.stamp.write_text(version + "\n", encoding="utf-8") + if absent: + did = "downloaded %d" % len(absent) + elif changed: + did = "refreshed after a version change" + else: + did = "confirmed with Mathlib's download tool" + say("Mathlib files: %s; %s, all present." % (did, what)) + return 0 + except Problem as problem: + say("get_mathlib: %s" % problem) + return 2 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/scripts/setup.sh b/scripts/setup.sh index 718b999..52160fd 100755 --- a/scripts/setup.sh +++ b/scripts/setup.sh @@ -1,5 +1,8 @@ #!/usr/bin/env bash -# Set up this project: Lean, linglib and Mathlib, then build the worked example. +# Set up this project: Lean, linglib and the Mathlib files it uses, then build the worked example. +# +# bash scripts/setup.sh # download only the parts of Mathlib the project uses +# bash scripts/setup.sh --full # download all of Mathlib (for work that imports much of linglib) # # Safe to run more than once; finished steps are skipped quickly. # Prints one line per step. Full output of each step goes to .lake/setup-logs/. @@ -10,9 +13,19 @@ set -uo pipefail cd "$(dirname "$0")/.." +FULL=0 +for arg in "$@"; do + case "$arg" in + --full) FULL=1 ;; + *) printf 'Unknown option: %s\nUsage: bash scripts/setup.sh [--full]\n' "$arg"; exit 2 ;; + esac +done + LOGDIR=".lake/setup-logs" mkdir -p "$LOGDIR" export PATH="$HOME/.elan/bin:$PATH" +# Without this, Mathlib downloads all of its prebuilt files (about 7 GB) whenever Lake updates it. +export MATHLIB_NO_CACHE_ON_UPDATE=1 START=$(date +%s) step() { STEP_NAME="$1"; STEP_START=$(date +%s); printf '%s ... ' "$1"; } @@ -28,11 +41,15 @@ fail() { step "1/5 Checking prerequisites" command -v git >/dev/null 2>&1 || fail "git is not installed." command -v curl >/dev/null 2>&1 || fail "curl is not installed." +if [ "$FULL" -eq 0 ]; then + command -v python3 >/dev/null 2>&1 || fail "python3 is not installed. It runs the script that downloads only the Mathlib files this project uses." +fi free_gb() { df -Pk "$1" | awk 'NR==2 { print int($4 / 1048576) }'; } FREE_GB=$(free_gb .) HOME_FREE_GB=$(free_gb "$HOME") -if [ ! -d .lake/packages/mathlib ] && [ "$FREE_GB" -lt 12 ]; then - fail "Only ${FREE_GB} GB of disk space is free here. Setup needs about 12 GB in this folder." +if [ "$FULL" -eq 1 ]; then NEED_GB=10; else NEED_GB=3; fi +if [ ! -d .lake/packages/mathlib ] && [ "$FREE_GB" -lt "$NEED_GB" ]; then + fail "Only ${FREE_GB} GB of disk space is free here. Setup needs about ${NEED_GB} GB in this folder." fi if [ ! -d "$HOME/.elan/toolchains" ] && [ "$HOME_FREE_GB" -lt 3 ]; then fail "Only ${HOME_FREE_GB} GB is free in your home folder. Lean needs about 3 GB there." @@ -55,12 +72,28 @@ lake --version > "$LOGDIR/3-toolchain.log" 2>&1 \ done_step # 4. linglib and its dependencies, and the prebuilt Mathlib files -step "4/5 Downloading linglib and the prebuilt Mathlib files" -lake exe cache get > "$LOGDIR/4-dependencies.log" 2>&1 \ - || fail "Could not download dependencies. This step needs internet access to github.com and cache.mathlib.org." "$LOGDIR/4-dependencies.log" +NETWORK="This step needs internet access to github.com and cache.mathlib.org." +if [ "$FULL" -eq 1 ]; then + step "4/5 Downloading linglib and all of the prebuilt Mathlib files" +else + step "4/5 Downloading linglib and the prebuilt Mathlib files this project uses" +fi +: > "$LOGDIR/4-dependencies.log" +# Any Lake command fetches the packages named in lake-manifest.json; this one builds nothing. +# A download as large as Mathlib's source sometimes drops, so it is tried twice. +fetch_packages() { lake env lean --version >> "$LOGDIR/4-dependencies.log" 2>&1; } +fetch_packages || { sleep 5; fetch_packages; } \ + || fail "Could not download dependencies. $NETWORK" "$LOGDIR/4-dependencies.log" +if [ "$FULL" -eq 1 ]; then + lake exe cache get >> "$LOGDIR/4-dependencies.log" 2>&1 \ + || fail "Could not download the prebuilt Mathlib files. $NETWORK" "$LOGDIR/4-dependencies.log" +else + python3 scripts/get_mathlib.py --verbose >> "$LOGDIR/4-dependencies.log" 2>&1 \ + || fail "Could not download the prebuilt Mathlib files. $NETWORK" "$LOGDIR/4-dependencies.log" +fi done_step -# 5. Build the worked example (compiles the parts of linglib it uses) +# 5. Build the worked example (downloads linglib's prebuilt files and unpacks the parts it uses) step "5/5 Building the worked example" lake build MyProject.Example > "$LOGDIR/5-build.log" 2>&1 \ || fail "The worked example did not build." "$LOGDIR/5-build.log" diff --git a/scripts/test_get_mathlib.py b/scripts/test_get_mathlib.py new file mode 100644 index 0000000..9aacf7f --- /dev/null +++ b/scripts/test_get_mathlib.py @@ -0,0 +1,178 @@ +"""Tests for get_mathlib.py that need neither Lean nor a network connection. + + python3 -m unittest discover -s scripts -p 'test_*.py' +""" + +import json +import sys +import tempfile +import unittest +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import get_mathlib as gm # noqa: E402 + + +class HeaderImports(unittest.TestCase): + def check(self, text, expected): + self.assertEqual(gm.header_imports(text), expected) + + def test_plain_imports(self): + self.check("import A.B\nimport C\n\ndef x := 1\n", ["A.B", "C"]) + + def test_module_system_forms(self): + self.check( + "module\n\npublic import A\nmeta import B\npublic meta import C\nimport all D\n" + "import E\n\n@[expose] public section\n", + ["A", "B", "C", "D", "E"]) + + def test_prelude(self): + self.check("prelude\nimport Init.Core\n", ["Init.Core"]) + self.check("module\nprelude\npublic import Init.Core\n", ["Init.Core"]) + + def test_copyright_block_before_imports(self): + self.check("/-\nCopyright (c) someone.\nimport Not.This\n-/\nimport A\n", ["A"]) + + def test_nested_block_comment(self): + self.check("/- outer /- inner import X -/ still a comment import Y -/\nimport A\n", ["A"]) + + def test_comments_between_imports(self): + self.check( + "import A -- why\n-- import Skipped\n/-- a doc comment -/\nimport B\n" + "/-! module doc -/\nimport C\n", + ["A", "B", "C"]) + + def test_comment_touching_the_name(self): + self.check("import A--note\nimport B/- note -/\nimport C\n", ["A", "B", "C"]) + + def test_stops_at_first_declaration(self): + for rest in ("namespace N", "open Lean", "set_option autoImplicit false", "public section", + "@[expose] public section", "def import := 1", "theorem t : True := trivial"): + self.check("import A\n\n%s\nimport B\n" % rest, ["A"]) + + def test_module_doc_does_not_end_the_header_but_code_does(self): + self.check("import A\n\n/-! # Title\nimport Fake -/\n\nnamespace N\nimport B\n", ["A"]) + + def test_two_imports_on_one_line(self): + self.check("import A import B\n", ["A", "B"]) + + def test_windows_line_endings(self): + self.check("module\r\n\r\npublic import A\r\nimport B\r\n\r\ndef x := 1\r\n", ["A", "B"]) + + def test_no_imports(self): + self.check("", []) + self.check("-- only a comment\n", []) + self.check("def x := 1\n", []) + self.check("/- never closed\nimport A\n", []) + + +class Batches(unittest.TestCase): + def test_every_module_once_and_within_the_limit(self): + modules = ["Mathlib.Some.Module%d" % i for i in range(1000)] + parts = list(gm.batches(modules, limit=500)) + self.assertEqual([m for part in parts for m in part], modules) + self.assertTrue(all(sum(len(m) + 1 for m in part) <= 500 for part in parts)) + self.assertGreater(len(parts), 1) + + def test_empty(self): + self.assertEqual(list(gm.batches([])), []) + + +def write(path: Path, text: str = "") -> None: + path.parent.mkdir(parents=True, exist_ok=True) + path.write_text(text, encoding="utf-8") + + +class Project(unittest.TestCase): + """A small made-up project: MyProject -> Linglib -> Mathlib and Batteries.""" + + def setUp(self): + self.tmp = tempfile.TemporaryDirectory() + self.root = root = Path(self.tmp.name).resolve() + pk = root / ".lake" / "packages" + write(root / "lakefile.toml", 'name = "my_project"\n') + write(root / "lean-toolchain", "leanprover/lean4:v4.34.1\n") + write(root / "lake-manifest.json", json.dumps({ + "packagesDir": ".lake/packages", + "packages": [{"name": "mathlib", "rev": "abc"}, {"name": "linglib", "rev": "def"}]})) + write(root / "MyProject.lean", "import MyProject.Example\n") + write(root / "MyProject" / "Example.lean", "import Linglib.Core\nimport Init.Data\n") + write(root / "MyProject" / "Other.lean", "import Linglib.Extra\n") + write(pk / "linglib" / "Linglib" / "Core.lean", + "module\n\npublic import Mathlib.A\npublic import Batteries.Direct\n") + write(pk / "linglib" / "Linglib" / "Extra.lean", "import Linglib.Core\nimport Mathlib.C\n") + write(pk / "mathlib" / "lake-manifest.json", json.dumps({ + "packages": [{"name": "batteries"}, {"name": "aesop"}]})) + write(pk / "mathlib" / "Mathlib" / "A.lean", "import Mathlib.B\nimport Aesop\n") + write(pk / "mathlib" / "Mathlib" / "B.lean", "import Batteries.Deep\n") + write(pk / "mathlib" / "Mathlib" / "C.lean", "import Mathlib.B\n") + write(pk / "mathlib" / "Mathlib" / "Unused.lean", "") + write(pk / "batteries" / "Batteries" / "Direct.lean", "") + write(pk / "batteries" / "Batteries" / "Deep.lean", "") + write(pk / "aesop" / "Aesop.lean", "") + self.ws = gm.Workspace(root) + + def tearDown(self): + self.tmp.cleanup() + + def olean(self, package: str, module: str) -> Path: + return self.ws.olean(self.root / ".lake" / "packages" / package, module) + + def test_needed_and_asked_for(self): + needed, ask = gm.needed_files(self.ws, ["MyProject.Example"]) + self.assertEqual(set(needed), + {"Mathlib.A", "Mathlib.B", "Aesop", "Batteries.Direct", "Batteries.Deep"}) + # Only what is imported directly from outside Mathlib and its packages is asked for. + self.assertEqual(ask, {"Mathlib.A", "Batteries.Direct"}) + + def test_a_second_importer_from_outside_is_asked_for_too(self): + _, ask = gm.needed_files(self.ws, ["MyProject.Example", "MyProject.Other"]) + self.assertEqual(ask, {"Mathlib.A", "Batteries.Direct", "Mathlib.C"}) + + def test_default_targets_are_the_project_files(self): + self.assertEqual(gm.project_modules(self.root), + ["MyProject", "MyProject.Example", "MyProject.Other"]) + + def test_target_given_as_a_path(self): + path = str(self.root / "MyProject" / "Example.lean") + self.assertEqual(gm.as_module(self.root, path), "MyProject.Example") + with self.assertRaises(gm.Problem): + gm.as_module(self.root, str(self.root / "MyProject" / "Missing.lean")) + + def test_unknown_target(self): + with self.assertRaises(gm.Problem): + gm.needed_files(self.ws, ["MyProject.NoSuchFile"]) + + def test_check_mode(self): + argv = ["--dir", str(self.root), "--check", "MyProject.Example"] + self.assertEqual(gm.main(argv), 1) + for package, module in (("mathlib", "Mathlib.A"), ("mathlib", "Mathlib.B"), + ("aesop", "Aesop"), ("batteries", "Batteries.Direct")): + write(self.olean(package, module)) + self.assertEqual(gm.main(argv), 1) # Batteries.Deep is still missing + write(self.olean("batteries", "Batteries.Deep")) + self.assertEqual(gm.main(argv), 0) + # A file another module needs does not affect this one. + self.assertEqual(gm.main(["--dir", str(self.root), "--check"]), 1) + write(self.olean("mathlib", "Mathlib.C")) + self.assertEqual(gm.main(["--dir", str(self.root), "--check"]), 0) + + def test_check_fails_after_a_version_change(self): + for package, module in (("mathlib", "Mathlib.A"), ("mathlib", "Mathlib.B"), + ("aesop", "Aesop"), ("batteries", "Batteries.Direct"), + ("batteries", "Batteries.Deep")): + write(self.olean(package, module)) + argv = ["--dir", str(self.root), "--check", "MyProject.Example"] + write(self.ws.stamp, self.ws.mathlib_version() + "\n") + self.assertEqual(gm.main(argv), 0) + write(self.ws.stamp, "an older revision\n") + self.assertEqual(gm.main(argv), 1) + + def test_no_packages_yet(self): + with tempfile.TemporaryDirectory() as empty: + write(Path(empty) / "lakefile.toml", "") + self.assertEqual(gm.main(["--dir", empty, "--check"]), 2) + + +if __name__ == "__main__": + unittest.main()