   "Like `fstar-subp--parse-prover-args-1' on ARGSV, but infer VAR-NAME."
   `(fstar-subp--parse-prover-args-1 ,argsv ',argsv))
 
-(defun fstar-subp-get-prover-args ()
+(defun fstar-subp-get-prover-args (&optional no-ide)
   "Compute F*'s arguments.
 Function is public to make it easier to debug
 `fstar-subp-prover-args' and
-`fstar-subp-prover-additional-args'."
+`fstar-subp-prover-additional-args'.
+Non-nil NO-IDE means don't include `--ide' and `--in'."
   (let ((smt-path (fstar--maybe-cygpath (fstar-subp-find-smt-solver)))
-        (ide-flag (if (fstar--has-feature 'json-subp) "--ide" "--in"))
+        (ide-flag (if no-ide nil
+                    (if (fstar--has-feature 'json-subp) '("--ide") '("--in"))))
         (usr-args (append
                    (fstar-subp--parse-prover-args fstar-subp-prover-args)
                    (fstar-subp--parse-prover-args fstar-subp-prover-additional-args))))
-    `(,(fstar-subp--buffer-file-name) ,ide-flag "--smt" ,smt-path ,@usr-args)))
+    `(,(fstar-subp--buffer-file-name) ,@ide-flag "--smt" ,smt-path ,@usr-args)))
 
 (defun fstar-subp--prover-includes-for-compiler-hacking ()
   "Compute a list of folders to include for hacking on the F* compiler."

      (define-key-after map [queries-sep] '(menu-item "--"))
      (add-item 'fstar-quit-windows "quit-windows")
      (add-item 'fstar-subp-kill-one-or-many "stop")
      (define-key-after map `[process-management-sep] '(menu-item "--"))
      (add-item 'fstar-customize "settings"))
    (fstar-tool-bar--cleanup-map map)))

               (apply-partially #'fstar-subp--flycheck-continuation callback))
            (funcall callback 'finished nil)))
      (funcall callback 'interrupted nil))))

(defun fstar--flycheck-verify-subp-available ()
  "Create a verification result announcing availability of the F* subprocess."
  (list
   (flycheck-verification-result-new
    :label "Subprocess running"
    :message (if (fstar-subp-live-p) "OK, F* started."
               "This checker requires a running F* subprocess.")
    :face (if (fstar-subp-live-p) 'success '(bold error)))
   (flycheck-verification-result-new
    :label "Subprocess started"
    :message (if (fstar-subp-available-p) "OK, F* idle."
               "This checker only runs when the F* subprocess is idle.")
    :face (if (fstar-subp-available-p) 'success '(bold error)))))

(flycheck-define-generic-checker 'fstar-interactive
  "Flycheck checker for F*'s interactive mode.
