2.6.0

CHANGES:

Added

• Add tactic set.
• Decimal notation for integers.

Fixed

• Why3 tactic.
• Induction tactic.

Changed

• Improved Core.Term.eq_modulo (Claudio Sacerdoti) -> speed up factor between 2 and 9
• The export option --requiring does not require as argument a file with extension .v anymore: the argument must be a module name.
• Option '--erasing' renamed into '--mapping'.
• Builtins necessary for the decimal notation.

2.5.1

CHANGES:

Added

• Add export format raw_dk.
• Fix of the color of the text in command line when console.out is used.
• Use black text instead of red when diplaying query answers.
• Allow negative numbers in notation priorities.
• New release 0.2.2 of the VSCode plugin.

2.5.0

CHANGES:

Added

• Add the opaque command to turn a defined symbol into a constant
• Add the tactic try that tries to apply a tactic to the focused goal.
  If the application of the tactic fails, it catches the error and leaves the goal unchanged.

Fixed

• Coq export: do not rename module names
• Sequential symbols: fix order of rules

2.4.1

CHANGES:

Added

• support for Pratter 3.0.0
• printing of unification and coercion rules

Improved

• unification

Fixed

• Coq export
• matita.sh script

2.4.0

CHANGES:

Added

• Several options for export -o stt_coq.
• Tactic remove.
• Option --no-sr-check to disable subject reduction checking.
• CLI command index to build ~/.LPSearch.db.
• Indexed terms can be normalized wrt rules with the option --rules
  (note that this new option --rules could be used to implement the equivalent
  of dkmeta later).
• CLI command search and LP command search to send queries to the index.
• Query language.
• CLI command websearch to run a webserver that can answer search queries.
• Option --port to specify the port to use.

Improved

• Output for export -o stt_coq.

Changed

• Private definitions are not kept in memory and in lpo files anymore.
• The record type Eval.config is extended with a new field allowing to specify
  which dtree to use for each symbol.

2.3.1

CHANGES:

Fixed

• Opaque definitions are not kept in memory and in lpo files anymore
• A few bug fixes.

Changed

• Why3 dependency updated to 1.6.

2.3.0

CHANGES:

Added

• Export to Coq.
• (API) the rewrite engine can match on the constant TYPE.
• Automatic coercion insertion mechanism.
  For example, the command coerce_rule coerce Int Float $x ↪ FloatOfInt $x;
  can be used to instruct Lambdapi to automatically coerce integers to floats
  using the function FloatOfInt.

Fixed

• Generation of metavariables through the rewriting engine.
• Application of pattern variables in rewrite rules RHS in the Dedukti
  export.
• Dedukti export: invalid Dedukti module name were not brace-quoted,
  for instance, #REQUIRE module-name. could be exported, while module-name
  is not recognised by Dedukti2. It is now exported as #REQUIRE {|module-name|},
  and symbols are exported as {|module-name|}.foo.
• HRS and XTC exports.

Changed

• Do not propose installation of Emacs mode via opam anymore as it can easily be installed from Emacs.

2.2.1

CHANGES:

Added

• Propagate recompile flag to dependencies.
• Postfix operators with the notation <op> postfix <priority>;

Removed

• Logic directory since it is now available on the Lambdapi Opam repository.
• Option --recompile.

Changed

• Use short options in system commands to be POSIX compliant.

2.2.0

CHANGES:

Added

• Incremental local confluence checking for non higher-order and non AC rules.
• Add options -o hrs and -o xtc to the export command.

Changed

• whnf function takes a problem as argument and a list of tags that configure
  the rewriting. Tags may block beta reduction, block definition expansion or
  block rewriting.
• Do not print empty term environments .[].
• Allow users to use the pattern variables $0, $1, etc. and internally name pattern variables by their index.
• Fixed debug flag printing in Pretty.
• Compatibility with Cmdliner 1.1.0 and Bindlib 6.0.0.

Removed

• tree_walk is no longer in the API

2.1.0

CHANGES:

Added

• In Logic/, a library of logics.

• The command export to translate signatures to the lp or dk files formats.

• New release of the VSCode extension.

• A small tutorial in tests/OK/tutorial.lp.

• The why3 tactic handles universal and existential quantifiers through
  two new builtins ("ex" and "all"). Codewise, it requires a new
  translation from encoded types to Why3 types.

• Tems may be placeholders. Placeholders are holes in the
  concrete syntax. They are refined into metavariables. Placeholders
  cannot appear nonlinearly in terms. From A Bidirectional Refinement
  Algorithm..., p. 31,

  Non linear placeholders are not allowed since two occurrences could be
  in contexts that bind different set of variables and instantiation with
  terms that live in one context would make no sense in the other one.

Changed

• Moved the files tool/hrs.ml and tool/xtc.ml into the new export/ directory.

• Because placeholders are simple holes, the term _ → _ is scoped
  into a full dependent product Π x: M, N where N is a metavariable
  that depend on x (see file tests/OK/767.lp)

• Type checking is slower following #696 because of refinement (not only
  the type but also the term must be destructured and rebuilt),

  	master	refiner
  holide	7:0	11:33
  iprover	5:58	6:50

Removed

• The command beautify superseded by the new command export.

• Unused variable warning: whether a variable is used or not cannot be
  decided while scoping (following #696) since placeholders that do not
  depend on variables may be refined later into metavariables that may
  depend on them.

• Metavariables cannot be referenced by their name anymore, hence the
  syntax ?M.[x;y] is obsolete, but ?0.[x;y] isn't.