Andrey Klaus (Mar 21 2022 at 10:15): Andrey Klaus (Mar 21 2022 at 10:15):Hello all!
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..
Andrey Klaus (Mar 21 2022 at 11:41):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 25 2022 at 01:17):Just FTR: see this topic for further discussion on this question.
Last updated: Apr 18 2024 at 02:01 UTC