One Mathlib
for every Lean project.

Every Lean project normally downloads and builds its own multi-gigabyte copy of Mathlib. sharlean points every project at one shared, globally installed copy instead.

$ sharlean new my_proof --require mathlib

Many copies, or one

The same three proof projects, set up the usual way and with sharlean.

Without sharlean

Each project clones and builds its own dependencies. lake update re-clones them all again.

With sharlean

Each project's manifest points at the shared copy by local path. Nothing is downloaded or rebuilt.

Commands

Install a library once, then scaffold as many projects against it as you like.

sharlean list                                  # installed shared libs (toolchain + git rev)
sharlean install mathlib --tag v4.29.0         # clone + cache-get + lock build dir (idempotent)
sharlean install cslib --tag v4.36.0-rc1       # built against the shared Mathlib
sharlean new <dir> --require mathlib          # scaffold + build a thin project (no lake update)
sharlean manifest <lib>                        # regenerate the path manifest after a version bump
sharlean unlock <name>                         # re-enable writes on a lib's build dir for upgrades

How it keeps the shared copy safe

Never runs `lake update`

Manifests hold only local path entries, pointing at packages the shared clone already has checked out.

Locks the build

After a successful build the shared .lake/build is made read-only, so Lake cannot delete it. An interrupted install resumes.

Matches the toolchain

Each new project copies its lean-toolchain from the shared library, because a mismatch means an hours-long rebuild.

Links libraries to each other

cslib is rewired to build only its own files against the prebuilt Mathlib, and projects get Mathlib through it.

Known limits

One --require per new for now. To combine libraries, scaffold with the primary one, add require lines, and rerun sharlean manifest.
Hyphens in the project directory break the build (expected a 'Name'). Use underscores: my_project.
With LAKE_ARTIFACT_CACHE=true, Lake tries to write into the locked build and fails, so linked projects build without it.

Install

git clone https://github.com/theTyster/sharlean.git
cd sharlean && lake build
ln -s "$(pwd)/bin/sharlean" ~/.local/bin/sharlean

Needs only elan on your PATH.

One Mathlibfor every Lean project.