Stream: math-comp devs

Topic: 1.15.0 on 8.17+rc1


view this post on Zulip Karl Palmskog (Jan 04 2023 at 08:38):

1.15.0 is broken on 8.17+rc1. However, it's only because hint-without-locality was turned into an error. Is it maybe an option to add this patch in opam? Or will there be a new release?

diff --git a/mathcomp/algebra/Make b/mathcomp/algebra/Make
index 0d0629f..68ea194 100644
--- a/mathcomp/algebra/Make
+++ b/mathcomp/algebra/Make
@@ -26,3 +26,4 @@ zmodp.v
 -arg -w -arg +duplicate-clear
 -arg -w -arg -ambiguous-paths
 -arg -w -arg +undeclared-scope
+-arg -w -arg -deprecated-hint-without-locality
diff --git a/mathcomp/ssreflect/Make b/mathcomp/ssreflect/Make
index 9f71f55..9174856 100644
--- a/mathcomp/ssreflect/Make
+++ b/mathcomp/ssreflect/Make
@@ -32,3 +32,4 @@ order.v
 -arg -w -arg -ambiguous-paths
 -arg -w -arg +undeclared-scope
 -arg -w -arg -non-reversible-notation
+-arg -w -arg -deprecated-hint-without-locality

view this post on Zulip Théo Zimmermann (Jan 04 2023 at 08:43):

Isn't it bad practice anyway to make warnings fatal in an opam package?

view this post on Zulip Karl Palmskog (Jan 04 2023 at 08:45):

ah, to be specific: Coq 8.17 itself turned the deprecated-hint-without-locality warning into a fatal error

view this post on Zulip Pierre Roux (Jan 04 2023 at 08:46):

This is known and a new release is planned

view this post on Zulip Karl Palmskog (Jan 04 2023 at 08:46):

I think we discussed this elsewhere, but my terminology may be off. In 8.16 and before, deprecated-hint-without-locality just gave a regular warning and didn't error.

view this post on Zulip Théo Zimmermann (Jan 04 2023 at 08:49):

Karl Palmskog said:

ah, to be specific: Coq 8.17 itself turned the deprecated-hint-without-locality warning into a fatal error

Ah, right!


Last updated: May 18 2024 at 08:40 UTC