Fixes build with current ocaml.
Note: this update includes the import semantics fixes from 8.11 that
break a lot of developments.
pkgsrc change: docs build now works.
Summary of changes in 8.12:
Coq version 8.12 integrates many usability improvements, in particular
with respect to notations, scopes and implicit arguments, along with
many bug fixes and major improvements to the reference manual. The
main changes include:
New binder notation for non-maximal implicit arguments using [ ]
allowing to set and see the implicit status of arguments
immediately.
New notation Inductive I A | x : s := ... to distinguish the
uniform from the non-uniform parameters in inductive definitions.
More robust and expressive treatment of implicit inductive
parameters in inductive declarations.
Improvements in the treatment of implicit arguments and partially
applied constants in notations, parsing of hexadecimal number
notation and better handling of scopes and coercions for printing.
A correct and efficient coercion coherence checking algorithm,
avoiding spurious or duplicate warnings.
An improved Search command which accepts complex queries. Note
that this takes precedence over the now deprecated ssreflect
search.
Many additions and improvements of the standard library.
Improvements to the reference manual include a more logical
organization of chapters along with updated syntax descriptions
that match Coq's grammar in most but not all chapters.
Additionally, the omega tactic is deprecated in this version of Coq,
and we recommend users to switch to lia in new proof scripts (see also
the warning message in the corresponding chapter).
Summary of changes in 8.11:
The main changes brought by Coq version 8.11 are:
Ltac2, a new tactic language for writing more robust larger scale
tactics, with built-in support for datatypes and the multi-goal
tactic monad.
Primitive floats are integrated in terms and follow the binary64
format of the IEEE 754 standard, as specified in the
Coq.Float.Floats library.
Cleanups of the section mechanism, delayed proofs and further
restrictions of template polymorphism to fix soundness issues
related to universes.
New unsafe flags to disable locally guard, positivity and universe
checking. Reliance on these flags is always printed by Print
Assumptions.
Fixed bugs of Export and Import that can have a significant impact
on user developments (common source of incompatibility!).
New interactive development method based on vos interface files,
allowing to work on a file without recompiling the proof parts of
their dependencies.
New Arguments annotation for bidirectional type inference
configuration for reference (e.g. constants, inductive)
applications.
New refine attribute for Instance can be used instead of the
removed Refine Instance Mode.
Generalization of the under and over tactics of SSReflect to
arbitrary relations.
Revision of the Coq.Reals library, its axiomatisation and
instances of the constructive and classical real numbers.
Additionally, while the omega tactic is not yet deprecated in this
version of Coq, it should soon be the case and we already recommend
users to switch to lia in new proof scripts (see also the warning
message in the corresponding chapter).
The full (huge) changelog is here:
https://coq.inria.fr/distrib/V8.12.2/refman/changes.html
(without it the new coqide is missing things, and it seems to
specifically refer to adwaita-icon-theme by name)
Bump PKGREVISION to 1, since coqide is a default-on option.
Changes include:
- native 63-bit machine integers;
- a new sort of definitionally proof-irrelevant propositons: SProp;
- private universes for opaque polymorphic constants;
- string notations and numeral notations;
- a new simplex-based proof engine for the tactics lia, nia, lra and nra;
- new introduction patterns for SSReflect;
- a tactic to rewrite under binders: under;
- easy input of non-ASCII symbols in CoqIDE, which now uses GTK3.
and many small improvements and bugfixes.
Main changes:
* some quality-of-life bug fixes,
* many improvements to the documentation,
* a critical bug fix related to primitive projections and native_compute,
* several additional Coq libraries shipped with the Windows installer.
The list of improvements, additions, bugfixes and so on is quite large;
those interested can refer to the CHANGES file in the distribution.
The reference manual has been fully ported to Sphinx.
Unsorted entries in PLIST files have generated a pkglint warning for at
least 12 years. Somewhat more recently, pkglint has learned to sort
PLIST files automatically. Since pkglint 5.4.23, the sorting is only
done in obvious, simple cases. These have been applied by running:
pkglint -Cnone,PLIST -Wnone,plist-sort -r -F
Includes many improvements and bugfixes (none that seem to be breaking
backwards compatibility though), see the CHANGELOG.
For packaging:
- camlp4 support removed, package now uses camlp5 exclusively
- fix for PR pkg/52651
- Fix#5380: Default colors for CoqIDE are actually applied.
- Fix plugin warnings
- Document named evars (including Show ident)
- Fix Bug #5574, document function scope
- Adding a test case as requested in bug 5205.
- Fix Bug #5568, no dup notation warnings on repeated module imports
- Fix documentation of Typeclasses eauto :=
- Refactor documentation of records.
- Protecting from warnings while compiling 8.6
- Fixing an inconsistency between configure and configure.ml
- Add test-suite checks for coqchk with constraints
- Fix bug #5019 (looping zify on dependent types)
- Fix bug 5550: "typeclasses eauto with" does not work with section variables.
- Bug 5546, qualify datatype constructors when needed in Show Match
- Bug #5535, test for Show with -emacs
- Fix bug #5486, don't reverse ids in tuples
- Fixing #5522 (anomaly with free vars of pat)
- Fix bug #5526, don't check for nonlinearity in notation if printing only
- Fix bug #5255
- Fix bug #3659: -time should understand multibyte encodings.
- FIx bug #5300: Anomaly: Uncaught exception Not_found" in "Print Assumptions".
- Fix outdated description in RefMan.
- Repairing `Set Rewriting Schemes`
- Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).
- Fix description of command-line arguments for Add (Rec) LoadPath
- Fix bug #5377: @? patterns broken.
- add XML protocol doc
- Fix anomaly when doing [all:Check _.] during a proof.
- Correction of bug #4306
- Fix#5435: [Eval native_compute in] raises anomaly.
- Instances should obey universe binders even when defined by tactics.
- Intern names bound in match patterns
- funind: Ignore missing info for current function
- Do not typecheck twice the type of opaque constants.
- show unused intro pattern warning
- [future] Be eager when "chaining" already resolved future values.
- Opaque side effects
- Fix#5132: coq_makefile generates incorrect install goal
- Run non-tactic comands without resilient_command
- Univs: fix bug #5365, generation of u+k <= v constraints
- make `emit' tail recursive
- Don't require printing-only notation to be productive
- Fix the way setoid_rewrite handles bindings.
- Fix for bug 5244 - set printing width ignored when given enough space
- Fix bug 4969, autoapply was not tagging shelved subgoals correctly
