search

FStarLang / fstar-mode.el

Emacs support for F*
Apache License 2.0
67 stars 17 forks source link

fstar-mode over docker-tramp #104

Closed jaybosamiya closed 5 years ago

jaybosamiya commented 5 years ago

Using docker-tramp, when trying to start up fstar-mode for interactive proving, it fails with "the input device is not a TTY". Any suggestions on how to work around this/fix it?

Reproduction steps

  1. docker pull projecteverest/fstar-linux:806126a6e270 (use a more recent commit hash got from FStar CI if that hash isn't on docker hub at that time)
  2. docker exec youthful_bose sudo ln -s /home/everest/FStar/bin/fstar.exe /usr/bin/ (change youthful_bose to the actual container name from docker ps)
  3. docker exec youthful_bose sudo ln -s /home/everest/everest/z3-4.5.1.1f29cebd4df6-x64-ubuntu-14.04/bin/z3 /usr/bin/ (same as above)
  4. Run C-x C-f RET /docker:youthful_bose:/home/everest/temp.fst RET inside emacs to go into the docker image.
  5. Try C-x C-n.
  6. BOOM!
cpitclaudel commented 5 years ago

Looks like a bug in docker-tramp, actually ^^

Can you try adding this to your .emacs?

(require 'docker-tramp)
(defun docker-tramp-add-method ()
  "Add docker tramp method."
  (add-to-list 'tramp-methods
               `(,docker-tramp-method
                 (tramp-login-program      ,docker-tramp-docker-executable)
                 (tramp-login-args         (,docker-tramp-docker-options ("exec") ("-u" "%u") ("%h") ("sh")))
                 (tramp-remote-shell       "/bin/sh")
                 (tramp-remote-shell-args  ("-c")))))
cpitclaudel commented 5 years ago

(If that doesn't work, modifying docker-tramp.el directly might)

cpitclaudel commented 5 years ago

Ping?

jaybosamiya commented 5 years ago

Sorry, I haven't had a chance (need) to work with F* within docker via tramp yet, so I can't confirm whether it works with the fixes you suggested :/ Feel free to close this issue, since it doesn't seem to be an fstar-mode bug.

cpitclaudel commented 5 years ago

No problem. Feel free to reopen if needed.