Installing the latest platform ran into a stack overflow running Coq (https://github.com/HoTT/HoTT/issues/1643). I guess the platform should increase stack size during the build?
But I'm not sure that's the only action. For instance, maybe there's an ocamlc bug.
Oh, OCaml 4.14.0 (+flambda) fixes it!
I suspect 4.14.0 fixed tail call elimination on ARM.
In that case, the stack overflow was on some code that ought to be tail recursive, and coqc used much less stack on x86. Here, with the fix the code uses much less stack (and if I shrink the stack enough to cause an overflow, it's elsewhere).
So I guess you are suggesting to choose 4.14.0 for ARM? Afair this is not compatible with some packages, so these would have to be dropped then.
By the time of the next release, it could be the case that these packages can be made compatible.
does it really make sense to drop packages? Ideally, we would work with the authors of packages that don't support 4.14 to fix issues there...
Might make sense that a few weeks before Platform release, a call is made on the OCaml version to use, based on supporting maximum number of Platform packages (ideally all). To help Platform package maintainers, we could mention a "target" OCaml version in the Platform GitHub release issues which they should ideally adapt to.
the main problem with 4.14 right now in my view is that we don't even have Docker images with 4.14, so Platform packages have no easy way of doing CI on it: https://hub.docker.com/r/coqorg/coq/tags
@Karl Palmskog : the idea was to drop the packages on ARM only, and also to use 4.14.0 on ARM only. ARM is not (yet) officiall supported by Coq Platform exactly cause of issues like this. But I try to support it as much as possible without impeding the platforms which are officially supported.
is it really a good idea to use different OCaml compilers across platforms for the same Platform release? I understand the appeal, but it means we don't really give the same environment, and issue reproducibility will likely be difficult.
As I said, ARM is not officially supported, but "best effort".
OK, sure, but as a Platform package maintainer I don't even know if my packages compile, much less run on 4.14. I think you need some big warning message so as not let the ARM experience reflect on package maintainers.
Well it says clearly in the release notes that it is not supported and that we try our best.
I guess one could add a warning page in the install scripts.
I don't see how I could officially support it without support for ARM in CI.
Agreed. That being said, it's simpler if we can manage to use 4.14.0 for all operating systems.
Which could be a realistic target for the next release.
given what is said about OCaml versions in the Docker-Coq wiki, I think Docker support for 4.14 will be forthcoming (cc: @Erik Martin-Dorel)
Each Coq version will be prebuilt with:
The last two compatible OCaml versions
This depends on if the next release is 2022.04.1 or 2022.09. I expect a 2022.04.1 cause of the current inconsistencies.
I also expect that ARM stuff is much more stable in 6 months, but I am not sure there will be GitHub support for it. I guess we could have our own runners, though.
can one really be sure that ARM-on-Apple-silicon and ARM-not-on-Apple-silicon behaves the same? For example, people may run Coq on Raspberry Pi or similar (I did the latter a couple of years ago to deploy an extracted program)
with that said, any ARM runner is probably a good thing
I don't think from a cost and effort point of view it makes much of a difference if it is a Mac-Mini or Raspberry - I can't tell what would be easier to maintain for INRIA.
But it would definitely be a good thing to have such a runner soon. From what I hear the Apple ARM silicon is quite fast for Coq and it might soon be a big problem in lectures to not support it - and as I said without CI I can't support it.
I agree it's still a bit early for 4.14.0, my idea was to rely on
ulimit for now. But it seems promising, especially with Coq 8.16.0 findlib support.
@Maxime Dénès @Enrico Tassi : any chances to get an Apple Silicon CI runner hosted by INRIA IT within 3 months?
IMHO the ARM support is meanwhile quite reasonable and as I said above I see real issues for teaching Coq if we don't fully support this.
Last time I looked on Github when they want to support it the answer was "unknown".
See (https://github.com/actions/virtual-environments/issues/2187) - it is still "no ETA".
@Karl Palmskog on Apple Silicon, using Docker will give you a mostly-normal Linux ARM VM
what I meant is that the implementation of the ARM ISA might be different by Apple, and that therefore Coq issues might not be reproducible on "other ARM"[-implementing silicon], regardless of whether you run the same OS/VM
in contrast to RISC-V [which has the Sail stuff], there is to my knowledge no publicly available "golden formal model" of any ARM ISA, so it's not even possible in principle to show same behavior across different silicon. x64 and friends at least have the advantage that "everyone" is using it for whatever, and most people are either using Intel or AMD silicon.
@Karl Palmskog : yes, makes sense - although I would think ARM is further down the road in terms of formal specification of the ISA than Intel.
Anyway - with Coq Platform we should concentrate on main stream personal computers. If someone wants to run Coq on Raspberry fine, but (s)he should run the test suite then on the specific platform. I see this way beyond the scope of Coq Platform.
OK sure, I can buy that, but then we can be specific about that the Platform supports "ARM by Apple", and other ARM is on best effort basis
so in my view the tier 1 platforms would be:
And tier 2 [not directly tested in Platform CI] is something like:
And tier 3/best effort:
macOS on x64 has binary installers today, so I’d have expected tier 1 there?
re formal models, sail supports ARM as well https://github.com/rems-project/sail-arm/tree/master/arm-v8.5-a — but I haven’t studied it myself. I agree that there can be differences — just like between Intel and AMD, extensions exist.
sure, everyone and their brother has come up with formal ISA models in ITPs (I counted 10+ just the last few years). The difference with Sail+RISCV is that the RISCV consortium declared Sail some form of winner.
OK, so I guess macOS x64 is tier 1, but will probably be demoted in the not-too-distant future. And I guess we only do Win 10 at the moment?
The Windows version shouldn't make any difference. It is not tested, but I haven't heard anything that it doesn't work and I am not aware that we are using any APIs which are different on any still supported Windows.
And Indeed I would say that for the time being x64 bases Macs are much more common than ARM Macs.
Last updated: Jan 30 2023 at 12:03 UTC