How to get rid of warnings like "Warning: Cannot open directory /usr/games/."?

Using Coq
1

Hello!

Every time I run coqc (using dune), I get a bunch of warnings about directories which cannot be opened., like (excerpt from the log):

(cd _build/default && /snap/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ...
Warning: Cannot open directory /usr/games/. [cannot-open-dir,filesystem]
Warning: Cannot open directory /sbin/. [cannot-open-dir,filesystem]
Warning: Cannot open directory /usr/sbin/. [cannot-open-dir,filesystem]

These warnings show up for each run of coqc. The compilation itself succeeds.

I’m a little bit lost here as this is annoying because it shadows real warnings and errors.

There is nothing in the env or somewhere I searched which gave me a hint (e.g. home or /snap/coq-prover).

Any idea?

Kind regards,

Andre

Version / Env:

Debian 12.4 using snapd

$ coqc --version
The Coq Proof Assistant, version 8.17.1
compiled with OCaml 4.14.1

2

Is that the snap sandbox in action? There’s probably a tool to control it.

Sorry I can’t be specific, I’m in the “enemy” (flatpak) camp.

If you build coq yourself with opam, I bet you won’t have this problem.

3

Presumably, all these directories are part of your PATH environment variable. If you remove them before running dune, it should get rid of the warning messages, e.g., by typing PATH=/usr/bin in your console. (You might need some more directories than just /usr/bin in your PATH. Type echo $PATH to see which are the currently existing ones.)

4

No, none of these dirs (e.g. /usr/games) is in my PATH.
This was also my first assumption.
PATH=/usr/local/bin:/usr/bin:/bin:/snap/bin

And also this returns nothing:
rgrep "/usr/games" /snap/coq-prover/

5

I do not know if Snap reads the file /etc/environment, but the extra directories might come from here.

6

Don’t think so :slight_smile:

$ ls -l /etc/environment
-rw-r--r-- 1 root root 0 Dec 28 04:52 /etc/environment

7

I am not sure what your point is; you have just showed that /etc/environment indeed exists on your system, but neither that it is free of /usr/games nor that it is ignored by Snap. That being said, the content of that file might be irrelevant, because Snap itself presumably comes with its own /etc/environment file (under /snap/coreXX/current/etc/environment) which would override the system one, I guess.

8

Hm.
It’s hard to fit “/usr/games” or something else in 0 bytes :slight_smile:

Thanks for the hint to the separate environment file in the snap domain. The contents is:

$ cat /snap/core20/current/etc/environment
PATH="/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/usr/local/games:/snap/bin"

$ for dir in $(cut -f 2 -d "=" </snap/core20/current/etc/environment | tr ":" " "); do ls -ld $dir; done
ls: cannot access '"/usr/local/sbin': No such file or directory
drwxr-xr-x 2 root root 4096 Dec 28 04:52 /usr/local/bin
drwxr-xr-x 2 root root 12288 Dec 31 07:31 /usr/sbin
drwxr-xr-x 2 root root 28672 Jan  4 16:37 /usr/bin
lrwxrwxrwx 1 root root 8 Dec 28 04:52 /sbin -> usr/sbin
lrwxrwxrwx 1 root root 7 Dec 28 04:52 /bin -> usr/bin
drwxr-xr-x 2 root root 4096 Dec  9 21:08 /usr/games
drwxr-xr-x 2 root root 4096 Dec 28 04:52 /usr/local/games
ls: cannot access '/snap/bin"': No such file or directory

But:

  1. why in the world should coqc use PATH to look something up? (What “something”?)
  2. The PATH contains of nine different parts. Why are only three warnings logged in each call to coqc? Why are some logged which are in path an can be accessed (e.g. /usr/games) and other with are in PATH and do not exists are not logged (e.g. /usr/local/sbin)?

For me this does not makes much sense.

9

Coq does look up in the PATH for some helper tools, e.g., csdp, which is used by the nia and nra tactics. (The odd part is that the lookup is always performed at startup rather than being delayed until the tactics are actually used.)