Michael Soegtrop (Dec 14 2020 at 17:40): 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.
Paolo Giarrusso (Dec 15 2020 at 12:43):BTW, no pressure but looking forward to any benchmarks of Coq on M1 vs non-M1 :-)
Enrico Tassi (Dec 15 2020 at 12:55):Especially the core temperature ;-)
Paolo Giarrusso (Dec 15 2020 at 12:58):oh yeah, it'd be great to run Coq and typing comfortably without a leafblower fan
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).
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.
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)
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
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)
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.
Paolo Giarrusso (Dec 16 2020 at 10:55):not in particular
Paolo Giarrusso (Dec 16 2020 at 10:56):so coq platform sounds great, especially if it already includes Iris
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
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)
Paolo Giarrusso (Dec 16 2020 at 11:10):there's an issue since months
Paolo Giarrusso (Dec 16 2020 at 11:10):not sure where
Paolo Giarrusso (Dec 16 2020 at 11:10):https://github.com/coq/platform/issues/4
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.
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.
Paolo Giarrusso (Dec 16 2020 at 11:28):Is that CI-only?
Paolo Giarrusso (Dec 16 2020 at 11:29):(can't find a link)
Théo Zimmermann (Dec 16 2020 at 11:32):Yes, it's CI only.
Théo Zimmermann (Dec 16 2020 at 11:32):I'll dig the link.
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
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.
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/
Théo Zimmermann (Aug 11 2022 at 21:21):Maybe we can hope for official M1 support in 2022.09?
Paolo Giarrusso (Aug 11 2022 at 22:20):Does _self-hosted_ means you must provide the actual machines (or pay a cloud for it)?
Guillaume Melquiond (Aug 12 2022 at 01:32):Yes.
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.
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.
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.
Maxime Dénès (Sep 05 2022 at 13:18):I got more information on the process and will initiate it.
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?
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.
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).
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.
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.
Maxime Dénès (Sep 08 2022 at 11:33):We should limit the memory available to Coq developers :D
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
Maxime Dénès (Sep 08 2022 at 11:47):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
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.
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
Michael Soegtrop (Sep 09 2022 at 09:01):And again: for Coq Platform alone one instance is sufficient - for Coq I don't know.
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.
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.
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.
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.
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.
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.
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...
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?
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).
Maxime Dénès (Feb 13 2023 at 19:47):@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
Ali Caglayan (Feb 13 2023 at 23:13):@Maxime Dénès Will we have that runner available in the main repo?
Michael Soegtrop (Feb 14 2023 at 08:24):@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