Stream: Coq Platform devs & users

Topic: Coq on Apple M1 (ARM64)


view this post on Zulip Michael Soegtrop (Dec 14 2020 at 17:40):

Some good news: I got a Mac with M1 (ARM64) processor and except for some minor hickups when installing opam (I had to remove the checksum test from the install script) it did compile OCaml 4.10.2 and Coq 8.12.1 fine. Some basic smoke tests of Coq did work well. So a Coq platform for Apple M1 might not be that far away. The main issue is the state of Homebrew and/or MacPorts.

view this post on Zulip Paolo Giarrusso (Dec 15 2020 at 12:43):

BTW, no pressure but looking forward to any benchmarks of Coq on M1 vs non-M1 :-)

view this post on Zulip Enrico Tassi (Dec 15 2020 at 12:55):

Especially the core temperature ;-)

view this post on Zulip Paolo Giarrusso (Dec 15 2020 at 12:58):

oh yeah, it'd be great to run Coq and typing comfortably without a leafblower fan

view this post on Zulip Michael Soegtrop (Dec 15 2020 at 13:19):

I will run some profiles against my MacBook with i9-9980HK. For the M1 I have a MacMini and fan activity during an "opam install coq" was pretty low (almost unaudible).

view this post on Zulip Michael Soegtrop (Dec 15 2020 at 13:29):

Btw.: Homebrew and MacPorts don't look good, so I have lillte hope to get CoqIDE compiled any time soon. I hope VSCoq is ready for use meanwhile and VSCode runs (didn't test as yet). For stuff like GMP, MPFR, ... I would create an opam from sources package, so that we could live without MacPorts and Homebrew for a while.

view this post on Zulip Paolo Giarrusso (Dec 15 2020 at 14:29):

I'd vote for an early release over waiting for everything (not that I count, I have no M1)

view this post on Zulip Paolo Giarrusso (Dec 15 2020 at 14:30):

Emacs exists and VsCoq is doing okay, though you probably want to give commit rights to Fabian

view this post on Zulip Paolo Giarrusso (Dec 15 2020 at 14:33):

(opened https://coq.zulipchat.com/#narrow/stream/237662-VsCoq-devs.20.26.20users/topic/Adding.20maintainers to explain that part better)

view this post on Zulip Michael Soegtrop (Dec 16 2020 at 10:25):

@Paolo Giarrusso : do you have something especially interesting to test? I thought about profiling building the part of the Coq platform which does build, but I am open to suggestions.

view this post on Zulip Paolo Giarrusso (Dec 16 2020 at 10:55):

not in particular

view this post on Zulip Paolo Giarrusso (Dec 16 2020 at 10:56):

so coq platform sounds great, especially if it already includes Iris

view this post on Zulip Paolo Giarrusso (Dec 16 2020 at 10:56):

uh, it doesn't! Can you also use the standard Coq benchmarks from the infrastructure? Those do include Iris and libraries using it

view this post on Zulip Enrico Tassi (Dec 16 2020 at 11:06):

I think iris deserves to be in the platform, but I see no issue here https://github.com/coq/platform/issues (putting the upstreams in CC and pointing them to the charter file)

view this post on Zulip Paolo Giarrusso (Dec 16 2020 at 11:10):

there's an issue since months

view this post on Zulip Paolo Giarrusso (Dec 16 2020 at 11:10):

not sure where

view this post on Zulip Paolo Giarrusso (Dec 16 2020 at 11:10):

https://github.com/coq/platform/issues/4

view this post on Zulip Michael Soegtrop (Dec 16 2020 at 11:13):

@Paolo Giarrusso : it will come soon. I first want to get out the first release with the current set. I would think that adding additional packages is quick, assuming they build nicely and don't require complicated non-ocaml/coq dependencies.

view this post on Zulip Paolo Giarrusso (Dec 16 2020 at 11:28):

that's alright, and probably more important :-). But there's a standard Coq benchmark that people use and it already has a selection of packages.

view this post on Zulip Paolo Giarrusso (Dec 16 2020 at 11:28):

Is that CI-only?

view this post on Zulip Paolo Giarrusso (Dec 16 2020 at 11:29):

(can't find a link)

view this post on Zulip Théo Zimmermann (Dec 16 2020 at 11:32):

Yes, it's CI only.

view this post on Zulip Théo Zimmermann (Dec 16 2020 at 11:32):

I'll dig the link.

view this post on Zulip Théo Zimmermann (Dec 16 2020 at 11:33):

The list is here: https://github.com/coq/coq/blob/1c400a19aeb70842453f83a26f5abafc59901242/dev/bench/gitlab.sh#L55

view this post on Zulip Michael Soegtrop (Dec 16 2020 at 16:07):

I guess I can make a wrapper script around this which runs this based on Coq platform.

view this post on Zulip Théo Zimmermann (Aug 11 2022 at 21:20):

M1 processors are available as GitHub runners now :tada: https://github.blog/changelog/2022-08-09-github-actions-self-hosted-runners-now-support-apple-m1-hardware/

view this post on Zulip Théo Zimmermann (Aug 11 2022 at 21:21):

Maybe we can hope for official M1 support in 2022.09?

view this post on Zulip Paolo Giarrusso (Aug 11 2022 at 22:20):

Does _self-hosted_ means you must provide the actual machines (or pay a cloud for it)?

view this post on Zulip Guillaume Melquiond (Aug 12 2022 at 01:32):

Yes.

view this post on Zulip Michael Soegtrop (Aug 12 2022 at 07:13):

Could INRIA provide two runners?

I guess the issue with M1 IN datacenterS is that there is no M1 blade HW (afaik) and mac minis in a datacenter are not that nice.

view this post on Zulip Théo Zimmermann (Aug 12 2022 at 08:13):

Ah sorry, I read two fast. Yes, something can probably done on Inria's side, though probably not in time for 2022.09.

view this post on Zulip Maxime Dénès (Sep 03 2022 at 10:35):

I just checked again, one of the main French cloud providers (Scaleway) has M1 available right now (I had checked after the Coq meeting in Sophia, but they didn't have any left). Should be fairly easy to get one or two paid by Inria for Coq CI.

view this post on Zulip Maxime Dénès (Sep 05 2022 at 13:18):

I got more information on the process and will initiate it.

view this post on Zulip Maxime Dénès (Sep 08 2022 at 08:45):

@Michael Soegtrop How many Mac Minis do you think we'd need to rent? Two?

view this post on Zulip Michael Soegtrop (Sep 08 2022 at 09:13):

In case we want to have the CI just for Coq Platform, I think even one would be sufficient. Coq Platform CI anyway takes quite long (5..6 hours), and the Mac Mini will hardly be the bottle neck. Also Coq Platform CI is low volume (a daily CI run and not that many PRs).

If you want to run Coq CI on it, it will be a different story, 2 might not suffice then - I would have to make statistics.

But IMHO running Apple silicon CI just in Coq Platform should be sufficient. I don't expect many deviations from Intel silicon Macs.

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

What might make more sense is btw a Mac Studio, since it is available with 32 GB of RAM. I would rather have one Mac Studio with 32 GB (or even 64) than two Mac Mini with 16 GB (and definitely not a Mac Mini with 8 GB).

https://www.apple.com/shop/buy-mac/mac-studio/10-core-cpu-24-core-gpu-16-core-neural-engine-32gb-memory-512gb

view this post on Zulip Maxime Dénès (Sep 08 2022 at 09:24):

Ah! Unfortunately Scaleway offers only 8 Gb Mac minis. I'm not sure if we have access to AWS ARM instances.

view this post on Zulip Michael Soegtrop (Sep 08 2022 at 09:56):

Well currently a 8 GB machine is fine, but the memory consumption of Coq projects increases with what is generally available. As soon as most Coq researchers have 32 GB Laptops 8GB might not be enough.

view this post on Zulip Maxime Dénès (Sep 08 2022 at 11:33):

We should limit the memory available to Coq developers :D

view this post on Zulip Maxime Dénès (Sep 08 2022 at 11:46):

AWS has 16 Gb M1 instances, but they cost ~500€/month if used continously, vs 73€/month for the Scaleway Mac Mini

view this post on Zulip Maxime Dénès (Sep 08 2022 at 11:47):

And it's tricky not use them fully on demand, because Apple's license terms are so that you have to pay at least 24h of usage each time you start it

view this post on Zulip Michael Soegtrop (Sep 08 2022 at 12:09):

Well let's go with the 8GB instances. We can still exclude ultra memory hungry projects from M1 testing. It should hardly make a difference which Coq projects we test for the question if Coq runs on M1.

view this post on Zulip Paolo Giarrusso (Sep 08 2022 at 20:28):

Are there labels for such platform-specific bugs? We've seen stack overflows but OCaml fixed those, so might be worth looking for ways Coq stresses OCaml in a way OCaml's own tests wouldn't find... native_compute comes to mind

view this post on Zulip Michael Soegtrop (Sep 09 2022 at 09:01):

And again: for Coq Platform alone one instance is sufficient - for Coq I don't know.

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

@Paolo Giarrusso : in Coq Platform there are labels for platform specific bugs including Apple M1. I have a generic macOS category and specialized ones for Apple silicon and for homebrew (I should also have one for MacPorts, but since I use MacPorts myself bugs there didn't happen so far). Maybe in some future we need one for Apple Intel silicon.

view this post on Zulip Théo Zimmermann (Sep 09 2022 at 09:06):

I think the priority is to test the Coq Platform on Apple M1, the Coq repo itself can wait.

view this post on Zulip Maxime Dénès (Sep 09 2022 at 12:13):

I asked for two instances, since the process is fairly heavy. Once we get the credits, we can use them as is the most efficient, though. I think we'll first put an always-on runner first, then experiment spawning one on-demand.

view this post on Zulip Maxime Dénès (Sep 09 2022 at 12:15):

We're making progress, if everything goes well we should be able to get them next week.

view this post on Zulip Maxime Dénès (Sep 16 2022 at 12:57):

I was a bit too optimistic, unfortunately. Still trying to figure out some of the remaining steps.

view this post on Zulip Maxime Dénès (Sep 29 2022 at 19:16):

Getting close, I have a call with our financial services next week to unblock what should be the last steps.

view this post on Zulip Maxime Dénès (Oct 17 2022 at 23:06):

It is now our "service mutualisé dépenses" which has to perform the last step...

view this post on Zulip Maxime Dénès (Oct 20 2022 at 18:23):

@Michael Soegtrop We finally got one Mac Mini! I'd like to experiment a bit with pluging it as a runner in a safe way. Is there a Coq Platform CI job I should try?

view this post on Zulip Michael Soegtrop (Oct 21 2022 at 07:27):

@Maxime Dénès : great! The MacOS CI job (https://github.com/coq/platform/blob/main/.github/workflows/macos.yml) should work on Apple Silicon (I am meanwhile myself on Apple silicon btw). For faster experiments you can change "-extent=x" to "-extent=i" - this will build only Coq and CoqIDE then (which is for a Apple vs Intel silicon question the main part).


Last updated: Jan 30 2023 at 11:03 UTC