Stream: VsCoq devs & users

Topic: Snap


view this post on Zulip Maxime Dénès (Jan 23 2023 at 07:29):

Hi there! The issue of using VsCoq with Coq installed via Snap was mentioned to me more than once at POPL. I read https://github.com/coq-community/vscoq/issues/221 but it is still not completely clear to me what the current status is. @Enrico Tassi @Laurent Théry do you know more? What is still to be done?

view this post on Zulip Karl Palmskog (Jan 23 2023 at 07:35):

@Maxime Dénès the issue is likely not in VsCoq but in the Snap itself, as evidenced by this topic, where a user could use the non-sandboxed binaries just fine with VsCoq. However, this requires using a binary path that changes with every Snap release.

view this post on Zulip Michael Soegtrop (Jan 23 2023 at 07:57):

I mostly maintain snap now. To my best knowledge the snap binaries should be usable directly from the snap install location (not via the shortcuts). This has to do with the hacks I did to OCamlfind.

view this post on Zulip Michael Soegtrop (Jan 23 2023 at 07:57):

(This is new in 2022.09)

view this post on Zulip Karl Palmskog (Jan 23 2023 at 08:18):

@Michael Soegtrop yes, they can be executed directly from the snap install location. But the point is that when you run a binary via /snap/, it gets sandboxed, and for some reason VsCoq fails to use the sandboxed binary. The non-sandboxed binary, which lives in another location, works fine.

view this post on Zulip Maxime Dénès (Jan 23 2023 at 08:37):

Do we know why VsCoq doesn't work with the sandboxed binary?

view this post on Zulip Paolo Giarrusso (Jan 23 2023 at 09:28):

@Michael Soegtrop do you know if the Coq snap has applied for home permission? https://github.com/coq-community/vscoq/issues/221#issuecomment-1374708486

view this post on Zulip Enrico Tassi (Jan 23 2023 at 09:30):

I don't know why it doesn't work, I had no time to investigate this.

view this post on Zulip Paolo Giarrusso (Jan 23 2023 at 13:18):

Something that is worth noting is that this problem only occurs if both Coq and VSCode were installed through snap.

view this post on Zulip Paolo Giarrusso (Jan 23 2023 at 13:19):

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).

I haven't verified, but this is from contributor @4ever2 and they're pretty good

view this post on Zulip Karl Palmskog (Jan 23 2023 at 13:20):

unfortunately this is a very common use case (both from snap)

view this post on Zulip Karl Palmskog (Jan 23 2023 at 13:24):

ah, and it might be due to the VS Code snap using the classic sandboxing

view this post on Zulip Karl Palmskog (Jan 23 2023 at 13:49):

and also, doesn't this mean it affects every VS Code extension for Coq? ping @Emilio Jesús Gallego Arias that Coq-LSP can likely not be run via Coq Snap without the non-sandboxed path workaround (when VS Code is installed via Snap)

view this post on Zulip Emilio Jesús Gallego Arias (Jan 23 2023 at 14:10):

@Karl Palmskog I don't know, but yes, in principle coq-lsp will need access to the workspace to load .vo files, read _CoqProject, etc...

view this post on Zulip Michael Soegtrop (Jan 23 2023 at 15:11):

@
Paolo Giarrusso said:

Michael Soegtrop do you know if the Coq snap has applied for home permission? https://github.com/coq-community/vscoq/issues/221#issuecomment-1374708486

As far as I understand this, these lines should do it (https://github.com/coq/platform/blob/2397a58954ca2a8f4861c8333bd66ef21fc9a6d0/linux/snap/snapcraft.yaml.in#L81).

But if you start it directly from the install directory, it doesn't matter, since you don't go through the sandbox wrapper.

view this post on Zulip Michael Soegtrop (Jan 23 2023 at 15:14):

Paolo Giarrusso said:

Something that is worth noting is that this problem only occurs if both Coq and VSCode were installed through snap.

Although afaik @Enrico Tassi thinks it is a (bad ?) hack, I would recommend try to start coq via the snap installation directory without the sandbox if you have issues. The reason I implemented support for this is exactly to get around such issues.

view this post on Zulip Maxime Dénès (Jan 23 2023 at 15:16):

But can VsCoq guess this path, so that it works out of the box?

view this post on Zulip Karl Palmskog (Jan 23 2023 at 15:17):

the problem with using the directory of binaries without the sandbox is that it changes with every Snap release. So if you update your Snap for Coq, the unsandboxed binaries are suddenly somewhere else

view this post on Zulip Michael Soegtrop (Jan 23 2023 at 15:17):

@Maxime Dénès : the path to the latest installed version is fixed. I am on Mac right now, so I can't look it up ...

view this post on Zulip Michael Soegtrop (Jan 23 2023 at 15:18):

@Karl Palmskog : there is symlink called "x" in the release folder - this is always the latest.

view this post on Zulip Michael Soegtrop (Jan 23 2023 at 15:18):

Let me boot up my Linux machine ...

view this post on Zulip Maxime Dénès (Jan 23 2023 at 15:18):

Ah ok, maybe that's the bit we were missing.

view this post on Zulip Karl Palmskog (Jan 23 2023 at 15:21):

ah, it seems like in the latest snap, you can actually get a version-independent path like this:

/snap/coq-prover/current/coq-platform/bin/

view this post on Zulip Michael Soegtrop (Jan 23 2023 at 15:22):

The path to the latest version should be "/snap/coq-prover/current/coq-platform/bin/coqc" modulo typos

view this post on Zulip Karl Palmskog (Jan 23 2023 at 15:22):

but this path is not available in previous snaps, as far as I can see

view this post on Zulip Michael Soegtrop (Jan 23 2023 at 15:22):

Well in previous versions (before 2022.09.0) it anyway doesn't work.

view this post on Zulip Michael Soegtrop (Jan 23 2023 at 15:23):

But I don't quite see why this path shouldn't be available ...

view this post on Zulip Michael Soegtrop (Jan 23 2023 at 15:24):

I just darkly remember that it was "x" instead of "current" at some point ...

view this post on Zulip Karl Palmskog (Jan 23 2023 at 15:24):

for me, VsCoq worked fine with the following path on 2022.04.1: /snap/coq-prover/30/coq-platform/2022-04-1/bin/

view this post on Zulip Karl Palmskog (Jan 23 2023 at 15:24):

but:

$ sudo snap refresh coq-prover --channel=2022.04/stable
coq-prover (2022.04/stable) 2022-04-1 from Coq Development Team (coq-team) refreshed
$ ls -l /snap/coq-prover/current/coq-platform/bin/
ls: cannot access '/snap/coq-prover/current/coq-platform/bin/': No such file or directory

view this post on Zulip Michael Soegtrop (Jan 23 2023 at 15:25):

Ah yes, I removed this version path

view this post on Zulip Michael Soegtrop (Jan 23 2023 at 15:25):

(to make it easier to find)

view this post on Zulip Michael Soegtrop (Jan 23 2023 at 15:25):

This changed in 2022.09.0

view this post on Zulip Michael Soegtrop (Jan 23 2023 at 15:26):

I could produce updated snaps for the old versions ...

view this post on Zulip Michael Soegtrop (Jan 23 2023 at 15:27):

What is the general view on using sandbox links vs. the above paths for command line tools?

view this post on Zulip Michael Soegtrop (Jan 23 2023 at 15:28):

IMHO the sandbox links are nice for coqide, but otherwise not terribly useful, since e.g. the names are different.

view this post on Zulip Karl Palmskog (Jan 23 2023 at 15:30):

isn't the big thing with sandbox links that they show up in the user's $PATH?

view this post on Zulip Karl Palmskog (Jan 23 2023 at 15:31):

I think it might be enough if we tell everyone who wants to use Snap Coq + Snap VS Code to update to 2022.09 Coq Snap and use /snap/coq-prover/current/coq-platform/bin/ (inside VS Code) and it will keep working.

view this post on Zulip Michael Soegtrop (Jan 23 2023 at 15:38):

Well IMHO it is less work to add this to the path than to change the tool names in all my scripts. So, yes I would recommend to use the path you give.

As I said, if it helps I could update the older snaps to use the same path if this helps someone.

view this post on Zulip Karl Palmskog (Jan 23 2023 at 15:40):

but I don't understand why we'd need to change anything in the Snap with this approach. We want people to use the sandboxed binaries by default, right? It's only because of this interaction issue between the VS Code snap and other snaps that this path to unsandboxed binaries is needed.

view this post on Zulip Paolo Giarrusso (Jan 23 2023 at 16:13):

wanted to write: can I suggest moving this to github so to involve @4ever2 better?

view this post on Zulip Paolo Giarrusso (Jan 23 2023 at 16:15):

at least for the thread about "why's the sandbox interfering"

view this post on Zulip Michael Soegtrop (Jan 23 2023 at 18:11):

@Karl Palmskog : I personally don't use the sanbox links for command line tools (I use it for CoqIDE), simply because I am too lazy to adjust the make files. Also is e.g. dune compatible with the sandbox names?

view this post on Zulip Karl Palmskog (Jan 23 2023 at 18:16):

I may be missing something about the Snap technicalities, but when I do sudo snap install coq-prover, I get a bunch of sandboxed stuff in /snap/bin. If there is no opam stuff in the way, I'd get coqc from /snap/bin.

view this post on Zulip Karl Palmskog (Jan 23 2023 at 18:18):

so then I'd get that coqc with make files and similar

view this post on Zulip Michael Soegtrop (Jan 23 2023 at 18:29):

@Karl Palmskog : ah yes, there is a short list of aliases - I keep forgetting this. My issue is that I am regularly using more binaries, like menhir or gappa.

view this post on Zulip Karl Palmskog (Jan 23 2023 at 18:30):

right, and most users are not using stuff like gappa, menhir, etc., they just want to go from 0 to basic Coq setup, which is essentially what /snap/bin provides

view this post on Zulip Karl Palmskog (Jan 23 2023 at 21:28):

OK, I can confirm that setting /snap/coq-prover/current/coq-platform/bin/ under "Coqtop: bin path" in VsCoq settings just works with latest Snaps.

view this post on Zulip Karl Palmskog (Jan 23 2023 at 21:29):

rather than hoping for an old Snap --classic bug to be fixed, that seems the best approach to document and support going forward...

view this post on Zulip Michael Soegtrop (Jan 24 2023 at 08:14):

@Karl Palmskog : do you think it would make sense to update 1 or 2 older snaps? It would not be much work and in the end we have all the different tracks to do this.

view this post on Zulip Karl Palmskog (Jan 24 2023 at 08:51):

if it doesn't take too much time to update, sure. But I think most people using snaps will be on the latest one.

view this post on Zulip Michael Soegtrop (Jan 24 2023 at 08:53):

@Enrico Tassi : what is your opinion on the "update snap for old Coq versions" question?

view this post on Zulip Karl Palmskog (Jan 24 2023 at 08:54):

I think the Snap tracks explicitly permit this? If you update, there will just be a new 2022.04/stable, etc. and people who follow that track will get that.

view this post on Zulip Théo Zimmermann (Jan 24 2023 at 09:59):

Karl Palmskog said:

if it doesn't take too much time to update, sure. But I think most people using snaps will be on the latest one.

Don't we even have stats for which versions people are using?

view this post on Zulip Théo Zimmermann (Jan 24 2023 at 10:00):

Karl Palmskog said:

rather than hoping for an old Snap --classic bug to be fixed, that seems the best approach to document and support going forward...

Could VsCoq be adapted to even automatically try to find coqtop under this directory?

view this post on Zulip Enrico Tassi (Jan 24 2023 at 15:58):

@Michael Soegtrop sorry, I'm still on and off. I'm sure I get what you propose as a fix, here the discussion suggests a workaround "on the UI side". Am I missing something? (yes, we can update old snaps; x is for snap installed via a file, if you get it from the store you get a number)

view this post on Zulip Michael Soegtrop (Jan 24 2023 at 16:16):

@Enrico Tassi : the question is if changing the folder structure is possibly annoying to some people.

view this post on Zulip Enrico Tassi (Jan 24 2023 at 16:39):

Oh, I see. Do we really need to change it, or a symlink (to hide the platform version number) would do?

view this post on Zulip Enrico Tassi (Jan 24 2023 at 16:41):

IMO the only API of a snap is in /snap/bin, I don't consider calling binaries from /snap/$p/$v/ a supported feature of snap (of course if it is a workaround it's fine). If you need to access other binaries, imo you should either export them or export a single wrapper (I think these is already one for debugging) to dispatch to them.

view this post on Zulip Karl Palmskog (Jan 24 2023 at 16:43):

if we can only rely on /snap/bin, then it can't work, since the problem is that sandboxing breaks interaction between VS Code and Coq.

view this post on Zulip Karl Palmskog (Jan 24 2023 at 16:44):

the bug pointed to above (--classic install of VS Code via snap) has been open since 2019 and likely will not go away anytime soon

view this post on Zulip Karl Palmskog (Jan 24 2023 at 16:45):

the change discussed here was about whether we can have a consistent symlink/path to the non-sandboxed binaries

view this post on Zulip Karl Palmskog (Jan 24 2023 at 16:46):

I'm guessing that "exporting" a binary means sandboxing at the user level

view this post on Zulip Michael Soegtrop (Jan 24 2023 at 17:18):

@Enrico Tassi : well if doing anything directly with what is in the snap has never been encouraged, I think it shouldn't hurt to change it. I wouldn't like to add a symlink, since this would also affect new snaps then. I think the options are rebuild the snap with the current generator or leave it as is.

view this post on Zulip Enrico Tassi (Jan 24 2023 at 20:30):

I suggested a symlink to not break old code, but indeed I think relying on the layout of the files in the snap has never been encouraged so we can just ignore the potential breakage and go ahead and rebuild.

view this post on Zulip Enrico Tassi (Jan 24 2023 at 20:34):

Karl Palmskog said:

if we can only rely on /snap/bin, then it can't work, since the problem is that sandboxing breaks interaction between VS Code and Coq.

I agree, but I see the fix (of using unsandboxed binaries) as a workaround. In some sense I would not document/advice it for other binaries (unless they have the same problem). Example: if you want to use/export menhir, we export it as sandboxed (either directly or via a single bridge for all of the binaries, eg /snap/bin/coq-prover.exec menhir)

view this post on Zulip Enrico Tassi (Jan 24 2023 at 20:37):

What I'd like to avoid is to have users export PATH=/snap/coq-prover/current/bin:$PATH unless we document what is in there. I mean, we may have a different version of make/dune/menhir/z3... and that could be confusing

view this post on Zulip Paolo Giarrusso (Jan 24 2023 at 22:28):

From the present symptoms, we just want that extra path in VsCoq's configuration, ideally by autodetection

view this post on Zulip Michael Soegtrop (Jan 25 2023 at 09:13):

@Enrico Tassi : I think the problem with sandbox exporting is that one needs approval from the snap team to export it without prefix, and I don't think they will allow us to export say 20 binaries without prefix. Also the sandbox comes with some overhead. I don't quite see why one shouldn't document both ways - sandoxed and non sandboxed and describe the pros and cons.

view this post on Zulip Karl Palmskog (Jan 25 2023 at 09:18):

we should be able to say something like:

view this post on Zulip Michael Soegtrop (Jan 25 2023 at 09:23):

I will then regenerate the snaps for older Coq (Platform) versions with the current generator - also as an exercise to see how this goes.

view this post on Zulip Enrico Tassi (Jan 25 2023 at 09:47):

I'm fine documenting them, but I'm just saying that I did not see anywhere in the snap doc that the place where the image of a snap is unpacked is /snap/program/current/ and that its dependency snaps are bind-mounted in there. It seems a (reasonable) implementation detail, but they could change it.

What I mean is that "non sanboxed .." is not something the snap system sells as a feature/API, as far as I know (unless you use --classic). In a sense, I'd prefer coq-prover to come in classic mode (as vscode) if that fixes the problem. We can ask for it, but I don't know which are the requirements.

view this post on Zulip Enrico Tassi (Jan 25 2023 at 09:49):

Anyway, I'm not against it, it fixes a problem in an easy way, so go ahead.

view this post on Zulip Laurent Théry (Jan 25 2023 at 10:13):

who is in charge of the snap coq-prover?

view this post on Zulip Michael Soegtrop (Jan 25 2023 at 10:14):

@Laurent Théry : Enrico originally created it and I maintain it now.

view this post on Zulip Laurent Théry (Jan 25 2023 at 10:15):

would it be possible to update it to a classic confinement to see if this solves the issue?

view this post on Zulip Karl Palmskog (Jan 25 2023 at 10:54):

right apparently --classic needs special permission:

Warning: flag --classic ignored for strictly confined snap coq-prover

Do we have any way to test without going through the bureaucracy?

view this post on Zulip Karl Palmskog (Jan 25 2023 at 10:56):

if the unsandboxed stuff is completely unsupported and may break going forward, then we might consider cutting down the Snap so that all that is included comes in /snap/bin...

view this post on Zulip Paolo Giarrusso (Jan 25 2023 at 11:23):

"both programs in classic mode" seems unlikely to make things better. In fact, all we know is that both sandboxes are required to trigger the problem.

view this post on Zulip Paolo Giarrusso (Jan 25 2023 at 11:25):

And then we have a bug report about classic-to-classic mode which might or might not apply, specifically, but which points to a general problem: snap might be placing coq and vscoq in separate sandboxes by default, and it'd need a new feature to allow for exceptions

view this post on Zulip Paolo Giarrusso (Jan 25 2023 at 11:30):

Also, that specific bug report is about inherited file descriptors. Basically, the sandbox will prevent the called programs from using stdin/stdout/stderr, which explains why coqc --version always failed; the code can work around that, but (later?) maybe coqidetop started failing because it started using stdin/stdout/stderr in addition to the socket connection

view this post on Zulip Eske Nielsen (Jan 25 2023 at 13:15):

Building coq-prover in classic mode doesn't solve the issue. In fact, coq-prover won't build in classic mode because coqide depends on gnome-3-28 which uses strict confinement.

view this post on Zulip Michael Soegtrop (Jan 25 2023 at 13:37):

IMHO the probability that snap changes the layout every other release is rather small. They might change it every 5 years, and I guess we can handle this.
Btw.: as far as I can see the Coq Platform snap can access the home folder - the VSCoq config file should be in there. How about adding a script to adjust the VSCoq configuration in home?

view this post on Zulip Théo Zimmermann (Jan 25 2023 at 13:43):

That seems pretty invasive to me. What about the opposite: adding logic to VsCoq to detect that Coq was installed via Snap?

view this post on Zulip Michael Soegtrop (Jan 25 2023 at 13:54):

I mean I would supply a script the user can run or not. I have no idea how flexible VSCode is in running scripts to determine default settings.

view this post on Zulip Paolo Giarrusso (Jan 25 2023 at 15:49):

we'd have to think about running a _script_ — are there even security implications? — but hardcoding extra logic in vscoq itself seems easier:
https://github.com/coq-community/vscoq/blob/4b9197e297345cf213d9043d411733312ef79bfc/client/src/CoqDocument.ts#L299-L341

view this post on Zulip Paolo Giarrusso (Jan 25 2023 at 15:50):

I haven't volunteered because I'm away, but as long as you don't try to "simplify" the code, it's probably easy to extend the logic.

view this post on Zulip Paolo Giarrusso (Jan 25 2023 at 15:51):

as in, I can't _really_ program TypeScript specifically and I think I could do it

view this post on Zulip Paolo Giarrusso (Jan 25 2023 at 15:53):

(now, simplifying that code might also be desirable, but IIRC many reasonable simplifications would break some scenarios — at least that's what I remember from reviewing changes there)

view this post on Zulip Paolo Giarrusso (Jan 25 2023 at 15:54):

easy _in VsCode_, that is

view this post on Zulip Paolo Giarrusso (Jan 25 2023 at 15:56):

negotiating the _right_ business logic to add remains tricky

view this post on Zulip Enrico Tassi (Jan 25 2023 at 16:01):

Paolo Giarrusso said:

"both programs in classic mode" seems unlikely to make things better. In fact, all we know is that both sandboxes are required to trigger the problem.

I'm a bit lost, vscode is not sandboxed.

view this post on Zulip Enrico Tassi (Jan 25 2023 at 16:01):

I mean, it is in classic mode (some snaps, with the agreement of the store, come in classic mode).

view this post on Zulip Karl Palmskog (Jan 25 2023 at 16:04):

isn't AppArmor involved even in classic mode? The bug report seems to indicate this...

view this post on Zulip Paolo Giarrusso (Jan 25 2023 at 16:22):

yes, the evidence is that the problem _only_ shows up when _both_ programs are sandboxed

view this post on Zulip Paolo Giarrusso (Jan 25 2023 at 16:27):

_and_ the bug report specifically says "if two programs are classic snaps, snap considers them as living in separate sandboxes and interferes; _in this case_ you'd want to allow a more flexible policy but we don't have code for it"

view this post on Zulip Enrico Tassi (Jan 25 2023 at 20:04):

Thanks, I did not get it. So classic mode is not an option, sorry for insisting on it.

view this post on Zulip Paolo Giarrusso (Jan 25 2023 at 20:29):

FWIW, I wonder if a non-classic VsCode would help, but no idea if it's worth speculating.

view this post on Zulip Karl Palmskog (Jan 25 2023 at 20:32):

is non-classic VS Code even possible? Even VSCodium uses classic.

view this post on Zulip Paolo Giarrusso (Jan 25 2023 at 20:39):

no idea it'd help, but if it did at least we could ask VsCode?
Enrico found https://github.com/snapcore/snapd/pull/8699 "interfaces/desktop-launch: support confined snaps launching other snaps". Does "confined" mean "non-classic snaps"?


Last updated: Jun 13 2024 at 04:03 UTC