Coq Platform does not work with make

[jwnhy]

I installed Coq Platform with snapd. It seems incompatible with the system-level make.

COQDEP VFILES
/bin/sh: line 1: coqdep: command not found
COQDEP VFILES
/bin/sh: line 1: coqdep: command not found
COQDEP VFILES
/bin/sh: line 1: coqdep: command not found
COQC Verif_sumarray.v
File "./Verif_sumarray.v", line 116, characters 8-18:
Error: Cannot find a physical path bound to logical path matching suffix VC.

make[1]: *** [makefile:763: Verif_sumarray.vo] Error 1
make: *** [makefile:386: all] Error 2

If using coqide's make, everything is fine.
I am guessing it is due to some $PATH issue between host system and snap image.
Any ideas on how to fix this?

[Zimmi48]

The issue seems to be that coqdep is not available in PATH. Snap hides most commands from the global path by sealing them into a Snap-specific namespace. But we can require global aliases and we have done so for several toplevel commands including coqdep: https://forum.snapcraft.io/t/aliases-request-for-coq-prover/21925/12. Since this request has been granted, it is strange that you are hitting this issue. Could it be a regression in the aliases or could it be due to your Snap environment not taking these aliases into account? I unfortunately cannot test this Snap on my side to attempt to reproduce the issue.

[MSoegtropIMC]

@gares : do you have time to look into this?

[gares]

No, coqdep is not an alias:

$ snap aliases coq-prover
Command                  Alias          Notes
coq-prover.coq-makefile  coq_makefile   -
coq-prover.coqc          coqc           -
coq-prover.coqide        coqide         -
coq-prover.coqidetop     coqidetop.opt  -
coq-prover.coqtop        coqtop         -

but if you use the coq_makefile from the snap, then it should pick the coqdep in the snap, since the, say Makefile.conf, should contain:

COQBIN = /snap/coq-prover/28/coq-platform/2022-01-0/bin/

and Makefile should contain:

# Coq binaries
COQC     ?= "$(COQBIN)coqc"
COQTOP   ?= "$(COQBIN)coqtop"
COQCHK   ?= "$(COQBIN)coqchk"
COQNATIVE ?= "$(COQBIN)coqnative"
COQDEP   ?= "$(COQBIN)coqdep"
COQDOC   ?= "$(COQBIN)coqdoc"
COQPP    ?= "$(COQBIN)coqpp"
COQMKFILE ?= "$(COQBIN)coq_makefile"
OCAMLLIBDEP ?= "$(COQBIN)ocamllibdep"

@Zimmi48 if you want to also ask an alias for the other binaries not in this list, I'm OK with it but I don't have time right now.

[gares]

@jwnhy can you confirm you did not run the coq_makefile from the snap package?

[gares]

(also, ftr, if you install the snap by hand, eg snap install ./my-file.snap --dangerous then aliases are not created)

[jwnhy]

@jwnhy can you confirm you did not run the coq_makefile from the snap package?

Actually, I tried both the original makefile in the SF and use coq_makefile to make one.

Different error but both related to $PATH, saying something not found.

[Zimmi48]

@Zimmi48 if you want to also ask an alias for the other binaries not in this list, I'm OK with it but I don't have time right now.

You've missed my point, the link that I've provided contains:

coqdep -> coq-prover.coqdep

So the alias was already requested and granted, although maybe it was never correctly set up...

[jwnhy]

I don't think it is correctly set up.
My snap folder showed something like this.

I didn't setup snap manually, but to use a one-line command

snap install coq-prover

[gares]

OK, so we have 2 problems:

• the alias request was not fulfilled
• still, even without the alias coq_makefile should work

For the second problem, @jwnhy, could you please start afresh, generate the makefile with coq_makefile from the snap and type make debug; make VERBOSE=1, thanks

[jwnhy]

So I ran the make debug > ~/temp 2>&1; make VERBOSE=1 >> ~/temp 2&>1
and it spit out a huge chunk.
@gares Hope this is useful to you.

[gares]

Something is very fishy, for example this does not exist:

• /snap/coq-prover/28/coq-platform/2022-01-0/bin//coqc

While your screenshot suggests that

• /var/lib/snapd/snap/coq-prover/28/coq-platform/2022-01-0/bin//coqc

does. Which Linux distro are you on? It is probably a bug of the snap package which assumes snap is installed in /snap/ but it is not the case.

[gares]

@Zimmi48 the problem with aliases is probably that we don't declare a corresponding app, see

platform/linux/snap/snapcraft.yaml.in

Line 43 in 88d69fc

apps:

[jwnhy]

Something is very fishy, for example this does not exist:

• /snap/coq-prover/28/coq-platform/2022-01-0/bin//coqc

While your screenshot suggests that

• /var/lib/snapd/snap/coq-prover/28/coq-platform/2022-01-0/bin//coqc

does. Which Linux distro are you on? It is probably a bug of the snap package which assumes snap is installed in /snap/ but it is not the case.

I am using Gentoo...LOL
It took me a while to get every kernel stuff for snap to work...

[Zimmi48]

@Zimmi48 the problem with aliases is probably that we don't declare a corresponding app, see

platform/linux/snap/snapcraft.yaml.in

Line 43 in 88d69fc

apps:

It seems that we are missing both coqdep and coqidetop.opt.

[gares]

coqidetop.opt is there, see the listing I posted above. My guess is that it won't generate an alias pointing to a non existing app.

[gares]

It took me a while to get every kernel stuff for snap to work...

Are the paths configured in a standard way? I don't get why coq_makefile spits path containing /snap (I cannot find it hardcoded anywhere).

[jwnhy]

It took me a while to get every kernel stuff for snap to work...

Are the paths configured in a standard way? I don't get why coq_makefile spits path containing /snap (I cannot find it hardcoded anywhere).

Yes, here is my $PATH

/home/john/.cargo/bin:/home/john/.elan/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/opt/bin:/usr/lib/llvm/13/bin:/var/lib/snapd/snap/bin:/opt/x86_64-linux-musl-cross/bin/:/home/john/Android/Sdk/platform-tools/:/home/john/tools/xfel/:/home/john/tools/bsc/bin:/opt/toolbox:/opt/arm64/bin/:/opt/riscv/bin:/home/john/tools/Xilinx/Vivado/2020.3/bin/:/home/john/.local/bin:/opt/JLink_Linux_V760b_x86_64:/opt/FreedomStudio-4.18.0.2021-04-1-x86_64-linux-ubuntu14/

[jwnhy]

My snap version is 2.54.4

[MSoegtropIMC]

@gares : is there something I can do for 2022.03 to improve things?

[gares]

Hum, no, I'm out of ideas.

[MSoegtropIMC]

OK, I postponed this and put it on my agenda to become less snap agnostic. Maybe as snap newbe I can more easily reproduce such issues than as a snap pro like you.

[gares]

In thos specific case it seems a snapd with a weird path layout on a niche distribution... not exactly where I would start.

[MSoegtropIMC]

Ah OK, I didn't read the Gentoo thing.

Well I would say that Gentoo doesn't really support snap and we should simply document this and recommend that users on Gentoo should use the from sources scripts.

[Zimmi48]

Just for the record, while we might wish to close the "Gentoo" part of this issue as "won't fix" / unsupported, there remains the fact that some of the commands that we decided to export (at some point) are not exported because they are not listed under:

platform/linux/snap/snapcraft.yaml.in

Line 43 in 88d69fc

apps:

I think this latter part should still be fixed (for Proof General users) or documented (e.g., in the case of coqdoc, for which no alias was requested).

[MSoegtropIMC]

@gares : isn't it so that one also needs some sort of approval from the snap team to export apps without prefix?

[gares]

Yes, but Theo already did. They don't show up since there is no entry in the app: stanza, I believe.
See https://forum.snapcraft.io/t/aliases-request-for-coq-prover/21925/13