# Apparently bad installation of coq (im a newbie)

**URL:** <https://discourse.rocq-prover.org/t/apparently-bad-installation-of-coq-im-a-newbie/1267>\
**Category:** Using Rocq\
**Created:** [April 10, 2021, 4:56pm UTC](https://discourse.rocq-prover.org/t/apparently-bad-installation-of-coq-im-a-newbie/1267 "2021-04-10T16:56:11Z")\
**Posts on this page:** 6\
**Page:** 1

<div class="post-metadata">

**Author:** ![pat0rb](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/pat0rb/32/512_2.png) [@pat0rb](https://discourse.rocq-prover.org/u/pat0rb)\
**Post date:** [April 10, 2021, 4:56pm UTC](https://discourse.rocq-prover.org/t/apparently-bad-installation-of-coq-im-a-newbie/1267/1 "2021-04-10T16:56:11Z")

</div>

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!

---

<div class="post-metadata">

**Author:** ![silene](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/silene/32/485_2.png) [@silene](https://discourse.rocq-prover.org/u/silene)\
**Post date:** [April 11, 2021, 6:14am UTC](https://discourse.rocq-prover.org/t/apparently-bad-installation-of-coq-im-a-newbie/1267/2 "2021-04-11T06:14:14Z")

</div>

> [@pat0rb](#):
>
> I get the following message:
> 
> ```none
> Gtk-Message: 11:15:01.106: Failed to load module “xapp-gtk3-module”
> 
> ```

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

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

Are you using the Snap package for Coq?

---

<div class="post-metadata">

**Author:** ![jeremydaw](https://avatars.discourse-cdn.com/v4/letter/j/e99b99/32.png) [@jeremydaw](https://discourse.rocq-prover.org/u/jeremydaw)\
**Post date:** [April 11, 2021, 7:17am UTC](https://discourse.rocq-prover.org/t/apparently-bad-installation-of-coq-im-a-newbie/1267/3 "2021-04-11T07:17:49Z")

</div>

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.

Jeremy

---

<div class="post-metadata">

**Author:** ![pat0rb](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/pat0rb/32/512_2.png) [@pat0rb](https://discourse.rocq-prover.org/u/pat0rb)\
**Post date:** [April 11, 2021, 9:56pm UTC](https://discourse.rocq-prover.org/t/apparently-bad-installation-of-coq-im-a-newbie/1267/4 "2021-04-11T21:56:14Z")

</div>

> [@silene](#):
>
> Are you running the Xfce window manager? Do you have something special in your `GTK_MODULES` environment variable? ( `echo $GTK_MODULES` )

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.

---

<div class="post-metadata">

**Author:** ![pat0rb](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/pat0rb/32/512_2.png) [@pat0rb](https://discourse.rocq-prover.org/u/pat0rb)\
**Post date:** [April 11, 2021, 10:03pm UTC](https://discourse.rocq-prover.org/t/apparently-bad-installation-of-coq-im-a-newbie/1267/5 "2021-04-11T22:03:13Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![Blaisorblade](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/blaisorblade/32/56_2.png) [@Blaisorblade](https://discourse.rocq-prover.org/u/Blaisorblade)\
**Post date:** [April 16, 2021, 11:31pm UTC](https://discourse.rocq-prover.org/t/apparently-bad-installation-of-coq-im-a-newbie/1267/6 "2021-04-16T23:31:26Z")

</div>

> [@pat0rb](#):
>
> 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,

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 😑