Stream: Coq devs & plugin devs

Topic: 32 bit broken

Gaëtan Gilbert (Nov 21 2022 at 12:38):

What are we doing about this?

Michael Soegtrop (Nov 21 2022 at 12:42):

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.

Gaëtan Gilbert (Nov 21 2022 at 12:43):

https://github.com/coq/coq/pull/14519#issuecomment-1319279001

Pierre-Marie Pédrot (Nov 21 2022 at 12:46):

it was probably broken by https://github.com/coq/coq/pull/14519

Pierre-Marie Pédrot (Nov 21 2022 at 12:46):

shouldn't we just revert this PR?

Pierre-Marie Pédrot (Nov 21 2022 at 12:47):

I'm wondering about the original motivations for this. cc @Emilio Jesús Gallego Arias @Guillaume Melquiond

Jason Gross (Nov 21 2022 at 17:37):

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

Michael Soegtrop (Nov 22 2022 at 08:53):

Is it understood why this breaks the 32 bit build? The changes don't seem to be directly connected to 32 vs 64 bit.

Emilio Jesús Gallego Arias (Nov 22 2022 at 10:29):

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.

Théo Zimmermann (Nov 22 2022 at 11:02):

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.

Pierre-Marie Pédrot (Nov 22 2022 at 12:40):

It should be reverted at least for the 8.17 branch, except if we have a quick fix.

Théo Zimmermann (Nov 22 2022 at 13:18):

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.

Jason Gross (Nov 22 2022 at 21:38):

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:

• OCaml does a bunch of system-specific configuration to determine what flags need to be passed to the C compiler to compile the OCaml compiler. This is things like: if the compiler is an old gcc, pass -std=gnu99 to get access to some loop constructs. It also includes things like "always pass -O2"
• There's not much separation between options like -O2 that are general and not strictly required and are for doing nice things, and options like -std=gnu99 which 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
• Some of our C code is similar to some of the OCaml compiler code, and needs some of the same possibly-platform-and-compiler-dependent flags.
• Either we can replicate all the logic that the OCaml compiler is doing to determine what options we should be passing to what compilers on what platforms (tweaking it for our needs), or we can assume that OCaml picks mostly reasonable flags and simply tweak the ones we want to tweak (such as removing -O2 in favor of something else if we want to).
• The existing PR tried to do the former without including any compiler-/platform- specific flag logic. This obviously breaks the build on any compilers (old gcc) or platforms (32-bit) which require flags other than the ones picked by default. Plausibly there's some set of flags that will generate the right behavior across all platforms and all compilers, but it's not clear to me a priori why we should expect to be able to avoid platform-/compiler- specific logic.

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

Jason Gross (Nov 22 2022 at 21:39):

(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.)

Gaëtan Gilbert (Nov 23 2022 at 11:45):

https://github.com/coq/coq/pull/16885

Pierre-Marie Pédrot (Nov 23 2022 at 11:58):

should we merge this asap? I'm really getting tired of having a broken ci.

Last updated: Oct 13 2024 at 01:02 UTC