Stream: Coq devs & plugin devs

Topic: ✔ Non fatal warning in default target


view this post on Zulip Maxime Dénès (Mar 18 2022 at 12:56):

Hi ! I have a local branch which emits some warning 40 occurrences. However, when I build it with dune build, it does not fail. If I push the exact same branch to Coq's repo, the CI fails (because the warning is considered fatal). My dune local conf doesn't seem to contain anything fancy. Does this ring a bell to anybody before I start minimizing / reproducing?

I use the Coq nix setup : Dune 2.9.1 & Ocaml 4.09.1

view this post on Zulip Gaëtan Gilbert (Mar 18 2022 at 13:02):

can we see the CI run?

view this post on Zulip Ali Caglayan (Mar 18 2022 at 13:11):

This one right? https://gitlab.com/coq/coq/-/pipelines/495573563

view this post on Zulip Ali Caglayan (Mar 18 2022 at 13:11):

Those look like warning 16s to me

view this post on Zulip Ali Caglayan (Mar 18 2022 at 13:11):

You have some optional args somewhere

view this post on Zulip Ali Caglayan (Mar 18 2022 at 13:11):

You probably need to thunk those

view this post on Zulip Gaëtan Gilbert (Mar 18 2022 at 13:13):

on my machine I can reproduce warning 40 being non-error
btw I maintain that this warning is more trouble than it's worth -which is 0) and we should turn it off

view this post on Zulip Ali Caglayan (Mar 18 2022 at 13:15):

i.e. OCaml isn't happy with f ?a ?b ~c since it is ambiguous when passed out of order. You need to add a thunk and do f ?a ?b ~c ().

view this post on Zulip Ali Caglayan (Mar 18 2022 at 13:16):

This is of course we are actually talking about the pipeline I linked

view this post on Zulip Ali Caglayan (Mar 18 2022 at 13:20):

I see you in fact removed a lot of thunks

view this post on Zulip Ali Caglayan (Mar 18 2022 at 13:22):

I seem to recall that warning appearing in OCaml 4.12 but not in 4.10 which explains why base is completely fine.

view this post on Zulip Ali Caglayan (Mar 18 2022 at 13:22):

Doesn't look like warning 40 is the culprit

view this post on Zulip Maxime Dénès (Mar 18 2022 at 13:39):

Yeah the two warnings behave the same

view this post on Zulip Maxime Dénès (Mar 18 2022 at 13:39):

My question is not about the warnings, though

view this post on Zulip Maxime Dénès (Mar 18 2022 at 13:39):

It is about why they are not fatal

view this post on Zulip Ali Caglayan (Mar 18 2022 at 13:40):

Warning 16 is newer and seems to be only fatal around 4.12

view this post on Zulip Maxime Dénès (Mar 18 2022 at 13:40):

That's why I picked warning 40

view this post on Zulip Ali Caglayan (Mar 18 2022 at 13:40):

That is done in the dune file

view this post on Zulip Maxime Dénès (Mar 18 2022 at 13:41):

Gaëtan Gilbert said:

on my machine I can reproduce warning 40 being non-error
btw I maintain that this warning is more trouble than it's worth -which is 0) and we should turn it off

So there's a bug somewhere I guess.

view this post on Zulip Ali Caglayan (Mar 18 2022 at 13:41):

(env
 (dev     (flags :standard -rectypes -w -9-27+40+60-70 \ -short-paths))
 (release (flags :standard -rectypes)
          (ocamlopt_flags :standard -O3 -unbox-closures))
 (ireport (flags :standard -rectypes -w -9-27-40+60-70)
          (ocamlopt_flags :standard -O3 -unbox-closures -inlining-report)))

view this post on Zulip Maxime Dénès (Mar 18 2022 at 13:42):

Or is what I observe a combination of:

view this post on Zulip Maxime Dénès (Mar 18 2022 at 13:42):

I guess that's it

view this post on Zulip Maxime Dénès (Mar 18 2022 at 13:43):

Although https://gitlab.com/coq/coq/-/jobs/2221116439 fails and is OCaml 4.05

view this post on Zulip Ali Caglayan (Mar 18 2022 at 13:45):

But that is a different warning

view this post on Zulip Ali Caglayan (Mar 18 2022 at 13:45):

Warning 3: deprecated: module Vernacstate.Declare

view this post on Zulip Ali Caglayan (Mar 18 2022 at 13:45):

At no point do I see 40 being fatal

view this post on Zulip Enrico Tassi (Mar 18 2022 at 13:46):

About that deprecated module, the commit I did disabled the warning in my UI (with 4.09) but I was not very convinced of why it did disable it

view this post on Zulip Maxime Dénès (Mar 18 2022 at 13:50):

Ali Caglayan said:

At no point do I see 40 being fatal

Indeed, I just got confused when reading the dune file (I saw +40)

view this post on Zulip Maxime Dénès (Mar 18 2022 at 13:51):

So I guess the root of my problem is that the Coq Nix dev setup ships an OCaml version that is too old.

view this post on Zulip Maxime Dénès (Mar 18 2022 at 13:51):

I can try to update it, which version would be recommended?

view this post on Zulip Ali Caglayan (Mar 18 2022 at 13:54):

I'm using 4.12.1+flambda

view this post on Zulip Ali Caglayan (Mar 18 2022 at 13:55):

I only started seeing 16 as fatal in 4.12

view this post on Zulip Ali Caglayan (Mar 18 2022 at 13:55):

Edge in CI is testing 4.13

view this post on Zulip Ali Caglayan (Mar 18 2022 at 13:58):

Looks like nix file in the repo is pulling OCaml 4.09

view this post on Zulip Ali Caglayan (Mar 18 2022 at 13:59):

Warning 16 definitely seems like a 4.12 thing: https://github.com/ocaml/ocaml/pull/9783

view this post on Zulip Maxime Dénès (Mar 18 2022 at 13:59):

Thanks for the feedback guys, I'll test and open a PR bumping the nix dev setup to OCaml 4.12

view this post on Zulip Ali Caglayan (Mar 18 2022 at 14:01):

Bumping the nix file in general might have some caveats tho

view this post on Zulip Ali Caglayan (Mar 18 2022 at 14:01):

https://github.com/coq/coq/issues/14260

view this post on Zulip Maxime Dénès (Mar 18 2022 at 14:02):

is there a TL;DR somewhere? ^^

view this post on Zulip Ali Caglayan (Mar 18 2022 at 14:03):

Yeah ocamldebug on newer versions = broken

view this post on Zulip Ali Caglayan (Mar 18 2022 at 14:03):

But I have been developing with ocaml 4.12 fine

view this post on Zulip Maxime Dénès (Mar 18 2022 at 14:04):

What we update in Nix is just the default value, developers can always pick 4.09 instead of they need ocamldebug

view this post on Zulip Maxime Dénès (Mar 18 2022 at 14:05):

Not having the same build setup by default as the CI is more problematic IMHO. And I'm also an ocamldebug user.

view this post on Zulip Ali Caglayan (Mar 18 2022 at 14:09):

btw I shouldn't be too pessimistic about ocamldebug, @Gaëtan Gilbert knows how to get it working, but I am not sure on which version

view this post on Zulip Gaëtan Gilbert (Mar 18 2022 at 14:10):

you can't have the same setup as CI because CI has multiple setups

view this post on Zulip Maxime Dénès (Mar 18 2022 at 14:11):

Let's say having the closest thing to the strictest of these setups

view this post on Zulip Maxime Dénès (Mar 18 2022 at 14:12):

Early feedback is always better than late surprises when you develop. It reduces context switch.

view this post on Zulip Gaëtan Gilbert (Mar 18 2022 at 14:12):

there is no strictest
eg if you use newer ocaml you see deprecated warnings on old apis but no error on new apis

view this post on Zulip Ali Caglayan (Mar 18 2022 at 14:13):

I think the best solution is to use a newer OCaml and keep in mind fancy fings like monadic lets are not supported until 4.08.

view this post on Zulip Ali Caglayan (Mar 18 2022 at 14:14):

Currently we support 4.05-4.13?

view this post on Zulip Gaëtan Gilbert (Mar 18 2022 at 14:14):

I use 4.09 as it's the last version with working ocamldebug
when 4.14 is out and elpi moves on from camlp5 I'll update

view this post on Zulip Emilio Jesús Gallego Arias (Mar 18 2022 at 14:29):

That's something that indeed needs improvement, dune allows to associate different flags to different compilers but that only works with opam I think (as of today)

view this post on Zulip Maxime Dénès (Mar 18 2022 at 14:30):

Bumping the OCaml version in the Nix setup should be a reasonable approximation of what I'd like to get.

view this post on Zulip Maxime Dénès (Mar 18 2022 at 14:30):

I'll have to be aware when I use very recent OCaml APIs but that's better than not seeing fatal warnings

view this post on Zulip Emilio Jesús Gallego Arias (Mar 18 2022 at 14:31):

At some point I used dev/dune-workspace.all for that purpose, dune build @check works pretty well for that

view this post on Zulip Emilio Jesús Gallego Arias (Mar 18 2022 at 14:31):

but requires opam

view this post on Zulip Emilio Jesús Gallego Arias (Mar 18 2022 at 14:32):

A modified version of it, with only 4.05 and 4.12

view this post on Zulip Gaëtan Gilbert (Mar 18 2022 at 14:41):

see also https://github.com/coq/coq/pull/15827

view this post on Zulip Notification Bot (Mar 23 2022 at 09:05):

Maxime Dénès has marked this topic as resolved.


Last updated: Feb 02 2023 at 13:03 UTC