   (let ((map (make-sparse-keymap)))
     ;; Basics
     (define-key map (kbd "RET") #'fstar-newline)
+    (define-key map (kbd "C-c C-v") #'fstar-cli-verify)
     ;; Navigation
     (define-key map (kbd "M-p") 'fstar-subp-previous-block-start)
     (define-key map (kbd "M-n") 'fstar-subp-next-block-start)

     ["Switch to reStructuredText mode"
      fstar-literate-fst2rst])
    ("Utilities"
     ["Copy error message at point"
      fstar-copy-help-at-point (fstar--check-help-at-point)])
    ["Configuration" fstar-customize]))

        (setq fstar-subp--continuations (make-hash-table :test 'equal))
        (when (fstar--has-feature 'json-subp)
          (fstar-subp--wait-for-features-list proc))))))

;;; Running F* on the CLI

(defconst fstar--cli-verification-buffer-name "*fstar: CLI verification of %S")
(push fstar--cli-verification-buffer-name fstar--all-temp-buffer-names)

(defun fstar-cli-verify ()
  "Send the whole buffer to a fresh instance of F* running in CLI mode.
This is useful to spot discrepancies between the CLI and IDE frontends."
  (interactive)
  (let* ((f* (fstar-subp-find-fstar))
         (args (fstar-subp-get-prover-args t))
         (cmd (mapconcat #'shell-quote-argument (cons f* args) " "))
         (buf-name (buffer-file-name))
         (name-fn (lambda (_) (format fstar--cli-verification-buffer-name buf-name)))
         (compilation-buffer (compilation-start cmd t name-fn)))
    (with-current-buffer compilation-buffer
      (defvar compilation-error-regexp-alist)
      (setq-local compilation-error-regexp-alist
                  (flycheck-checker-compilation-error-regexp-alist 'fstar)))))

;;; ;; Keybindings

