What publish does
1
Build
lake build compiles the library and checks every proof. --skip-build skips this when the workspace is already built.2
Audit
Audit.lean lists the main theorems and their axioms. Publishing fails if any of them uses anything beyond propext, Classical.choice and Quot.sound.3
Export
For every model (or only those given with
--model), theformalera-spec exports the nodes, the value-flow graph, the shape and value domains, the configuration in config.json form and the architecture summary into the manifest.4
Attach trust status
With
--conformance, the result of a theformalera-conformance verify-all --report run is recorded for each model.5
Sign and store
Each package is signed with the publisher key and written with its manifest, its version index entry and the model list. Its public key is added to
keys.json.unchanged. To change a spec, bump the version. Patch versions may change only docs and metadata.
After publishing a new library version
The engine’s certificates import the spec library’s Lean modules, including its built-in lemmas. Projects pick up a new package withtheformalera pull --update.
If you add Lean lemmas that certificates use, republish the package. An older package lacks them, and proofs that need them fail to check against it.
Advisories
When a published spec turns out to be wrong:pull, and nightly CI runs report it.