Tags give the ability to mark specific points in history as being important
-
2.3.1
60243e46 · ·Release 2.3.1 CHANGES: - Opaque definitions are not kept in memory and in lpo files anymore - A few bug fixes. - Why3 dependency updated to 1.6.
-
2.3.0
4939b93c · ·Release 2.3.0 CHANGES: - 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`. - 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. - Do not propose installation of Emacs mode via opam anymore as it can easily be installed from Emacs. -
2.2.1
33348d83 · ·Release 2.2.1 CHANGES: - Propagate recompile flag to dependencies. - Postfix operators with the `notation <op> postfix <priority>;` - Logic directory since it is now available on the [Lambdapi Opam repository](https://github.com/Deducteam/opam-lambdapi-repository). - Option --recompile. - Use short options in system commands to be POSIX compliant.
-
2.2.0
0476fbec · ·Release 2.2.0 CHANGES: - Incremental local confluence checking for non higher-order and non AC rules. - Add options -o hrs and -o xtc to the export command. - `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. - `tree_walk` is no longer in the API
-
2.1.0
215a0e24 · ·Release 2.1.0 CHANGES: - 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...](https://arxiv.org/abs/1202.4905), 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. - 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 | - 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. -
2.0.0
96b01a11 · ·Release 2.0.0 CHANGES: - Add `editors/vscode/CHANGES.md` and `editors/vscode/CONTRIBUTING.md`. - Update documentation and README.md files. A tactic replacing the current goal by n new goals must be followed by n proof scripts enclosed in curly brackets. For instance, instead of writing `induction; /* case 0 */ t1; ..; tm; /* case s */ q1; ..; qn`, we must now write `induction {t1; ..; tm} {q1; ..; qn}`. Exception for tactics not really changing the current goal like "have": `/* proof of u */ have h: t; /* proof of t */ t1; ..; tm; /* proof of u continued */ q1; ..; qn` must now be written `have h: t {t1; ..; tm}; q1; ..; qn`. Other modifications in the grammar: - Curly brackets are reserved for proof script structuration. - Implicit arguments must be declared using square brackets instead of curly brackets: we must write `[a:Set]` instead of `{a:Set}`. - Term environments and rewrite patterns must be preceded by a dot: we must now write `$f.[x]` instead of `$f[x]`. - The `focus` command is removed since it breaks structuration. - allow nested comments (fix #710) - replace everywhere `%S` by `\"%s\"` - move checking compatibility with Bindlib of identifiers from lexer to scope - move `is_keyword` from `lexer` to `pretty` - move `package.ml` from `common/` to `parsing/` - change `Config.map_dir` field type to `(Path.t * string) list`, `Library.add_mapping` type to `Path.t * string -> unit` and Compile.compile argument `lm` type to `Path.t * string` - fix `_LLet` by calling mk_LLet - substitute arguments in TEnv's at construction time (mk_TEnv) - improve eq_modulo to avoid calling whnf when possible - use `Eval.pure_eq_modulo` in Infer and Unif (fix #693) - add Base.out = Format.fprintf - uniformize printing code using Base.out - rename oc arguments into ppf - complete Term.pp_term - improve some functions in Debug.D - improve logging messages in Infer by adding a level argument - mk_LLet removes useless let's - rename Eval.config into strat - factorize whnf_beta and whnf - fix handling of variable unfoldings in whnf_stk - optimize context lookup by using a map - gather problem, context, map and rewrite into a record data type - abstract whnf in hnf, snf and eq_modulo - fix typing of let's - improve printing - Error messages are shown in logs buffer - Improvements in behaviour of Emacs interface - New shortcuts `C-c C-k` and `C-c C-r` for killing and reconnecting to the LSP server - the record type problem gets a new field metas, and all its fields are now mutable - many functions now take as argument a problem - the functions infer_noexn, check_noexn and check_sort are moved to Query (they do not need to take a solver as argument anymore) - in Unif, add_constr was defined twice; this is now fixed - the modules Meta in Term and LibTerm are moved to the new file libMeta - various mli files are created - in Unif, initial is removed and instantiation is allowed to generate new constraints - Add tests on product matching - Fixed scoping of product in LHS - Wildcard created during tree compilation are the most general ones, any free variable may appear. - Updated documentation of decision trees The types `Term.rw_patt` and `Syntax.p_rw_patt_aux` are merged into a single polymorphic type `Syntax.rw_patt`. Several functions are exposed, - `Parsing.Scope.rule_of_pre_rule`: converts a pre rewriting rule into a rewriting rule, - `Handle.Command.handle`: now processes proof data, - `Handle.Command.get_proof_data`: is the old handle, - `Handle.Compile.compile_with`: allows to provide a command handler to compile modules - Add `term.mli` and turn the `term` type into a *private* type so that term constructors are not exported anymore (they are available for pattern-matching though). For constructing terms, one now needs to use the provided construction functions `mk_Vari` for `Vari`, `mk_Appl` for `Appl`, etc. - Move some functions `LibTerm` to `Term`, in particular `get_args`, `add_args` and `cmp_term`. - Rename the field `sym_tree` into `sym_dtree`. - Redefine the type `rhs` as `(term_env, term) Bindlib.mbinder` instead of `(term_env, term) Bindlib.mbinder * int` so that the old `rhs` needs to be replaced by `rhs * int` in a few places. - fix `have` - improve the behavior of `apply` - `assume` not needed before `reflexivity` anymore - `assume` checks that identifiers are distinct - `solve`: simplify goals afterwards - `libTerm`: permute arguments of `unbind_name`, and add `add_args_map` and `unbind2_name` - `syntax`: add `check_notin` and `check_distinct` - split `misc/listings.tex` into `misc/lambdapi.tex` and `misc/example.tex` - `./tools/` -> `./misc` - `./src/core/tree_types.ml` -> `./src/core/tree_type.ml` - escaped regular identifiers are automatically unescaped in lexing - unescaping is done in filenames only - `Escape.add_prefix` and `Escape.add_suffix` allow to correctly extend potentially escaped identifiers - move `scope.ml` from `Core` to `Parsing` * `scope.ml`: - the inner functions of scope are brought to the top-level - `scope_term_with_params` is introduced: it is similar to `scope_term` but does not check that top-level bound variables are used - `_Meta_Type` is moved to `env.ml` as `fresh_meta_type` * `command.ml`: - use `scope_term_with_params` and check that parameters are indeed used - `get_implicitness` moved to `syntax.ml` as `get_impl_term` - fix implicit arguments computation in case of no type by introducing `Syntax.get_impl_params_list` * in various places: use `pp_var` instead of `Bindlib.name_of` * replace expo argument in scoping and handling by boolean telling if private symbols are allowed * allow private symbols in queries - Content of `lambdapi.opam` is moved to `dune-project` and the former is generated using `dune build @install`. - Vim files are installed in `opam` prefix using dune. - The emacs mode is declared as a sub-package. and slightly improve `Ctxt.def_of` - fix type inference in the case of an application (t u) where the type of t is not a product yet (uncomment code commented in #596) - fix the order in which emacs prints hypotheses - fix opam dependencies: add constraint why3 <= 1.3.3 - fix and improve in `inverse.ml` the computation of the inverse image of a term wrt an injective function (no unification rule is needed anymore in common examples, fix #342) - fix management of "initial" constraints in unification (initial is now a global variable updated whenever a new constraint is added) - when applying a unification rule, add constraints on types too (fix #466) - turn `Infer.make_prod` into `Infer.set_to_prod` - add pp_constrs for printing lists of constraints - make time printing optional - improve visualization of debugging data using colors: . blue: top-level type inference/checking . magenta: new constraint . green: constraint to solve . yellow: data from signature or context . red: instantiations (and handled commands) - rename command `admit` into `admitted` - `admitted`: admit the initial goal instead of the remaining goals (when the proof is an opaque definition) - move code on `admit` from `command.ml` to `tactic.ml` - add tactic `admit` (fix #380) As a consequence, tactics can change the signature state now. - improve type inference and unification - add flag `"print_meta_args"` - print metavariables unescaped, add parentheses in domains - replace `(current_sign()).sign_path` by `current_path()` - improve logging: . debug +h now prints data on type inference/checking . provide time of type inference/checking and constraint solving . give more feedback when instantiation fails - allow matching on abstraction/product type annotations (fix #573) - Infer: do not check constraint duplication and return constraints in the order they have been added (fix #579) - inductive type symbols are now declared as constant (fix #580) - fix parsing and printing of unification rules - Extra.files returns only the files that satisfy some user-defined condition - tests/ok_ko.ml: test only .dk and .lp files - Pretty: checking that identifiers are LP keywords is now optional (useful for debug) - `set infix ... "<string>" := <qid>` is replaced by `set notation <qid> infix ...` - `set prefix ... "<string>" := <qid>` is replaced by `set notation <qid> prefix ...` - `set quantifier <qid>` is replaced by `set notation <qid> quantifier` - the flag `print_meta_type` is renamed into `print_meta_types` - `LibTerm.expl_args` is renamed into `remove_impl_args` - Ghost paths and unification rule symbols managed in LpLexer now (no hard-coded strings anymore except for their definition) - Allow users to type system-generated metavariable identifiers (integers) - Fix printing of metavariable identifiers - `key_counter` renamed into `meta_counter` - `Meta.name` does not return a `?`-prefixed string anymore - code factorization and reorganization in `query.ml` - Electric mode for Emacs - Buttons for Proof Navigation in Emacs - Navigate by commands/tactics in Emacs and VScode - Evaluated region shrinks on edit in Emacs and VScode - Evaluated region changes colour after error in Emacs and VScode - LSP server sends logs only from last command/tactic - Few minor corrections in LSP server - Improve VSCode indentation - `env.ml`: add functions for generating fresh metavariable terms (factorizes some code in `scope.ml` and `tactics.ml`) - add fields in type `Sign.inductive` renamed into `ind_data` - functions from `rewrite.ml` now take a `goal_typ` as argument - code factorization in `tactic.ml` - remove type aliases `p_type` and `p_patt` - rename `P_Impl` into `P_Arro`, and `P_tac_intro` into `P_tac_assume` - variable renamings in `sig_state` - File renamings and splittings: * `lpLexer` -> `escape`, `lpLexer` * `console` -> `base`, `extra`, `debug`, `error`, `console` * `module` -> `filename`, `path`, `library` * `cliconf` -> `config` * `install_cmd` -> `install` * `init_cmd` -> `init` - Improve handling of escaped identifiers in `escape.ml` and fix printing - Improve `tests/ok_ko.ml` to allow sub-directories in `tests/OK/` or `tests/KO/` - File renamings: * `terms` -> `term` * `basics` -> `libTerm` * `tactics` -> `tactic` * `queries` -> `query` * `stubs` -> `realpath` * `files` -> `module` * `handle` -> `command` - `Core` library divided into the following sub-libraries: * `Common` that contains shared basic files (`pos`, `console`, `module` and `package`) * `Parsing` that contains everything related to parsing (`syntax`, `pretty`, lexers and parser) * `Handle` that uses `Core` to type check commands and modules (contains `query`, `tactic`, `command`, `compile`, `inductive`, `rewrite`, `proof` and `why3_tactic`) * `Tool` that provides miscellaneous tools that use `Core` (`external`, `hrs`, `xtc`, `tree_graphviz`, `sr`) Replace Earley by Menhir, Pratter and Sedlex Syntax modifications: - Add multi-lines comments `/*` ... `*/`. - Commands and tactics must now be ended by a semi-colon `;`. - The syntax `λx y z: nat, ...` with multiple variables is not authorised anymore, but `λ(x y z: nat), ...` is, as well as `λ x : N, t` with a single variable. - In unification rules, the right hand-side must now be enclosed between square brackets, so ``` set unif_rule $x + $y ≡ 0 ↪ $x ≡ 0; $y ≡ 0 ``` becomes ``` set unif_rule $x + $y ≡ 0 ↪ [ $x ≡ 0; $y ≡ 0 ]; ``` - `set declared` has been removed. - Any (depending on accepted codepoints) UTF8 identifier is by default valid. *Warning:* string `λx` is now a valid identifier. Hence, expression `λx, t` isn't valid, but `λ x, t` is. - Declared quantifiers now need a backquote to be applied. The syntax `` `f x, t`` represents `f (λ x, t)` (and a fortiori `f {T} (λ x, t)`). - `assert` always takes a turnstile (or vdash) to specify a (even empty) context, so the syntax is `assert ⊢ t: A;` - The minus sign `-` in the rewrite tactic has been replaced by the keyword `left`. Code modifications: - Parsing and handling are interleaved (except in the LSP server): the parser returns a stream of parsed commands. Requesting an item of the stream parses one command in the file. - The type `pp_hint` is renamed to `notation` and moved to `sign.ml`. - Notations (that is, ex-`pp_hint`) are kept in a `SymMap`, which allowed to simplify some code in `sig_state.ml` and `sign.ml`. - Positions are not lazy anymore, because Sedlex doesn't use lazy positions. - `p_terms` do not have `P_BinO` and `P_UnaO` constructors anymore. changes in the syntax: - definition -> symbol - theorem -> opaque symbol - proof -> begin - qed -> end - Added `sequential` keyword for symbol declarations - Removed `--keep-rule-order` option - `$F` is shorthand for `$F[]` - Empty environment mandatory under binders Allow users to match on product `Πx: t, u` and on the domain of binders. - Allow users to declare a symbol [f] as quantifier. Then, [f x,t] stands for [f(λx,t)]. Introduction of unification rules, taken from <http://www.cs.unibo.it/~asperti/PAPERS/tphol09.pdf>. A unification rule can be set with ``` set unif_rule t ≡ u ↪ v ≡ w, x ≡ y ``` - Pretty-printing hints managed in signature state now. - `→` is replaced by `↪` in rewriting rules, - `&` is replaced by `$` for pattern variables in rewriting rules, - the syntax `rule ... and ...` becomes `rule ... with ...`, - `⇒` is replaced by `→` for implication, and - `∀` is replaced by `Π` for the dependent product type Adding let-bindings to the terms structure. - Contexts can now contain term definitions. - Unification is carried out with a context. - Reduction functions (`whnf`, `hnf`, `snf` &c.) are called with a context. - Type annotation for `let` in the concrete syntax. - Use `Stdlib` instead of `Pervasives` (enforced by sanity checks). - Rely on `stdlib-shims` to provide `Stdlib` on older version of OCaml. - New module system. - Revised command line arguments parsing and introduce subcommands. - LSP server is now a Lambdapi subcommand: run with `lambdapi lsp`. - New `--no-warning` option (fixes #296). Simplification of the decision tree structure - trees do not depend on term variables; - tree constructor type depends on generated at compile-time branch-wise unique integral identifiers; - graph output is more consistent: variables are the same in the nodes and the leaves. Introducing protected and private symbols. Introducing the `why3` tactic to call external provers. -
-