Andrey Klaus (Mar 24 2022 at 09:51): Andrey Klaus (Mar 24 2022 at 09:51):Hello all!
This is repost from pg-users.
I'm trying to use PG with remote coq compiler.
So, my host is 192.168.1.11 and host which I would like to use for compilation is 192.168.1.10.
I set up option proof-rsh-command to ssh 192.168.1.10 .
And when I do from terminal ssh 192.168.1.10 coqtop it runs coqtop as it is expected.
When I open my local .v , I have next problem during compilation:
Error: Cannot find a physical path bound to logical path matching suffix MyNameSpace.NS1.
on next string
Require Import MyNameSpace.NS1.Environment.
Among others I have next string in my _CoqProject file:
-R src MyNameSpace
I was trying to pass this -R to compiler using coq-prog-args but it didn't help.
I think it didn't help just because remote compiler does not have access to my local file system, so, it is kind of expected thing (but i'm not sure).
I'm not sure I understand how this process is going on: what compiler does when it needs the file.. in my vision it should ask PG for file, but I think it can search local file system by default..
As for using tramp mode, it looks to me like it calls local coqdep instead of remote one. and variable 'tramp-remote-path does not have an influence on this. Error is next one
coqdep -R /home/andrey/1/src MyNameSpace /tmp/ProofGeneral-coqJPQukp.v
Fatal error: exception Sys_error("/home/andrey/1/src: No such file or directory")
but there is such file on remote host and no such file on local host.
Erik Martin-Dorel (Mar 24 2022 at 23:28):Thanks @Andrey Klaus for your detailed question!
Tweaking coq-prog-args should be unnecessary provided you have a _CoqProject file.
Just to be sure, could you summarize your use case?
IIUC:
Is it so?
I Cc @Hendrik Tews which is more TRAMP-savvy than me (I use TRAMP a bit but not for PG)
At first sight, my very first guess is that:
C-x C-f /ssh:user@bigserver:/home/…/file.v RETcoqtop and coqdep, transparently… but not on your local file.proof-rsh-command should probably be set to nil for this use case.Hendrik, does this wrap-up looks good to you?
Meanwhile, feel free @Andrey Klaus to give a minimal working example, e.g., sharing a link to a GitHub public repo(?) or sharing it privately (FWIW, my GitHub login is @erikmd)
Andrey Klaus (Mar 25 2022 at 20:53):Thanks for the answer, @Erik Martin-Dorel !
Sorry, a bit messy description, saying truth. I will try to make it more clear.
My current setup is:
/home/andrey/mwe/1. coqc path is andrey@andrey:~$ which coqc
/storage/home_andrey_hidden/.opam/4.12.1/bin/coqc
coq-server.lan. There is the same coq project (so, copy of all files) on the coq-server. Local path for the project on the server is /home/andrey/mwe/2 (so, paths are almost the same, the only difference is 1 vs 2 just to make sure one can distinguish them when one sees an error message). coqc path isandrey@coq-server:~$ which coqc
/home/andrey/.opam/4.12.1/bin/coqc
coq-server.lan by ssh (using public_key):andrey@andrey:~$ ssh coq-server.lan
Welcome to Ubuntu Jammy Jellyfish (development branch) (GNU/Linux 5.16.10-051610-generic x86_64)
...
andrey@coq-server.lan:~$
===============
Now, I try to use TRAMP.
coq-prog-args are set up automatically (so, I dont touch it now).emacs (please, point attention on the very last path in the list) '(tramp-remote-path
(quote
(tramp-default-remote-path "/bin" "/usr/bin" "/sbin" "/usr/sbin" "/usr/local/bin" "/usr/local/sbin" "/local/bin" "/local/freeware/bin" "/local/gnu/bin" "/usr/freeware/bin" "/usr/pkg/bin" "/usr/contrib/bin" "/opt/bin" "/opt/sbin" "/opt/local/bin" "/home/andrey/.opam/4.12.1/bin")))
C-x C-f /ssh:coq-server.lan:/home/andrey/mwe/2/src/File1.v RETC-c C-b to run proof checkerI think it is worth to notice that sometimes (when I run emacs another time in example.. not sure how to reproduce) I see error like coqdep: /home/andrey/mwe/2/src/ - no such file or directory . but there is such directory on server, so, most likely it is local coqdep who is answering.
Please, let me know if description works for you and whether you are able to reproduce behavior.
Thank you,
Andrey
Andrey Klaus (Mar 25 2022 at 21:17):btw, logs:
...
Tramp: Encoding remote file ‘/ssh:coq-server.lan:/home/andrey/mwe/2/_CoqProject’ with ‘base64 <%s’...done
Tramp: Decoding local file ‘/tmp/tramp.lZ1gxM’ with ‘base64-decode-region’...done
Tramp: Inserting ‘/ssh:coq-server.lan:/home/andrey/mwe/2/_CoqProject’...done
Coq project file detected: /ssh:coq-server.lan:/home/andrey/mwe/2/_CoqProject.
Starting: coqtop -emacs -impredicative-set -w -notation-overridden,-unexpected-implicit-declaration -R /home/andrey/mwe/2/src MyNameSpace
Tramp: Opening connection for coq-server.lan using ssh...
Tramp: Sending command ‘exec ssh -q -o ControlMaster=auto -o ControlPath='tramp.%C' -o ControlPersist=no -e none coq-server.lan’
Tramp: Waiting for prompts from remote shell...done
Tramp: Found remote shell prompt on ‘coq-server.lan’
Tramp: Opening connection for coq-server.lan using ssh...done
Process coq exited abnormally with code 127
, shutting down scripting...
*coq*, cleaning up and exiting...
*coq* exited.
Process coq exited abnormally with code 127
, shutting down scripting...done.
proof-activate-scripting: coq process exited!
when I enter commands manually, it looks like they work..:
andrey@andrey:~/mwe$ ssh -q -o ControlMaster=auto -o ControlPath='tramp.%C' -o ControlPersist=no -e none coq-server.lan
Welcome to Ubuntu Jammy Jellyfish (development branch) (GNU/Linux 5.16.10-051610-generic x86_64)
...
andrey@coq-server.lan:~$ coqtop -emacs -impredicative-set -w -notation-overridden,-unexpected-implicit-declaration -R /home/andrey/mwe/2/src MyNameSpace
Welcome to Coq 8.13.2 (March 2022)
<prompt>Coq < 1 || 0 < </prompt>
Naive question until @Hendrik Tews comes;
: what happens when you type M-! echo $PATH ?
Andrey Klaus (Mar 28 2022 at 06:48):Thanks! A good question! /bin:/usr/bin:/sbin:/usr/sbin:/usr/local/bin:/usr/local/sbin .
when I do customize-variable tramp-remote-path, I do not see /home/andrey/.opam/4.12.1/bin there. So, I think that is why it does not see coqtop.
How to fix?
I already tryed to use customize-variable. It saves correct value to .emacs, but according to M-! echo $PATH it does not have any effect. What can be problem?
Andrey Klaus (Apr 01 2022 at 06:01):JFTR: Answer from @Hendrik Tews
Hi Andrey,
I am not sure I ever came across proof-rsh-command command - this
seems to be an ancient feature, which is not supported to work
with Coq.
I'm trying to use PG with remote coq compiler.
Unfortunately, there is no support for that. You can try PR 569
and tramp, but please read the comments on 569. If the background
compilation is too slow, disable compile-before-require and
compile manually, possibly with M-x compile.
I set up option proof-rsh-command to 'ssh 192.168.1.10' .
From briefly looking at the code, proof-rsh-command is prefixed
to the coqtop invocation Proof General does in the background for
your proof-script buffer. Simply using ssh will execute coqtop in
your home directory on the server and it seems coqtop is unable
to find the expected directories there. Instead of ssh, you would
need to use a command that cd's into the right directory on the
server. And, of course, also disable compile-before-require and
compile manually. And note that your coq session will load the
compiled files on the server, while your currently open file will
be saved locally.
If you want to discuss this topic further, I would suggest to
open an issue for Proof General at github.
Bye,
Hendrik
Last updated: Feb 06 2023 at 05:03 UTC