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.
BTW, no pressure but looking forward to any benchmarks of Coq on M1 vs non-M1 :-)
Especially the core temperature ;-)
oh yeah, it'd be great to run Coq and typing comfortably without a leafblower fan
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).
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.
I'd vote for an early release over waiting for everything (not that I count, I have no M1)
Emacs exists and VsCoq is doing okay, though you probably want to give commit rights to Fabian
(opened https://coq.zulipchat.com/#narrow/stream/237662-VsCoq-devs.20.26.20users/topic/Adding.20maintainers to explain that part better)
@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.
not in particular
so coq platform sounds great, especially if it already includes Iris
uh, it doesn't! Can you also use the standard Coq benchmarks from the infrastructure? Those do include Iris and libraries using it
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)
there's an issue since months
not sure where
@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.
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.
Is that CI-only?
(can't find a link)
Yes, it's CI only.
I'll dig the link.
The list is here: https://github.com/coq/coq/blob/1c400a19aeb70842453f83a26f5abafc59901242/dev/bench/gitlab.sh#L55
I guess I can make a wrapper script around this which runs this based on Coq platform.
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/
Maybe we can hope for official M1 support in 2022.09?
Does _self-hosted_ means you must provide the actual machines (or pay a cloud for it)?
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.
Ah sorry, I read two fast. Yes, something can probably done on Inria's side, though probably not in time for 2022.09.
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.
I got more information on the process and will initiate it.
@Michael Soegtrop How many Mac Minis do you think we'd need to rent? Two?
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.
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).
Ah! Unfortunately Scaleway offers only 8 Gb Mac minis. I'm not sure if we have access to AWS ARM instances.
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.
We should limit the memory available to Coq developers :D
AWS has 16 Gb M1 instances, but they cost ~500€/month if used continously, vs 73€/month for the Scaleway Mac Mini
And it's tricky to 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
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.
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
And again: for Coq Platform alone one instance is sufficient - for Coq I don't know.
@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.
I think the priority is to test the Coq Platform on Apple M1, the Coq repo itself can wait.
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.
We're making progress, if everything goes well we should be able to get them next week.
I was a bit too optimistic, unfortunately. Still trying to figure out some of the remaining steps.
Getting close, I have a call with our financial services next week to unblock what should be the last steps.
It is now our "service mutualisé dépenses" which has to perform the last step...
@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?
@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).
@Michael Soegtrop As discussed today, I added a runner. The first test jobs are running here: https://github.com/coq/platform/actions/runs/4167189305/jobs/7212456449 https://github.com/coq/platform/actions/runs/4167189305/jobs/7212456323
@Maxime Dénès Will we have that runner available in the main repo?
@Ali Caglayan : these runners are Apple silicon runners intended for Coq Platform cross platform tests. They are not intended for general Coq CI. Looking it the timing it might make sense to have M1 runners for that, though.
Last updated: Jun 03 2023 at 05:01 UTC