fstar-debug-invocation and include paths

[mtzguido]

I have the following saucy invocation:

emacs -f fstar-debug-invocation /home/guido/r/fstar/bin/fstar.exe --max_fuel 1 --max_ifuel 1 --initial_ifuel 0 --z3cliopt smt.arith.nl=false --z3cliopt smt.QI.EAGER_THRESHOLD=100 --z3cliopt smt.CASE_SPLIT=3 --hint_info --use_hints --cache_checked_modules --use_extracted_interfaces true --smtencoding.elim_box true --smtencoding.l_arith_repr native --smtencoding.nl_arith_repr wrapped --smt /home/guido/bin/z3/z3-4.5.1.1f29cebd4df6-x64-ubuntu-14.04/bin/z3 --include obj/Vale/test --include obj/test --include obj/arch --include obj/arch/x64/ --include obj/lib/collections/ --include obj/lib/math --include obj/lib/util --include obj/crypto/aes/ --include obj/crypto/aes/x64 --include obj/crypto/poly1305/ --include obj/crypto/poly1305/x64/ --include obj/thirdPartyPorts/OpenSSL/poly1305/x64/ --include obj/external/ obj/crypto/aes/x64/FastMul_helpers_i.fst

It opens FastMul_helpers_i.fst correctly, and runs F with the options exactly as shown, but it seems F is running inside the obj/crypto/aes/x64 directory, since it fails with:

not a valid include directory: /home/guido/r/everest/vale/obj/crypto/aes/x64/obj/Vale/test

when it should really be pointing to /home/guido/r/everest/vale/obj/Vale/test. FWIW I think it's just plain emacs that's changing the directory, but could we work around it?

[cpitclaudel]

Ah, right, I didn't think to preserve the current directory. Getting the right directory is a matter of calling command-line-default-directory. But I'm not sure that we have a mechanism to change the directory in which F* should be run ATM

[cpitclaudel]

Right, we need to bind default-directory in fstar-subp-start.

Should be fairly easy: we need a new defvar called fstar-subp-default-directory that defaults to nil, and we need to wrap the call to fstar--subp-start-process in a (let ((default-directory (or fstar-default-directory default-directory))) …). Or we could put that let-binding in fstar-subp--start-process (I think I prefer the latter).

I'm going on holidays tomorrow; wanna take a crack at a patch?

[cpitclaudel]

Any update on this?

[mtzguido]

Sorry for the radio silence :). This is what I had tried, but by the time I set fstar-subp--default-directory, the default-directory already changed to that of the file and not the one where Emacs started. I'm mostly unfamiliar with Emacs Lisp, so perhaps I'm just doing something really stupid.

diff --git a/fstar-mode.el b/fstar-mode.el
index 4580391..bc73f28 100755
--- a/fstar-mode.el
+++ b/fstar-mode.el
@@ -5225,9 +5225,12 @@ Current file: %S" fstar-executable fstar-subp-prover-args buffer-file-name)

 (defconst fstar-subp--process-name "F* interactive")

+(defvar fstar-subp--default-directory nil)
+
 (defun fstar-subp--start-process (buf prog args)
   "Start an F* subprocess PROG in BUF with ARGS."
-  (apply #'start-file-process fstar-subp--process-name buf prog args))
+  (let ((default-directory (or fstar-subp--default-directory default-directory)))
+    (apply #'start-file-process fstar-subp--process-name buf prog args)))

 (defun fstar-subp--wait-for-features-list (proc)
   "Busy-wait until the first protocol-info message from PROC."
@@ -5248,6 +5251,7 @@ Could it be a typo in `fstar-subp-prover-args' or \
   (unless (and buffer-file-name (file-exists-p buffer-file-name))
     (user-error "Can't start F* subprocess without a backing file (save this buffer first)"))
   (unless (process-live-p fstar-subp--process)
+    (setq fstar-subp--default-directory default-directory)
     (let ((f*-abs (fstar-subp-find-fstar)))
       (fstar--init-compatibility-layer f*-abs)
       (let* ((buf (fstar-subp-make-buffer))

[cpitclaudel]

This looks great; just one small thing: instead of setting fstar-subp--default-directory in fstar-subp-start, set it in fstar-debug-invocation, and set it to command-line-default-directory, not default-directory.

[mtzguido]

Awesome! I didn't know about command-line-default-directory, thanks. Making a PR in a minute.