The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT inria.fr>]

Dear Coq users,

  here is a summary of the planned features of Coq 8.6, which is expected to go into beta testing in september. We welcome any feedback from you users (preferably on mailto:coqdev AT inria.fr), in particular on the points marked with a [*] which can introduce incompatibilities (many of them can be tamed using the compatibility flags in Coq.Compat.Coq85 and the -compat 8.5 mode). If you feel brave and want to play with it, there are links to snapshot packages at the end of this email. 

Main Changes:

Universes: a new, more efficient constraint checking algorithm was implemented by J. H. Jourdan, considerably speeding up type-checking and elaboration time.

Reduction flags: New flags [fix], [cofix] and [match] are now available to use with simpl, cbv etc..., the [iota] flag is a shorthand for the three of them.

Warning System: * most warnings are now classified, can be set on, off or fatal and are output by coqc by default.

Patterns in abstractions:

Gallina terms can now use irrefutable patterns ('pat := c) in abstractions (lambdas and foralls), which get compiled to pattern-matching constructs (work by D. de Rauglaudre).

Typeclass resolution/eauto *:

typeclasses eauto has been reimplemented by M. Sozeau using the primitives of the new proof-engine for backtracking and goal handling. It is 99% compatible with the old engine, which can still be called using a compatibility flag. The 1% difference is due to bugs in the old engine.

Ltac:

-* Thanks to the efforts of P.M. Pédrot, the Ltac language is now almost entirely decoupled from the tactics themselves, allowing its future extension or replacement thanks to this modular implementation. This required a syntactic change at the user level to uniformly handle generic arguments: the constr:c parsing rule is now replaced with constr:(c) (likewise for other grammar entries like ltac, uconstr etc).

- Goal range selectors allow to apply a tactic to a named goal or a range of goals (by C. Mangin)

-* The [fresh] tactic accepts more things (terms which can be seen as identifiers) (by P. Courtieu)

- Support for profiling Ltac scripts has been added (by J. Gross, T. Tebbi and P. Steckler).

Tactics:

- New is_ind, is_constructor, .. tactics

-* [contradiction] now solves ~ True, ~ (x = x), and is part of the [easy] ending tactic.

-* [injection H] works in place, not putting anything in the goal (by H. Herbelin).

-* The [Regular Subst Tactic] mode is now on, following the specification of [subst] in the manual  (by H. Herbelin).

-* Invariants on intro-patterns for generalized cartesian products (e.g. intros (x, y, ...)) not doing auto-completion anymore (by H. Herbelin)

- Pattern-matching facilities to select subterms with the semantics of the ssreflect term selection strategy (by E. Tassi)

Standard Library:

-* nil, cons, Some and None have their implicit type argument maximally inserted now, potential source of incompatibility.

CoqIDE:

- Finer-grain error resilience and reporting in structured proof scripts (by E. Tassi, also available to other IDE's based on PIDE).

- Configurable shortcuts for user queries (by C. Mangin)

- Modernized preferences (by. P.M. Pédrot)

A more detailed and technical roadmap can be found here: https://github.com/coq/roadmaps/blob/master/text/roadmap-8.6.md or in the CHANGES file.

Snapshot packages (also available from sources at https://github.com/coq/coq.git#v8.6):

OS X:

https://ci.inria.fr/coq/job/coq-8.6-macos/1/artifact/CoqIDE_trunk.dmg

Windows:

https://ci.inria.fr/coq/job/coq-8.6-win64/lastSuccessfulBuild/artifact/dev/nsis/coq-installer-trunk-win64.exe

https://ci.inria.fr/coq/view/windows/job/coq-8.6-win32/lastSuccessfulBuild/artifact/dev/nsis/coq-installer-trunk-win32.exe

For The Coq Development Team,

-- Matthieu Sozeau