Andrew Appel (Jan 28 2021 at 17:40): Andrew Appel (Jan 28 2021 at 17:40):Does CoqIDE 8.13.0 work reliably on Mac? I'm not a Macintosh person myself, but in 3 days I'll be again teaching my class with another 30 Coq newbies doing Software Foundations. Someone mentioned to me that there are problems with CoqIDE on the new M1-based Macs. What IDE should my students use? In past years I've been happy with CoqIDE for my students (and myself).
Karl Palmskog (Jan 28 2021 at 17:42):if CoqIDE doesn't work on some Mac, the most obvious alternative is likely VsCode+VsCoq
Karl Palmskog (Jan 28 2021 at 17:43):but to my knowledge CoqIDE is tested on Mac as part of the Coq Platform, and Michael Soegtrop has added various MacOS fixes to the OPAM packages over time
Enrico Tassi (Jan 28 2021 at 18:36):I'm not aware on any M1 specific issues. There is a know issue about the missing "notarization" which means that even if the app is signed, one has to right-click + open the first time, then OSX is happy.
Enrico Tassi (Jan 28 2021 at 18:37):@Michael Soegtrop has an M1 at hand, I hope he can confirm.
Enrico Tassi (Jan 28 2021 at 18:38):vscode + vscoq are also a good option IMO (and for sure vscode got more testing on M1 macs than CoqIDE).
Enrico Tassi (Jan 28 2021 at 18:41):There is also this issue, which I don't think is fixed: https://github.com/coq/coq/issues/12779 (the issue contains workarounds)
Enrico Tassi (Jan 28 2021 at 18:41):But is not 8.13 nor M1 specific
Michael Soegtrop (Jan 30 2021 at 10:47):@Andrew Appel : I am using CoqIDE regularly on Mac and it does work. I also regularly test the Coq Platform script on macOS Catalina and macOS BigSur with both Homebrew and MacPorts to install prerequisites and this does work (the script expects that either MacPorts or Homebrew is installed). I also did some first tests with M1 which required some opam hacking but did work then. I wanted to pick this up soon. MacBooks with M1 are delivered since October last year or so.
The biggest problem for VST might be that MacOS since Catalina (this is the 2nd newest version - newest is BigSur) does not support building or running 32 bit code so 32 bit CompCert does not compile. The Opam Package for CompCert-32 3.8 explicitly excludes macOS. I am not exactly sure what CompCert-32 3.7 does if you try to compile it on macOS Catalina or BigSur - it might depend on what binutils you have installed.
If the 32 bit support is required, I can push a 32 bit ARM cross CompCert package to the 8.13 branch and a patched VST-32 package which would pick up this then.
Jacques Garrigue (Apr 25 2022 at 04:30):As a follow-up to this thread, is anybody compiling CoqIDE on Mac M1 ?
I'm maintaining LablGtk 2 and 3, but while LablGtk 2 runs fine on my M1Pro Mac, LablGtk 3 results in a Trace/BPT trap (looks like the equivalent of a segfault).
I'm using X11 versions of Gtk2 and Gtk3 installed through macports.
Note that CoqIDE from the CoqPlatform runs fine, but this is a x64 executable.
Jacques Garrigue (Apr 25 2022 at 04:43):Sorry for the noise.
After upgrading Gtk3 to version @3.24.31_1+quartz the problem seems gone; that was probably a bug in Gtk itself.
It is even snappy.
Configuration is: ocaml 4.14.0, lablgtk3 3.1.2, coqide 8.15.1.
Théo Zimmermann (Apr 25 2022 at 08:15):At least some people have managed to install the Coq Platform from sources on Mac M1 (in this case, this results in a native executable).
Paolo Giarrusso (Apr 25 2022 at 09:32):I have, but opening the configuration dialog still crashes for me
Paolo Giarrusso (Apr 25 2022 at 09:33):and others: https://github.com/coq/coq/issues/15486
YAMAMOTO Mitsuharu (Apr 25 2022 at 10:29):Jacques Garrigue said:
I'm maintaining LablGtk 2 and 3, but while LablGtk 2 runs fine on my M1Pro Mac, LablGtk 3 results in a Trace/BPT trap (looks like the equivalent of a segfault).
I'm using X11 versions of Gtk2 and Gtk3 installed through macports.
Perhaps this is due to the following bug in a Glib2 patch for MacPorts:
https://trac.macports.org/ticket/64377
It is supposed to be fixed now, but you may need to rebuild some ports that depend on Glib2.
Karl Palmskog (Apr 25 2022 at 10:31):is it even possible for us to impose requirements on the underlying GTK3 versions via opam? I think all that we can do is specify opam dependency on conf-gtk3, which may not catch these issues
Théo Zimmermann (Apr 25 2022 at 10:39):If we know of some incompatibility, we could check them dynamically (at configure time).
Last updated: Oct 13 2024 at 01:02 UTC