New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
CoqIDE (>= 8.13) crashes when opening preferences (platform-specific) #15486
Comments
Stacktrace:
EDIT: I can currently reproduce this easily and I have saved a full Apple crash log, but that has too much info. |
This does not look like a Coq bug. Is it specific to Coqide 8.15 or can you reproduce it with 8.14 too? |
Same bug here with macOS Big Sur 11.6.3 (Intel), OCaml 4.11.2 or 4.12.1, CoqIDE 8.15.0. |
This seems to be the same bug that was reported yesterday in the platform repo (cc @MSoegtropIMC): coq/platform#217 |
Same bug here on a fresh installation macOS 12.2.1 (ARM), CoqIDE 8.15.0. |
Depending on whether the bug is in GTK or in Quartz/MacOS, the following might succeed: broadwayd &
sleep 1
firefox http://localhost:8080/ # or chrome or ...
export GDK_BACKEND=broadway
coqide & This will open Coqide inside your browser, thus side-stepping a lot of code in GTK, Quartz, and MacOS. (But be aware that this is hardly tested.) |
No easy broadwayd on mac AFAICT... at least |
@Blaisorblade : in case you can reproduce the issue, how about looking at it with ocamldebug? Btw.: it might also be useful to check if this is a Homebrew vs. Macports issue. I am using Macports and I don't see the issue (at least not for compiled from sources CoqIDE - I see it with (otherwise identical) installed CoqIDE). |
I just tried, but I'm stuck here:
I'll try asking in the CoqWG. EDIT: I tried extending (DY)LD_LIBRARY_PATH or patching dev/dune-dbg to pass extra args to ocamlfind, but had success with neither :-| |
I am afraid I can't help here - I did pretty deep debugging of CoqIDE a few years back - including mixed C and OCaml debugging and debugging of coqidetop, but that was before dune ... |
|
@Blaisorblade : I recently had issues with labgtk3.3.1.1 on BigSur (see #15857) - which went away by switching to lablgtk3.3.1.2. Can you verify if this helps you? |
I already had
since you use MacPorts and I use Homebrew, I wonder whether that's a factor, but installing both to try is probably going to be tricky... @davidnowak @orilahav do you use Homebrew or MacPorts? |
I can test it on a VM. |
@Blaisorblade I use homebrew. |
Hi, any idea how to address this? Estimate on which version? |
@orilahav Unfortunately developers willing to spend time on CoqIDE are in short supply, let alone ones who can test on MacOS. I would like to make progress with this, but I don't know how to test on MacOS. Have you tried VSCoq? https://github.com/coq-community/vscoq If your goal is to introduce Coq to students, you can point them to CoqIDE, VSCoq if that doesn't work and also mention Proof General for emacs and I believe there is Vim support also. |
The solution that I found was just to download an older release. For me 8.15 was not working on MacOS Monterey and the release 8.13.0 worked just fine: |
FTR it was discussed today in the working group. We will spend some time in the near future, making sure that we are compatible with M1 and M2 architectures. We would ideally like to be able to reproduce this issue reliably, and for that having M1 workers would be ideal. Unfortunately, this is not something GitHub ships by default, so perhaps an INRIA aided solution will be explored. |
Thank you. Happy to assist with testing or anything within my capability. |
running |
This could be a style error, and not related to M1 then. Since it is happening on Intel Macs. I couldn't find anything about GTK failing on M1 on Google. @jfehrle what do you think? |
See if you have the $XDG_DATA_DIRS environment variable set, and if so, clear it and try CoqIDE again. See #16211. Or (less likely) maybe the data it points to has gotten corrupted. |
In my case this variable It is not set. |
Just to add a data point: I have the same problem with CoqIDE 8.13.2 on MacOS Monterey 12.0.1 with Intel chips, with the same error message before exiting: |
Copying the conclusion of #16136: due to a bug introduced in pango 1.49.4 and fixed in pango development branch. |
Closing as duplicate of #16136. |
And I should have clarified this is, indeed, fixed (#16136). |
Noticed in ocaml/opam-repository#20456.
To reproduce, install coqide, go to Edit -> Preferences. Clearing
~/.config/coq
doesn't seem to make a difference.Version:
CoqIDE 8.15, but also 8.13 and 8.14 from the respective platforms (
__coq-platform.2021.11.0~8.13~2021.11
and__coq-platform.2021.11.0~8.14~2021.11
).Platform:
The text was updated successfully, but these errors were encountered: