The addition of the missing-mli warning in recent OCaml seems to break Coq projects that build plugins and that use coq_makefile (which enables the warning via -w +a
), because a .mlg
produces a .ml
file without an .mli
. What is a proper workaround, at least on the short-term?
Right now I've overridden the option by calling Makefile.coq
with COQMF_WARN="-warn-error +a-3-70"
...
please open a bugreport (or a PR if you prefer) to make -70 be a default
https://github.com/coq/coq/blob/98e1885d721da87c29fad6c03a48c4c1ec559693/lib/envars.ml#L180
is that the right place or should it be https://github.com/coq/coq/blob/98e1885d721da87c29fad6c03a48c4c1ec559693/tools/configure/configure.ml#L135
?
also there is nothing stopping you from having a mli next to a mlg
Gaëtan Gilbert said:
is that the right place or should it be https://github.com/coq/coq/blob/98e1885d721da87c29fad6c03a48c4c1ec559693/tools/configure/configure.ml#L135
envars.ml
, where -warn-error
is set, is the right one. configure.ml
sets -w
which is for the non-fatal messages.
Gaëtan Gilbert said:
also there is nothing stopping you from having a mli next to a mlg
I have an allergy to bureaucracy.
Maybe @Gaëtan Gilbert is right, the setting is there twice: https://github.com/coq/coq/blob/98e1885d721da87c29fad6c03a48c4c1ec559693/tools/configure/configure.ml#L138 , so the nice fix would be to unify them.
But here the problem is that it is a regression for coq-makefile users, even without upgrading Coq (just upgrading ocaml). IMO this issue should reach @Guillaume Melquiond and @Michael Soegtrop and be fixed in 8.14.0
So I would be happy with a less nice but immediate fix ;-)
What was the original rationale for -warn-error +a
? It seems like a severe footgun. In fact, even the OCaml documentation agrees: "it is not recommended to use the -warn-error option in production code".
well, it was added (to coq_makefile) to be on par with dune I guess. (no comment on the default, I've been already too vocal on this)
keep in mind that -warn-error +a
means error for enabled warnings, not all warnings
coq_makefile gets from configure the list of enabled warnings but not the warn-error, coq_makefile's warn-error is hardcoded in envars (it could be hardcoded directly in coqmakefile.in since it's constant)
the configure warnings are used by the test suite (for unit-tests and fake_ide, through CAMLFLAGS in config/Makefile) and by coq_makefile (through coq_config printed by envars)
the configure warn-error is used by the test suite (through CAMLFLAGS) and the old makefile when building coq (if prefs.warn_error then pass -w +default
to coqc, through COQWARNERROR in config/Makefile)
dune uses some unknown set of warnings (whatever dune's default is, in dev mode concatenated with -9-27+40+60
, in /kernel
in dev mode +a-4-44-50
)
note that dune autoconfig does not set warn-error, configure -profile devel does set warn-error (so no warn-error in production), and dune itself sets warn-error in dev mode (dev mode is a dune concept independent of configure -profile devel)
so a possible refactor is to hardcode warning sets directly in coqmakefile.in and test-suite/makefile (accepting the possibility that they diverge), there's no reason they should be in configure
note that we want warn-error in coq_makefile when running ci
@Enrico Tassi : thanks for CCing me. To which OCaml version does this apply? Coq Platform is currently on OCaml 4.10 and uses a fixed OCaml version, but of course there are users just using the opam packages.
I think 4.13
Last updated: Oct 13 2024 at 01:02 UTC