Set up and run
Every figure and every number of a lesson comes from code in the repository. Each lesson has an experiment: a program that computes what the page shows and writes its figures and numbers into a folder of your choice, so that you can change the code and run it again. The last section of every lesson gives its commands. This page says what to install for each of three things you may want to do:
- Run an experiment of a simulation or a measured-data lesson. This needs Git and uv, and nothing else.
- Replay an agent lesson. The same setup: the replay runs every tool call of a recorded run again, without a model and without a key. A live run with a model is a separate, optional step with your own account.
- Check a proof of a Lean lesson, or work on its exercises. This adds the Lean toolchain.
None of these builds the website. Commands that the site’s own checks run are shown plainly. Every other command is marked “Not verified” and names the account or key it needs.
Run an experiment
A computer running macOS or Linux, about 1 GB of free disk space, and an internet connection for the first run. Windows is not supported. Install these two tools once; this is the only step that may need administrator rights.
| Tool | Purpose | macOS | Linux |
|---|---|---|---|
| Git | Source control | Xcode command line tools, or brew install git |
System package manager |
| uv | The pinned Python and the Python packages | brew install uv |
curl -LsSf https://astral.sh/uv/install.sh \| sh |
Then fetch the repository and its locked Python packages:
git clone https://github.com/taspinar/physics-by-construction.git
cd physics-by-construction
uv sync --locked --no-dev--no-dev installs the packages the lessons need, NumPy, SciPy, Matplotlib, and PyYAML at the versions of uv.lock, and nothing else: no site generator, no notebook kernel, no browser, and no test tools, which only the maintainers of the site use.
Each lesson’s experiment is a Python module of the repository. Its command, from the folder of the clone, runs it and writes the figures of the page as <label>.png and every number and table of the page, as the page shows them, into results/results.json. For the first lesson:
uv run --locked --no-dev python -m pbc.mechanics.experiments.kinematics resultsA lesson that analyses measured data runs the same way; its data is a sample committed to the repository:
uv run --locked --no-dev python -m pbc.mechanics.experiments.automated_analysis_pipelines resultsThe pattern, with the lesson’s own module in place of the name in angle brackets; the last section of every lesson names it:
Not verified. The build of this site did not run or check the material in this box.
uv run --locked --no-dev python -m pbc.<course>.experiments.<lesson> resultsThe experiment of a lesson is in src/pbc/<course>/experiments/, and it calls the lesson’s code in src/pbc/. Change either and run the command again to see what changes. The numbers match the page to the digits it shows; digits beyond those can differ between machines, because floating-point libraries differ.
Replay an agent lesson
The agent lessons need no more than the setup above. Their experiment replays the recorded run of the agent: it sends every tool call of the recording to the allowlist and the simulation again, compares the results, and writes the figures and numbers of the page. It calls no model and needs no key:
uv run --locked --no-dev python -m pbc.mechanics.experiments.agent_experiment resultsOptional: a live run
This runs an agent lesson against a language model, with your own account. It needs an OpenAI account and an API key, and the optional dependency openai; it costs a few cents. The key stays in an environment variable of your shell, never in a file or in code. The site never does this, so the commands are not verified. The last section of each agent lesson names its own module.
Not verified. The build of this site did not run or check the material in this box.
# needs: an OpenAI account and its API key, and the optional dependency openai
uv sync --locked --no-dev --extra openai
export OPENAI_API_KEY="..." # this shell only
uv run --locked --no-dev --extra openai python -m pbc.agents.projectile_labOptional: check a proof
The Lean lessons state theorems that a computer has checked. To check them yourself, or to work on the exercises of Lean exercises on your machine, add the Lean toolchain. It needs no account, but about 11 GB of free disk space for the Mathlib build cache.
| Tool | Purpose | macOS | Linux |
|---|---|---|---|
| elan | The pinned Lean toolchain | brew install elan-init |
curl -sSf https://elan.lean-lang.org/elan-init.sh \| sh |
Put ~/.elan/bin on your PATH; the elan installer offers to do it. Then, in the clone:
cd lean
lake exe cache get
lake buildlake exe cache get fetches the Mathlib build cache (about 0.5 GB, unpacking to roughly 11 GB); never compile Mathlib yourself. lake build checks every proof of the site; the last section of a Lean lesson names the modules of that lesson. To work on an exercise, open the lean/ folder in an editor with Lean support, such as Visual Studio Code with the Lean 4 extension, replace a sorry, and check the file:
Not verified. The build of this site did not run or check the material in this box.
# in lean/, after editing the exercise
lake env lean Exercises/ConstantAcceleration.leanOptional: drive a coding agent
You can ask a coding agent, such as Claude Code or Codex, to write a simulation from a specification. You choose the agent and supply its account and credential; the site names none as a requirement and never runs one. The rules of the sandbox profile (ADR 010) apply:
- Work in a scratch checkout, never in a checkout you care about.
- Let the agent run only the listed commands: the experiments, the tests, the formatter, and the lesson’s own scripts.
- Give it no network access beyond its own provider. Its credential stays in your environment, in the variable that agent documents.
- Set a budget in steps, time, and cost before you start.
- Read every diff before you run it.
Not verified. The build of this site did not run or check the material in this box.
# needs: an account with the coding agent's provider, and its credential in
# your environment (see the agent's own documentation)
git clone https://github.com/taspinar/physics-by-construction.git scratch
cd scratch
uv sync --locked --no-dev
# start your coding agent here, with the allowlist and budget set aboveTroubleshooting
| What you see | Cause | What to do |
|---|---|---|
git: command not found or uv: command not found |
A tool of the setup is missing | Install it from the first table |
uv sync --locked says the lock file needs an update |
uv.lock and pyproject.toml differ in your checkout |
Check out a clean commit; do not run uv lock to get past it |
No module named 'pbc' or No module named 'pbc.mechanics.experiments' |
The command ran outside the folder of the clone, or before uv sync |
Change to the folder of the clone and run uv sync --locked --no-dev first |
An experiment stops with ReplayMismatch |
The code of an agent lesson changed, so a recorded result no longer comes out | Expected after you change the code: the replay says which call differs. A live run records a new run |
No module named 'openai' in a live run |
The optional dependency is missing | uv sync --locked --no-dev --extra openai, and run with --extra openai |
| The live agent says the key variable is not set | OPENAI_API_KEY is not exported in this shell |
Export it in the shell that runs the command |
lake: command not found |
elan is missing, or ~/.elan/bin is not on PATH |
Install elan, then add ~/.elan/bin to PATH and open a new shell |
lake exe cache get cannot reach its host |
The Lean release host or the cache host is unreachable from your network | Retry later or from another network |
lake stops at a prompt for GitHub credentials while cloning Mathlib |
GitHub refused an anonymous clone | Retry; if it persists, set a GitHub credential helper or run gh auth login |
lake build starts to compile Mathlib |
The build cache was not fetched or is incomplete | Stop it and run lake exe cache get again |