Stream: Coq Platform devs & users

Topic: Coq Platform and stack overflows


view this post on Zulip Paolo Giarrusso (Apr 18 2022 at 13:33):

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?

view this post on Zulip Paolo Giarrusso (Apr 18 2022 at 13:41):

But I'm not sure that's the only action. For instance, maybe there's an ocamlc bug.

view this post on Zulip Paolo Giarrusso (Apr 18 2022 at 14:05):

Oh, OCaml 4.14.0 (+flambda) fixes it!

view this post on Zulip Paolo Giarrusso (Apr 18 2022 at 14:08):

I suspect 4.14.0 fixed tail call elimination on ARM.

view this post on Zulip Paolo Giarrusso (Apr 18 2022 at 14:08):

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

view this post on Zulip Michael Soegtrop (Apr 19 2022 at 09:04):

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.

view this post on Zulip Théo Zimmermann (Apr 19 2022 at 09:07):

By the time of the next release, it could be the case that these packages can be made compatible.

view this post on Zulip Karl Palmskog (Apr 19 2022 at 09:07):

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.

view this post on Zulip Karl Palmskog (Apr 19 2022 at 09:09):

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

view this post on Zulip Michael Soegtrop (Apr 19 2022 at 09:14):

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

view this post on Zulip Karl Palmskog (Apr 19 2022 at 09:15):

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.

view this post on Zulip Michael Soegtrop (Apr 19 2022 at 09:15):

As I said, ARM is not officially supported, but "best effort".

view this post on Zulip Karl Palmskog (Apr 19 2022 at 09:17):

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.

view this post on Zulip Michael Soegtrop (Apr 19 2022 at 09:19):

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.

view this post on Zulip Théo Zimmermann (Apr 19 2022 at 09:21):

Agreed. That being said, it's simpler if we can manage to use 4.14.0 for all operating systems.

view this post on Zulip Théo Zimmermann (Apr 19 2022 at 09:21):

Which could be a realistic target for the next release.

view this post on Zulip Karl Palmskog (Apr 19 2022 at 09:23):

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

view this post on Zulip Michael Soegtrop (Apr 19 2022 at 09:23):

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.

view this post on Zulip Karl Palmskog (Apr 19 2022 at 09:25):

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)

view this post on Zulip Karl Palmskog (Apr 19 2022 at 09:26):

with that said, any ARM runner is probably a good thing

view this post on Zulip Michael Soegtrop (Apr 19 2022 at 09:42):

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.

view this post on Zulip Paolo Giarrusso (Apr 19 2022 at 10:13):

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.

view this post on Zulip Michael Soegtrop (Apr 19 2022 at 15:43):

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

view this post on Zulip Michael Soegtrop (Apr 19 2022 at 15:43):

Last time I looked on Github when they want to support it the answer was "unknown".

view this post on Zulip Michael Soegtrop (Apr 19 2022 at 15:46):

See (https://github.com/actions/virtual-environments/issues/2187) - it is still "no ETA".

view this post on Zulip Paolo Giarrusso (Apr 19 2022 at 16:50):

@Karl Palmskog on Apple Silicon, using Docker will give you a mostly-normal Linux ARM VM

view this post on Zulip Karl Palmskog (Apr 19 2022 at 18:08):

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

view this post on Zulip Karl Palmskog (Apr 19 2022 at 18:11):

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.

view this post on Zulip Michael Soegtrop (Apr 19 2022 at 18:17):

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

view this post on Zulip Karl Palmskog (Apr 19 2022 at 18:18):

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

view this post on Zulip Karl Palmskog (Apr 19 2022 at 18:23):

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:

view this post on Zulip Paolo Giarrusso (Apr 19 2022 at 18:47):

macOS on x64 has binary installers today, so I’d have expected tier 1 there?

view this post on Zulip Paolo Giarrusso (Apr 19 2022 at 18:50):

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.

view this post on Zulip Karl Palmskog (Apr 19 2022 at 18:58):

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?

view this post on Zulip Michael Soegtrop (Apr 20 2022 at 07:23):

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.

view this post on Zulip Michael Soegtrop (Apr 20 2022 at 07:24):

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