Hello all! I'm trying to use PG with remote coq compiler. 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 expected. When I open my local .v , I have next problem with compilation:
*Error: Cannot find a physical path bound to logical path matching suffix MyNameSpace.NS1.* If I see right the problem is I have next in my _CoqProject file: -R src MyNameSpace Question: how to pass this -R to remote compiler (or what is the problem and what to try?). Thanks! Andrey.
_______________________________________________ ProofGeneral mailing list ProofGeneral@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral
