Stream: Coq devs & plugin devs

Topic: Building via coq_makefile running into missing-mli error


view this post on Zulip Li-yao (Sep 28 2021 at 19:41):

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?

view this post on Zulip Li-yao (Sep 28 2021 at 19:52):

Right now I've overridden the option by calling Makefile.coq with COQMF_WARN="-warn-error +a-3-70"...

view this post on Zulip Enrico Tassi (Sep 28 2021 at 19:53):

please open a bugreport (or a PR if you prefer) to make -70 be a default

view this post on Zulip Enrico Tassi (Sep 28 2021 at 19:57):

https://github.com/coq/coq/blob/98e1885d721da87c29fad6c03a48c4c1ec559693/lib/envars.ml#L180

view this post on Zulip Gaëtan Gilbert (Sep 28 2021 at 21:05):

is that the right place or should it be https://github.com/coq/coq/blob/98e1885d721da87c29fad6c03a48c4c1ec559693/tools/configure/configure.ml#L135

view this post on Zulip Gaëtan Gilbert (Sep 28 2021 at 21:05):

?

view this post on Zulip Gaëtan Gilbert (Sep 28 2021 at 21:07):

also there is nothing stopping you from having a mli next to a mlg

view this post on Zulip Li-yao (Sep 29 2021 at 01:39):

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.

view this post on Zulip Li-yao (Sep 29 2021 at 01:40):

Gaëtan Gilbert said:

also there is nothing stopping you from having a mli next to a mlg

I have an allergy to bureaucracy.

view this post on Zulip Enrico Tassi (Sep 29 2021 at 08:09):

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

view this post on Zulip Enrico Tassi (Sep 29 2021 at 08:10):

So I would be happy with a less nice but immediate fix ;-)

view this post on Zulip Guillaume Melquiond (Sep 29 2021 at 08:41):

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".

view this post on Zulip Enrico Tassi (Sep 29 2021 at 08:42):

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)

view this post on Zulip Gaëtan Gilbert (Sep 29 2021 at 09:41):

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)

view this post on Zulip Gaëtan Gilbert (Sep 29 2021 at 09:45):

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

view this post on Zulip Michael Soegtrop (Sep 29 2021 at 12:09):

@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.

view this post on Zulip Enrico Tassi (Sep 29 2021 at 12:13):

I think 4.13


Last updated: Feb 01 2023 at 16:03 UTC