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
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.
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))
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.
It is just for testing, I did add these with an Emacs macro
and to get an idea of how much code was impacted
Last updated: Dec 05 2023 at 11:01 UTC