Maxime Dénès (Jan 23 2023 at 07:29): 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?
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.
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.
Michael Soegtrop (Jan 23 2023 at 07:57):(This is new in 2022.09)
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.
Maxime Dénès (Jan 23 2023 at 08:37):Do we know why VsCoq doesn't work with the sandboxed binary?
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
Enrico Tassi (Jan 23 2023 at 09:30):I don't know why it doesn't work, I had no time to investigate this.
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.
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
Karl Palmskog (Jan 23 2023 at 13:20):unfortunately this is a very common use case (both from snap)
Karl Palmskog (Jan 23 2023 at 13:24):ah, and it might be due to the VS Code snap using the classic sandboxing
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)
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...
Michael Soegtrop (Jan 23 2023 at 15:11):@
Paolo Giarrusso said:
Michael Soegtrop do you know if the Coq snap has applied for
homepermission? 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.
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.
Maxime Dénès (Jan 23 2023 at 15:16):But can VsCoq guess this path, so that it works out of the box?
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
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 ...
Michael Soegtrop (Jan 23 2023 at 15:18):@Karl Palmskog : there is symlink called "x" in the release folder - this is always the latest.
Michael Soegtrop (Jan 23 2023 at 15:18):Let me boot up my Linux machine ...
Maxime Dénès (Jan 23 2023 at 15:18):Ah ok, maybe that's the bit we were missing.
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/
The path to the latest version should be "/snap/coq-prover/current/coq-platform/bin/coqc" modulo typos
Karl Palmskog (Jan 23 2023 at 15:22):but this path is not available in previous snaps, as far as I can see
Michael Soegtrop (Jan 23 2023 at 15:22):Well in previous versions (before 2022.09.0) it anyway doesn't work.
Michael Soegtrop (Jan 23 2023 at 15:23):But I don't quite see why this path shouldn't be available ...
Michael Soegtrop (Jan 23 2023 at 15:24):I just darkly remember that it was "x" instead of "current" at some point ...
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/
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
Ah yes, I removed this version path
Michael Soegtrop (Jan 23 2023 at 15:25):(to make it easier to find)
Michael Soegtrop (Jan 23 2023 at 15:25):This changed in 2022.09.0
Michael Soegtrop (Jan 23 2023 at 15:26):I could produce updated snaps for the old versions ...
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?
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.
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?
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.
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.
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.
Paolo Giarrusso (Jan 23 2023 at 16:13):wanted to write: can I suggest moving this to github so to involve @4ever2 better?
Paolo Giarrusso (Jan 23 2023 at 16:15):at least for the thread about "why's the sandbox interfering"
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?
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.
Karl Palmskog (Jan 23 2023 at 18:18):so then I'd get that coqc with make files and similar
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.
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
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.
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...
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.
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.
Michael Soegtrop (Jan 24 2023 at 08:53):@Enrico Tassi : what is your opinion on the "update snap for old Coq versions" question?
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.
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?
Théo Zimmermann (Jan 24 2023 at 10:00):Karl Palmskog said:
rather than hoping for an old Snap
--classicbug 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?
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)
Michael Soegtrop (Jan 24 2023 at 16:16):@Enrico Tassi : the question is if changing the folder structure is possibly annoying to some people.
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?
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.
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.
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
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
Karl Palmskog (Jan 24 2023 at 16:46):I'm guessing that "exporting" a binary means sandboxing at the user level
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.
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.
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)
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
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
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.
Karl Palmskog (Jan 25 2023 at 09:18):we should be able to say something like:
/snap/bin and are sandboxed, which provide additional local security guarantees (even though Platform maintainers audit packages) - these binaries do not work with VS Code installed via Snap/snap/coq-prover/current/bin, please add this to your path if you want access to them, or if you use VS Code, input this directory in extension settings 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.
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.
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.
Laurent Théry (Jan 25 2023 at 10:13):who is in charge of the snap coq-prover?
Michael Soegtrop (Jan 25 2023 at 10:14):@Laurent Théry : Enrico originally created it and I maintain it now.
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?
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?
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...
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.
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
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
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.
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?
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?
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.
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
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.
Paolo Giarrusso (Jan 25 2023 at 15:51):as in, I can't _really_ program TypeScript specifically and I think I could do it
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)
Paolo Giarrusso (Jan 25 2023 at 15:54):easy _in VsCode_, that is
Paolo Giarrusso (Jan 25 2023 at 15:56):negotiating the _right_ business logic to add remains tricky
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.
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).
Karl Palmskog (Jan 25 2023 at 16:04):isn't AppArmor involved even in classic mode? The bug report seems to indicate this...
Paolo Giarrusso (Jan 25 2023 at 16:22):yes, the evidence is that the problem _only_ shows up when _both_ programs are sandboxed
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"
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.
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.
Karl Palmskog (Jan 25 2023 at 20:32):is non-classic VS Code even possible? Even VSCodium uses classic.
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 04 2023 at 23:30 UTC