Version 2.0.8

Changes in 2.0.8 from 2.0.7

Possibly breaking changes

• Abella now uses Dune instead of ocamlbuild.
  (#138, additional contributions: Chase Johnson)
• The command line for the abella command has slightly changed.
  • 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.
• Abella's parser changed from ocamlyacc to Menhir
• Abella's annotation mode (-a) now produces annotations in JSON format
  instead of in HTML fragments. The JSON schema should be seen as
  experimental for now and subject to change in the future.
• Abella's dependency generator option (-M) has now been moved to
  a separate program (see "Additions" below).

Additions

• Documentation Generation (abella_doc): There is now a special program
  called abella_doc that can be used to convert a collection of Abella
  sources into HTML pages that resemble the Abella examples on the
  web-site: https://abella-prover.org/examples/

  Run abella_doc --help for usage instructions.

• Dependency Generation (abella_dep): There is now a special
  program called abella_dep that can be used to generate a
  Makefile-based dependency graph. Executing make on that
  Makefile will recompile all the Abella sources specified to
  abella_dep. This Makefile can be used in parallel (i.e., make -j)
  mode.

• Mention that a proof contained "skip" during interactive mode, and a
  summary of skipped theorems in batch mode.
  (#137, reported by Farah Al Wardani)

• The types flag when set to on will now print the types of
  quantified variables as well.

Bugfixes

• Automatic compilation in Import statements now does not clobber existing
  partial compilation results. This improves the support for multiple runs
  of Abella in parallel using the same source files.
• The first Type or Kind declaration was accidentally being added to
  the specification signature.
  (Identified by Farah Al Wardani, @innofarah)
• Unification of reasoning-level formulas attempts type unification instead
  of assuming ground types.
  (#143, reported by @RandomActsOfGrammar)
• Hypothesis name hints that match generated hypothesis names should update
  the generator count.
  (#145, reported by Todd Wilson @lambdacalculator)
• Apply with unknowns now requires each computed subgoal to fully instantiate
  logic variables. SOUNDNESS BUG
  (#146, reported by @Chen-PL, @jiangsy)
• Apply with unknowns now undoes variable instantiations on failed search
  for generated logic variables. 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.
  SOUNDNESS BUG
  (#147, discovered by Sebastiaan Joosten, reported by Gopalan Nadathur)
• Backchaining specification clauses now respects subordination when raising
  newly introduced variables.