Apparently bad installation of coq (im a newbie)

Hi everyone,

I am new to programming in general and learning to use coq with Software Foundations, so sorry if my questions seem kinda tedious. I can’t access coq IDE by clicking on the icon but only by running coqide from my terminal, and when I do I get the following message:
Gtk-Message: 11:15:01.106: Failed to load module “xapp-gtk3-module”

Also, I get these warnings anytime I try open some file on the IDE:
(coqide:4354): GLib-GIO-WARNING **: 11:36:58.447: Error creating IO channel for /proc/self/mountinfo: Permission denied (g-file-error-quark, 2)

Also, I think that the “compile buffer” option on the IDE doesn’t actually compile the files as no .vo file appears on my directory after clicking on it, and they actually compile when I run the files from the terminal using: coqc - Q . LF Basics.v for example, because only then do the .vo files appear.

Could anyone point out how to solve these issues?
Thanks in advance!

Are you running the Xfce window manager? Do you have something special in your GTK_MODULES environment variable? (echo $GTK_MODULES)

Are you using the Snap package for Coq?

I get this message ie Failed to load module “xapp-gtk3-module”
when I run something which puts a window on the screen (namely git
fetch, which throws up a window to ask user and p/w), nothing to do with
coq. In my case I ignore it since the program seems to behave just fine
anyway (apart from giving the message). I do use xfce. And nothing
from echo $GTK_MODULES

This happens on one of my machines and not the other, although I would
have said they are running the same software.


1 Like

No, I’m running muffin. I get this answer to echo $GTK_MODULES : xapp-gtk3-module:gail:atk-bridge. Thanks for the answer! And yes, I am using the snap package.

Yeah, I also don’t have any big problem, and it only happens with CoqIDE, although I can’t access it by clicking on it’s icon and can’t compile coq files by clicking on “compile buffer”, but only through terminal.

IIRC that option is not meant to compile anything, but to show the window/buffer with the output of compilation. I forget what the right command is called :expressionless: