search

coq / platform

Multi platform setup for Coq, Coq libraries and tools
Creative Commons Zero v1.0 Universal
189 stars 50 forks source link

snap-installed Coq Platform does not work in emacs/ProofGeneral #361

Open RalfJung opened 1 year ago

RalfJung commented 1 year ago

I'm considering using the Coq Platform for a course, but I am running into a problem with emacs/ProofGeneral. While coqc works perfectly fine on the terminal, when it is invoked from emacs I get error messages:

coqdep -Q /home/r/Dokumente/Unisachen/teaching/2023-ffpl/material/coq/Autosubst Autosubst -Q /home/r/Dokumente/Unisachen/teaching/2023-ffpl/material/coq/theories/lib semantics.lib -Q /home/r/Dokumente/Unisachen/teaching/2023-ffpl/material/coq/theories/type_systems semantics.ts /tmp/ProofGeneral-coqf1TfY9.v
*** Error: /tmp/ProofGeneral-coqf1TfY9.v: No such file or directory

I think what is happening is that emacs puts some temporary files into /tmp, but snap applies some form of isolation and so the coqc inside the snap cannot see those files. Is there a known (easy) solution for this?

MSoegtropIMC commented 1 year ago

I can see if I can do something about the snap to enable /tmp folder access. This whole snap mechanisms still seems to be a bit experimental (e.g. on my Linux machine I can't open local HTML files using the firefox snap).

Two suggestions:

1.) change the TMP variable to something in your user folder - the coq tools should have access there.

2.) not use the snap wrappers (under /snap/bin afair), but put the snap installation bin folder for Coq Platform directly into the PATH (also somewhere under /snap, but I don't remember the exact path). This also has the advantage that you get all Coq tools with original name. If this works depends on if the system shared libraries of your Ubuntu version are compatible with the snap base version. I am trying this regularly with 20.04 and 22.04 and so far didn't have any issues, but it is a hack and not guaranteed to work.

RalfJung commented 1 year ago

Thanks for the quick reply! Indeed, setting PATH="/snap/coq-prover/31/coq-platform/bin:$PATH" helps, good to know. But I am a bit concerned that that might be too fragile.

Setting TMP=~/tmp also works. That's better, and I can set temporary-file-directory in emacs to not have to change the environment.

MSoegtropIMC commented 1 year ago

Fine that you have a solution - I anyway try to fix both issues in an update.

"The hack" is used by some people in CI setups and I haven't heard anything negative so far, but indeed this might be much more appropriate in a controlled environment like CI than for a course. On the other hand a lot of commercial / proprietary Linux software is installed in a quite similar way (not using snap but making certain assumptions about shared library versions). I am not that deep in this aspects of Linux, but I think this is done in Linux in a relatively robust way via symlinks between upwards compatible libraries, so it might work stable. Some people even use it on non Ubuntu systems which don't have snap by extracting the snap package to a folder. If there are sufficiently many successful tests of "the hack" I might just document it. Feedback on the stability of this is welcome, since it offers a "second use" for the snap.

There is btw a symlink to the latest version - afair it is x instead of the 31 in your path above. If you share this, you should use this latest version symlink path.