Using F* remotely, over TRAMP

[jaybosamiya]

I recently tried to use F* remotely over TRAMP, and most of it works beautifully! Thus I thought I should document a few small issues that I faced when trying to do so (and workarounds where I could find them).

• [X] fstar-executable path doesn't work correctly, if you use an absolute path
  • ~This might just be me, but what I did was simply change it over to "fstar.exe" (and similarly for z3)~
  • Fixed by @cpitclaudel (see below)
• [X] "fstar.exe" not found
  • ~Turns out, the PATH variable is not set up correctly by TRAMP. I had to add (add-to-list 'tramp-remote-path 'tramp-own-remote-path) to my .emacs and mess around with the .profile, .bash_profile, and .zprofile files remotely (I just set all of them to be the same and contain the PATH exports)~
  • Added note to README by @cpitclaudel (see below)
• [X] Code jumping via fstar-jump-to-definition (M-.) and fstar-jump-to-related-error (C-c C-') tries to jump to local files instead of remote files
  • ~A temporary workaround I have is to keep a local copy of all remote files, and jump to that, but this is clearly not a great solution, since it means I would need to constantly be syncing. It would be nice to have fstar-mode detect that it is inside TRAMP and jump to the correct remote file.~
  • Fixed by @cpitclaudel (see below)

[cpitclaudel]

Thanks! Do you have a machine that I could test this on? I used to use Kenji's machine at INRIA, but I don't have access to that one anymore.

fstar-executable path doesn't work correctly, if you use an absolute path

I think I need to test that to understand what the issue is.

"fstar.exe" not found

We could (should?) add a link to the relevant docs to the README.

Code jumping via fstar-jump-to-definition (M-.) and fstar-jump-to-related-error (C-c C-') tries to jump to local files instead of remote files

Just pushed a fix. Please give it a try? :)

[jaybosamiya]

The fix works perfectly (updated checklist above). Thanks for fixing it so quickly! :)

BTW, I had to manually update fstar-mode.el on my machine to pull this. Does it require a manual push on your side to go over to elpa?

As for the testing, I unfortunately do not have the permissions required to grant you access.

The error that comes when using an absolute path is this (copying relevant stuff from *Messages* buffer):

Tramp: Inserting ‘/sshx:jayb@XXXXXX:/home/jayb/lowstar-dlist-trials/ind/DListLowInd.fst’...done
if: Failed to check F*’s version: “/bin/sh: 168: /sshx:jayb@XXXXXX:/home/jayb/everest/FStar/bin/fstar.exe: not found
”

For the remote-path thing, the relevant link (from TRAMP documentation) is: https://www.gnu.org/software/emacs/draft/manual/html_mono/tramp.html#Remote-programs

[cpitclaudel]

BTW, I had to manually update fstar-mode.el on my machine to pull this. Does it require a manual push on your side to go over to elpa?

Updates usually takes a few hours to propagate

The error that comes when using an absolute path is this

Thanks, I tried a blind fix. Please give it a try.

[jaybosamiya]

Updates usually takes a few hours to propagate

Ah, good to know.

Thanks, I tried a blind fix. Please give it a try.

Worked perfectly! Thanks a lot! Updated checklist above.

PS: One of my friends recommended using TRAMP to ssh to localhost to test the effect of having TRAMP in the middle (might be useful for diagnosing things in the future).

[cpitclaudel]

Thanks for testing. I've updated the README. Let me know if you run into further issues!