 First argument must be an F* executable, not %S" err-header executable))
     (with-current-buffer (find-file-existing fname)
       (setq-local fstar-subp-prover-args args)
+      (setq-local fstar-subp--default-directory command-line-default-directory)
       (message "\
 F* binary: %S
 F* arguments: %S

    ,@(-mapcat (lambda (dir) `("--include" ,dir))
               (fstar-subp--prover-includes-for-compiler-hacking))))

;;;###autoload
(defun fstar-debug-invocation ()
  "Compute F*'s arguments from `argv' and visit the corresponding file.


(defun fstar-subp--start-process (buf prog args)
  "Start an F* subprocess PROG in BUF with 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."
