Discussion:
Coq 8.9+beta1 is out!
(too old to reply)
Guillaume Melquiond
2018-11-06 09:46:14 UTC
Permalink
Dear Coq users,

The Coq development team is pleased to announce the release of the
first beta version of Coq 8.9, available at

https://github.com/coq/coq/releases/tag/V8.9%2Bbeta1

Source, Windows and OS X packages are available.

The main changes are as follows.

Kernel: mutually recursive records are now supported.

Notations:

- Support for autonomous grammars of terms called "custom entries".

- Deprecated notations of the standard library will be removed in the
next version of Coq, see the CHANGES.md file for a script to ease porting.

- Added the Numeral Notation command for registering decimal numeral
notations for custom types.

Tactics: 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.

Decision procedures: deprecation of tactic romega in favor of lia and
removal of fourier, replaced by lra which subsumes it.

Proof language: focusing bracket "{" now supports named goals, e.g.
"[x]:{" will focus on a goal (existential variable) named x.

SSReflect: the implementation of delayed clear was simplified: 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.

Vernacular:

- Experimental support for attributes on commands 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 Arguments.

- New flag Uniform Inductive Parameters to avoid repeating uniform
parameters in constructor declarations.

- New commands Hint Variables and Hint Constants for controlling the
opacity status of variables and constants in hint databases. It is
recommended to always use these commands after creating a hint databse
with Create HintDb.

- Multiple sections with the same name are now allowed.

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 (source of incompatibility, see
CHANGES.md for details).

Toplevels: coqtop and coqide can now display diffs between proof steps
in color, using the Diffs option.

Documentation: we integrated a large number of fixes to the new Sphinx
documentation.

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.

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 CHANGES.md file.
Beta Ziliani
2018-11-06 10:03:14 UTC
Permalink
Hi devs, I have little questions regarding the changes:

On Tue, Nov 6, 2018 at 6:46 AM Guillaume Melquiond
***@inria.fr <http://mailto:***@inria.fr>
wrote:

Dear Coq users,
Post by Guillaume Melquiond
Tactics: 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.
Uh,.. why? Will the following tactic endlessly loop? repeat (intros ?)
Post by Guillaume Melquiond
- Experimental support for attributes on commands as in "#[local] Lemma
foo : bar." Tactics and tactic notations now support the deprecated
attribute.
What is #[local]? Why is there now support for a deprecated thing?
Many thanks,
Beta
Théo Zimmermann
2018-11-06 10:14:44 UTC
Permalink
Hi,
Post by Beta Ziliani
On Tue, Nov 6, 2018 at 6:46 AM Guillaume Melquiond
Dear Coq users,
Tactics: 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.
Uh,.. why? Will the following tactic endlessly loop? |repeat (intros ?)|
Why would you use repeat (intros ?) instead of intros * exactly?

Anyways, here is the link to the corresponding PR if you want to comment
or see the context: https://github.com/coq/coq/pull/7304
You may also open an issue if you think this PR is bad and should be
reverted.
Post by Beta Ziliani
- Experimental support for attributes on commands as in "#[local] Lemma
foo : bar." Tactics and tactic notations now support the deprecated
attribute.
What is |#[local]|? Why is there now support for a deprecated thing?
Guillaume, could you upload the manual so that we can point people to it?
Essentially #[local] is the same as Local and we advise not to rely on
it as the feature is completely experimental and the syntax may change.
Support for the deprecated attribute means that a deprecated attribute
may be attached to tactics defined with Ltac or Tactic Notation to mark
them as deprecated. Again, this is documented in the manual (but it is
not online yet).
Post by Beta Ziliani
Many thanks,
Beta
Best,
Théo
Beta Ziliani
2018-11-06 10:24:22 UTC
Permalink
Great, thanks Théo!
Post by Théo Zimmermann
Hi,
Post by Beta Ziliani
On Tue, Nov 6, 2018 at 6:46 AM Guillaume Melquiond
Dear Coq users,
Tactics: 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.
Uh,.. why? Will the following tactic endlessly loop? |repeat (intros ?)|
Why would you use repeat (intros ?) instead of intros * exactly?
Anyways, here is the link to the corresponding PR if you want to comment
or see the context: https://github.com/coq/coq/pull/7304
You may also open an issue if you think this PR is bad and should be
reverted.
Post by Beta Ziliani
- Experimental support for attributes on commands as in "#[local]
Lemma
Post by Beta Ziliani
foo : bar." Tactics and tactic notations now support the deprecated
attribute.
What is |#[local]|? Why is there now support for a deprecated thing?
Guillaume, could you upload the manual so that we can point people to it?
Essentially #[local] is the same as Local and we advise not to rely on
it as the feature is completely experimental and the syntax may change.
Support for the deprecated attribute means that a deprecated attribute
may be attached to tactics defined with Ltac or Tactic Notation to mark
them as deprecated. Again, this is documented in the manual (but it is
not online yet).
Post by Beta Ziliani
Many thanks,
Beta
Best,
Théo
Clément Pit-Claudel
2018-11-06 14:31:43 UTC
Permalink
Post by Théo Zimmermann
Why would you use repeat (intros ?) instead of intros * exactly?
I don't typically write [repeat (intros ?)], but I've definitely written things like [repeat (intro; try apply xxx)] as part of larger tactics. Here's a simplified example:

Goal forall A B C, (A -> B) -> (C -> A -> B).
intros A B C H.
repeat (intro; try apply H).

Clément.
Ralf Jung
2018-11-16 14:59:51 UTC
Permalink
Hi,
Post by Théo Zimmermann
Post by Beta Ziliani
What is |#[local]|? Why is there now support for a deprecated thing?
Guillaume, could you upload the manual so that we can point people to it?
Essentially #[local] is the same as Local and we advise not to rely on
it as the feature is completely experimental and the syntax may change.
Support for the deprecated attribute means that a deprecated attribute
may be attached to tactics defined with Ltac or Tactic Notation to mark
them as deprecated. Again, this is documented in the manual (but it is
not online yet).
Do you mean a #[deprecated] attribute? What you wrote ("a deprecated
attribute") makes it look like deprecated here is an adjective referring to
attribute... Hence me and I guess Beta as well were confused by that changelog
statement.

Kind regards,
Ralf
Théo Zimmermann
2018-11-16 15:07:34 UTC
Permalink
Hi Ralf,

Yes, that's right, it is #[deprecated(...)] that is meant here. There is
a debate though whether this mention of this experimental feature
belongs to the release notes:
https://github.com/coq/coq/issues/8027#issuecomment-436724533

(although I have been said that I shouldn't discourage users from using
the feature: https://github.com/coq/coq/issues/8027#issuecomment-436196797)

In any case, some clarification is needed.
Théo
Post by Ralf Jung
Hi,
Post by Théo Zimmermann
Post by Beta Ziliani
What is |#[local]|? Why is there now support for a deprecated thing?
Guillaume, could you upload the manual so that we can point people to it?
Essentially #[local] is the same as Local and we advise not to rely on
it as the feature is completely experimental and the syntax may change.
Support for the deprecated attribute means that a deprecated attribute
may be attached to tactics defined with Ltac or Tactic Notation to mark
them as deprecated. Again, this is documented in the manual (but it is
not online yet).
Do you mean a #[deprecated] attribute? What you wrote ("a deprecated
attribute") makes it look like deprecated here is an adjective referring to
attribute... Hence me and I guess Beta as well were confused by that changelog
statement.
Kind regards,
Ralf
Théo Zimmermann
2018-11-08 14:06:04 UTC
Permalink
Dear Coq-Club,

The reference manual for the beta version of Coq 8.9 is available at:
https://coq.inria.fr/distrib/V8.9+beta1/refman

You may notice error messages in Coq snippets. There is currently no
infrastructure for detecting those (see also
https://github.com/coq/coq/issues/7755) thus if you notice some error
messages, we would really like that you open bug reports (except in the
cases where it's clear from the context that the error was expected), or
even better that you submit a pull request fixing the problem (use the
"Edit on GitHub" button and here is some documentation on getting
started with Sphinx:
https://github.com/coq/coq/tree/master/doc/sphinx#documenting-coq-with-sphinx;
fixing the kind of problem I am mentioning is generally a matter of
adding a `reset` at the right `.. coqtop::` directive as explained here
https://github.com/coq/coq/tree/master/doc/sphinx#coq-directives).

Thanks,
Théo
Post by Guillaume Melquiond
Dear Coq users,
The Coq development team is pleased to announce the release of the
first beta version of Coq 8.9, available at
https://github.com/coq/coq/releases/tag/V8.9%2Bbeta1
Source, Windows and OS X packages are available.
The main changes are as follows.
Kernel: mutually recursive records are now supported.
- Support for autonomous grammars of terms called "custom entries".
- Deprecated notations of the standard library will be removed in the
next version of Coq, see the CHANGES.md file for a script to ease porting.
- Added the Numeral Notation command for registering decimal numeral
notations for custom types.
Tactics: 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.
Decision procedures: deprecation of tactic romega in favor of lia and
removal of fourier, replaced by lra which subsumes it.
Proof language: focusing bracket "{" now supports named goals, e.g.
"[x]:{" will focus on a goal (existential variable) named x.
SSReflect: the implementation of delayed clear was simplified: 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.
- Experimental support for attributes on commands 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 Arguments.
- New flag Uniform Inductive Parameters to avoid repeating uniform
parameters in constructor declarations.
- New commands Hint Variables and Hint Constants for controlling the
opacity status of variables and constants in hint databases. It is
recommended to always use these commands after creating a hint databse
with Create HintDb.
- Multiple sections with the same name are now allowed.
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 (source of incompatibility, see
CHANGES.md for details).
Toplevels: coqtop and coqide can now display diffs between proof steps
in color, using the Diffs option.
Documentation: we integrated a large number of fixes to the new Sphinx
documentation.
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.
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 CHANGES.md file.
Loading...