Karl Palmskog (Dec 07 2023 at 15:39): 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?
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.
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.
Gaëtan Gilbert (Dec 07 2023 at 15:45):Does that mean metacoq still works on 32 bit linux?
Karl Palmskog (Dec 07 2023 at 15:48):that would be surprising, I don't think it's tested
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).
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: Oct 13 2024 at 01:02 UTC