Wrong path send to coqtop through ssh

[ildyria]

TL;DR: On Require Import on a project through ssh (tramp) the path sent to coqtop are wrong.

Some informations about my configuration:

Set the .profile / .zshrc so that Tramp works correctly:

if [[ $TERM == "dumb" ]]; then  # in emacs
    PS1='%(?..[%?])%!:%~%# '
    # for tramp to not hang, need the following. cf:
    # http://www.emacswiki.org/emacs/TrampMode
    unsetopt zle
    unsetopt prompt_cr
    unsetopt prompt_subst
    unfunction precmd
    unfunction preexec
else
    source $ZSH/oh-my-zsh.sh
fi

Set .spacemacs parameters:

(defun dotspacemacs/user-config ()
  "Configuration function for user code.
This function is called at the very end of Spacemacs initialization after
layers configuration.
This is the place where most of your configurations should be done. Unless it is
explicitly specified that a variable should be set before a package is loaded,
you should place your code here."
  ;; Open .v files with Proof General's Coq mode
  (load "~/.emacs.d/lisp/PG/generic/proof-site")
  (setq auto-mode-alist (cons'("\\.v$" . coq-mode) auto-mode-alist))
  ;; with tramp this is not required:
  ;; (setq proof-rsh-command "ssh sandor")
  (autoload 'coq-mode "coq" "Major mode for editing Coq vernacular." t)
  ;; coqtop is coqtop (no need for -emacs, it is added by PG)
  (setq coq-prog-name "coqtop")

  (setq tramp-default-method "ssh")
  (with-eval-after-load 'tramp-sh
    (add-to-list 'tramp-remote-path 'tramp-own-remote-path)
    ;; making sure that coqtop is in the path:
    (add-to-list 'tramp-remote-path "/home/benoit/.opam/4.05.0/bin/")
  )
)

The following _CoqProject will be prepended by ssh:<server>:<path_to_project>

-Q msl VST.msl
-Q sepcomp VST.sepcomp
-Q veric VST.veric
-Q floyd VST.floyd
-Q progs VST.progs
-Q concurrency VST.concurrency
-Q ccc26x86 VST.ccc26x86
-Q wand_demo wand_demo
-Q sha sha
-Q fcf fcf
-Q hmacfcf hmacfcf
-Q tweetnacl20140427 tweetnacl20140427
-Q hmacdrbg hmacdrbg
-Q aes aes
-Q mailbox mailbox
-R ../CompCert compcert
-R ../tweetnacl Tweetnacl
-R ../coq-stdpp/theories stdpp

Screenshot of the problem:

Related : https://github.com/ProofGeneral/PG/issues/104

[Matafou]

Hi, thanks for reporting.

@hendriktews how far from making this work are we? It seems we should revive coqdep #409 PR.

P.

[hendriktews]

@Benoît: Automatic background compilation does not work through tramp mode. Currently you have the following solutions:

• run Emacs/Proof General remotely, either via X11 forwarding or vnc or similar
• disable automatic background compilation and run make on the remote side, maybe tramp mode does the right thing, if you do M-x compile?

@hendriktews how far from making this work are we?

I don't know for sure. The background process primitives that I am using for automatic compilation have support for tamp mode. If all this works as the documentation suggests, then there is indeed not much to do.

It seems we should revive coqdep #409 PR.

Yes, coqdep only being able to work on real files seems to be the biggest show-stopper right now.

How many people are there that would like to use Proof General with tramp mode? Before Benoît, we only had one user asking for it.

Bye,

Hendrik

[ildyria]

@hendriktews

My situation is as follow:

• I have a 3.7 GB ram computer on which I cannot run my proofs (or very slowly...)
• My supervisor provided me with a 32Go ram server on which I log through ssh -X.
• When I am at work (Netherlands) everything is fine, the latency is not an issue (there is like 20m between me and the server).
• When I am not at my work place (e.g. Summer School in Croatia, DeepSpec in UPenn, CHES in Taipei, Summer School in Aarhus...) then the X-forwarding gets really slow...

I already compile directly through CLI via SSH, that is not a problem and that's what I'm used to do.

• Using Emacs/PG through terminal is just a no-go.
• Using it through X is a no-go as well. I am already doing that with CoqIDE, why would I bother with learning another IDE when CoqIDE is enough for me.

Using a local Spacemacs/PG while editing remotely through Tramp while forwarding coqtop is the sole reason for me to move to this new IDE. The possibility to decrease the load of ssh -X and thus have a better fluidity is just too good to pass on... (e.g. bye 5~15 seconds scrolls).

About M-x compile, in my case lead to (while choosing the valid target tweetnacl_ecc) the following error:

-*- mode: compilation; default-directory: "/ssh:sandor:/home/benoit/VST/" -*-
Compilation started at Thu Sep 28 15:46:26

make -C /ssh:sandor:/home/benoit/VST/ -j1 tweetnacl_ecc
make: *** /ssh:sandor:/home/benoit/VST/: No such file or directory.  Stop.

Compilation exited abnormally with code 2 at Thu Sep 28 15:46:37

[Matafou]

Interesting use case, thanks for sharing. It would be nice to make this work indeed. I guess coq running on big servers is something that is not going to disappear given the proofs currently being developed around the world.

You can still workaround this right? You lose some feature (auto-compilation and auto-locked files) but it is ok if you remember to compile things by hand and retract buffers before going into another one.

P.S. I know at least one people who uses emacs in a terminal/ssh and is happy with it. Needs a bit of configuration to make colors readable etc but it works.

P.

2017-09-28 18:05 GMT+02:00 Benoît Viguier notifications@github.com:

@hendriktews https://github.com/hendriktews

My situation is as follow:

• I have a 3.7 GB ram computer on which I cannot run my proofs (or very slowly...)
• My supervisor provided me with a 32Go ram server on which I log through ssh -X.
• When I am at work (Netherlands) everything is fine, the latency is not an issue (there is like 20m between me and the server).
• When I am not at my work place (e.g. Summer School in Croatia, DeepSpec in UPenn, CHES in Taipei, Summer School in Aarhus...) then the X-forwarding gets really slow...

I already compile directly through CLI via SSH, that is not a problem and that's what I'm used to do.

• Using Emacs/PG through terminal is just a no-go.
• Using it through X is a no-go as well. I am already doing that with CoqIDE, why would I bother with learning another IDE when CoqIDE is enough for me.

Using a local Spacemacs/PG while editing remotely through Tramp while forwarding coqtop is the sole reason for me to move to it to this new IDE. The possibility to decrease the load of ssh -X and thus have a better fluidity is just too good to pass on... (e.g. bye 5~15 seconds scrolls).

About M-x compile, in my case lead to (while choosing the valid target tweetnacl_ecc) the following error:

-- mode: compilation; default-directory: "/ssh:sandor:/home/benoit/VST/" -- Compilation started at Thu Sep 28 15:46:26

make -C /ssh:sandor:/home/benoit/VST/ -j1 tweetnacl_ecc make: *** /ssh:sandor:/home/benoit/VST/: No such file or directory. Stop.

Compilation exited abnormally with code 2 at Thu Sep 28 15:46:37

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/ProofGeneral/PG/issues/203#issuecomment-332884489, or mute the thread https://github.com/notifications/unsubscribe-auth/AEsl6t_t93DiBU_-zJpW4AX_qfLkdK7Kks5sm8O7gaJpZM4PjwTE .

[ildyria]

When using emacs and trying to go through the first line i.e. C-c C-Ret here is what I get (the corresponding file file has already been compiled):

When looking at the first screenshot provided (htop), this is expected because the path does not match as coqtop can't understand the Tramp prefix.

When using emacs -nw (directly through ssh) and going through a file, everything works fine. But I'm clearly not happy with the readability of output (I feel like going 20 years in the past):

also the lack of C-c C-RET and the need to do all the C-c C-n in emacs -nw is very frustrating. Adding a secondary binding for proof-goto-point would be a nice addition (by default).

Benoît

[hendriktews]

* When I am not at my work place (e.g. Summer School in Croatia,
  DeepSpec in UPenn, CHES in Taipei, Summer School in Aarhus...)
  then the X-forwarding gets really slow... 

OK, I see. I will have a look at it, but it will take some time. Have you tried vnc? For Taipei, the delay is probably to big to work comfortably with vnc, but Aarhus might just work.

About M-x compile, in my case lead to (while choosing the valid target

Please read the emacs docu about compilation. What emacs (or Proof General) offers you is an ordinary shell command. You just need to change it to

ssh sandor make -C /home/benoit/VST ...

with an appropriate ssh configuration. There is also some configuration setting that tells emacs to automatically save all buffers before starting a compilation. You can also configure a default compile command, or you can set it per file via file-local variables. Please have a look at the emacs docu.

Hendrik

[ildyria]

I do believe VNC would not provided me with better solution that X forwarding.

Anyway,
I managed to make it work by completely bypassing the way emacs set the arguments for coqtop,
see bellow.

---

1. I created an executable file coqtopp in my repository which contains what the call from emacs as it should look like (thus hardcoded paths):

coqtop -emacs -Q /home/benoit/VST/msl VST.msl -Q /home/benoit/VST/sepcomp VST.sepcomp ...

2. In the .emacs, I make sure that tramp is aware of the important paths:

(setq coq-prog-name "coqtopp")
(add-to-list 'tramp-remote-path "/home/benoit/.opam/4.05.0/bin/")
(add-to-list 'tramp-remote-path "/home/benoit/VST/")

As a result, when emacs calls coqtop args, the first is replaced by my coqtopp and args are completely ignored, making sure that the arguments are correctly set. While this is not the most elegant solution, at least it does the job. Still it would be nice if the paths were correctly set by PG.

[hendriktews]

Interesting hack - thanks for sharing!