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

harashimahashi · 2021-03-17T23:49:00Z

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

The text was updated successfully, but these errors were encountered:

fakusb · 2021-03-18T12:23:34Z

"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 · 2021-03-18T13:01:36Z

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

harashimahashi · 2021-03-18T13:07:16Z

"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 · 2021-03-18T13:08:17Z

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 · 2021-03-18T13:19:54Z

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 · 2021-03-18T13:23:00Z

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 · 2021-03-18T14:34:51Z

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 coq/platform#93 should be merged followed by a full CI run (including the upload to the store)

gares · 2021-03-18T15:32:33Z

it does not work (yet)

gares · 2021-03-18T15:42:03Z

Unfortunately it seems an open problem canonical/snapd#8699

gares · 2021-03-18T17:11:17Z

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 · 2021-03-18T17:25:52Z

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 · 2021-03-18T17:42:24Z

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

gares · 2021-03-18T18:29:05Z

@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 · 2021-03-19T10:45:31Z

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 · 2021-04-02T14:05:47Z

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 · 2021-04-02T15:12:49Z

I think the easiest workaround is to install the hacked vsix as per #53

gares · 2021-04-02T15:15:34Z

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 · 2021-04-02T15:57:57Z

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

fakusb · 2021-04-06T13:24:06Z

@Zimmi48 I will publish this hotfix asap

Zimmi48 · 2021-04-06T13:28:35Z

Thanks!

Hotfix for #221

fakusb · 2021-04-06T15:19:44Z

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

Zimmi48 · 2021-04-06T17:19:28Z

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

karunasagark · 2023-01-06T07:12:46Z

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 · 2023-01-07T09:53:01Z

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 · 2023-01-07T13:48:17Z

Wait I must be missing something: shouldn't the existing patch be included in 0.3.6 from last January?
And indeed, MR coq/vscoq#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 · 2023-01-08T01:10:14Z

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 · 2023-01-08T04:49:42Z

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 · 2023-01-23T13:10:41Z

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 · 2023-01-25T20:36:37Z

@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 (#53); but too many moving components to be 100% sure, especially since the theory was "classic snaps have no confinement".

4ever2 · 2023-01-26T00:23:46Z

@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

Zimmi48 · 2024-10-11T16:37:34Z

The Snap package is being retired, so perhaps this issue can be closed.

Zimmi48 changed the title ~~Cannot interpret coq file on ubuntu~~ Cannot interpret coq file on ubuntu with Coq and VsCode installed through Snap. Mar 18, 2021

gares mentioned this issue Mar 18, 2021

grant coqidetop.top network access coq/platform#93

Closed

fakusb referenced this issue in fakusb/vscoq Apr 6, 2021

hotfix for #221

e4070a0

fakusb mentioned this issue Apr 6, 2021

Hotfix for #221 coq/vscoq#223

Merged

fakusb closed this as completed in coq/vscoq#223 Apr 6, 2021

fakusb referenced this issue in coq/vscoq Apr 6, 2021

Merge pull request #223 from fakusb/hotfix221

a302529

Hotfix for #221

fakusb reopened this Apr 6, 2021

fakusb closed this as completed Apr 6, 2021

fakusb reopened this Apr 6, 2021

gares transferred this issue from coq/vscoq Oct 10, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

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

harashimahashi commented Mar 17, 2021

fakusb commented Mar 18, 2021 •

edited

Loading

Zimmi48 commented Mar 18, 2021

harashimahashi commented Mar 18, 2021 •

edited

Loading

harashimahashi commented Mar 18, 2021

gares commented Mar 18, 2021

harashimahashi commented Mar 18, 2021

gares commented Mar 18, 2021

gares commented Mar 18, 2021

gares commented Mar 18, 2021

gares commented Mar 18, 2021 •

edited

Loading

gares commented Mar 18, 2021 •

edited

Loading

harashimahashi commented Mar 18, 2021

gares commented Mar 18, 2021 •

edited

Loading

fakusb commented Mar 19, 2021

ztatlock commented Apr 2, 2021

gares commented Apr 2, 2021

gares commented Apr 2, 2021 •

edited

Loading

Zimmi48 commented Apr 2, 2021

fakusb commented Apr 6, 2021 •

edited

Loading

Zimmi48 commented Apr 6, 2021

fakusb commented Apr 6, 2021

Zimmi48 commented Apr 6, 2021

karunasagark commented Jan 6, 2023 •

edited

Loading

thery commented Jan 7, 2023

Blaisorblade commented Jan 7, 2023

4ever2 commented Jan 8, 2023 •

edited

Loading

Blaisorblade commented Jan 8, 2023 •

edited

Loading

4ever2 commented Jan 23, 2023

Blaisorblade commented Jan 25, 2023

4ever2 commented Jan 26, 2023

Zimmi48 commented Oct 11, 2024

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

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

Comments

harashimahashi commented Mar 17, 2021

fakusb commented Mar 18, 2021 • edited Loading

Zimmi48 commented Mar 18, 2021

harashimahashi commented Mar 18, 2021 • edited Loading

harashimahashi commented Mar 18, 2021

gares commented Mar 18, 2021

harashimahashi commented Mar 18, 2021

gares commented Mar 18, 2021

gares commented Mar 18, 2021

gares commented Mar 18, 2021

gares commented Mar 18, 2021 • edited Loading

gares commented Mar 18, 2021 • edited Loading

harashimahashi commented Mar 18, 2021

gares commented Mar 18, 2021 • edited Loading

fakusb commented Mar 19, 2021

ztatlock commented Apr 2, 2021

gares commented Apr 2, 2021

gares commented Apr 2, 2021 • edited Loading

Zimmi48 commented Apr 2, 2021

fakusb commented Apr 6, 2021 • edited Loading

Zimmi48 commented Apr 6, 2021

fakusb commented Apr 6, 2021

Zimmi48 commented Apr 6, 2021

karunasagark commented Jan 6, 2023 • edited Loading

thery commented Jan 7, 2023

Blaisorblade commented Jan 7, 2023

4ever2 commented Jan 8, 2023 • edited Loading

Blaisorblade commented Jan 8, 2023 • edited Loading

4ever2 commented Jan 23, 2023

Blaisorblade commented Jan 25, 2023

4ever2 commented Jan 26, 2023

Zimmi48 commented Oct 11, 2024

fakusb commented Mar 18, 2021 •

edited

Loading

harashimahashi commented Mar 18, 2021 •

edited

Loading

gares commented Mar 18, 2021 •

edited

Loading

gares commented Mar 18, 2021 •

edited

Loading

gares commented Mar 18, 2021 •

edited

Loading

gares commented Apr 2, 2021 •

edited

Loading

fakusb commented Apr 6, 2021 •

edited

Loading

karunasagark commented Jan 6, 2023 •

edited

Loading

4ever2 commented Jan 8, 2023 •

edited

Loading

Blaisorblade commented Jan 8, 2023 •

edited

Loading