Cannot interpret coq file on ubuntu with Coq and VsCode installed through Snap.

[harashimahashi]

I have installed coq via snap. If I use coqide everything works well. Then I have created a new directory and a coq file inside and created new vscode project by typing code . I have installed vscoq. When I press alt + home or other shortcut there is almost no reaction. alt + up brings up a proofview window with the "Not running" words written. Setting path to directory with coqtop does not help. Ubuntu 20.10

[fakusb]

"alt + end" or "alt + down" does also not do anything? "alt + up" giving not running is the normal behaviour, so I'm optimistic.

Can you paste the log of the "Coq language server" after attempting one of those commands? (Ctrl + j -> "Output" (tabs on bottom) -> Coq language server (dropdown menu at right of "output" )).

[Zimmi48]

If you run coqidetop.opt -v in a console, does it correctly print "The Coq Proof Assistant ... 8.13.1"?

[harashimahashi]

"alt + end" or "alt + down" does also not do anything? "alt + up" giving not running is the normal behaviour, so I'm optimistic.

Can you paste the log of the "Coq language server" after attempting one of those commands? (Ctrl + j -> "Output" (tabs on bottom) -> Coq language server (dropdown menu at right of "output" )).

Yes, these commands do nothing.

starting coqtop exec: /snap/bin/coqtop -v Listening at 127.0.0.1:38693 Listening at 127.0.0.1:44127 Listening at 127.0.0.1:43829 Listening at 127.0.0.1:40901 [Warn - 15:04:33] Could not detect coqtop version

[harashimahashi]

If you run coqidetop.opt -v in a console, does it correctly print "The Coq Proof Assistant ... 8.13.1"?

The Coq Proof Assistant, version 8.13.1 (February 2021) compiled on Feb 26 2021 9:08:25 with OCaml 4.07.1

[gares]

I can reproduce it here using both coq and vscode from snap packages. I'm pretty sure I tested it before with vscode as a regular debian package. Can you confirm you are using code from a snap?

[harashimahashi]

I can reproduce it here using both coq and vscode from snap packages. I'm pretty sure I tested it before with vscode as a regular debian package. Can you confirm you are using code from a snap?

Yes, I can. I am using code from a snap.

[gares]

This workflow will produce a snap containing the tentative fix in about 1h https://github.com/coq/platform/actions/runs/664854685 if it is confirmed to work then https://github.com/coq/platform/pull/93 should be merged followed by a full CI run (including the upload to the store)

[gares]

it does not work (yet)

[gares]

Unfortunately it seems an open problem https://github.com/snapcore/snapd/pull/8699

[gares]

OK, I did some digging:

• it's not related to snap confinement models, since code is in classic mode (not really confined) and apparently to connect to localhost one does not need the network plug, so my patch above is useless
• the whole problem seems to be in the detection of Coq version. Runing coqtop -v or even /snap/bin/coqtop -v exists with 2 and prints nothing. If I replace coqtop -v with ls /usr/bin then I get an exit 0 code but still no output
• if I hack https://github.com/coq-community/vscoq/blob/dcfb225d49dce6cf71eac8405082e0a0e431b75c/server/src/coqtop/CoqTop.ts#L105 and return "8.13.1" then things work (/snap/bin/coqidetop.opt starts and get going)
• if the failure to get a Coq version leads to this code path https://github.com/coq-community/vscoq/blob/dcfb225d49dce6cf71eac8405082e0a0e431b75c/server/src/coqtop/CoqTop8.ts#L230 then we are served, since -ideslave makes coqidetop.opt fail to start

I'm not very familiar with spawn, I tried to get messages from stderr but nothing, I really don't know what is wrong with coqtop and why it would exit 2 (I don't even fond where in code of Coq one exist with 2). Now I'm out of time, it would be nice if you could test the vsix I attach here (code --install-extension path/to/vscoq-0.3.4.vsix) which is version 0.3.4 + this patch

diff --git a/server/src/coqtop/CoqTop.ts b/server/src/coqtop/CoqTop.ts
index c7ddb4e..4626d5a 100644
--- a/server/src/coqtop/CoqTop.ts
+++ b/server/src/coqtop/CoqTop.ts
@@ -105,7 +105,7 @@ export function detectVersion(coqtopModule: string, cwd: string, console?: {log:
         const ver = /^\s*The Coq Proof Assistant, version (.+?)\s/.exec(result);
         // if(!ver)
         //   console.warn('Could not detect coqtop version');
-        resolve(!ver ? undefined : ver[1]);
+        resolve(!ver ? "8.13.1" : ver[1]);
       });
       coqtop.on('error', (code:number) => {
         // console.warn(`Could not start coqtop; error code: ${code}`)

vsix.zip

If it works, then it means I've identified the problem but I still need some help since my fix is just a hack. A slightly better one would be to default to the most recent set of options if the version of Coq cannot be detected.

[gares]

FTR, if one is willing to clean up this code, coqc now accepts -print-version which prints the version in an easy to parse way (the regexp is not what is failing here, but still looks hackish).

[harashimahashi]

It seems like your hack works, I have tested it.

[gares]

@fakusb any idea how to debug this? I don't have more time for this, but it may not even be worth digging deeper if we

default to the most recent set of options if the version of Coq cannot be detected.

WDYT?

[fakusb]

I don't have an good idea on debugging this. It does not have to do with the version-check code executing 'coqtop' instead of 'coqtop.opt' , does it (I don't use snap myself)? Defaulting seems like a good idea.

[ztatlock]

It looks like we've had some students in a large course bump into this issue. Is there any short term workaround?

Many thanks for any advice or help folks can provide!

[gares]

I think the easiest workaround is to install the hacked vsix as per https://github.com/coq-community/vscoq/issues/221#issuecomment-802132705

[gares]

Just in case, it does not really matter if vscoq "detects" 8.13.1 but the student is running 8.12.x or any other non-super-old versions of Coq.

[Zimmi48]

@fakusb Maybe it would be worth implementing the defaulting idea and hot releasing a new version ASAP, WDYT?

[fakusb]

@Zimmi48 I will publish this hotfix asap

[Zimmi48]

Thanks!

[fakusb]

I think #223 fixes this, could someone test it inside snap before I release? Here is a build vscoq-0.3.4.zip

[Zimmi48]

Unfortunately, I can't help here, because I can't install Snap packages on NixOS :disappointed:

[karunasagark]

Still facing this issue on Ubuntu

$ coqc -v The Coq Proof Assistant, version 8.15.2 compiled with OCaml 4.13.1

Logs from Coq Language Server:

starting coqtop
exec: /snap/bin/coqtop -v
Listening at 127.0.0.1:39067
Listening at 127.0.0.1:42177
Listening at 127.0.0.1:36445
Listening at 127.0.0.1:34445
[Warn  - 11:06:10 PM] Could not detect coqtop version, defaulting to >= 8.10.
Coqtop version parsed into semver version 8.10.0
exec: /snap/bin/coqidetop.opt -main-channel 127.0.0.1:39067:42177 -control-channel 127.0.0.1:36445:34445 -async-proofs on -topfile file:///home/karuna/gitlab/cse505-23wi/hw1/HW1.v
coqtop started with pid 146376
Client connected on main channel R (port 39067)
Client connected on main channel W (port 42177)
Client connected on control channel R (port 36445)
Client connected on control channel W (port 34445)
--------------------------------
Call Init()
Init: () --> 1
--------------------------------
Call Add("(*

    _   _    ___...", editId: 0, stateId: 1, verbose: true)
coqtop exited with code: 2
onCoqClosed(coqtop closed with code: 2)
onCoqClosed(undefined)
coqtop closed with code: 2
Listening at 127.0.0.1:35605
Listening at 127.0.0.1:45195
Listening at 127.0.0.1:41699
Listening at 127.0.0.1:45665

[thery]

unfortunately I think the patch as not been published yet. We should do a release very soon. Could you try with the master version vscoq.zip

[Blaisorblade]

Wait I must be missing something: shouldn't the existing patch be included in 0.3.6 from last January? And indeed, MR #223 is where Could not detect coqtop version, defaulting to >= 8.10. comes from, IIUC.

AFAICT, the problem has gotten worse. Recall VsCoq runs coqtop and then coqidetop:

• before coqtop failed with error 2, and we added code to ignore that failure
• now coqidetop fails with error 2 — and it seems not right away but only when VsCoq actually sends text.

[4ever2]

This might be related to https://coq.zulipchat.com/#narrow/stream/237662-VsCoq-devs-.26-users/topic/Coq.20in.20VS.20Code Setting the bin path to /snap/coq-prover/current/coq-platform/2022-04-1/bin/ rather than /snap/bin/ solves the issue on my machine.

[Blaisorblade]

Thanks for the find! At least that sounds like a work around.

@4ever2 Can you try giving the Coq snap permission to access files? https://snapcraft.io/docs/home-interface suggests this might not be automatically enabled.

• Could you report the output from snap connections coq-prover
• Could you test if snap connect coq-prover:home :home makes a difference?

Enrico wrote that this

• it's not related to snap confinement models, since code is in classic mode (not really confined) and apparently to connect to localhost one does not need the network plug, so my patch above is useless

But IIUC Coq is a confined snap, and file access via the home plug is not "automatically connected".

EDIT: links for (my) references:

• https://github.com/coq/platform/blob/2021.02/linux/snap/snapcraft.yaml.in has the snap config
• https://forum.snapcraft.io/search?q=coq-prover%20category%3A19 has snap store requests, nothing about home there (but maybe it's elsewhere).

[4ever2]

• Could you report the output from snap connections coq-prover

Permission for home is included in the output and is also specified in the snap config https://github.com/coq/platform/blob/7c6c45e52a4bbf48174f6089e660c383f55bbbd7/linux/snap/snapcraft.yaml.in#L61

• Could you test if snap connect coq-prover:home :home makes a difference?

This doesn't make any difference.

Something that is worth noting is that this problem only occurs if both Coq and VSCode were installed through snap. I believe that this isn't a VsCoq problem but rather a more general problem with snap/NodeJS (maybe related https://bugs.launchpad.net/ubuntu/+source/snapd/+bug/1849753).

[Blaisorblade]

@4ever2 How familiar are you with strace/ltrace? I wonder what coqidetop is doing when it's being terminated, and if it could stop doing that — based on your linked report, it might be violating the sandbox restrictions, and if that's the specific problem, it might just be "printing to stdout".

After all, it's possible coqidetop used to not run into this problem — around 8.13 @gares reproduced the problem and (IIUC) fixed it by ignoring coqtop failures (https://github.com/coq-community/vscoq/issues/221#issuecomment-802132705); but too many moving components to be 100% sure, especially since the theory was "classic snaps have no confinement".

[4ever2]

@Blaisorblade I don't have much experience with strace or ltrace. I can try looking at it tomorrow.

coqidetop and coqtop both exit with error code 2 without writing anything to stdout. AppArmor log:

[  293.879691] audit: type=1400 audit(1674690564.754:97): apparmor="DENIED" operation="file_inherit" profile="/snap/core/14447/usr/lib/snapd/snap-confine" pid=2498 comm="snap-confine" family="unix" sock_type="stream" protocol=0 requested_mask="send receive" denied_mask="send receive" addr=none peer_addr=none
[  293.880095] audit: type=1400 audit(1674690564.754:98): apparmor="DENIED" operation="file_inherit" profile="/snap/core/14447/usr/lib/snapd/snap-confine" pid=2498 comm="snap-confine" family="unix" sock_type="stream" protocol=0 requested_mask="send receive" denied_mask="send receive" addr=none peer_addr=none
[  293.880097] audit: type=1400 audit(1674690564.754:99): apparmor="DENIED" operation="file_inherit" profile="/snap/core/14447/usr/lib/snapd/snap-confine" pid=2498 comm="snap-confine" family="unix" sock_type="stream" protocol=0 requested_mask="send receive" denied_mask="send receive" addr=none peer_addr=none
[  293.880098] audit: type=1400 audit(1674690564.754:100): apparmor="DENIED" operation="file_inherit" profile="/snap/core/14447/usr/lib/snapd/snap-confine" name="/home/ubuntu/.config/Code/logs/20230126T004732/window1/exthost/extensionTelemetry.log" pid=2498 comm="snap-confine" requested_mask="a" denied_mask="a" fsuid=1000 ouid=1000
[  293.880099] audit: type=1400 audit(1674690564.754:101): apparmor="DENIED" operation="file_inherit" profile="/snap/core/14447/usr/lib/snapd/snap-confine" name="/home/ubuntu/.config/Code/logs/20230126T004732/window1/exthost/exthost.log" pid=2498 comm="snap-confine" requested_mask="a" denied_mask="a" fsuid=1000 ouid=1000
[  294.029838] audit: type=1400 audit(1674690564.902:102): apparmor="DENIED" operation="file_inherit" profile="snap-update-ns.coq-prover" name="/apparmor/.null" pid=2522 comm="5" requested_mask="wr" denied_mask="wr" fsuid=0 ouid=0
[  294.029841] audit: type=1400 audit(1674690564.902:103): apparmor="DENIED" operation="file_inherit" profile="snap-update-ns.coq-prover" name="/apparmor/.null" pid=2522 comm="5" requested_mask="wr" denied_mask="wr" fsuid=0 ouid=0
[  294.029843] audit: type=1400 audit(1674690564.902:104): apparmor="DENIED" operation="file_inherit" profile="snap-update-ns.coq-prover" name="/apparmor/.null" pid=2522 comm="5" requested_mask="wr" denied_mask="wr" fsuid=0 ouid=0
[  294.029845] audit: type=1400 audit(1674690564.902:105): apparmor="DENIED" operation="file_inherit" profile="snap-update-ns.coq-prover" name="/snap/code/117/usr/share/code/v8_context_snapshot.bin" pid=2522 comm="5" requested_mask="r" denied_mask="r" fsuid=0 ouid=0
[  294.029846] audit: type=1400 audit(1674690564.902:106): apparmor="DENIED" operation="file_inherit" profile="snap-update-ns.coq-prover" name="/apparmor/.null" pid=2522 comm="5" requested_mask="wr" denied_mask="wr" fsuid=0 ouid=0