pac #

pac is a mechanised package calculus in Rocq: a minimal core semantics of dependency resolution, extended with the features of real package managers, each extension reduced to the core with the reduction proved sound and complete. The reductions extract to OCaml, and frontends for Debian, Alpine, opam, Cargo and npm use them to drive PubGrub.

Build #

rocq-stdlib comes from the coq-released opam repository.

opam repo add coq-released https://coq.inria.fr/opam/released
opam install . --deps-only
dune build

Usage #

Fetch an index for each ecosystem into repos/ (or name a subset):

scripts/fetch-repos.sh

pac debian --native amd64 repos/debian/Packages nano
pac alpine repos/alpine/APKINDEX nginx
pac opam repos/opam-repository lwt
pac cargo repos/crates.io-index path/to/Cargo.toml
pac npm --cache repos/npm --tree use-sync-external-store

pac npm reads manifests as npm does; --reading=shared reads them as npm and Yarn Berry both do, so that an answer is one both accept; and --reading=placement answers npm's node_modules layout itself, within --depth levels.

Trusted base #

The reductions and the decoding of their answers are proved in Rocq. Trusted: PubGrub (its answer is decoded unchecked), each frontend's parsers and version comparators, the lookup tables' faithfulness to the parsed index, pac npm --omit, which leaves out of a decoded answer what the omitted class's edges alone reach, and the placement reading's orders on names and versions, restated in OCaml from the extracted ones (PAC_NPM_CHECKCMP compares the two). The --order hooks are not: they only choose among what PubGrub offers.

Evaluation #

See eval/README.md for the tests and for comparing pac against apt, apk, opam, cargo and npm.

Programmed with Claude Code