Stream: Coq devs & plugin devs

Topic: OCaml warnings 67 and 69

Emilio Jesús Gallego Arias (Jul 03 2023 at 19:16):

Hi folks, these impact Coq massively (cc https://github.com/coq/coq/pull/17808 ), what should we do with them?

67 seems mostly bogus, however I'm wondering about 69

Emilio Jesús Gallego Arias (Jul 03 2023 at 19:17):

Note that in the current build they are disabled by Dune (as to ensure forward stability), but once you bump the (lang dune ...) version they are added to the default set, so a decision needs to be taken.

Emilio Jesús Gallego Arias (Jul 03 2023 at 19:18):

This works in order to see the effect:

diff --git a/dune b/dune
index 0e3b24fea3..44918ab444 100644
--- a/dune
+++ b/dune
@@ -1,6 +1,6 @@
 ; Default flags for all Coq libraries.
 (env
- (dev     (flags :standard -w -9-27@60@70 \ -short-paths)
+ (dev     (flags :standard -w -9-27@60@70+67+69 \ -short-paths)
           (coq (flags :standard -w +default)))
  (release (flags :standard)
           (ocamlopt_flags :standard -O3 -unbox-closures))

Emilio Jesús Gallego Arias (Jul 03 2023 at 19:18):

then do make check

Gaëtan Gilbert (Jul 03 2023 at 19:52):

69 unused-field looks pretty legitimate IMO, we need to deactivate it when we do obj magic trickery but the other cases indeed look like dead code
67 unused functor parameter is a bit unfortunate as it seems legitimate in implementations but more annoying in signatures

I think globally disabling 67 is fine, I guess the alternative is to do module Make (_ : T) : OtherT instead of module Make (X : T) : OtherT. Locally disabling feels worse than either of those options.

For 69 we can globally disable to upgrade the dune lang, or we can fix the correct ones and locally disable the rest with a comment. However I don't like the way you did it in the PR where even the correct ones are locally disabled (if it's just for testing it's fine but not for merging), it makes it harder to fix them once we're ready to do it.

Emilio Jesús Gallego Arias (Jul 03 2023 at 19:56):

It is just for testing, I did add these with an Emacs macro

Emilio Jesús Gallego Arias (Jul 03 2023 at 19:57):

and to get an idea of how much code was impacted

Last updated: Dec 05 2023 at 11:01 UTC