Stream: Coq devs & plugin devs

Topic: 32 bit broken


view this post on Zulip Gaëtan Gilbert (Nov 21 2022 at 12:38):

What are we doing about this?

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Nov 21 2022 at 12:43):

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

view this post on Zulip Pierre-Marie Pédrot (Nov 21 2022 at 12:46):

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

view this post on Zulip Pierre-Marie Pédrot (Nov 21 2022 at 12:46):

shouldn't we just revert this PR?

view this post on Zulip 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

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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:

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

view this post on Zulip 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.)

view this post on Zulip Gaëtan Gilbert (Nov 23 2022 at 11:45):

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

view this post on Zulip 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: Feb 01 2023 at 16:03 UTC