[Coq-Club] Coq 8.8.2 is out!

[Théo Zimmermann]

Dear Coq users,

We are pleased to announce the 8.8.2 release of Coq.

Main changes:

- The kernel does not tolerate capture of global universes by
polymorphic universe binders, fixing a soundness break (triggered
only through custom plugins)

- A PDF version of the reference manual is available once again.

- The coq-makefile targets `print-pretty-timed`,
`print-pretty-timed-diff`, and `print-pretty-single-time-diff` now
correctly label the "before" and "after" columns, rather than swapping
them.

- The Windows installer now includes many more external packages that
can be individually selected for installation.

This release includes many other bug fixes and lots of documentation
improvements (for details, see the 8.8.2 milestone at
https://github.com/coq/coq/milestone/15?closed=1). Feedback and bug
reports are extremely welcome (https://github.com/coq/coq/issues).

You can download the PDF manual, an installer for MacOS or for Windows
from https://github.com/coq/coq/releases/tag/V8.8.2. Note that the
Windows installers that are currently provided are not signed and will
trigger a warning when you try to run them. Signed installers will be
added as soon as they are ready (most likely tomorrow).

OPAM and Nix packages will be available soon.

The Coq Development Team

[Perry E. Metzger]

On Wed, 26 Sep 2018 17:22:02 +0200 Théo Zimmermann

Post by Théo Zimmermann
Dear Coq users,
We are pleased to announce the 8.8.2 release of Coq.

FYI, the update to the MacPorts Coq package is now in, so MacPorts
users should be able to update with minimum fuss later today.

Perry

[Théo Zimmermann]

FYI, the signed Windows packages are now available on the release page, and
the OPAM package is now ready (for OPAM 2.0 users) thanks to Heiko Becker.

Théo

On Wed, 26 Sep 2018 17:22:02 +0200 Théo Zimmermann

Post by Théo Zimmermann
Dear Coq users,
We are pleased to announce the 8.8.2 release of Coq.

FYI, the update to the MacPorts Coq package is now in, so MacPorts
users should be able to update with minimum fuss later today.
Perry
--

[Christian Doczkal]

FYI, the signed Windows packages are now available on the release page, and the OPAM package is now ready (for OPAM 2.0 users) thanks to Heiko Becker.

Will there be an OPAM package for OPAM 1.2.x users? As of now, OPAM 2.0 has yet to arrive in the Gentoo or Ubuntu repositories. Other distributions will likely also still ship 1.2.x.

Best,
Christian

[Théo Zimmermann]

Hello,

Thanks for raising this question.
I was personally quite shocked by the decision of OPAM maintainers to
almost freeze the OPAM 1.2 repository when OPAM 2.0 was released (seemed
pretty aggressive to me). Especially since IIUC OPAM is not able to upgrade
itself. But then, I am not an OPAM user myself so my view might be
prejudiced.

So let's have this discussion: please share your opinion if you have one.

If we decide to continue providing an OPAM package for OPAM 1.2 users, it
should be pretty straightforward to do so using Coq's own OPAM repository
http://coq.inria.fr/opam/released, the same one that is currently used to
distribute Coq plugins and libraries.

If we decide against doing so, it might hinder adoption of Coq 8.8.2 and
upcoming Coq 8.9.0 (not a good thing). It could also lead to the weird
situation that users are able to test Coq 8.9+beta1 through
https://coq.inria.fr/opam/core-dev/ but are then not able to upgrade from
the beta to the final version. So a priori, I am personally in favor of
continued OPAM 1.2 support (but again I'm not in the best position to form
an opinion given that I don't use OPAM).

Best,
Théo

Le jeu. 4 oct. 2018 à 23:42, Christian Doczkal <

Post by Théo Zimmermann
FYI, the signed Windows packages are now available on the release page,

and the OPAM package is now ready (for OPAM 2.0 users) thanks to Heiko
Becker.
Will there be an OPAM package for OPAM 1.2.x users? As of now, OPAM 2.0
has yet to arrive in the Gentoo or Ubuntu repositories. Other distributions
will likely also still ship 1.2.x.
Best,
Christian

[Christian Doczkal]

Hello,

I currently install coq (and mathcomp, merlin, etc.) via OPAM, and I
agree with Théo on all points. Distributions like Ubuntu will take at
least a year (two for the current LTS release) before they will ship
OPAM 2.0 in their repositories. Currently, there isn't even an external
repository providing 2.0 for Ubuntu. So users would need to resort to
install scripts that dump binaries into system folders or manually set
up paths and the like. Not at all satisfactory.

Rolling Release distributions (e.g., Arch and Gentoo) should be faster,
but will still take weeks/months.

However, unless the OPAM developers/maintainers change their stance
regarding the repository for 1.2 users, this will require the Coq
developers to also provide packages for dependencies not to be found in
the 1.2 repository (I'm thinking of things like camlp5 here). This will
create a bit of extra effort.

Best,
Christian

Post by Théo Zimmermann
Hello,
Thanks for raising this question.
I was personally quite shocked by the decision of OPAM maintainers to
almost freeze the OPAM 1.2 repository when OPAM 2.0 was released (seemed
pretty aggressive to me). Especially since IIUC OPAM is not able to
upgrade itself. But then, I am not an OPAM user myself so my view might
be prejudiced.
So let's have this discussion: please share your opinion if you have one.
If we decide to continue providing an OPAM package for OPAM 1.2 users,
it should be pretty straightforward to do so using Coq's own OPAM
repository http://coq.inria.fr/opam/released, the same one that is
currently used to distribute Coq plugins and libraries.
If we decide against doing so, it might hinder adoption of Coq 8.8.2 and
upcoming Coq 8.9.0 (not a good thing). It could also lead to the weird
situation that users are able to test Coq 8.9+beta1 through
https://coq.inria.fr/opam/core-dev/ but are then not able to upgrade
from the beta to the final version. So a priori, I am personally in
favor of continued OPAM 1.2 support (but again I'm not in the best
position to form an opinion given that I don't use OPAM).
Best,
Théo
Le jeu. 4 oct. 2018 à 23:42, Christian Doczkal

Post by Théo Zimmermann
FYI, the signed Windows packages are now available on the release

page, and the OPAM package is now ready (for OPAM 2.0 users) thanks
to Heiko Becker.
Will there be an OPAM package for OPAM 1.2.x users? As of now, OPAM
2.0 has yet to arrive in the Gentoo or Ubuntu repositories. Other
distributions will likely also still ship 1.2.x.
Best,
Christian

[Emilio Jesús Gallego Arias]

Post by Christian Doczkal
However, unless the OPAM developers/maintainers change their stance
regarding the repository for 1.2 users, this will require the Coq
developers to also provide packages for dependencies not to be found in
the 1.2 repository (I'm thinking of things like camlp5 here). This will
create a bit of extra effort.

AFAICT the main 1.2 repository should contain dependencies good up to Coq 8.10.

E.

[Théo Zimmermann]

Hello all,

For the record, the discussion prompted by Christian was continued here
https://github.com/coq/opam-coq-archive/issues/257 and Coq developers are
in agreement that the Coq OPAM repository could be used to continue
distributing Coq packages that are compatible with OPAM 1.2 (and move only
the "dev" packages to OPAM 2.0). However, no action has been taken since
then for lack of motivated manpower mostly. So if a user wants to take care
of adding Coq stable packages to the released section of
https://github.com/coq/opam-coq-archive, they are most welcome!

Théo

Post by Emilio Jesús Gallego Arias

Post by Christian Doczkal
However, unless the OPAM developers/maintainers change their stance
regarding the repository for 1.2 users, this will require the Coq
developers to also provide packages for dependencies not to be found in
the 1.2 repository (I'm thinking of things like camlp5 here). This will
create a bit of extra effort.

AFAICT the main 1.2 repository should contain dependencies good up to Coq 8.10.
E.

[Christian Doczkal]

Hello,

I was already using a local OPAM package for 8.8.2 and was essentially waiting for the discussion to finish. There is now a pull request, so no need for anyone else to become active ;)

Best,
Christian

Post by Théo Zimmermann
Hello all,
For the record, the discussion prompted by Christian was continued here https://github.com/coq/opam-coq-archive/issues/257 and Coq developers are in agreement that the Coq OPAM repository could be used to continue distributing Coq packages that are compatible with OPAM 1.2 (and move only the "dev" packages to OPAM 2.0). However, no action has been taken since then for lack of motivated manpower mostly. So if a user wants to take care of adding Coq stable packages to the released section of https://github.com/coq/opam-coq-archive, they are most welcome!
Théo

Post by Christian Doczkal
However, unless the OPAM developers/maintainers change their stance
regarding the repository for 1.2 users, this will require the Coq
developers to also provide packages for dependencies not to be found in
the 1.2 repository (I'm thinking of things like camlp5 here). This will
create a bit of extra effort.

AFAICT the main 1.2 repository should contain dependencies good up to Coq 8.10.
E.

[Vadim Zaliva]

What about Coq itself? My opam-1.2 has Coq-8.8.1 as the latest version,
while opam2 has 8.8.2.

--
CMU ECE Ph.D. candidate
Mobile/Signal/WhatsApp: [phone]

Post by Théo Zimmermann
Hello all,
For the record, the discussion prompted by Christian was continued here
https://github.com/coq/opam-coq-archive/issues/257 and Coq developers are
in agreement that the Coq OPAM repository could be used to continue
distributing Coq packages that are compatible with OPAM 1.2 (and move only
the "dev" packages to OPAM 2.0). However, no action has been taken since
then for lack of motivated manpower mostly. So if a user wants to take care
of adding Coq stable packages to the released section of
https://github.com/coq/opam-coq-archive, they are most welcome!
Théo

Post by Emilio Jesús Gallego Arias

Post by Christian Doczkal
However, unless the OPAM developers/maintainers change their stance
regarding the repository for 1.2 users, this will require the Coq
developers to also provide packages for dependencies not to be found in
the 1.2 repository (I'm thinking of things like camlp5 here). This will
create a bit of extra effort.

AFAICT the main 1.2 repository should contain dependencies good up to Coq 8.10.
E.

[Théo Zimmermann]

Hi Vadim,

That was precisely the question asked by Christian. He has opened a pull
request now (https://github.com/coq/opam-coq-archive/pull/495) so this
issue should be solved soon.

Théo

Post by Vadim Zaliva
What about Coq itself? My opam-1.2 has Coq-8.8.1 as the latest version,
while opam2 has 8.8.2.
--
CMU ECE Ph.D. candidate
Mobile/Signal/WhatsApp: [phone] <+1%20510-220-1060>

Post by Théo Zimmermann
Hello all,
For the record, the discussion prompted by Christian was continued here
https://github.com/coq/opam-coq-archive/issues/257 and Coq developers
are in agreement that the Coq OPAM repository could be used to continue
distributing Coq packages that are compatible with OPAM 1.2 (and move only
the "dev" packages to OPAM 2.0). However, no action has been taken since
then for lack of motivated manpower mostly. So if a user wants to take care
of adding Coq stable packages to the released section of
https://github.com/coq/opam-coq-archive, they are most welcome!
Théo

Post by Emilio Jesús Gallego Arias

Post by Christian Doczkal
However, unless the OPAM developers/maintainers change their stance
regarding the repository for 1.2 users, this will require the Coq
developers to also provide packages for dependencies not to be found in
the 1.2 repository (I'm thinking of things like camlp5 here). This will
create a bit of extra effort.

AFAICT the main 1.2 repository should contain dependencies good up to Coq 8.10.
E.

[Christian Doczkal]

Hi,

the pull request has been merged. Thus, Coq-8.8.2 should now also be available to opam-1.x users via the coq-released repository.

Best,
Christian

Post by Théo Zimmermann
Hi Vadim,
That was precisely the question asked by Christian. He has opened a pull request now (https://github.com/coq/opam-coq-archive/pull/495) so this issue should be solved soon.
Théo
What about Coq itself? My opam-1.2 has Coq-8.8.1 as the latest version, while opam2 has 8.8.2.
--
CMU ECE Ph.D. candidate
Mobile/Signal/WhatsApp: [phone] <tel:+1%20510-220-1060>
Hello all,
For the record, the discussion prompted by Christian was continued here https://github.com/coq/opam-coq-archive/issues/257 and Coq developers are in agreement that the Coq OPAM repository could be used to continue distributing Coq packages that are compatible with OPAM 1.2 (and move only the "dev" packages to OPAM 2.0). However, no action has been taken since then for lack of motivated manpower mostly. So if a user wants to take care of adding Coq stable packages to the released section of https://github.com/coq/opam-coq-archive, they are most welcome!
Théo

Post by Christian Doczkal
However, unless the OPAM developers/maintainers change their stance
regarding the repository for 1.2 users, this will require the Coq
developers to also provide packages for dependencies not to be found in
the 1.2 repository (I'm thinking of things like camlp5 here). This will
create a bit of extra effort.

AFAICT the main 1.2 repository should contain dependencies good up to Coq 8.10.
E.

[Emilio Jesús Gallego Arias]

Hi Christian,

Post by Christian Doczkal
Will there be an OPAM package for OPAM 1.2.x users? As of now, OPAM
2.0 has yet to arrive in the Gentoo or Ubuntu repositories. Other
distributions will likely also still ship 1.2.x.

I'm afraid the official OPAM repository doesn't allow to update the 1.2
branch anymore.

You can however use Coq's private one:
https://coq.inria.fr/opam/www/using.html

E.