Minor compatibility release: 2.0.8.2

• Byte-compile for arch=ppc32|ppc64. Possibly fixes #151.

Small bugfix release: 2.0.8.1

Changes

• Abella now compiles with Dune version 3.7 or later.
  (#154, reported by @yurivict)

Bugfixes

• Import ... with now requires the replacements for the declared
  predicates in the importee to be pairwise distinct.
  (#152, discovered in discussions with Farah Al Wardani @innofarah and Dale
  Miller @ThatDaleMiller)
  SOUNDNESS BUG

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.

Version 2.0.7: Bugfixes

This release adds no functionality, but fixes a number of minor bugs. It also
makes Abella compilable with OCaml versions 4.08.0 and higher.

Bugfixes

• Import statements with file paths containing . no longer break
  the HTML exporter
• Quote filenames when making shell calls
  (#115, reported by @JimmyZJX)
• Asserting trivial facts incorrectly left variables instantiated
  (#113, reported by Jinxu Zhao)
• Fully check that types are well-formed
  (#128, reported by @RandomActsOfGrammar)
• Case for async object sequents should normalize before clause selection
  (#129, reported by Guillaume Melquiond)
• Monotone for backchaining sequents should preserve backchaining
  (Related to #129, formally justified by conjunct 2 of logic/hh_meta.thm)

Version 2.0.6: Schematic Polymorphism

Changes in 2.0.6 from 2.0.5

Additions

• The schematic polymorphism branch has been merged.

  You can read more about it here:

  http://abella-prover.org/schm-poly/index.html

  Thanks to Yuting Wang and Gopalan Nadathur for developing the theory
  to match the implementation by Yuting.

Tweaks to existing functionality

• Polymorphic definitions and theorems in the style of version 2.0.5
  are now recast in the style of schematic polymorphism in 2.0.6.
  There should be minimal user-visible impact.

Bugfixes

• Confusing nominal and other constants in eta-contraction
  #110 (Reported by Yuting Wang)
• Permutations of nominal constants in equivariant
  matching failed to respect types.
  #107 (Reported by Matija Pretnar)
• Error in renaming of bound variabls in metaterms.
  #106 (Reported by Yuting Wang)
• Incorrect pretty-printing of (pi x\ p x).
  #104 (Reported by Dan DaCosta)

Release 2.0.5

Changes in 2.0.5 from 2.0.4

Additions

• Added support for (first-order) polymorphic definitions. Definitions
  such as the following are now accepted.

    Define fresh : A -> B -> prop by
      nabla x, fresh x M.
  

  In every use of the definition, the type arguments are implicitly
  instantiated. The type-checking for such definitions is identical to
  taking all the unbound variable names and quantifying them on the outside.
  In other words, for the above definition, the behavior of type-checking is
  the same as if there were:

    Kind A,B  type
    Define fresh : A -> B -> prop by
      nabla x, fresh x M.
  

  Once such a definition is type-checked, the defined symbols are added to
  the signature as new polymorphic constants, in a vein similar to the pi
  constant. Whenever it is used, the type arguments are implicitly
  instantiated based on the types of the arguments.

• Added support for (first-order) polymorphic theorems. A theorem such as
  the following is now accepted.

    Theorem prune[A] : forall E L, nabla (x:A), member (E x) L ->
       exists F, E = x\ F.
  

  The A here is a type parameter, which must be distinct from the other
  basic types in scope. To use such a theorem, you must supply enough
  arguments. An example:

    Theorem bar : forall E G, nabla (x:tm) (y:ty),
       member (E x y) G -> exists F, E = x\ y\ F.
    intros.
    apply prune[tm] to H1.
    apply prune[ty] to H1.
    search.
  

Tweaks to existing functionality

• The syntax for quantifiers now allows for multiple bound variables of the
  same type. Example:

    /* Type p i -> i -> prop. */
    forall (x y : i) (f g : i -> i), p (f (g y)) (g (f x))
  

• The apply tactic now takes an optional numerical argument that defines
  the search depth for automatic searches performed for omitted arguments. A
  bound of 0 means that no searches are attempted.

• The abbrev and unabbrev tactics now both take a list of hypotheses to
  (un)abbreviate. The display of abbreviations has also been compressed.

• Error messages in interactive mode are printed to stderr in addition to any
  other output file specified with -o.

• The monotone tactic now accepts hypothesis naming hints. (#91)

Bugfixes

• Query was broken since 2.0.4-beta2.
  (#69; reported by Ahn Ki Yung)
• Backchain now correctly takes into account inductive restrictions
  (#70; reported by Ahn Ki Yung)
• Search now correctly raises eigenvariables over support
  (#71; reported by Morten Rhiger)
• Undo/ProofGeneral now handles abbrev and unabbrev correctly.
• Do not normalize object sequents except when they occur shallowly
  among the assumptions or goal. Deep normalization is unsound.
  (Reported by Dale Miller)
• The apply tactic was invalidly raising guessed instances over
  nominal constants that already occur in the body of the lemma.
  (#96; reported by Ahn Ki Yung and Alwen Tiu)

Release 2.0.4

Changes in 2.0.4 from 2.0.3

Possibly breaking changes

• The search tactic has the same error handling behavior in interactive
  and non-interactive modes, functioning like a failed tactic in both cases
  if no subgoals were closed.
• The character & can no longer appear inside the names of identifiers.

Additions

• Added support for specification-level conjunction, written using &.

• Added a new tactic form:

  search with <witness>.
  

  This tactic runs the search command with a given search witness. To see
  these witnesses, run any of the other search forms with:

    Set witnesses on.
  

  The witness string that is printed can then be used to replay the exact
  same search. There is no backtracking involved with witness strings.
  Hence, the replay will tend to be a lot faster.

  Witnesses have the following grammar:

    witness ::= true | =
              | left witness | right witness
              | split(witness,witness)
              | apply hyp
              | intros[id1, ..., idn] witness
              | exists[id1=term1, ..., idn=termn] witness
              | unfold(id,n,witness1,...,witnessn)
              | (witness)
              | *
  

  The last witness form stands for a place-holder so you can give partial
  witnesses to search. In fact, the default search tactic is identical to:

    search with *.
  

  Please use this feature sparingly, and only when building proofs. After
  you are done with the proof, delete the "with" statements. These witnesses
  will NOT be portable across different versions of Abella, as they are very
  particular to the "search" tactic implementation.

• Added a new tactic form for backchain and `assert:

  backchain <num> <hyp_or_lemma>.
  assert <num> <formula>.
  

  where the <num>, which is optional, can give a depth bound to the search
  that is automatically attempted on generated goals. Give it a depth of 0
  if you want to prevent searching. The default value is the value of the
  search_depth flag.

• Added a new command line flag -f that takes a comma-separated list of
  key=value pairs and initializes the flags based on them. For flags that
  can be set to on/off, you can just use the key and it means to set
  them to on. For example, -f subgoals=off,witnesses sets subgoals to
  off and witnesses to on.

Tweaks to existing functionality

• Import declarations automatically compile if needed. An explicit Makefile
  is very rarely needed any more.
• The exists and witness tactics now take a comma-separated list of
  existential witnesses. Each witness can also be of the form <id> = <term>
  which selects a particular existential variable to instantiate. Without
  the <id> = part it always instantiates the first variables.
• The induction tactic can now traverse an arbitrary sequence of forall,
  nabla, and -> connectives when finding the induction argument.
• The search tactic now does a small amount of asynchronous reasoning
  for newly created hypotheses (e.g., reducing pattern equations).

Experimental changes (may be changed or removed in the future)

• Added support for (first-order) polymorphic definitions. Definitions
  such as the following are now accepted.

    Define fresh : A -> B -> prop by
      nabla x, fresh x M.
  

  In every use of the definition, the type arguments are implicitly
  instantiated. The type-checking for such definitions is identical to
  taking all the unbound variable names and quantifying them on the outside.
  In other words, for the above definition, the behavior of type-checking is
  the same as if there were:

    Kind A,B  type
    Define fresh : A -> B -> prop by
      nabla x, fresh x M.
  

  Once such a definition is type-checked, the defined symbols are added to
  the signature as new polymorphic constants, in a vein similar to the pi
  constant. Whenever it is used, the type arguments are implicitly
  instantiated based on the types of the arguments.

• Added support for (first-order) polymorphic theorems. A theorem such as
  the following is now accepted.

    Theorem prune_arg[A] : forall E L, nabla (x:A), member (E x) L ->
       exists F, E = x\ F.
  

  The A here is a type parameter, which must be distinct from the other
  basic types in scope. To use such a theorem, you must supply enough
  arguments. An example:

    Theorem bar : forall E G, nabla (x:tm) (y:ty),
       member (E x y) G -> exists F, E = x\ y\ F.
    intros.
    apply prune_arg[tm] to H1.
    apply prune_arg[ty] to H1.
    search.
  

• Added limited support for predicate instantiation during import. The form

  Import "thmfile" with id1 := defid1, ..., idn := defidn.
  

  performs an import as usual, but any undefined predicates id in "thmfile"
  are instantiated with defined predicates defid. An undefined predicate is
  declared as usual with:

    Type id  T1 -> T2 -> ... -> Tn -> prop.
  

  It remains illegal to import a thm with undefined predicates without
  giving the predicate instantiations.

• Added a new "extrusive" tactic form clear -> that can be used to do the
  opposite of the intros tactic, i.e., intros H1 ... Hn is opposite to
  clear -> Hn ... H1. Variables can also be extruded in this form and they
  universally close the goal with respect to the variable if the variable is
  not free in any hypothesis.

• Extended the subgoals flag to take a subgoal specification string
  argument that can be used to fine tune the subgoals to display. As an
  example, the invocation:

    Set subgoals "0[0];1[2];2[3];3;4[10]".
  

  instructs Abella to show 0 additinoal subgoals at depth 0, max 2
  additional subgoals at 1, max 3 additional subgoals at depth 2, all
  subgoals at depth 3, and max 10 subgoals at depth 4. The depths need not
  be given in order, and any omitted depths display the default number of
  subgoals. The default flags on, off, and an unquoted number have the
  following meanings:

  • on : the same as "0[∞];1[∞];…"
  • off : the same as "0[0];1[0];…"
  • n : the same as "0[0];̣…;n-1[0];n[∞];n+1[0];…"

Bugfixes

• Annotation mode (-a) output is no longer printed in other modes
• Import statements can now be undone as well from ProofGeneral
• Importing .thcs made with a different Abella binary will now print an
  error message instead of causing a segmentation fault (#39)
• Importing from different directories now works correctly
• Multiple occurrences of a single variable in a binding list is now
  correctly rejected. (#56)
• Better error messages. (#64)

New examples

• Bisimulations relating the π-calculus and the λ-calculus
  (contributed by Horace Blanc and Beniamino Accattoli)
• Type-preservation of Curry-style System F
  (contributed by Ahn Ki Yung)

Release 2.0.3

Potentially breaking changes

• Removed ~ and != notations (introduced in 2.0.2, and unused by anyone as
  far as I know). A general notation support may be considered for Abella
  in the future. Meanwhile, we prefer simplicity and predictability.

Additions

• The unfold tactic has an optional argument, "(all)", that produces a
  disjunction of all solutions to the matching problem of the conclusion of
  a subgoal and its relevant (co)definition. The disjuncts are produced in
  the same order as the clauses, but if a single clause has multiple ways to
  match the head then the disjuncts for that clause are in some unspecified
  order (that depends on the details of the unification algorithm).

• The following tactic forms have been added:

  apply *H to ...
  apply ... to ... *H ...
  backchain *H
  cut *H ...
  cut ... with *H
  inst *H with ...
  monotone *H with ...

  In each case, if H names a hypothesis, then the tactic consumes the
  hypothesis (like the clear tactic). Note that if hypothesis hints are
  given, then these hints are used after consuming the hypotheses. Thus,
  if one writes:

  foo : apply lem to *foo bar baz.
  

  then the hypothesis named foo is effectively replaced with a new
  hypothesis named foo that is the result of applying the lem to the old foo
  and the other arguments.

• Optional semi-colon allowed before the first clause in a definition or
  co-definition block.

• Variable renaming can overwrite old variables that have already been
  instantiated.

• The clear tactic can also remove instantiated variables.

• The settable option "types" displays the types of variables in subgoals

Internal changes

• The parser has stronger checks to enforce the lexical convention that all
  identifiers matching n[0-9]+ are nominal constants.
• Most user-visible error messages have been made a bit more precise and
  informative.
• The undo commands have been completely reworked.

Bugfixes

• Abella now builds on versions of OCaml between 3.12.1 and 4.01.0
  (inclusive) again.
• Unfolding named clauses now raises clauses over the support of the goal
  and existentially closes over residual logic variables (soundness bug
  introduced in 2.0.2) (#33)
• Unfolding named clauses whose heads do not unify with goal now causes
  failure instead of success. (soundness bug introduced in 2.0.2)
• Web-page generating scripts properly handle proof syntax changes since
  version 1.3.5.
• The toplevel now prints tactics using the same syntax as in proof scripts.
• The apply tactic can now apply lemmas that do not have a forall prefix.
• In the Query command, fresh logic variables are allocated to be
  independent of existing capitalized identifiers in the query. This
  prevents the generated solutions from appearing to be non-idempotent.
• ProofGeneral 4.3pre should now work with Abella. (#6)

New examples

• The process calculus examples have been re-organized. There are now two
  medium sized new developments of the meta-theory of bisimulation-up-to
  techniques for CCS and the pi-calculus.

Quality of Life Improvements (2.0.2)

Potentially breaking changes.

• Constants with names matching n[0-9]+ are forcibly treated as
  nominal constants. This fixes an unsoundness due to ambiguous
  parsing of such constants in proofs.
• The tactic exists now has a synonym: witness. This adds
  witness to the list of keywords.

Additions

• Specification language now supports <= in addition to =>
• Binders are printed using variable naming hints from the
  source instead of in a normalized form (x1, x2, etc.)
• Can unfold the nth clause of an inductive or co-inductive
  definition block using unfold n.
• Can name clauses in the specification (in .mod files) using a
  comment of the form %:nm: right before a clause. There must be a
  single Abella identifier and no spaces between the two :s.
• Can unfold a specific clause named nm of a specification using
  unfold nm.
• New flag "instantiations" shows variable instantiations at the top
  of a subgoal.
• New notation ~ F for F -> false.
• The backchain tactic now allows backchaining formulas that are
  not prenex-quantified implications. The "head" of the backchained
  formula is interpreted as any formula that is not an implication.
• The rename tactic has been extended to also allow renaming
  variables, with an identical syntax.

Internal changes

• Terms and meta-terms now have pretty-printer with a plugin
  architecture for future extensions.

Bug fixes

• The exists/witness tactics now rename to avoid capture (#22)
• Raising over nominal constants in spec. sequents raises over the
  support of the whole sequent rather than just its conclusion.
• Normalizing of binders now avoid capture (#23)
• Instantiated variables are no longer printed in the variables list
  of a sequent.
• Higher-order definitions have a stricter stratification check that
  complains both about actual and potential unsound definitions.
• The subordination checker now does not complain about invalid
  subterms for types that have not been explicitly Closed.
• The rename tactic cannot rename lemmas (i.e., theorems proved
  earlier)

New examples

• Formalization of the meta-theory of higher-order HH using only the
  reasoning logic of Abella (examples/logic/hh_meta.thm).

Minor bugfix release for 2.0.0

This version fixes the following issues

• Restored a number of missing commits that were lost during the hh_omega branch merge (specifically, commits ca3a05c 316db8a 5e0a40f ef9ddf4).
• URLs in the examples and documentation updated to abella-prover.org
• Fixed code to generate src/version.ml