     (error "Can't start F* subprocess without a backing file (save this buffer first)"))
   (unless fstar-subp--process
     (let ((prog-abs (fstar-find-executable)))
-      (fstar--init-compatibility-layer)
+      (fstar--init-compatibility-layer prog-abs)
       (let* ((buf (fstar-subp-make-buffer))
              (process-connection-type nil)
+             (tramp-process-connection-type nil)
              (args (fstar-subp-with-interactive-args (fstar-subp-get-prover-args)))
              (proc (fstar-subp-start-process buf prog-abs args)))
         (fstar-log "Started F* interactive: %S" (cons prog-abs args))


(defun fstar-subp-start-process (buf prog args)
  "Start an F* subprocess PROG in BUF with ARGS."
  (apply #'start-process "F* interactive" buf prog args))

(defun fstar-subp-start ()
  "Start an F* subprocess attached to the current buffer, if none exists."

(defun fstar-subp-with-interactive-args (args)
  "Return ARGS precedeed by --in and the filename of the current buffer."
  (let ((file-name
         (cond
          ((tramp-tramp-file-p buffer-file-name)
           (tramp-file-name-localname
            (tramp-dissect-file-name buffer-file-name)))
          ((eq system-type 'cygwin)
           (string-trim-right
            (shell-command-to-string
             (format "cygpath -w %s" (shell-quote-argument buffer-file-name)))))
          (t buffer-file-name))))
    (append `(,file-name "--in") args)))

(defun fstar-subp-adjust-path (fn buf prog args)
