Maxime Dénès (Mar 18 2022 at 12:56): 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
Gaëtan Gilbert (Mar 18 2022 at 13:02):can we see the CI run?
Ali Caglayan (Mar 18 2022 at 13:11):This one right? https://gitlab.com/coq/coq/-/pipelines/495573563
Ali Caglayan (Mar 18 2022 at 13:11):Those look like warning 16s to me
Ali Caglayan (Mar 18 2022 at 13:11):You have some optional args somewhere
Ali Caglayan (Mar 18 2022 at 13:11):You probably need to thunk those
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
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 ().
Ali Caglayan (Mar 18 2022 at 13:16):This is of course we are actually talking about the pipeline I linked
Ali Caglayan (Mar 18 2022 at 13:20):I see you in fact removed a lot of thunks
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.
Ali Caglayan (Mar 18 2022 at 13:22):Doesn't look like warning 40 is the culprit
Maxime Dénès (Mar 18 2022 at 13:39):Yeah the two warnings behave the same
Maxime Dénès (Mar 18 2022 at 13:39):My question is not about the warnings, though
Maxime Dénès (Mar 18 2022 at 13:39):It is about why they are not fatal
Ali Caglayan (Mar 18 2022 at 13:40):Warning 16 is newer and seems to be only fatal around 4.12
Maxime Dénès (Mar 18 2022 at 13:40):That's why I picked warning 40
Ali Caglayan (Mar 18 2022 at 13:40):That is done in the dune file
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.
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)))
Or is what I observe a combination of:
Maxime Dénès (Mar 18 2022 at 13:42):I guess that's it
Maxime Dénès (Mar 18 2022 at 13:43):Although https://gitlab.com/coq/coq/-/jobs/2221116439 fails and is OCaml 4.05
Ali Caglayan (Mar 18 2022 at 13:45):But that is a different warning
Ali Caglayan (Mar 18 2022 at 13:45):Warning 3: deprecated: module Vernacstate.Declare
Ali Caglayan (Mar 18 2022 at 13:45):At no point do I see 40 being fatal
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
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)
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.
Maxime Dénès (Mar 18 2022 at 13:51):I can try to update it, which version would be recommended?
Ali Caglayan (Mar 18 2022 at 13:54):I'm using 4.12.1+flambda
Ali Caglayan (Mar 18 2022 at 13:55):I only started seeing 16 as fatal in 4.12
Ali Caglayan (Mar 18 2022 at 13:55):Edge in CI is testing 4.13
Ali Caglayan (Mar 18 2022 at 13:58):Looks like nix file in the repo is pulling OCaml 4.09
Ali Caglayan (Mar 18 2022 at 13:59):Warning 16 definitely seems like a 4.12 thing: https://github.com/ocaml/ocaml/pull/9783
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
Ali Caglayan (Mar 18 2022 at 14:01):Bumping the nix file in general might have some caveats tho
Ali Caglayan (Mar 18 2022 at 14:01):https://github.com/coq/coq/issues/14260
Maxime Dénès (Mar 18 2022 at 14:02):is there a TL;DR somewhere? ^^
Ali Caglayan (Mar 18 2022 at 14:03):Yeah ocamldebug on newer versions = broken
Ali Caglayan (Mar 18 2022 at 14:03):But I have been developing with ocaml 4.12 fine
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
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.
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
Gaëtan Gilbert (Mar 18 2022 at 14:10):you can't have the same setup as CI because CI has multiple setups
Maxime Dénès (Mar 18 2022 at 14:11):Let's say having the closest thing to the strictest of these setups
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.
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
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.
Ali Caglayan (Mar 18 2022 at 14:14):Currently we support 4.05-4.13?
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
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)
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.
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
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
Emilio Jesús Gallego Arias (Mar 18 2022 at 14:31):but requires opam
Emilio Jesús Gallego Arias (Mar 18 2022 at 14:32):A modified version of it, with only 4.05 and 4.12
Gaëtan Gilbert (Mar 18 2022 at 14:41):see also https://github.com/coq/coq/pull/15827
Notification Bot (Mar 23 2022 at 09:05):Maxime Dénès has marked this topic as resolved.
Last updated: Apr 20 2024 at 02:40 UTC