Stream: Coq users

Topic: Release of Std++ for 8.18

view this post on Zulip Karl Palmskog (Sep 14 2023 at 11:13):

Coq 8.18.0 is out on opam, but unfortunately there is no compatible release of Coq-Std++ for 8.18 since the last release, 1.8.0, is incompatible with 8.18. Myself and probably quite a few other Std++ users are hoping for new release compatible with 8.18 so we can have a stable target in CI and so on. Any chance of a release happening anytime soon @Robbert Krebbers @Ralf Jung?

view this post on Zulip Ralf Jung (Sep 14 2023 at 11:30):

yeah we do definitely want to make a release. sadly vacation during the summer and lectures in the fall make it hard to find a time when we both have enough free time to make a release...

view this post on Zulip Ralf Jung (Sep 14 2023 at 13:04):

but if someone wants to help us make a release, please let us know. :) it's all documented at the repos are in releasable state, it's just about finishing the release notes and creating the packages.

view this post on Zulip Karl Palmskog (Oct 02 2023 at 14:33):

@Julien Puydt given that a new release of Std++ might be a while, could we apply your "dirty patch" to make stdpp-1.8.0 work on 8.18 in opam? Do you have a link to the patch maybe? (For some reason, I get 500 error on Debian's Salsa VCS)

view this post on Zulip Julien Puydt (Oct 02 2023 at 16:15):

Indeed salsa.d.o is having issues today ; my very very dirty patch is:

--- coq-stdpp.orig/stdpp/base.v
+++ coq-stdpp/stdpp/base.v
@@ -696,9 +696,7 @@
 (** The Coq standard library swapped the names of curry/uncurry, see
 FIXME: Remove this workaround once the lowest Coq version we support is 8.13. *)
-Notation curry := prod_uncurry.
 Global Instance: Params (@curry) 3 := {}.
-Notation uncurry := prod_curry.
 Global Instance: Params (@uncurry) 3 := {}.

 Definition uncurry3 {A B C D} (f : A  B  C  D) (p : A * B * C) : D :=

Last updated: Jun 18 2024 at 22:01 UTC