What are we doing about this?
Can you be more specific? The Coq Platform 32 bit Windows build did run through last night, but this on 8.16 and 8.15, not dev.
it was probably broken by https://github.com/coq/coq/pull/14519
shouldn't we just revert this PR?
I'm wondering about the original motivations for this. cc @Emilio Jesús Gallego Arias @Guillaume Melquiond
According to the comment:
Flags -fno-strict-aliasing and -fwrapv do not make sense for Coq and having them just pessimize the generated code. As for -O2, we want to have control over it, which is why it is part of config/dune.c_flags.
It seems to me like we should invert the logic, removing specifically the flags we want control over while leaving the rest. Note that the same PR also broke the build on old gcc by removing OCaml's -std=gnu99. (Dune and OCaml do useful compiler-specific customization of flags, it seems like we shouldn't remove that in general.)
Is it understood why this breaks the 32 bit build? The changes don't seem to be directly connected to 32 vs 64 bit.
Pierre-Marie the original motivation for the PR was because dune started to warn us that we needed to do
(flags :standard ....) if we wanted to include flags from OCaml. This is what I did first, but then Guillaume suggested to try to use a more low-level configuration for this. Myself I am not expert on C flags, happy to help with the build part.
Looking at the discussion, it looks like nobody is perfectly understanding what's going on. Given that this is the likely culprit for the 32 build failure, my opinion is that we should just revert it and figure this out later.
It should be reverted at least for the 8.17 branch, except if we have a quick fix.
Yes, I will do it if nothing happens. But IMHO, if we do not have a quick fix, then it should reverted even in master.
Looking at the discussion, it looks like nobody is perfectly understanding what's going on.
This is not a perfect understanding, but I think it's most of the understanding:
-std=gnu99to get access to some loop constructs. It also includes things like "always pass
-O2that are general and not strictly required and are for doing nice things, and options like
-std=gnu99which are mandatory to handle some constructs like
for (int i = ...)at all, but only on some compilers.
dune(optionally) exposes the options that OCaml has decided should be passed to the C compiler
-O2in favor of something else if we want to).
The quick fix is to invert the logic in the current PR. There were a couple of flags that were deliberately removed by that PR; we should put back
:standard and explicitly remove the flags we want to remove.
IMO, finding the right whitelist of flags that is uniform across all compilers can wait for a future PR, if it's even desirable. (And such a PR should be much more heavily tested than the standard PR. AIUI, the current PR was merged without realizing that dune/OCaml was doing any platform-/compiler- specific logic.)
(The bit of understanding that is not present there is which particular flags are required on 32-bit which are not required on 64-bit.)
should we merge this asap? I'm really getting tired of having a broken ci.
Last updated: Dec 01 2023 at 06:01 UTC