There was recently a message on the cygwin mailing list, that support for 32 bit will be discontinued. In principle one can also install the 32 bit MinGW toolchain on a 64 bit cygwin, it is quite tricky though because Windows has the property that the contents of system DLLs depend on if a 32 bit or 64 bit process looks at it. So a 64 bit MinGW 32 linker would see the 64 bit DLLs and go wild. One can get around this by copying the DLLs with a 32 bit copy program somewhere else ... it is a bit messy.
In short: what do you think? Should we discontinue the 32 bit version of Coq?
Some people say that the 32 bit version is faster, because Coq is mostly pointers and these need less cache in 32 bit, but in CI the difference doesn't look significant.
I believe @Andrew Appel has been a proponent of 32-bit Coq (for the performance reasons stated by Michael), maybe we want to get his opinion on discontinuing it.
Would also be interesting to know what it actually requires on, say, Linux side of things to get 32 bit. Could be worth to keep 32 bit as a niche experimental thing on Linux without any official support.
Note that, sooner or later, the OCaml developers will make the choice for us, as discontinuing OCaml for x86-32 is on the drawing board.
At least for Linux there is a "mixed" architecture called x32 IIRC (which is 32 bits pointers but 64bits instructions/registers). OCaml has a patch for this one around. @Guillaume Melquiond do you know what they think about that?
(x32 is really what Appel's use case needs IMO)
My understanding is that it is not worth the effort, especially with OCaml 5.0/Multicore needing lots of virtual memory to accommodate minor heaps. But I follow OCaml's development from very far away, so take my interpretation with a grain of salt.
I suggest the reading of this thread, especially around the place where @Emilio Jesús Gallego Arias mentions the users of Coq who like the 32 bit version and the response of @Xavier Leroy to that. IMHO if @Xavier Leroy wishes to drop 32 bit OCaml (despite his proximity with @Andrew Appel), I think we should follow suit: https://discuss.ocaml.org/t/jane-street-packages-dropping-support-for-32-bit/8621
More precise link: https://discuss.ocaml.org/t/jane-street-packages-dropping-support-for-32-bit/8621/13
OK, then it seems really that the world is going to be a better place ;-)
I have already said, in other forums, that I don't expect that 32-bit Coq will be supported just for me if I'm the only user. But here are some things I believe:
For many years now I have been running a 64-bit operating system, 64-bit applications, and just 32-bit Coq for improved memory performance. It would not be a major problem for me to install 64-bit Coq instead.
if we actually start to advertise the x32 arch and provide it in Docker images and show the performance gains, I think we could convince a lot of users.
For sure, x32 would work fine on tens of projects in coq-community.
By the way, I think there are important applications of 32-bit architectures in embedded platforms. So it would be a shame if CompCert were to drop support for 32-bit architectures, because then we could not have verified compilation for those platforms (and also VST would have to drop 32-bit architecture support). But that's not at all the same question as "do we need to run Coq in 32-bit mode."
ah, then I think someone has to invest time in figuring out CompCert cross-compilation, because last time someone checked, Xavier said:
My advice is to not bother with cross-compilation and build only the version of CompCert that corresponds to the host platform.
just for the record, I think even the super-optimized Hotspot supports something x32-like — “compressed pointers”. With objects aligned to 8 bytes, the 3 low-order bits can be skipped, so you can support 32GB heaps with 32-bit pointers: https://www.baeldung.com/jvm-compressed-oops
of course shifting pointers at dereference has some (small) cost, but shifts could be pretty cheap when you’re stalled waiting for memory.
Andrew Appel said:
By the way, I think there are important applications of 32-bit architectures in embedded platforms.
I still have it on my ToDO list to add an Opam packages for 32 bit ARM CompCert+VST. As cross environment this should be independent of the OS. I don't think it will be a lot of effort to support it - afair from my discussion with Xavier on this last time the main issue he saw was with setting up the required cross linker in a reliable way - this shouldn't be much of an issue with opam and depext.
Regarding the speed ratio: I had a look at recent CI runs and indeed the 32 bit version seems to be about 30..40% faster, see e.g. (https://github.com/coq/platform/actions/runs/1413458927). The majority of the CI run time are Coq calls. Maybe the speed ratio reduced a bit in recent years because CPUs have larger and more advanced caches. Of course 30..40% is still substantial.
@Andrew Appel @Michael Soegtrop , it is good to hear this numbers, let's try to forward them to OCaml maintainers (cc @Xavier Leroy ) ; regarding Coq, I volunteer to maintain the 32-bit version as long of course as OCaml still does support 32 bits.
This should be a while, Coq would need to drop support for OCaml 4 at all.
A different issue is Cygwin of course, but maybe WSL can work here.
I am not a fan of WSL, because it requires a rather invasive hypervisor - much worse than VirtualBox & Co. If you use WSL, no other virtualization system will work any more. Also I have seen quite a few bad side effects of the hypervisor, say Windows blue screen core dumps are corrupted when you have WSL.
The Windows issue is solvable - worst case by archiving a 32 bit cygwin, but as I said one can get around the linker issues in 64/32 cross builds - I have done it before.
One note on the 32 vs 64 bit timing I gave: they are flawed because in 32 bit mode I don't compile Unimath - which needs more heap than possible in 32 bit OCaml. So I would have to run tests where this is rectified.
Last updated: Jan 30 2023 at 11:03 UTC