|
|
|
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
skolemization.pvs
Sprache: SML
Untersuchungsergebnis.rst Download desHaskell {Haskell[225] BAT[451] Ada[462]}zum Wurzelverzeichnis wechseln
--------------
Recent changes
--------------
.. ifconfig:: not coq_config.is_a_released_version
.. include:: ../unreleased.rst
Version 8.10
------------
Summary of changes
~~~~~~~~~~~~~~~~~~
|Coq| version 8.10 contains two major new features: support for a native
fixed-precision integer type and a new sort :math:`\SProp` of strict
propositions. It is also the result of refinements and stabilization of
previous features, deprecations or removals of deprecated features,
cleanups of the internals of the system and API, and many documentation improvements.
This release includes many user-visible changes, including deprecations that are
documented in the next subsection, and new features that are documented in the
reference manual. Here are the most important user-visible changes:
- Kernel:
- A notion of primitive object was added to the calculus. Its first
instance is primitive cyclic unsigned integers, axiomatized in
module :g:`UInt63`. See Section :ref:`primitive-integers`.
The `Coq.Numbers.Cyclic.Int31` library is deprecated
(`#6914 <https://github.com/coq/coq/pull/6914>`_, by Maxime Dénès,
Benjamin Grégoire and Vincent Laporte,
with help and reviews from many others).
- The :math:`\SProp` sort of definitionally proof-irrelevant propositions was
introduced. :math:`\SProp` allows to mark proof
terms as irrelevant for conversion, and is treated like :math:`\Prop`
during extraction. It is enabled using the `-allow-sprop`
command-line flag or the :flag:`Allow StrictProp` flag.
See Chapter :ref:`sprop`
(`#8817 <https://github.com/coq/coq/pull/8817>`_, by Gaëtan Gilbert).
- The unfolding heuristic in termination checking was made more
complete, allowing more constants to be unfolded to discover valid
recursive calls. Performance regression may occur in Fixpoint
declarations without an explicit ``{struct}`` annotation, since
guessing the decreasing argument can now be more expensive
(`#9602 <https://github.com/coq/coq/pull/9602>`_, by Enrico Tassi).
- Universes:
- Added :cmd:`Print Universes Subgraph` variant of :cmd:`Print Universes`.
Try for instance
:g:`Print Universes Subgraph(sigT2.u1 sigT_of_sigT2.u1 projT3_eq.u1).`
(`#8451 <https://github.com/coq/coq/pull/8451>`_, by Gaëtan Gilbert).
- Added private universes for opaque polymorphic constants, see the
documentation for the :flag:`Private Polymorphic Universes` flag,
and unset it to get the previous behaviour
(`#8850 <https://github.com/coq/coq/pull/8850>`_, by Gaëtan Gilbert).
- Notations:
- New command :cmd:`String Notation` to register string syntax for custom
inductive types
(`#8965 <https://github.com/coq/coq/pull/8965>`_, by Jason Gross).
- Experimental: :ref:`Numeral Notations <numeral-notations>` now parse decimal
constants such as ``1.02e+01`` or ``10.2``. Parsers added for :g:`Q` and :g:`R`.
In the rare case when such numeral notations were used
in a development along with :g:`Q` or :g:`R`, they may have to be removed or
disambiguated through explicit scope annotations
(`#8764 <https://github.com/coq/coq/pull/8764>`_, by Pierre Roux).
- Ltac backtraces can be turned on using the :flag:`Ltac Backtrace`
flag, which is off by default
(`#9142 <https://github.com/coq/coq/pull/9142>`_,
fixes `#7769 <https://github.com/coq/coq/issues/7769>`_
and `#7385 <https://github.com/coq/coq/issues/7385>`_,
by Pierre-Marie Pédrot).
- The tactics :tacn:`lia`, :tacn:`nia`, :tacn:`lra`, :tacn:`nra` are now using a novel
Simplex-based proof engine. In case of regression, unset :flag:`Simplex`
to get the venerable Fourier-based engine
(`#8457 <https://github.com/coq/coq/pull/8457>`_, by Fréderic Besson).
- SSReflect:
- New intro patterns:
- temporary introduction: `=> +`
- block introduction: `=> [^ prefix ] [^~ suffix ]`
- fast introduction: `=> >`
- tactics as views: `=> /ltac:mytac`
- replace hypothesis: `=> {}H`
See Section :ref:`introduction_ssr`
(`#6705 <https://github.com/coq/coq/pull/6705>`_, by Enrico Tassi,
with help from Maxime Dénès,
ideas coming from various users).
- New tactic :tacn:`under` to rewrite under binders, given an
extensionality lemma:
- interactive mode: :n:`under @term`, associated terminator: :tacn:`over`
- one-liner mode: :n:`under @term do [@tactic | ...]`
It can take occurrence switches, contextual patterns, and intro patterns:
:g:`under {2}[in RHS]eq_big => [i|i ?]`
(`#9651 <https://github.com/coq/coq/pull/9651>`_,
by Erik Martin-Dorel and Enrico Tassi).
- :cmd:`Combined Scheme` now works when inductive schemes are generated in sort
:math:`\Type`. It used to be limited to sort `Prop`
(`#7634 <https://github.com/coq/coq/pull/7634>`_, by Théo Winterhalter).
- A new registration mechanism for reference from ML code to Coq
constructs has been added
(`#186 <https://github.com/coq/coq/pull/186>`_,
by Emilio Jesús Gallego Arias, Maxime Dénès and Vincent Laporte).
- CoqIDE:
- CoqIDE now depends on gtk+3 and lablgtk3 instead of gtk+2 and lablgtk2.
The INSTALL file available in the Coq sources has been updated to list
the new dependencies
(`#9279 <https://github.com/coq/coq/pull/9279>`_,
by Hugo Herbelin, with help from Jacques Garrigue,
Emilio Jesús Gallego Arias, Michael Sogetrop and Vincent Laporte).
- Smart input for Unicode characters. For example, typing
``\alpha`` then ``Shift+Space`` will insert the greek letter alpha.
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. See Section :ref:`coqide-unicode` for details
(`#8560 <https://github.com/coq/coq/pull/8560>`_, by Arthur Charguéraud).
- Infrastructure and dependencies:
- Coq 8.10 requires OCaml >= 4.05.0, bumped from 4.02.3 See the
`INSTALL` file for more information on dependencies
(`#7522 <https://github.com/coq/coq/pull/7522>`_, by Emilio Jesús Gallego Arías).
- 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. Coq also ships a new parser
`coqpp` that plugin authors must switch to
(`#7902 <https://github.com/coq/coq/pull/7902>`_,
`#7979 <https://github.com/coq/coq/pull/7979>`_,
`#8161 <https://github.com/coq/coq/pull/8161>`_,
`#8667 <https://github.com/coq/coq/pull/8667>`_,
and `#8945 <https://github.com/coq/coq/pull/8945>`_,
by Pierre-Marie Pédrot and Emilio Jesús Gallego Arias).
The Coq developers would like to thank Daniel de Rauglaudre for many
years of continued support.
- Coq now supports building with Dune, in addition to the traditional
Makefile which is scheduled for deprecation
(`#6857 <https://github.com/coq/coq/pull/6857>`_,
by Emilio Jesús Gallego Arias, with help from Rudi Grinberg).
Experimental support for building Coq projects has been integrated
in Dune at the same time, providing an `improved experience
<https://coq.discourse.group/t/a-guide-to-building-your-coq-libraries-and-plugins-with-dune/>`_
for plugin developers. We thank the Dune team for their work
supporting Coq.
Version 8.10 also comes with a bunch of smaller-scale changes and
improvements regarding the different components of the system, including
many additions to the standard library (see the next subsection for details).
On the implementation side, the ``dev/doc/changes.md`` file documents
the numerous changes to the implementation and improvements of
interfaces. The file provides guidelines on porting a plugin to the new
version and a plugin development tutorial originally made by Yves Bertot
is now in `doc/plugin_tutorial`. The ``dev/doc/critical-bugs`` file
documents the known critical bugs of |Coq| and affected releases.
The efficiency of the whole system has seen improvements thanks to
contributions from Gaëtan Gilbert, Pierre-Marie Pédrot, and Maxime Dénès.
Maxime Dénès, Emilio Jesús Gallego Arias, Gaëtan Gilbert, Michael
Soegtrop, Théo Zimmermann worked on maintaining and improving the
continuous integration system and package building infrastructure.
Coq is now continuously tested against OCaml trunk, in addition to the
oldest supported and latest OCaml releases.
Coq's documentation for the development branch is now deployed
continuously at https://coq.github.io/doc/master/api (documentation of
the ML API), https://coq.github.io/doc/master/refman (reference
manual), and https://coq.github.io/doc/master/stdlib (documentation of
the standard library). Similar links exist for the `v8.10` branch.
The OPAM repository for |Coq| packages has been maintained by Guillaume
Melquiond, Matthieu Sozeau, Enrico Tassi (who migrated it to opam 2)
with contributions from many users. A list of packages is available at
https://coq.inria.fr/opam/www/.
The 61 contributors to this version are Tanaka Akira, Benjamin
Barenblat, Yves Bertot, Frédéric Besson, Lasse Blaauwbroek, Martin
Bodin, Joachim Breitner, Tej Chajed, Frédéric Chapoton, Arthur
Charguéraud, Cyril Cohen, Lukasz Czajka, David A. Dalrymple, Christian
Doczkal, Maxime Dénès, Andres Erbsen, Jim Fehrle, Emilio Jesus Gallego
Arias, Gaëtan Gilbert, Matěj Grabovský, Simon Gregersen, Jason Gross,
Samuel Gruetter, Hugo Herbelin, Jasper Hugunin, Mirai Ikebuchi,
Chantal Keller, Matej Košík, Sam Pablo Kuper, Vincent Laporte, Olivier
Laurent, Larry Darryl Lee Jr, Nick Lewycky, Yao Li, Yishuai Li, Assia
Mahboubi, Simon Marechal, Erik Martin-Dorel, Thierry Martinez,
Guillaume Melquiond, Kayla Ngan, Karl Palmskog, Pierre-Marie Pédrot,
Clément Pit-Claudel, Pierre Roux, Kazuhiko Sakaguchi, Ryan Scott,
Vincent Semeria, Gan Shen, Michael Soegtrop, Matthieu Sozeau, Enrico
Tassi, Laurent Théry, Kamil Trzciński, whitequark, Théo Winterhalter,
Xia Li-yao, Beta Ziliani and Théo Zimmermann.
Many power users helped to improve the design of the new features via
the issue and pull request system, the |Coq| development mailing list,
the [email protected] mailing list or the new Discourse forum. It would
be impossible to mention exhaustively the names of everybody who to some
extent influenced the development.
Version 8.10 is the fifth release of |Coq| developed on a time-based
development cycle. Its development spanned 6 months from the release of
|Coq| 8.9. Vincent Laporte is the release manager and maintainer of this
release. This release is the result of ~2500 commits and ~650 PRs merged,
closing 150+ issues.
| Santiago de Chile, April 2019,
| Matthieu Sozeau for the |Coq| development team
|
Other changes in 8.10+beta1
~~~~~~~~~~~~~~~~~~~~~~~~~~~
- Command-line tools and options:
- 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
(`#9095 <https://github.com/coq/coq/pull/9095>`_,
by Emilio Jesús Gallego Arias).
- 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``.
CoqIDE now properly sets the module name for a given file based on
its path
(`#8991 <https://github.com/coq/coq/pull/8991>`_,
closes `#8989 <https://github.com/coq/coq/issues/8989>`_,
by Gaëtan Gilbert).
- Experimental: Coq flags and options can now be set on the
command-line, e.g. ``-set "Universe Polymorphism=true"``
(`#9876 <https://github.com/coq/coq/pull/9876>`_, by Gaëtan Gilbert).
- 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`.
(`#8870 <https://github.com/coq/coq/pull/8870>`_, by Maxime Dénès)
- 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
(`#9872 <https://github.com/coq/coq/pull/9872>`_,
closes `#9767 <https://github.com/coq/coq/issues/9767>`_
and `#9705 <https://github.com/coq/coq/issues/9705>`_,
by Jason Gross)
- coq_makefile's install target now errors if any file to install is missing
(`#9906 <https://github.com/coq/coq/pull/9906>`_, by Gaëtan Gilbert).
- Preferences from ``coqide.keys`` are no longer overridden by
modifiers preferences in ``coqiderc``
(`#10014 <https://github.com/coq/coq/pull/10014>`_, by Hugo Herbelin).
- 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
(`#8217 <https://github.com/coq/coq/pull/8217>`_,
closes `#8215 <https://github.com/coq/coq/issues/8215>`_,
by Hugo Herbelin).
- A few improvements in inference of the return clause of `match` that
can exceptionally introduce incompatibilities. This can be
solved by writing an explicit `return` clause, sometimes even simply
an explicit `return _` clause
(`#262 <https://github.com/coq/coq/pull/262>`_, by Hugo Herbelin).
- Using non-projection values with the projection syntax is not
allowed. For instance :g:`0.(S)` is not a valid way to write :g:`S 0`.
Projections from non-primitive (emulated) records are allowed with
warning "nonprimitive-projection-syntax"
(`#8829 <https://github.com/coq/coq/pull/8829>`_, by Gaëtan Gilbert).
- An option and attributes to control the automatic decision to declare
an inductive type as template polymorphic were added. Warning
"auto-template" (off by default) can trigger when an inductive is
automatically declared template polymorphic without the attribute.
Inductive types declared by Funind will never be template polymorphic.
(`#8488 <https://github.com/coq/coq/pull/8488>`_, by Gaëtan Gilbert)
- Notations:
- New command :cmd:`Declare Scope` to explicitly declare a scope name
before any use of it. Implicit declaration of a scope at the time of
:cmd:`Bind Scope`, :cmd:`Delimit Scope`, :cmd:`Undelimit Scope`,
or :cmd:`Notation` is deprecated
(`#7135 <https://github.com/coq/coq/pull/7135>`_, by Hugo Herbelin).
- Various bugs have been fixed (e.g. `#9214
<https://github.com/coq/coq/pull/9214>`_ on removing spurious
parentheses on abbreviations shortening a strict prefix of an
application, by Hugo Herbelin).
- :cmd:`Numeral Notation` now support inductive types in the input to
printing functions (e.g., numeral notations can be defined for terms
containing things like :g:`@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
:g:`Nat.gcd x y = 1` will no longer fail to parse due to containing the
constant :g:`Nat.gcd` in the parameter-argument of :g:`eq_refl`)
(`#9874 <https://github.com/coq/coq/pull/9840>`_,
closes `#9840 <https://github.com/coq/coq/issues/9840>`_
and `#9844 <https://github.com/coq/coq/issues/9844>`_,
by Jason Gross).
- Deprecated compatibility notations have actually been
removed. Uses of these notations are generally easy to fix thanks
to the hint contained in the deprecation warning emitted by Coq
8.8 and 8.9. 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``
(`#8638 <https://github.com/coq/coq/pull/8638>`_, by Jason Gross).
- Allow inspecting custom grammar entries by :cmd:`Print Custom Grammar`
(`#10061 <https://github.com/coq/coq/pull/10061>`_,
fixes `#9681 <http://github.com/coq/coq/pull/9681>`_,
by Jasper Hugunin, review by Pierre-Marie Pédrot and Hugo Herbelin).
- The `quote plugin
<https://coq.inria.fr/distrib/V8.9.0/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
(`#7894 <https://github.com/coq/coq/pull/7894>`_, by Maxime Dénès).
- Ltac:
- 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:
:g:`Ltac foo := idtac. Section S. Ltac foo := fail. End S.`
(`#8555 <https://github.com/coq/coq/pull/8555>`_, by Maxime Dénès).
- Names of existential variables occurring in Ltac functions
(e.g. :g:`?[n]` or :g:`?n` in terms - not in patterns) are now interpreted
the same way as other variable names occurring in Ltac functions
(`#7309 <https://github.com/coq/coq/pull/7309>`_, by Hugo Herbelin).
- Tactics:
- Removed the deprecated `romega` tactic
(`#8419 <https://github.com/coq/coq/pull/8419>`_,
by Maxime Dénès and Vincent Laporte).
- 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
(`#8987 <https://github.com/coq/coq/pull/8987>`_, by Maxime Dénès).
- 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 :tacn:`lia`, :tacn:`nia`, 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
(`#8062 <https://github.com/coq/coq/pull/8062>`_, by Jason Gross).
- The syntax of the :tacn:`autoapply` tactic was fixed to conform with preexisting
documentation: it now takes a `with` clause instead of a `using` clause
(`#9524 <https://github.com/coq/coq/pull/9524>`_,
closes `#7632 <https://github.com/coq/coq/issues/7632>`_,
by Théo Zimmermann).
- Modes are now taken into account by :tacn:`typeclasses eauto` for
local hypotheses
(`#9996 <https://github.com/coq/coq/pull/9996>`_,
fixes `#5752 <https://github.com/coq/coq/issues/5752>`_,
by Maxime Dénès, review by Pierre-Marie Pédrot).
- New variant :tacn:`change_no_check` of :tacn:`change`, usable as a
documented replacement of :tacn:`convert_concl_no_check`
(`#10012 <https://github.com/coq/coq/pull/10012>`_,
`#10017 <https://github.com/coq/coq/pull/10017>`_,
`#10053 <https://github.com/coq/coq/pull/10053>`_, and
`#10059 <https://github.com/coq/coq/pull/10059>`_,
by Hugo Herbelin and Paolo G. Giarrusso).
- The simplified value returned by :tacn:`field_simplify` is not
always a fraction anymore. When the denominator is :g:`1`, it
returns :g:`x` while previously it was returning :g:`x/1`. This
change could break codes that were post-processing application of
:tacn:`field_simplify` to get rid of these :g:`x/1`
(`#9854 <https://github.com/coq/coq/pull/9854>`_,
by Laurent Théry,
with help from Michael Soegtrop, Maxime Dénès, and Vincent Laporte).
- SSReflect:
- 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}`
(`#9341 <https://github.com/coq/coq/pull/9341>`_, by Enrico Tassi).
- `inE` now expands `y \in r x` when `r` is a `simpl_rel`.
New `{pred T}` notation for a `pred T` alias in the `pred_sort` coercion
class, simplified `predType` interface: `pred_class` and `mkPredType`
deprecated, `{pred T}` and `PredType` should be used instead.
`if c return t then ...` now expects `c` to be a variable bound in `t`.
New `nonPropType` interface matching types that do _not_ have sort `Prop`.
New `relpre R f` definition for the preimage of a relation R under f
(`#9995 <https://github.com/coq/coq/pull/9995>`_, by Georges Gonthier).
- Vernacular commands:
- Binders for an :cmd:`Instance` now act more like binders for a :cmd:`Theorem`.
Names may not be repeated, and may not overlap with section variable names
(`#8820 <https://github.com/coq/coq/pull/8820>`_,
closes `#8791 <https://github.com/coq/coq/issues/8791>`_,
by Jasper Hugunin).
- Removed the deprecated `Implicit Tactic` family of commands
(`#8779 <https://github.com/coq/coq/pull/8779>`_, by Pierre-Marie Pédrot).
- The `Automatic Introduction` option has been removed and is now the
default
(`#9001 <https://github.com/coq/coq/pull/9001>`_,
by Emilio Jesús Gallego Arias).
- `Arguments` now accepts names for arguments provided with `extra_scopes`
(`#9117 <https://github.com/coq/coq/pull/9117>`_, by Maxime Dénès).
- The naming scheme for anonymous binders in a `Theorem` has changed to
avoid conflicts with explicitly named binders
(`#9160 <https://github.com/coq/coq/pull/9160>`_,
closes `#8819 <https://github.com/coq/coq/issues/8819>`_,
by Jasper Hugunin).
- Computation of implicit arguments now properly handles local definitions in the
binders for an `Instance`, and can be mixed with implicit binders `{x : T}`
(`#9307 <https://github.com/coq/coq/pull/9307>`_,
closes `#9300 <https://github.com/coq/coq/issues/9300>`_,
by Jasper Hugunin).
- :cmd:`Declare Instance` now requires an instance name.
The flag :flag:`Refine Instance Mode` has been turned off by default,
meaning that :cmd:`Instance` no longer opens a proof when a body is
provided. The flag has been deprecated and will be removed in the next
version.
(`#9270 <https://github.com/coq/coq/pull/9270>`_,
and `#9825 <https://github.com/coq/coq/pull/9825>`_,
by Maxime Dénès)
- Command :cmd:`Instance`, when no body is provided, now always opens
a proof. This is a breaking change, as instance of :n:`Instance
@ident__1 : @ident__2.` where :n:`@ident__2` is a trivial class will
have to be changed into :n:`Instance @ident__1 : @ident__2 := %{%}.`
or :n:`Instance @ident__1 : @ident__2. Proof. Qed.`
(`#9274 <https://github.com/coq/coq/pull/9274>`_, by Maxime Dénès).
- The flag :flag:`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
(`#9410 <https://github.com/coq/coq/pull/9410>`_, by Maxime Dénès).
- The algorithm computing implicit arguments now behaves uniformly for primitive
projection and application nodes
(`#9509 <https://github.com/coq/coq/pull/9509>`_,
closes `#9508 <https://github.com/coq/coq/issues/9508>`_,
by Pierre-Marie Pédrot).
- :cmd:`Hypotheses` and :cmd:`Variables` can now take implicit
binders inside sections
(`#9364 <https://github.com/coq/coq/pull/9364>`_,
closes `#9363 <https://github.com/coq/coq/issues/9363>`_,
by Jasper Hugunin).
- Removed deprecated option `Automatic Coercions Import`
(`#8094 <https://github.com/coq/coq/pull/8094>`_, by Maxime Dénès).
- The ``Show Script`` command has been deprecated
(`#9829 <https://github.com/coq/coq/pull/9829>`_, by Vincent Laporte).
- :cmd:`Coercion` does not warn ambiguous paths which are obviously
convertible with existing ones. The ambiguous paths messages have been
turned to warnings, thus now they could appear in the output of ``coqc``.
The convertibility checking procedure for coercion paths is complete for
paths consisting of coercions satisfying the uniform inheritance condition,
but some coercion paths could be reported as ambiguous even if they are
convertible with existing ones when they have coercions that don't satisfy
the uniform inheritance condition
(`#9743 <https://github.com/coq/coq/pull/9743>`_,
closes `#3219 <https://github.com/coq/coq/issues/3219>`_,
by Kazuhiko Sakaguchi).
- A new flag :flag:`Fast Name Printing` has been introduced. It changes the
algorithm used for allocating bound variable names for a faster but less
clever one
(`#9078 <https://github.com/coq/coq/pull/9078>`_, by Pierre-Marie Pédrot).
- Option ``Typeclasses Axioms Are Instances`` (compatibility option
introduced in the previous version) is deprecated. Use :cmd:`Declare
Instance` for axioms which should be instances
(`#8920 <https://github.com/coq/coq/pull/8920>`_, by Gaëtan Gilbert).
- Removed option `Printing Primitive Projection Compatibility`
(`#9306 <https://github.com/coq/coq/pull/9306>`_, by Gaëtan Gilbert).
- Standard Library:
- Added `Bvector.BVeq` that decides whether two `Bvector`\s are equal.
Added notations for `BVxor`, `BVand`, `BVor`, `BVeq` and `BVneg`
(`#8171 <https://github.com/coq/coq/pull/8171>`_, by Yishuai Li).
- Added `ByteVector` type that can convert to and from `string`
(`#8365 <https://github.com/coq/coq/pull/8365>`_, by Yishuai Li).
- 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`
(`#8815 <https://github.com/coq/coq/pull/8815>`_, by Yishuai Li).
- 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
(`#9013 <https://github.com/coq/coq/pull/9013>`_, by Gaëtan Gilert).
- Added `Coq.Structures.OrderedTypeEx.String_as_OT` to make strings an
ordered type, using lexical order
(`#7221 <https://github.com/coq/coq/pull/7221>`_, by Li Yao).
- Added lemmas about `Z.testbit`, `Z.ones`, and `Z.modulo`
(`#9425 <https://github.com/coq/coq/pull/9425>`_, by Andres Erbsen).
- Moved the `auto` hints of the `FSet` library into a new
`fset` database
(`#9725 <https://github.com/coq/coq/pull/9725>`_, by Frédéric Besson).
- Added :g:`Coq.Structures.EqualitiesFacts.PairUsualDecidableTypeFull`
(`#9984 <https://github.com/coq/coq/pull/9984>`_,
by Jean-Christophe Léchenet and Oliver Nash).
- Some error messages that show problems with a pair of non-matching
values will now highlight the differences
(`#8669 <https://github.com/coq/coq/pull/8669>`_, by Jim Fehrle).
- Changelog has been moved from a specific file `CHANGES.md` to the
reference manual; former Credits chapter of the reference manual has
been split in two parts: a History chapter which was enriched with
additional historical information about Coq versions 1 to 5, and a
Changes chapter which was enriched with the content formerly in
`CHANGES.md` and `COMPATIBILITY`
(`#9133 <https://github.com/coq/coq/pull/9133>`_,
`#9668 <https://github.com/coq/coq/pull/9668>`_,
`#9939 <https://github.com/coq/coq/pull/9939>`_,
`#9964 <https://github.com/coq/coq/pull/9964>`_,
and `#10085 <https://github.com/coq/coq/pull/10085>`_,
by Théo Zimmermann,
with help and ideas from Emilio Jesús Gallego Arias, Gaëtan
Gilbert, Clément Pit-Claudel, Matthieu Sozeau, and Enrico Tassi).
Changes in 8.10+beta2
~~~~~~~~~~~~~~~~~~~~~
Many bug fixes and documentation improvements, in particular:
**Tactics**
- Make the :tacn:`discriminate` tactic work together with
:flag:`Universe Polymorphism` and equality in :g:`Type`. This,
in particular, makes :tacn:`discriminate` compatible with the HoTT
library https://github.com/HoTT/HoTT
(`#10205 <https://github.com/coq/coq/pull/10205>`_,
by Andreas Lynge, review by Pierre-Marie Pédrot and Matthieu Sozeau).
**SSReflect**
- Make the ``case E: t`` tactic work together with
:flag:`Universe Polymorphism` and equality in :g:`Type`.
This makes :tacn:`case <case (ssreflect)>` compatible with the HoTT
library https://github.com/HoTT/HoTT
(`#10302 <https://github.com/coq/coq/pull/10302>`_,
fixes `#10301 <https://github.com/coq/coq/issues/10301>`_,
by Andreas Lynge, review by Enrico Tassi)
- Make the ``rewrite /t`` tactic work together with
:flag:`Universe Polymorphism`.
This makes :tacn:`rewrite <rewrite (ssreflect)>` compatible with the HoTT
library https://github.com/HoTT/HoTT
(`#10305 <https://github.com/coq/coq/pull/10305>`_,
fixes `#9336 <https://github.com/coq/coq/issues/9336>`_,
by Andreas Lynge, review by Enrico Tassi)
**CoqIDE**
- Fix CoqIDE instability on Windows after the update to gtk3
(`#10360 <https://github.com/coq/coq/pull/10360>`_, by Michael Soegtrop,
closes `#9885 <https://github.com/coq/coq/issues/9885>`_).
**Miscellaneous**
- Proof General can now display Coq-generated diffs between proof steps
in color
(`#10019 <https://github.com/coq/coq/pull/10019>`_ and
(in Proof General) `#421 <https://github.com/ProofGeneral/PG/pull/421>`_,
by Jim Fehrle).
Changes in 8.10+beta3
~~~~~~~~~~~~~~~~~~~~~
**Kernel**
- Fix soundness issue with template polymorphism (`#9294
<https://github.com/coq/coq/issues/9294>`_).
Declarations of template-polymorphic inductive types ignored the
provenance of the universes they were abstracting on and did not
detect if they should be greater or equal to :math:`\Set` in
general. Previous universes and universes introduced by the inductive
definition could have constraints that prevented their instantiation
with e.g. :math:`\Prop`, resulting in unsound instantiations later. The
implemented fix only allows abstraction over universes introduced by
the inductive declaration, and properly records all their constraints
by making them by default only :math:`>= \Prop`. It is also checked
that a template polymorphic inductive actually is polymorphic on at
least one universe.
This prevents inductive declarations in sections to be universe
polymorphic over section parameters. For a backward compatible fix,
simply hoist the inductive definition out of the section.
An alternative is to declare the inductive as universe-polymorphic and
cumulative in a universe-polymorphic section: all universes and
constraints will be properly gathered in this case.
See :ref:`Template-polymorphism` for a detailed exposition of the
rules governing template-polymorphic types.
To help users incrementally fix this issue, a command line option
`-no-template-check` and a global flag :flag:`Template Check` are
available to selectively disable the new check. Use at your own risk.
(`#9918 <https://github.com/coq/coq/pull/9918>`_, by Matthieu Sozeau
and Maxime Dénès).
**User messages**
- Improve the ambiguous paths warning to indicate which path is ambiguous with
new one
(`#10336 <https://github.com/coq/coq/pull/10336>`_,
closes `#3219 <https://github.com/coq/coq/issues/3219>`_,
by Kazuhiko Sakaguchi).
**Extraction**
- Fix extraction to OCaml of primitive machine integers;
see :ref:`primitive-integers`
(`#10430 <https://github.com/coq/coq/pull/10430>`_,
fixes `#10361 <https://github.com/coq/coq/issues/10361>`_,
by Vincent Laporte).
- Fix a printing bug of OCaml extraction on dependent record projections, which
produced improper `assert false`. This change makes the OCaml extractor
internally inline record projections by default; thus the monolithic OCaml
extraction (:cmd:`Extraction` and :cmd:`Recursive Extraction`) does not
produce record projection constants anymore except for record projections
explicitly instructed to extract, and records declared in opaque modules
(`#10577 <https://github.com/coq/coq/pull/10577>`_,
fixes `#7348 <https://github.com/coq/coq/issues/7348>`_,
by Kazuhiko Sakaguchi).
**Standard library**
- Added ``splitat`` function and lemmas about ``splitat`` and ``uncons``
(`#9379 <https://github.com/coq/coq/pull/9379>`_,
by Yishuai Li, with help of Konstantinos Kallas,
follow-up of `#8365 <https://github.com/coq/coq/pull/8365>`_,
which added ``uncons`` in 8.10+beta1).
Changes in 8.10.0
~~~~~~~~~~~~~~~~~
- Micromega tactics (:tacn:`lia`, :tacn:`nia`, etc) are no longer confused by
primitive projections (`#10806 <https://github.com/coq/coq/pull/10806>`_,
fixes `#9512 <https://github.com/coq/coq/issues/9512>`_
by Vincent Laporte).
Changes in 8.10.1
~~~~~~~~~~~~~~~~~
A few bug fixes and documentation improvements, in particular:
**Kernel**
- Fix proof of False when using |SProp| (incorrect De Bruijn handling
when inferring the relevance mark of a function) (`#10904
<https://github.com/coq/coq/pull/10904>`_, by Pierre-Marie Pédrot).
**Tactics**
- Fix an anomaly when unsolved evar in :cmd:`Add Ring`
(`#10891 <https://github.com/coq/coq/pull/10891>`_,
fixes `#9851 <https://github.com/coq/coq/issues/9851>`_,
by Gaëtan Gilbert).
**Tactic language**
- Fix Ltac regression in binding free names in uconstr
(`#10899 <https://github.com/coq/coq/pull/10899>`_,
fixes `#10894 <https://github.com/coq/coq/issues/10894>`_,
by Hugo Herbelin).
**CoqIDE**
- Fix handling of unicode input before space
(`#10852 <https://github.com/coq/coq/pull/10852>`_,
fixes `#10842 <https://github.com/coq/coq/issues/10842>`_,
by Arthur Charguéraud).
**Extraction**
- Fix custom extraction of inductives to JSON
(`#10897 <https://github.com/coq/coq/pull/10897>`_,
fixes `#4741 <https://github.com/coq/coq/issues/4741>`_,
by Helge Bahmann).
Version 8.9
-----------
Summary of changes
~~~~~~~~~~~~~~~~~~
|Coq| version 8.9 contains the result of refinements and stabilization
of features and deprecations or removals of deprecated features,
cleanups of the internals of the system and API along with a few new
features. This release includes many user-visible changes, including
deprecations that are documented in the next subsection and new features that
are documented in the reference manual. Here are the most important
changes:
- Kernel: mutually recursive records are now supported, by Pierre-Marie
Pédrot.
- Notations:
- Support for autonomous grammars of terms called “custom entries”, by
Hugo Herbelin (see Section :ref:`custom-entries` of the reference
manual).
- Deprecated notations of the standard library will be removed in the
next version of |Coq|, see the next subsection for a script to
ease porting, by Jason Gross and Jean-Christophe Léchenet.
- Added the :cmd:`Numeral Notation` command for registering decimal
numeral notations for custom types, by Daniel de Rauglaudre, Pierre
Letouzey and Jason Gross.
- Tactics: Introduction tactics :tacn:`intro`/:tacn:`intros` on a goal that is an
existential variable now force a refinement of the goal into a
dependent product rather than failing, by Hugo Herbelin.
- Decision procedures: deprecation of tactic ``romega`` in favor of
:tacn:`lia` and removal of ``fourier``, replaced by :tacn:`lra` which
subsumes it, by Frédéric Besson, Maxime Dénès, Vincent Laporte and
Laurent Théry.
- Proof language: focusing bracket ``{`` now supports named
:ref:`goals <curly-braces>`, e.g. ``[x]:{`` will focus
on a goal (existential variable) named ``x``, by Théo Zimmermann.
- SSReflect: the implementation of delayed clear was simplified by
Enrico Tassi: the variables are always renamed using inaccessible
names when the clear switch is processed and finally cleared at the
end of the intro pattern. In addition to that, the use-and-discard flag
``{}`` typical of rewrite rules can now be also applied to views,
e.g. ``=> {}/v`` applies ``v`` and then clears ``v``. See Section
:ref:`introduction_ssr`.
- Vernacular:
- Experimental support for :ref:`attributes <gallina-attributes>` on
commands, by Vincent Laporte, as in ``#[local] Lemma foo : bar.``
Tactics and tactic notations now support the ``deprecated``
attribute.
- Removed deprecated commands ``Arguments Scope`` and ``Implicit
Arguments`` in favor of :cmd:`Arguments (scopes)` and
:cmd:`Arguments (implicits)`, with the help of Jasper Hugunin.
- New flag :flag:`Uniform Inductive Parameters` by Jasper Hugunin to
avoid repeating uniform parameters in constructor declarations.
- New commands :cmd:`Hint Variables` and :cmd:`Hint Constants`, by
Matthieu Sozeau, for controlling the opacity status of variables and
constants in hint databases. It is recommended to always use these
commands after creating a hint database with :cmd:`Create HintDb`.
- Multiple sections with the same name are now allowed, by Jasper
Hugunin.
- Library: additions and changes in the ``VectorDef``, ``Ascii``, and
``String`` libraries. Syntax notations are now available only when using
``Import`` of libraries and not merely ``Require``, by various
contributors (source of incompatibility, see the next subsection for details).
- Toplevels: ``coqtop`` and ``coqide`` can now display diffs between proof
steps in color, using the :opt:`Diffs` option, by Jim Fehrle.
- Documentation: we integrated a large number of fixes to the new Sphinx
documentation by various contributors, coordinated by Clément
Pit-Claudel and Théo Zimmermann.
- Tools: removed the ``gallina`` utility and the homebrewed ``Emacs`` mode.
- Packaging: as in |Coq| 8.8.2, the Windows installer now includes many
more external packages that can be individually selected for
installation, by Michael Soegtrop.
Version 8.9 also comes with a bunch of smaller-scale changes and
improvements regarding the different components of the system. Most
important ones are documented in the next subsection file.
On the implementation side, the ``dev/doc/changes.md`` file documents
the numerous changes to the implementation and improvements of
interfaces. The file provides guidelines on porting a plugin to the new
version and a plugin development tutorial kept in sync with Coq was
introduced by Yves Bertot http://github.com/ybertot/plugin_tutorials.
The new ``dev/doc/critical-bugs`` file documents the known critical bugs
of |Coq| and affected releases.
The efficiency of the whole system has seen improvements thanks to
contributions from Gaëtan Gilbert, Pierre-Marie Pédrot, and Maxime Dénès.
Maxime Dénès, Emilio Jesús Gallego Arias, Gaëtan Gilbert, Michael
Soegtrop, Théo Zimmermann worked on maintaining and improving the
continuous integration system.
The OPAM repository for |Coq| packages has been maintained by Guillaume
Melquiond, Matthieu Sozeau, Enrico Tassi with contributions from many
users. A list of packages is available at https://coq.inria.fr/opam/www/.
The 54 contributors for this version are Léo Andrès, Rin Arakaki,
Benjamin Barenblat, Langston Barrett, Siddharth Bhat, Martin Bodin,
Simon Boulier, Timothy Bourke, Joachim Breitner, Tej Chajed, Arthur
Charguéraud, Pierre Courtieu, Maxime Dénès, Andres Erbsen, Jim Fehrle,
Julien Forest, Emilio Jesus Gallego Arias, Gaëtan Gilbert, Matěj
Grabovský, Jason Gross, Samuel Gruetter, Armaël Guéneau, Hugo Herbelin,
Jasper Hugunin, Ralf Jung, Sam Pablo Kuper, Ambroise Lafont, Leonidas
Lampropoulos, Vincent Laporte, Peter LeFanu Lumsdaine, Pierre Letouzey,
Jean-Christophe Léchenet, Nick Lewycky, Yishuai Li, Sven M. Hallberg,
Assia Mahboubi, Cyprien Mangin, Guillaume Melquiond, Perry E. Metzger,
Clément Pit-Claudel, Pierre-Marie Pédrot, Daniel R. Grayson, Kazuhiko
Sakaguchi, Michael Soegtrop, Matthieu Sozeau, Paul Steckler, Enrico
Tassi, Laurent Théry, Anton Trunov, whitequark, Théo Winterhalter,
Zeimer, Beta Ziliani, Théo Zimmermann.
Many power users helped to improve the design of the new features via
the issue and pull request system, the |Coq| development mailing list or
the [email protected] mailing list. It would be impossible to mention
exhaustively the names of everybody who to some extent influenced the
development.
Version 8.9 is the fourth release of |Coq| developed on a time-based
development cycle. Its development spanned 7 months from the release of
|Coq| 8.8. The development moved to a decentralized merging process
during this cycle. Guillaume Melquiond was in charge of the release
process and is the maintainer of this release. This release is the
result of ~2,000 commits and ~500 PRs merged, closing 75+ issues.
The |Coq| development team welcomed Vincent Laporte, a new |Coq|
engineer working with Maxime Dénès in the |Coq| consortium.
| Paris, November 2018,
| Matthieu Sozeau for the |Coq| development team
|
Details of changes in 8.9+beta1
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Kernel
- Mutually defined records are now supported.
Notations
- New support for autonomous grammars of terms, called "custom
entries" (see chapter "Syntax extensions" of the reference manual).
- Deprecated compatibility notations will actually be removed in the
next version of Coq. 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.
Tactics
- Added toplevel goal selector `!` which expects a single focused goal.
Use with `Set Default Goal Selector` to force focusing before tactics
are called.
- The undocumented "nameless" forms `fix N`, `cofix` that were
deprecated in 8.8 have been removed from Ltac's syntax; please use
`fix ident N/cofix ident` to explicitly name the (co)fixpoint
hypothesis to be introduced.
- Introduction tactics `intro`/`intros` on a goal that is an
existential variable now force a refinement of the goal into a
dependent product rather than failing.
- Support for `fix`/`cofix` added in Ltac `match` and `lazymatch`.
- Ltac backtraces now include trace information about tactics
called by OCaml-defined tactics.
- Option `Ltac Debug` now applies also to terms built using Ltac functions.
- Deprecated the `Implicit Tactic` family of commands.
- The default program obligation tactic uses a bounded proof search
instead of an unbounded and potentially non-terminating one now
(source of incompatibility).
- The `simple apply` tactic now respects the `Opaque` flag when called from
Ltac (`auto` still does not respect it).
- Tactic `constr_eq` now adds universe constraints needed for the
identity to the context (it used to ignore them). New tactic
`constr_eq_strict` checks that the required constraints already hold
without adding new ones. Preexisting tactic `constr_eq_nounivs` can
still be used if you really want to ignore universe constraints.
- Tactics and tactic notations now understand the `deprecated` attribute.
- The `fourier` tactic has been removed. Please now use `lra` instead. You
may need to add `Require Import Lra` to your developments. For compatibility,
we now define `fourier` as a deprecated alias of `lra`.
- The `romega` tactics have been deprecated; please use `lia` instead.
Focusing
- Focusing bracket `{` now supports named goal selectors,
e.g. `[x]: {` will focus on a goal (existential variable) named `x`.
As usual, unfocus with `}` once the sub-goal is fully solved.
Specification language
- A fix to unification (which was sensitive to the ascii name of
variables) may occasionally change type inference in incompatible
ways, especially regarding the inference of the return clause of `match`.
Standard Library
- Added `Ascii.eqb` and `String.eqb` and the `=?` notation for them,
and proved some lemmas about them. Note that this might cause
incompatibilities if you have, e.g., `string_scope` and `Z_scope` both
open with `string_scope` on top, and expect `=?` to refer to `Z.eqb`.
Solution: wrap `_ =? _` in `(_ =? _)%Z` (or whichever scope you
want).
- Added `Ndigits.N2Bv_sized`, and proved some lemmas about it.
Deprecated `Ndigits.N2Bv_gen`.
- The scopes `int_scope` and `uint_scope` have been renamed to
`dec_int_scope` and `dec_uint_scope`, to clash less with ssreflect
and other packages. They are still delimited by `%int` and `%uint`.
- Syntax notations for `string`, `ascii`, `Z`, `positive`, `N`, `R`,
and `int31` are no longer available merely by :cmd:`Require`\ing the files
that define the inductives. You must :cmd:`Import` `Coq.Strings.String.StringSyntax`
(after `Require` `Coq.Strings.String`), `Coq.Strings.Ascii.AsciiSyntax` (after
`Require` `Coq.Strings.Ascii`), `Coq.ZArith.BinIntDef`, `Coq.PArith.BinPosDef`,
`Coq.NArith.BinNatDef`, `Coq.Reals.Rdefinitions`, and
`Coq.Numbers.Cyclic.Int31.Int31`, respectively, to be able to use
these notations. Note that passing `-compat 8.8` or issuing
`Require Import Coq.Compat.Coq88` will make these notations
available. Users wishing to port their developments automatically
may download `fix.py` from
https://gist.github.com/JasonGross/5d4558edf8f5c2c548a3d96c17820169
and run a command like `while true; do make -Okj 2>&1 |
/path/to/fix.py; done` and get a cup of coffee. (This command must
be manually interrupted once the build finishes all the way though.
Note also that this method is not fail-proof; you may have to adjust
some scopes if you were relying on string notations not being
available even when `string_scope` was open.)
- Numeral syntax for `nat` is no longer available without loading the
entire prelude (`Require Import Coq.Init.Prelude`). This only
impacts users running Coq without the init library (`-nois` or
`-noinit`) and also issuing `Require Import Coq.Init.Datatypes`.
Tools
- Coq_makefile lets one override or extend the following variables from
the command line: `COQFLAGS`, `COQCHKFLAGS`, `COQDOCFLAGS`.
`COQFLAGS` is now entirely separate from `COQLIBS`, so in custom Makefiles
`$(COQFLAGS)` should be replaced by `$(COQFLAGS) $(COQLIBS)`.
- Removed the `gallina` utility (extracts specification from Coq vernacular files).
If you would like to maintain this tool externally, please contact us.
- Removed the Emacs modes distributed with Coq. You are advised to
use `Proof-General <https://proofgeneral.github.io/>`_ (and optionally
`Company-Coq <https://github.com/cpitclaudel/company-coq>`_) instead.
If your use case is not covered by these alternative Emacs modes,
please open an issue. We can help set up external maintenance as part
of Proof-General, or independently as part of coq-community.
Vernacular Commands
- Removed deprecated commands `Arguments Scope` and `Implicit Arguments`
(not the option). Use the `Arguments` command instead.
- Nested proofs may be enabled through the option `Nested Proofs Allowed`.
By default, they are disabled and produce an error. The deprecation
warning which used to occur when using nested proofs has been removed.
- Added option `Uniform Inductive Parameters` which abstracts over parameters
before typechecking constructors, allowing to write for example
`Inductive list (A : Type) := nil : list | cons : A -> list -> list.`
- New `Set Hint Variables/Constants Opaque/Transparent` commands for setting
globally the opacity flag of variables and constants in hint databases,
overwriting the opacity set of the hint database.
- Added generic syntax for "attributes", as in:
`#[local] Lemma foo : bar.`
- Added the `Numeral Notation` command for registering decimal numeral
notations for custom types
- The `Set SsrHave NoTCResolution` command no longer has special global
scope. If you want the previous behavior, use `Global Set SsrHave
NoTCResolution`.
- Multiple sections with the same name are allowed.
Coq binaries and process model
- Before 8.9, Coq distributed a single `coqtop` binary and a set of
dynamically loadable plugins that used to take over the main loop
for tasks such as IDE language server or parallel proof checking.
These plugins have been turned into full-fledged binaries so each
different process has associated a particular binary now, in
particular `coqidetop` is the CoqIDE language server, and
`coq{proof,tactic,query}worker` are in charge of task-specific and
parallel proof checking.
SSReflect
- The implementation of delayed clear switches in intro patterns
is now simpler to explain:
1. The immediate effect of a clear switch like `{x}` is to rename the
variable `x` to `_x_` (i.e. a reserved identifier that cannot be mentioned
explicitly)
2. The delayed effect of `{x}` is that `_x_` is cleared at the end of the intro
pattern
3. A clear switch immediately before a view application like `{x}/v` is
translated to `/v{x}`.
In particular, the third rule lets one write `{x}/v` even if `v` uses the variable `x`:
indeed the view is executed before the renaming.
- An empty clear switch is now accepted in intro patterns before a
view application whenever the view is a variable.
One can now write `{}/v` to mean `{v}/v`. Remark that `{}/x` is very similar
to the idiom `{}e` for the rewrite tactic (the equation `e` is used for
rewriting and then discarded).
Standard Library
- There are now conversions between `string` and `positive`, `Z`,
`nat`, and `N` in binary, octal, and hex.
Display diffs between proof steps
- `coqtop` and `coqide` can now highlight the differences between proof steps
in color. This can be enabled from the command line or the
`Set Diffs "on"/"off"/"removed"` command. Please see the documentation for
details. Showing diffs in Proof General requires small changes to PG
(under discussion).
Notations
- Added `++` infix for `VectorDef.append`.
Note that this might cause incompatibilities if you have, e.g., `list_scope`
and `vector_scope` both open with `vector_scope` on top, and expect `++` to
refer to `app`.
Solution: wrap `_ ++ _` in `(_ ++ _)%list` (or whichever scope you want).
Changes in 8.8.0
~~~~~~~~~~~~~~~~
Various bug fixes.
Changes in 8.8.1
~~~~~~~~~~~~~~~~
- Some quality-of-life fixes.
- Numerous improvements to the documentation.
- Fix a critical bug related to primitive projections and :tacn:`native_compute`.
- Ship several additional Coq libraries with the Windows installer.
Version 8.8
-----------
Summary of changes
~~~~~~~~~~~~~~~~~~
|Coq| version 8.8 contains the result of refinements and stabilization of
features and deprecations, cleanups of the internals of the system along
with a few new features. The main user visible changes are:
- Kernel: fix a subject reduction failure due to allowing fixpoints
on non-recursive values, by Matthieu Sozeau.
Handling of evars in the VM (the kernel still does not accept evars)
by Pierre-Marie Pédrot.
- Notations: many improvements on recursive notations and support for
destructuring patterns in the syntax of notations by Hugo Herbelin.
- Proof language: tacticals for profiling, timing and checking success
or failure of tactics by Jason Gross. The focusing bracket ``{``
supports single-numbered goal selectors, e.g. ``2:{``, by Théo
Zimmermann.
- Vernacular: deprecation of commands and more uniform handling of the
``Local`` flag, by Vincent Laporte and Maxime Dénès, part of a larger
attribute system overhaul. Experimental ``Show Extraction`` command by
Pierre Letouzey. Coercion now accepts ``Prop`` or ``Type`` as a source
by Arthur Charguéraud. ``Export`` modifier for options allowing to
export the option to modules that ``Import`` and not only ``Require``
a module, by Pierre-Marie Pédrot.
- Universes: many user-level and API level enhancements: qualified
naming and printing, variance annotations for cumulative inductive
types, more general constraints and enhancements of the minimization
heuristics, interaction with modules by Gaëtan Gilbert, Pierre-Marie
Pédrot and Matthieu Sozeau.
- Library: Decimal Numbers library by Pierre Letouzey and various small
improvements.
- Documentation: a large community effort resulted in the migration
of the reference manual to the Sphinx documentation tool. The result
is this manual. The new documentation infrastructure (based on Sphinx)
is by Clément Pit-Claudel. The migration was coordinated by Maxime Dénès
and Paul Steckler, with some help of Théo Zimmermann during the
final integration phase. The 14 people who ported the manual are
Calvin Beck, Heiko Becker, Yves Bertot, Maxime Dénès, Richard Ford,
Pierre Letouzey, Assia Mahboubi, Clément Pit-Claudel,
Laurence Rideau, Matthieu Sozeau, Paul Steckler, Enrico Tassi,
Laurent Théry, Nikita Zyuzin.
- Tools: experimental ``-mangle-names`` option to ``coqtop``/``coqc`` for
linting proof scripts, by Jasper Hugunin.
On the implementation side, the ``dev/doc/changes.md`` file
documents the numerous changes to the implementation and improvements of
interfaces. The file provides guidelines on porting a plugin to the new
version.
Version 8.8 also comes with a bunch of smaller-scale changes and
improvements regarding the different components of the system.
Most important ones are documented in the next subsection file.
The efficiency of the whole system has seen improvements thanks to
contributions from Gaëtan Gilbert, Pierre-Marie Pédrot, Maxime Dénès and
Matthieu Sozeau and performance issue tracking by Jason Gross and Paul
Steckler.
The official wiki and the bugtracker of |Coq| migrated to the GitHub
platform, thanks to the work of Pierre Letouzey and Théo
Zimmermann. Gaëtan Gilbert, Emilio Jesús Gallego Arias worked on
maintaining and improving the continuous integration system.
The OPAM repository for |Coq| packages has been maintained by Guillaume
Melquiond, Matthieu Sozeau, Enrico Tassi with contributions from many
users. A list of packages is available at https://coq.inria.fr/opam/www/.
The 44 contributors for this version are Yves Bertot, Joachim Breitner, Tej
Chajed, Arthur Charguéraud, Jacques-Pascal Deplaix, Maxime Dénès, Jim Fehrle,
Julien Forest, Yannick Forster, Gaëtan Gilbert, Jason Gross, Samuel Gruetter,
Thomas Hebb, Hugo Herbelin, Jasper Hugunin, Emilio Jesus Gallego Arias, Ralf
Jung, Johannes Kloos, Matej Košík, Robbert Krebbers, Tony Beta Lambda, Vincent
Laporte, Peter LeFanu Lumsdaine, Pierre Letouzey, Farzon Lotfi, Cyprien Mangin,
Guillaume Melquiond, Raphaël Monat, Carl Patenaude Poulin, Pierre-Marie Pédrot,
Clément Pit-Claudel, Matthew Ryan, Matt Quinn, Sigurd Schneider, Bernhard
Schommer, Michael Soegtrop, Matthieu Sozeau, Arnaud Spiwack, Paul Steckler,
Enrico Tassi, Anton Trunov, Martin Vassor, Vadim Zaliva and Théo Zimmermann.
Version 8.8 is the third release of |Coq| developed on a time-based
development cycle. Its development spanned 6 months from the release of
|Coq| 8.7 and was based on a public roadmap. The development process
was coordinated by Matthieu Sozeau. Maxime Dénès was in charge of the
release process. Théo Zimmermann is the maintainer of this release.
Many power users helped to improve the design of the new features via
the bug tracker, the pull request system, the |Coq| development mailing
list or the [email protected] mailing list. Special thanks to the users who
contributed patches and intensive brain-storming and code reviews,
starting with Jason Gross, Ralf Jung, Robbert Krebbers and Amin Timany.
It would however be impossible to mention exhaustively the names
of everybody who to some extent influenced the development.
The |Coq| consortium, an organization directed towards users and
supporters of the system, is now running and employs Maxime Dénès.
The contacts of the Coq Consortium are Yves Bertot and Maxime Dénès.
| Santiago de Chile, March 2018,
| Matthieu Sozeau for the |Coq| development team
|
Details of changes in 8.8+beta1
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Kernel
- Support for template polymorphism for definitions was removed. May trigger
more "universe inconsistency" errors in rare occasions.
- Fixpoints are no longer allowed on non-recursive inductive types.
Notations
- Recursive notations with the recursive pattern repeating on the
right (e.g. "( x ; .. ; y ; z )") now supported.
- Notations with a specific level for the leftmost nonterminal,
when printing-only, are supported.
- Notations can now refer to the syntactic category of patterns (as in
"fun 'pat =>" or "match p with pat => ... end"). Two variants are
available, depending on whether a single variable is considered as a
pattern or not.
- Recursive notations now support ".." patterns with several
occurrences of the recursive term or binder, possibly mixing terms
and binders, possibly in reverse left-to-right order.
- "Locate" now working also on notations of the form "x + y" (rather
than "_ + _").
Specification language
- When printing clauses of a "match", clauses with same right-hand
side are factorized and the last most factorized clause with no
variables, if it exists, is turned into a default clause.
Use "Unset Printing Allow Default Clause" do deactivate printing
of a default clause.
Use "Unset Printing Factorizable Match Patterns" to deactivate
factorization of clauses with same right-hand side.
Tactics
- On Linux, "native_compute" calls can be profiled using the "perf"
utility. The command "Set NativeCompute Profiling" enables
profiling, and "Set NativeCompute Profile Filename" customizes
the profile filename.
- The tactic "omega" is now aware of the bodies of context variables
such as "x := 5 : Z" (see #1362). This could be disabled via
Unset Omega UseLocalDefs.
- The tactic "romega" is also aware now of the bodies of context variables.
- The tactic "zify" resp. "omega with N" is now aware of N.pred.
- Tactic "decide equality" now able to manage constructors which
contain proofs.
- Added tactics reset ltac profile, show ltac profile (and variants)
- Added tactics restart_timer, finish_timing, and time_constr as an
experimental way of timing Ltac's evaluation phase
- Added tactic optimize_heap, analogous to the Vernacular Optimize
Heap, which performs a major garbage collection and heap compaction
in the OCaml run-time system.
- The tactics "dtauto", "dintuition", "firstorder" now handle inductive types
with let bindings in the parameters.
- The tactic ``dtauto`` now handles some inductives such as
``@sigT A (fun _ => B)`` as non-dependent conjunctions.
- A bug fixed in ``rewrite H in *`` and ``rewrite H in * |-`` may cause a
few rare incompatibilities (it was unintendedly recursively
rewriting in the side conditions generated by H).
- Added tactics "assert_succeeds tac" and "assert_fails tac" to ensure
properties of the execution of a tactic without keeping the effect
of the execution.
- `vm_compute` now supports existential variables.
- Calls to `shelve` and `give_up` within calls to tactic `refine` now working.
- Deprecated tactic `appcontext` was removed.
Focusing
- Focusing bracket `{` now supports single-numbered goal selector,
e.g. `2: {` will focus on the second sub-goal. As usual, unfocus
with `}` once the sub-goal is fully solved.
The `Focus` and `Unfocus` commands are now deprecated.
Vernacular Commands
- Proofs ending in "Qed exporting ident, .., ident" are not supported
anymore. Constants generated during `abstract` are kept private to the
local environment.
- The deprecated Coercion Local, Open Local Scope, Notation Local syntax
was removed. Use Local as a prefix instead.
- For the Extraction Language command, "OCaml" is spelled correctly.
The older "Ocaml" is still accepted, but deprecated.
- Using “Require” inside a section is deprecated.
- An experimental command "Show Extraction" allows to extract the content
of the current ongoing proof (grant wish #4129).
- Coercion now accepts the type of its argument to be "Prop" or "Type".
- The "Export" modifier can now be used when setting and unsetting options, and
will result in performing the same change when the module corresponding the
command is imported.
- The `Axiom` command does not automatically declare axioms as instances when
their type is a class. Previous behavior can be restored using `Set
Typeclasses Axioms Are Instances`.
Universes
- Qualified naming of global universes now works like other namespaced
objects (e.g. constants), with a separate namespace, inside and across
module and library boundaries. Global universe names introduced in an
inductive / constant / Let declaration get qualified with the name of
the declaration.
- Universe cumulativity for inductive types is now specified as a
variance for each polymorphic universe. See the reference manual for
more information.
- Inference of universe constraints with cumulative inductive types
produces more general constraints. Unsetting new option Cumulativity
Weak Constraints produces even more general constraints (but may
produce too many universes to be practical).
- Fix #5726: Notations that start with `Type` now support universe instances
with `@{u}`.
- `with Definition` now understands universe declarations
(like `@{u| Set < u}`).
Tools
- Coq can now be run with the option -mangle-names to change the auto-generated
name scheme. This is intended to function as a linter for developments that
want to be robust to changes in auto-generated names. This feature is experimental,
and may change or disappear without warning.
- GeoProof support was removed.
Checker
- The checker now accepts filenames in addition to logical paths.
CoqIDE
- Find and Replace All report the number of occurrences found; Find indicates
when it wraps.
coqdep
- Learned to read -I, -Q, -R and filenames from _CoqProject files.
This is used by coq_makefile when generating dependencies for .v
files (but not other files).
Documentation
- The Coq FAQ, formerly located at https://coq.inria.fr/faq, has been
moved to the GitHub wiki section of this repository; the main entry
page is https://github.com/coq/coq/wiki/The-Coq-FAQ.
- Documentation: a large community effort resulted in the migration
of the reference manual to the Sphinx documentation tool. The result
is partially integrated in this version.
Standard Library
- New libraries Coq.Init.Decimal, Coq.Numbers.DecimalFacts,
Coq.Numbers.DecimalNat, Coq.Numbers.DecimalPos,
Coq.Numbers.DecimalN, Coq.Numbers.DecimalZ,
Coq.Numbers.DecimalString providing a type of decimal numbers, some
facts about them, and conversions between decimal numbers and nat,
positive, N, Z, and string.
- Added [Coq.Strings.String.concat] to concatenate a list of strings
inserting a separator between each item
- Notation `'` for Zpos in QArith was removed.
- Some deprecated aliases are now emitting warnings when used.
Compatibility support
- Support for compatibility with versions before 8.6 was dropped.
Options
- The following deprecated options have been removed:
+ `Refolding Reduction`
+ `Standard Proposition Elimination`
+ `Dependent Propositions Elimination`
+ `Discriminate Introduction`
+ `Shrink Abstract`
+ `Tactic Pattern Unification`
+ `Intuition Iff Unfolding`
+ `Injection L2R Pattern Order`
+ `Record Elimination Schemes`
+ `Match Strict`
+ `Tactic Compat Context`
+ `Typeclasses Legacy Resolution`
+ `Typeclasses Module Eta`
+ `Typeclass Resolution After Apply`
Details of changes in 8.8.0
~~~~~~~~~~~~~~~~~~~~~~~~~~~
Tools
- Asynchronous proof delegation policy was fixed. Since version 8.7
Coq was ignoring previous runs and the `-async-proofs-delegation-threshold`
option did not have the expected behavior.
Tactic language
- The undocumented "nameless" forms `fix N`, `cofix` have been
deprecated; please use `fix ident N /cofix ident` to explicitly
name the (co)fixpoint hypothesis to be introduced.
Documentation
- The reference manual is now fully ported to Sphinx.
Other small deprecations and bug fixes.
Details of changes in 8.8.1
~~~~~~~~~~~~~~~~~~~~~~~~~~~
Kernel
--> --------------------
--> maximum size reached
--> --------------------
[ zur Elbe Produktseite wechseln0.316Quellennavigators
]
|
|
|
|
|
|
