{"action":"created","issue":{"url":"https://api.github.com/repos/ProofGeneral/PG/issues/104","repository_url":"https://api.github.com/repos/ProofGeneral/PG","labels_url":"https://api.github.com/repos/ProofGeneral/PG/issues/104/labels{/name}","comments_url":"https://api.github.com/repos/ProofGeneral/PG/issues/104/comments","events_url":"https://api.github.com/repos/ProofGeneral/PG/issues/104/events","html_url":"https://github.com/ProofGeneral/PG/issues/104","id":172566345,"number":104,"title":"remote compilation","user":{"login":"vzaliva","id":86581,"avatar_url":"https://avatars.githubusercontent.com/u/86581?v=3","gravatar_id":"","url":"https://api.github.com/users/vzaliva","html_url":"https://github.com/vzaliva","followers_url":"https://api.github.com/users/vzaliva/followers","following_url":"https://api.github.com/users/vzaliva/following{/other_user}","gists_url":"https://api.github.com/users/vzaliva/gists{/gist_id}","starred_url":"https://api.github.com/users/vzaliva/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/vzaliva/subscriptions","organizations_url":"https://api.github.com/users/vzaliva/orgs","repos_url":"https://api.github.com/users/vzaliva/repos","events_url":"https://api.github.com/users/vzaliva/events{/privacy}","received_events_url":"https://api.github.com/users/vzaliva/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":3,"created_at":"2016-08-22T22:04:58Z","updated_at":"2016-10-28T23:55:03Z","closed_at":null,"body":"I am trying to use PG on a file from remote machine opened using 'tramp':\r\n\r\nAfter coq process successfully started it fails on first import with following error:\r\n\r\n```\r\n-*- mode: compilation; -*-\r\n\r\necho \"Require VecUtil.\" > /tmp/ProofGeneral-coq259239Du.v /home/lord/.opam/4.03.0/bin/coqdep -Q /scp:spiral:/home/vzaliva/src/spiral-coq/ \"\" -I /scp:spiral:/home/vzaliva/src/spiral-coq -R /scp:spiral:/home/vzaliva/src/spiral-coq Top /tmp/ProofGeneral-coq259239Du.v\r\n/home/lord/.opam/4.03.0/bin/coqdep: \"opendir\" failed on \"/scp:spiral:/home/vzaliva/src/spiral-coq\": No such file or directory\r\n```\r\n\r\nIt looks like 'coqdep' is executed locally, not remotely.\r\n\r\n"},"comment":{"url":"https://api.github.com/repos/ProofGeneral/PG/issues/comments/257055333","html_url":"https://github.com/ProofGeneral/PG/issues/104#issuecomment-257055333","issue_url":"https://api.github.com/repos/ProofGeneral/PG/issues/104","id":257055333,"user":{"login":"vzaliva","id":86581,"avatar_url":"https://avatars.githubusercontent.com/u/86581?v=3","gravatar_id":"","url":"https://api.github.com/users/vzaliva","html_url":"https://github.com/vzaliva","followers_url":"https://api.github.com/users/vzaliva/followers","following_url":"https://api.github.com/users/vzaliva/following{/other_user}","gists_url":"https://api.github.com/users/vzaliva/gists{/gist_id}","starred_url":"https://api.github.com/users/vzaliva/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/vzaliva/subscriptions","organizations_url":"https://api.github.com/users/vzaliva/orgs","repos_url":"https://api.github.com/users/vzaliva/repos","events_url":"https://api.github.com/users/vzaliva/events{/privacy}","received_events_url":"https://api.github.com/users/vzaliva/received_events","type":"User","site_admin":false},"created_at":"2016-10-28T23:55:03Z","updated_at":"2016-10-28T23:55:03Z","body":"The preferred solution for me is for PG to run the compilation remotely.  For example, I am remotely accessing via SSH fast server at the university but it is: \r\n\r\n0. headless \r\n1. behind firewall \r\n2. have relatively slow connection \r\n3. I do not have admin access to easily install packages\r\n\r\nwhich makes some solutions like desktop sharing, remote FS or even X11 sessions unfeasible.\r\nSince PG could already run coqtop remotely, I do not see why running the compilation in the same manner should be any different. As @cpitclaudel mentioned tramp provides some infrastructure for that."}}
{"actor":{"display_login":"vzaliva"}}