-
Notifications
You must be signed in to change notification settings - Fork 701
Open
Labels
kind: bugAn error, flaw, fault or unintended behaviour.An error, flaw, fault or unintended behaviour.needs: triageThe validity of this issue needs to be checked, or the issue itself updated.The validity of this issue needs to be checked, or the issue itself updated.
Description
Description of the problem
Hello.
I'm trying to use CoqIDE on WSL Debian. But this message shows after I type coqide:
Fatal error: exception Gtk.Error("GtkMain.init: initialization failed\nml_gtk_init: initialization failed")
No interfaces pop up.
I reinstalled coqide and lablgtk3 through opam. It didn't work.
Small Rocq / Coq file to reproduce the bug
Version of Rocq / Coq where this bug occurs
Coq 8.20.1
Interface of Rocq / Coq where this bug occurs
No response
Last version of Rocq / Coq where the bug did not occur
No response
Metadata
Metadata
Assignees
Labels
kind: bugAn error, flaw, fault or unintended behaviour.An error, flaw, fault or unintended behaviour.needs: triageThe validity of this issue needs to be checked, or the issue itself updated.The validity of this issue needs to be checked, or the issue itself updated.