Stream: Proof General users

Topic: remote compilation with PG

view this post on Zulip Andrey Klaus (Mar 21 2022 at 10:15):

Hello all!

I'm trying to use PG with remote coq compiler.

So, my host is and host which I would like to use for compilation is

I set up option proof-rsh-command to ssh .
And when I do from terminal ssh 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..

view this post on Zulip 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.

view this post on Zulip Erik Martin-Dorel (Mar 25 2022 at 01:17):

Just FTR: see this topic for further discussion on this question.

Last updated: Feb 06 2023 at 05:03 UTC