       (buffer-disable-undo)
       (current-buffer))))
 
+(defun fstar-subp-prover-args-safe-p (args)
+  "Check whether ARGS is a known-safe value for `fstar-subp-prover-args'."
+  (equal args 'fstar-subp-prover-args-for-compiler-hacking))
+
 (defcustom fstar-subp-prover-args nil
   "Used for computing arguments to pass to F* in interactive mode.
 

multiple arguments as one string will not work: you should use
\\='(\"--aa\" \"--bb\"), not \"--aa --bb\"."
  :group 'fstar
  :type '(repeat string))

(defun fstar-subp-find-fstar ()
  "Find path to F* executable."

        (ide-flag (if (fstar--has-feature 'json-subp) "--ide" "--in")))
    `(,(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."
  (-if-let* ((fname (buffer-file-name))
             (default-directory (locate-dominating-file fname "_tags")))
      (let ((exclude-list '("." ".." "VS""tests""tools"
                            "ocaml-output" "u_ocaml-output" "u_boot_fsts"))
            (src-dir (expand-file-name "src" default-directory))
            (include-dirs nil))
        ;; (push (expand-file-name "ulib") include-dirs)
        (dolist (dir (directory-files src-dir nil))
          (unless (member dir exclude-list)
            (let ((fulldir (expand-file-name dir src-dir)))
              (when (file-directory-p fulldir)
                (push fulldir include-dirs)))))
        (nreverse include-dirs))
    (user-error (concat "Couldn't find _tags file while trying to "
                        " set up F*-mode for compiler hacking."))))

(defun fstar-subp-prover-args-for-compiler-hacking ()
  "Compute arguments suitable for hacking on the F* compiler."
  `("--eager_inference" "--lax" "--MLish"
    ,@(-mapcat (lambda (dir) `("--include" ,dir))
               (fstar-subp--prover-includes-for-compiler-hacking))))

(defun fstar-subp--buffer-file-name ()
  "Find name of current buffer, as sent to F*."
