Unreleased changes ================== OCaml and dependencies - Coq 8.10 requires OCaml >= 4.05.0, bumped from 4.02.3 See the INSTALL file for more information on dependencies. - Coq 8.10 doesn't need Camlp5 to build anymore. It now includes a fork of the core parsing library that Coq uses, which is a small subset of the whole Camlp5 distribution. In particular, this subset doesn't depend on the OCaml AST, allowing easier compilation and testing on experimental OCaml versions. The Coq developers would like to thank Daniel de Rauglaudre for many years of continued support. Coqide - CoqIDE now depends on gtk+3 and lablgtk3, rather than gtk+2 and lablgtk2. - CoqIDE now properly sets the module name for a given file based on its path, see -topfile change entry for more details. Coqtop - the use of `coqtop` as a compiler has been deprecated, in favor of `coqc`. Consequently option `-compile` will stop to be accepted in the next release. `coqtop` is now reserved to interactive use. (@ejgallego #9095) - new option -topfile filename, which will set the current module name (à la -top) based on the filename passed, taking into account the proper -R/-Q options. For example, given -R Foo foolib using -topfile foolib/bar.v will set the module name to Foo.Bar. Specification language, type inference - Fixing a missing check in interpreting instances of existential variables that are bound to local definitions might exceptionally induce an overhead if the cost of checking the conversion of the corresponding definitions is additionally high (PR #8215). - A few improvements in inference of the return clause of `match` can exceptionally introduce incompatibilities (PR #262). This can be solved by writing an explicit `return` clause, sometimes even simply an explicit `return _` clause. - Using non-projection values with the projection syntax is not allowed. For instance "0.(S)" is not a valid way to write "S 0". Projections from non-primitive (emulated) records are allowed with warning "nonprimitive-projection-syntax". Kernel - Added primitive integers - Unfolding heuristic in termination checking made more complete. In particular Coq is now more aggressive in unfolding constants when it looks for a iota redex. Performance regression may occur in Fixpoint declarations without an explicit {struct} annotation, since guessing the decreasing argument can now be more expensive. (PR #9602) Notations - New command `Declare Scope` to explicitly declare a scope name before any use of it. Implicit declaration of a scope at the time of `Bind Scope`, `Delimit Scope`, `Undelimit Scope`, or `Notation` is deprecated. - New command `String Notation` to register string syntax for custom inductive types. - Numeral notations now parse decimal constants such as 1.02e+01 or 10.2. Parsers added for Q and R. This should be considered as an experimental feature currently. Note: in -- the rare -- case when such numeral notations were used in a development along with Q or R, they may have to be removed or deconflicted through explicit scope annotations (1.23%Q, 45.6%R,...). - Various bugs have been fixed (e.g. PR #9214 on removing spurious parentheses on abbreviations shortening a strict prefix of an application). - Numeral Notations now support inductive types in the input to printing functions (e.g., numeral notations can be defined for terms containing things like `@cons nat O O`), and parsing functions now fully normalize terms including parameters of constructors (so that, e.g., a numeral notation whose parsing function outputs a proof of `Nat.gcd x y = 1` will no longer fail to parse due to containing the constant `Nat.gcd` in the parameter-argument of `eq_refl`). See #9840 for more details. - Deprecated compatibility notations have actually been removed. Uses of these notations are generally easy to fix thanks to the hint contained in the deprecation warnings. For projects that require more than a handful of such fixes, there is [a script](https://gist.github.com/JasonGross/9770653967de3679d131c59d42de6d17#file-replace-notations-py) that will do it automatically, using the output of coqc. The script contains documentation on its usage in a comment at the top. Plugins - The quote plugin (https://coq.inria.fr/distrib/V8.8.1/refman/proof-engine/detailed-tactic-examples.html#quote) was removed. If some users are interested in maintaining this plugin externally, the Coq development team can provide assistance for extracting the plugin and setting up a new repository. Tactics - Removed the deprecated `romega` tactics. - Tactic names are no longer allowed to clash, even if they are not defined in the same section. For example, the following is no longer accepted: `Ltac foo := idtac. Section S. Ltac foo := fail. End S.` - The tactics 'lia','nia','lra','nra' are now using a novel Simplex-based proof engine. In case of regression, 'Unset Simplex' to get the venerable Fourier-based engine. - Names of existential variables occurring in Ltac functions (e.g. `?[n]` or `?n` in terms - not in patterns) are now interpreted the same way as other variable names occurring in Ltac functions. - Hint declaration and removal should now specify a database (e.g. `Hint Resolve foo : database`). When the database name is omitted, the hint is added to the core database (as previously), but a deprecation warning is emitted. - There are now tactics in `PreOmega.v` called `Z.div_mod_to_equations`, `Z.quot_rem_to_equations`, and `Z.to_euclidean_division_equations` (which combines the `div_mod` and `quot_rem` variants) which allow `lia`, `nia`, `romega`, etc to support `Z.div` and `Z.modulo` (`Z.quot` and `Z.rem`, respectively), by posing the specifying equation for `Z.div` and `Z.modulo` before replacing them with atoms. - Ltac backtraces can be turned on using the "Ltac Backtrace" option. - The syntax of the `autoapply` tactic was fixed to conform with preexisting documentation: it now takes a `with` clause instead of a `using` clause. Vernacular commands - `Combined Scheme` can now work when inductive schemes are generated in sort `Type`. It used to be limited to sort `Prop`. - Binders for an `Instance` now act more like binders for a `Theorem`. Names may not be repeated, and may not overlap with section variable names. - Removed the deprecated `Implicit Tactic` family of commands. - The `Automatic Introduction` option has been removed and is now the default. - `Arguments` now accepts names for arguments provided with `extra_scopes`. - The naming scheme for anonymous binders in a `Theorem` has changed to avoid conflicts with explicitly named binders. - Computation of implicit arguments now properly handles local definitions in the binders for an `Instance`, and can be mixed with implicit binders `{x : T}`. - `Declare Instance` now requires an instance name. - Option `Refine Instance Mode` has been turned off by default, meaning that `Instance` no longer opens a proof when a body is provided. - `Instance`, when no body is provided, now always opens a proof. This is a breaking change, as instance of `Instance foo : C.` where `C` is a trivial class will have to be changed into `Instance foo : C := {}.` or `Instance foo : C. Proof. Qed.`. - Option `Program Mode` now means that the `Program` attribute is enabled for all commands that support it. In particular, it does not have any effect on tactics anymore. May cause some incompatibilities. - The algorithm computing implicit arguments now behaves uniformly for primitive projection and application nodes (bug #9508). - `Hypotheses` and `Variables` can now take implicit binders inside sections. - Removed deprecated option `Automatic Coercions Import`. - The `Show Script` command has been deprecated. - Option `Refine Instance Mode` has been deprecated and will be removed in the next version. - `Coercion` does not warn ambiguous paths which are obviously convertible with existing ones. - A new flag `Fast Name Printing` has been introduced. It changes the algorithm used for allocating bound variable names for a faster but less clever one. Tools - The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values: - `no` disables native_compute - `yes` enables native_compute and precompiles `.v` files to native code - `ondemand` enables native_compute but compiles code only when `native_compute` is called The default value is `ondemand`. Note that this flag now has priority over the configure flag of the same name. - A new `-bytecode-compiler` flag for `coqc` and `coqtop` controls whether conversion can use the VM. The default value is `yes`. - CoqIDE now supports input for Unicode characters. For example, typing "\alpha" then the "Shift+Space" will insert the greek letter alpha. In fact, typing the prefix string "\a" is sufficient. A larger number of default bindings are provided, following the latex naming convention. Bindings can be customized, either globally, or on a per-project basis, with the requirement is that keys must begin with a backslash and contain no space character. Bindings may be assigned custom priorities, so that prefixes resolve to the most convenient bindings. The documentation pages for CoqIDE provides further details. - The pretty timing diff scripts (flag `TIMING=1` to a `coq_makefile`-made `Makefile`, also `tools/make-both-single-timing-files.py`, `tools/make-both-time-files.py`, and `tools/make-one-time-file.py`) now correctly support non-UTF-8 characters in the output of `coqc`/`make` as well as printing to stdout, on both python2 and python3. Standard Library - Added lemmas about monotonicity of `N.double` and `N.succ_double`, and about the upper bound of number represented by a vector. Allowed implicit vector length argument in `Ndigits.Bv2N`. - Added `Bvector.BVeq` that decides whether two `Bvector`s are equal. - Added notations for `BVxor`, `BVand`, `BVor`, `BVeq` and `BVneg`. - Added `ByteVector` type that can convert to and from [string]. - The prelude used to be automatically Exported and is now only Imported. This should be relevant only when importing files which don't use -noinit into files which do. - Added `Coq.Structures.OrderedTypeEx.String_as_OT` to make strings an ordered type (using lexical order). - The `Coq.Numbers.Cyclic.Int31` library is deprecated. - Added lemmas about `Z.testbit`, `Z.ones`, and `Z.modulo`. - Moved the `auto` hints of the `FSet` library into a new `fset` database. Universes - Added `Print Universes Subgraph` variant of `Print Universes`. Try for instance `Print Universes Subgraph(sigT2.u1 sigT_of_sigT2.u1 projT3_eq.u1 eq_sigT2_rect.u1).` - Added private universes for opaque polymorphic constants, see doc for the "Private Polymorphic Universes" option (and Unset it to get the previous behaviour). SProp - Added a universe "SProp" for definitionally proof irrelevant propositions. Use with -allow-sprop. See manual for details. Inductives - An option and attributes to control the automatic decision to declare an inductive type as template polymorphic were added. Warning "auto-template" will trigger when an inductive is automatically declared template polymorphic without the attribute. Funind - Inductive types declared by Funind will never be template polymorphic. Misc - Option "Typeclasses Axioms Are Instances" is deprecated. Use Declare Instance for axioms which should be instances. - Removed option "Printing Primitive Projection Compatibility" SSReflect - New intro patterns: - temporary introduction: `=> +` - block introduction: `=> [^ prefix ] [^~ suffix ]` - fast introduction: `=> >` - tactics as views: `=> /ltac:mytac` - replace hypothesis: `=> {}H` See the reference manual for the actual documentation. - Clear discipline made consistent across the entire proof language. Whenever a clear switch `{x..}` comes immediately before an existing proof context entry (used as a view, as a rewrite rule or as name for a new context entry) then such entry is cleared too. E.g. The following sentences are elaborated as follows (when H is an existing proof context entry): - `=> {x..} H` -> `=> {x..H} H` - `=> {x..} /H` -> `=> /v {x..H}` - `rewrite {x..} H` -> `rewrite E {x..H}` Diffs - Some error messages that show problems with a pair of non-matching values will now highlight the differences.