Posts about the Acorn tools, like the VS Code extension.
View All Tags
Acorn 0.1 is out! It might not be obvious at first, but there's a big change in the guts of how the prover works. When a proof is successfully verified, the build directory now contains a "proof certificate" explaining step by step how the proof works.
There's a useful new feature in Acorn Prover 0.0.8: a build cache.
When you save changes to an Acorn project, the AI model automatically completes simple proofs with missing steps. Usually this works great, but this can make refactoring more difficult. In particular, if you make changes to a module like nat.ac that many other modules depend on, it can be slow to rebuild everything. If you want to remove a theorem that is used in many places, this can involve many slow rebuilds.