Karl Palmskog (Jan 04 2023 at 08:38): 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
Isn't it bad practice anyway to make warnings fatal in an opam package?
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
Pierre Roux (Jan 04 2023 at 08:46):This is known and a new release is planned
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.
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-localitywarning into a fatal error
Ah, right!
Last updated: Apr 20 2024 at 09:01 UTC