This artifact accompanies the paper Package Managers à la Carte: A Formal Model of Dependency Resolution.

This artifact is a Lean 4 mechanisation of the Package Calculus: a core calculus of dependency resolution, a family of extensions modelling features found in real-world package managers, a composition of two of those extensions, and the NP-completeness of dependency resolution (via a 3SAT reduction). For a mapping of paper definitions and theorems see the ./paper-mapping.md file.

This is a proof-script artifact; there is no executable tool to run: the contribution is the machine-checked development itself.

Requirements

• The Lean toolchain pinned in lean-toolchain (leanprover/lean4:v4.28.0). This is installed automatically by elan, and bundles the build tool lake.
• Mathlib, pinned to the revision in lakefile.toml and locked in lake-manifest.json.

The artifact has been tested on Linux. The Lean toolchain also runs on macOS and Windows, so the build is expected to work there too.

Building

Install Lean via elan (its version manager) following the official instructions (https://lean-lang.org/install/manual/) with curl https://elan.lean-lang.org/elan-init.sh -sSf | sh, or via your operating system's package manager. elan provides the lake build tool and installs the pinned toolchain automatically. Then, from the project root:

make cache    # fetch Mathlib's cached .olean files for the pinned revision
make build    # build the whole development
make validate # build, then print the axioms behind every headline theorem

make cache fetches Mathlib's cached .olean files matching the pinned revision; without it, Mathlib is compiled from source, which can take a long time.

make validate executes scripts/axioms.lean to audit axioms. A clean audit lists, for each headline theorem, only Lean's standard classical axioms -- propext, Classical.choice, and Quot.sound.

make clean drops only this development's .oleans, so make build recompiles just it against the cached Mathlib -- fast and offline.