Changelog

This page records the changes in the development version 2.1.0-dev and in the 2.0.8 series. The authoritative source is the CHANGES.md file in the Abella repository.

2.1.0-dev

Reasoning-level modules

• Added .thmod files with one top-level Module/End block and optionally nested parameterized modules. Declarations are scoped by module and stored in .thmodc artifacts.
• Added Import Module with quoted files or in-scope modules and instances, aliases, positional type arguments, and with clauses for declared predicates and axiom items.
• .thm files and interactive input may define modules inline. These are local to the file or session and are not exported by .thc.
• Added Show Module to print module summaries at top level or inside proofs.
• .thmod files reject specification-logic sequents ({ ... }); inline modules in .thm files may use them.
• abella_doc now generates pages for .thmod files, highlights module commands, and links quoted Import Module targets to their pages.

Abella Web

• Abella now has a web interface at abella-prover.org/web. The source distribution contains the Abella Web source and instructions for running a local server. See web/README.md.

Additions

• Added --strict-stratification to abella and abella_doc to treat stratification failures as errors. Abella Web exposes the same option as a saved preference.

• Added the Axiom command, which declares a theorem without requiring a proof. In batch mode, the axioms used are listed at the end of the run.

• Added the compute tactic for asynchronous computation on hypotheses. See examples/compute/.

• Added the no-argument form of clear, which removes duplicate predicate hypotheses.

• Added the fchain tactic for forward-chaining a list of lemmas:

  [hint:] fchain [depth] lem1 lem2 ... .

  The lemmas are tried from left to right, and their immediate consequences are added as hypotheses. The optional depth defaults to the number of lemmas. The tactic is branching.

• Added Suspend guards for compute, and the f^n t iteration syntax.

Changes

• The -i flag is deprecated and does nothing; use a frontend such as Abella Web for interactive sessions.
• The -c/--compile option is deprecated and its argument is ignored. The compiled artifact is always placed in its default location.
• Abella now requires Dune 3.20 or later.
• Abella is no longer supported on ppc32 and ppc64.
• abella_doc supports light and dark mode, accepts --verbosity, and forwards it to Abella. --verbose now sets verbosity to at least 2. It also accepts --web and --share for links to Abella Web and the ZIP Worker.

Bugfixes and soundness fixes

• apply now prevents capture when instantiating forall-quantified variables in a lemma. This is a breaking change that can change the numbering of variables, even bound variables (#164).
• Split is less picky about the forms of generated theorems (#161).
• File names in error locations are now correct (PR #157).
• Fixed the lambda-prefix for non-Llambda unification problems (#155).
• Import ... with now requires pairwise distinct replacements for declared predicates (#152, soundness bug).
• Import ... with performs replacements simultaneously (#153).
• Abella now compiles with OCaml 5.5 (#166).
• A bound-variable clash is now a unification error instead of a failure (#168).
• Left-unification no longer treats logic variables as constant-like, so a logic variable is not provably different from a constant (#170, soundness bug, breaking change).
• Left-unification no longer lowers the timestamp of an eigenvariable by renaming it (#171, soundness bug).
• Meta-right-unification now checks binder and operand types, so differently typed statements are not accepted as equal (soundness bug).
• Meta-right-unification no longer leaks tentative type bindings from its binder compatibility check, and compares each body under that side's own binder type.
• Case analysis now reports generic instantiations instead of dropping cases.
• Type substitutions are now simultaneous, fixing swapped type parameters.
• Split propagates the source theorem's tag: finished, unfinished (a proof containing skip), or axiomatic.
• Stratification checks inspect defined predicates passed to declared higher-order predicates, and can be configured as hard errors.
• Subordination checks reject new edges between separately closed types.
• Diagnostics and relative imports use the real input file name.
• Compiled declarations store declaration-local type parameters explicitly; existing .thc files are recompiled.

2.0.8.3

This is a very small bugfix release.

Changes:

• Abella compiles with Dune 3.7 or later (#154).
• Abella is byte-compiled for ppc32 and ppc64 (#153).
• The dependency on libcurl is removed, temporarily (#151).

Bugfixes:

• Import ... with requires the replacements for declared predicates in the importee to be pairwise distinct (#152). This fixes a soundness bug.

2.0.8.2

This is a very small bugfix release. It was tagged four days after 2.0.8.1 and differs from it only in packaging.

Changes:

• Abella compiles with Dune 3.7 or later.
• Abella is byte-compiled for ppc32 and ppc64.

Bugfixes:

• Import ... with requires pairwise distinct replacements. This fixes a soundness bug.

2.0.8.1

This is a very small bugfix release.

Changes:

• Abella compiles with Dune 3.7 or later.

Bugfixes:

• Import ... with requires pairwise distinct replacements. This fixes a soundness bug.

2.0.8

This release changed the build system, the parser, and the command line, and it moved the annotation and dependency outputs into separate programs.

Possibly breaking changes:

• Abella uses Dune instead of ocamlbuild.
• The -v option is removed; use --version.
• The -nr option is removed; use --non-recursive.
• In batch mode, Abella always produces file.thc from file.thm.
• The parser changed from ocamlyacc to Menhir.
• Annotation mode (-a) produces JSON instead of HTML fragments.
• The dependency generator option -M moved to abella_dep.

Additions:

• abella_doc generates HTML pages from Abella sources.
• abella_dep produces a Makefile-based dependency graph.
• Proofs that contain skip are reported.
• The types flag prints the types of quantified variables.

Bugfixes include the first Type/Kind declaration being added to the specification signature, type unification in reasoning-level formulas, and several soundness bugs in apply with unknowns and higher-order definitional clauses.

Earlier releases

Releases before 2.0.8 are listed in the same CHANGES.md file. The most recent of them is 2.0.7, which fixes a number of minor bugs and makes Abella compilable with OCaml 4.08.0 and later.