Install the pinned Lean by hand

Download Lean 4.34.1, check it against the committed pins and verify the extracted tree with lema verify-distribution.

scripts/cloud-setup.sh does all of this for you. Follow these steps when you want the distribution somewhere else, or want to run each check yourself. The directory you end up with is the one a runtime configuration names as distribution.

Before you start

Linux x86_64 with curl, sha256sum, and GNU tar with zstd.
A lema-lang checkout with lema on your PATH. cargo build --release -p lema-cli writes it to target/release/lema.
A shell at the repository root.

Steps

Choose a new, empty directory for the distribution. Its parents must not be writable by other users. The setup script uses this one:

Shell

DIST=$HOME/.lema/toolchains/lean-4.34.1-linux-x86_64
mkdir -p $HOME/.lema/toolchains
chmod go-w $HOME/.lema $HOME/.lema/toolchains

Download the archive. The URL is the archive_url in toolchain/lean-4.34.1-linux.extraction-manifest.json:
Shell
```
curl -fLO https://github.com/leanprover/lean4/releases/download/v4.34.1/lean-4.34.1-linux.tar.zst
```

Check the archive against ARCHIVE_SHA in crates/lema-check/src/pins.rs:

Shell

echo "47bf4bbd78f70c2e9670598ab7124d92b6efb7330ff33e5fbb4030f6fd72e4e4  lean-4.34.1-linux.tar.zst" | sha256sum -c -

Stop here unless it prints OK.

Extract it:
Shell
```
mkdir -p "$DIST"
tar --zstd --no-same-owner -xf lean-4.34.1-linux.tar.zst -C "$DIST"
```
Keep --no-same-owner if you run as root. Without it, tar keeps the archive’s file owners, and the check refuses files that belong to anyone but root or you.
Copy the committed extraction manifest into the distribution, under the name the check looks for:
Shell
```
cp toolchain/lean-4.34.1-linux.extraction-manifest.json "$DIST/extraction-manifest.json"
```
The manifest lists the SHA-256 of each of the 17,738 files and the target of each of the 12 symlinks. Its own SHA-256 is pinned as DISTRIBUTION_SHA (c82b7b44…97a5).
Make the tree read-only:
Shell
```
chmod -R a-w "$DIST"
```
The runtime records the metadata of every entry when it loads. If anything changes after that, native calls stop until the runtime is loaded again.

Verify it:

Shell

lema verify-distribution "$DIST"

It hashes every file, so it takes a while. On success it prints one line that starts with the path you gave:

Output

…: the pinned Lean distribution (17738 files, 12 symlinks; manifest c82b7b44dd02daae5aa46c3f7e0a1e564da1a183fd81c021f299370a51d297a5)

The lean binary is now at $DIST/lean-4.34.1-linux/bin/lean. To make scripts/cloud-setup.sh use this tree instead of downloading another, run it with LEMA_DIST=$DIST.

If verification fails

lema verify-distribution prints lema: and the first problem it finds, then exits 1.

Message	Cause
`…/extraction-manifest.json: No such file or directory (os error 2)`	Step 5 was skipped.
`distribution manifest drift`	The manifest is not the committed one.
`runtime path is writable by another user: …`	A file or directory is group- or world-writable, or belongs to another user.
`runtime parent is writable by another user: …`	A parent of `DIST` is writable by others. A root-owned sticky directory such as `/tmp` is allowed.
`runtime path is a symlink: …`	`DIST` is a symlink. Give the real directory.
`distribution file set drift`	Files are missing or extra, for example after extracting into a directory that was not empty.
`distribution file drift: …`	That file’s contents differ from the manifest.

To start again, make the tree writable before you remove it: chmod -R u+w "$DIST" && rm -rf "$DIST".

Written against lema-lang at commit 5a94951, 17 Oct 2026.