axsent
Measures what a formal library actually assumes — across Rocq, Agda and Isabelle, read from source, with nothing compiled.
pip install axsent · Rocq, Agda, Isabelle · builds nothing
What it does
Measures what a formal library actually assumes — its axioms, and the
interface assumptions that get counted alongside them — across Rocq,
Agda and Isabelle, read from source with nothing compiled.
pip install axsent
axsent <path-to-library>
Why nothing is built
A census that requires building the library can only measure libraries that
still build. That silently excludes the old, the abandoned and the ones
pinned to a compiler nobody has, which is a biased sample of exactly the
wrong kind, because those are the ones whose assumptions nobody has looked at
lately.
The finding behind it
Every census of this kind conflates two different things: assumptions that
are mathematical, and assumptions that are about the
interface to the outside world. They are counted together and
reported as one number. Separating them is most of what this tool is for, and
the measurements are written up in the papers.
How it works
- Install it
pip install axsent. - Point it at a libraryIt reads the source. There is no build step, no toolchain to match, and no compiler version to satisfy.
- Read the splitAssumptions that are mathematical, reported separately from assumptions about the interface to the outside world.
What it measures
Three systemsRocq, Agda and Isabelle, from one tool.
Nothing is builtA census that requires building can only measure libraries that still build, which silently excludes the old, the abandoned, and anything pinned to a compiler nobody has.
The finding behind itEvery census of this kind conflates mathematical assumptions with interface assumptions and reports one number. Separating them is most of what this is for.
Four populationsIncluding assumptions that assert nothing at all, which no previous census counted separately.
Agda's --safeThe only self-validating harness among the three, and the measurements say why.
DepositedThe measurements are written up and deposited with DOIs.
Specifications
| Install | pip install axsent |
|---|
| Reads | Rocq, Agda, Isabelle |
|---|
| Builds | Nothing |
|---|
| Source | vince-gonzalez/axsent |
|---|
Questions
- Why not just build the library and ask it?
- Because then you can only measure libraries that still build, and the ones that do not are exactly the ones nobody has checked lately.
- Is this the same as gonzalgo?
- No. gonzalgo does Lean 4 and Metamath. axsent does Rocq, Agda and Isabelle, and does it without building.