Skip to main content
Version: 2.0.8

Changelog

This page records the changes in the 2.0.8 series. The site documents the latest patch release, 2.0.8.3. The authoritative source is the CHANGES.md file in the Abella repository.

2.0.8.3​

This is a very small bugfix release.

Changes:

  • Abella now compiles with Dune version 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 now requires the replacements for the 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 now compiles with Dune version 3.7 or later.
  • Abella is byte-compiled for ppc32 and ppc64.

Bugfixes:

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

2.0.8.1​

This is a very small bugfix release. It contains the same source changes as 2.0.8.2 and 2.0.8.3 apart from the packaging and dependency changes listed above.

Changes:

  • Abella now compiles with Dune version 3.7 or later.

Bugfixes:

  • Import ... with now requires the replacements for the declared predicates in the importee to be pairwise distinct. 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. Some of these changes can require updates to existing scripts and build rules.

Possibly breaking changes:

  • Abella now uses Dune instead of ocamlbuild (#138, with additional contributions from Chase Johnson).
  • The command line of abella changed slightly:
    • the old -v option is removed; use --version instead;
    • the old -nr option is removed; use --non-recursive instead.
  • In batch mode, Abella always produces file.thc from file.thm.
  • The parser changed from ocamlyacc to Menhir.
  • Annotation mode (-a) now produces JSON instead of HTML fragments. The JSON schema is experimental and may change in future releases.
  • The dependency generator option -M has moved to a separate program, abella_dep.

Additions:

  • Documentation generation (abella_doc) converts a collection of Abella sources into HTML pages that resemble the official examples. Run abella_doc --help for usage instructions. See abella_doc.
  • Dependency generation (abella_dep) produces a Makefile-based dependency graph. Running make on that Makefile recompiles the Abella sources given to abella_dep, and the Makefile works with parallel make -j. See abella_dep.
  • A proof that contains skip is now reported in interactive mode, and batch mode prints a summary of skipped theorems (#137).
  • The types flag, when set to on, now prints the types of quantified variables as well.

Bugfixes:

  • Automatic compilation in Import statements no longer clobbers existing partial compilation results. This improves support for several Abella runs in parallel on the same sources.
  • The first Type or Kind declaration was accidentally added to the specification signature. This is fixed.
  • Unification of reasoning-level formulas attempts type unification instead of assuming ground types (#143).
  • Hypothesis name hints that match generated hypothesis names now update the generator count (#145).
  • Apply with unknowns now requires each computed subgoal to fully instantiate logic variables (#146). This fixes a soundness bug.
  • Apply with unknowns now undoes variable instantiations when the search for generated logic variables fails. This fixes a soundness bug related to #146.
  • Definitional clauses with higher-order parameters now trigger a non-well-formedness warning, because they can be used to prove false (#147). This fixes a soundness bug.
  • Backchaining specification clauses now respects subordination when raising newly introduced variables.

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.