Stream: MetaCoq

Topic: MetaCoq on 32-bit OCaml


view this post on Zulip Karl Palmskog (Dec 07 2023 at 15:39):

Just FYI, apparently MetaCoq can't be compiled at all on 32-bit platforms:

File "gen-src/mCUint63.ml", line 104, characters 10-28:
(x lxor 0x4000000000000000) < (y lxor 0x4000000000000000)
          ^^^^^^^^^^^^^^^^^^
Error: Integer literal exceeds the range of representable integers of type int

Maybe this should be flagged up somewhere, if it's not easy to fix?

view this post on Zulip Michael Soegtrop (Dec 07 2023 at 15:40):

Up to the Coq Platform release for 8.17, MetaCoq did build on 32 bit Windows. It stopped now to do so. Since Windows 32 is phasing out I consider this as benign. We still supported it because it was quite a bit faster than 64 bit Windows, but I guess most people who need speed and don't like Linux are on Apple silicon meanwhile. So unless you say you want me to report such issues, I won't.

view this post on Zulip Michael Soegtrop (Dec 07 2023 at 15:41):

One should probably add this information to opam in case we officially drop 32 bit Windows support for MetaCoq.

view this post on Zulip Gaëtan Gilbert (Dec 07 2023 at 15:45):

Does that mean metacoq still works on 32 bit linux?

view this post on Zulip Karl Palmskog (Dec 07 2023 at 15:48):

that would be surprising, I don't think it's tested

view this post on Zulip Michael Soegtrop (Dec 08 2023 at 10:34):

@Gaëtan Gilbert : I expect it does not work on any 32 bit platform. The MetaCoq for 8.17 did compile on 32 Bit Windows (I had it in CI) and I expect also on 32 bit Linux (but I don't have this in CI).

view this post on Zulip Matthieu Sozeau (Dec 13 2023 at 12:57):

Indeed we should do the same as Coq to support native 63bit integers on 32 bits platforms


Last updated: Jul 23 2024 at 21:01 UTC