F*-mode requires Emacs 24.3 or newer, and is distributed through MELPA.
-
Add the following to your init file (usually
.emacs
) if it is not already there:(require 'package) (add-to-list 'package-archives '("melpa" . "http://melpa.org/packages/") t) (package-initialize)
-
Restart Emacs, then run M-x package-refresh-contents and M-x package-install RET fstar-mode RET. Future updates can be downloaded using M-x list-packages U x y.
-
If
fstar.exe
andz3
are not already in your path, set thefstar-executable
andz3-executable
variables:(setq-default fstar-executable "PATH-TO-FSTAR.EXE") (setq-default fstar-smt-executable "PATH-TO-Z3(.EXE)")
fstar-mode
is compatible with Tramp: if you open an F* file on a remote machine, fstar-mode
run F* remotely over SSH.
⚡ indicates keybindings available once F* is running.
✨ indicates features added since the latest F* release.
🦄 indicates features that require yet-unmerged patches to F*.
The common prefix for fstar-mode
keybindings in C-c C-s
(short for star).
Key | Action |
---|---|
C-h . |
Show current error in echo area |
C-h M-w |
Copy current error message |
TAB / S-TAB |
Indent / Unindent |
C-RET |
⚡ ✨ Autocomplete word at point |
C-c C-v (verify) |
✨ Verify current file on the command line |
C-c C-s C-q (quit) |
Close temporary windows opened by fstar-mode |
Key | Action |
---|---|
M-n , M-p |
Jump to previous/next block in current file |
M-. , C-x 4 . , C-x 5 . |
⚡ Jump to definition (same window, other window, other frame) |
C-c C-' , C-x 4 ' , C-x 5 ' |
⚡ Browse to secondary location of current error (same window, other window, other frame) |
C-c C-a (alternate) |
Switch to interface file (and back to implementation) |
C-c C-s C-o (outline) |
Show an outline of the current buffer |
C-c C-s C-j C-d (jump to dependency) |
⚡ Jump to one of the dependencies of the current buffer |
M-, |
Return to point before last jump |
Key | Action |
---|---|
<menu> , M-<f12> |
⚡ Show type and docs in a small inline window (repeat to hide the window) |
C-c C-s C-e (eval) |
⚡ Evaluate (reduce) an expression (C-u to pick reduction rules) |
C-c C-s C-s (search) |
⚡ Search F*'s global context for functions and theorems |
C-c C-s C-d (documentation) |
⚡ Show type and documentation of a symbol |
C-c C-s C-p (print) |
⚡ Show type, documentation, and full definition of a symbol |
C-c C-s h o (help options) |
⚡ Show values of F* options |
C-c C-s h w (help wiki) |
Browse F*'s wiki in Emacs |
C-c C-s h W (help Wiki) |
Browse F*'s wiki in your browser |
Key | Action |
---|---|
C-c C-s C-c (cases) |
⚡ 🦄 Case split: insert a match, or refine match at point |
Proof-General | Atom | Action |
---|---|---|
C-c C-n (next) |
C-S-n |
⚡ Send the next paragraph to F* (with C-u , send it in lax mode) |
C-c C-p (previous) |
C-S-p |
⚡ Retract the last paragraph |
C-c C-. |
C-S-. |
⚡ Jump to beginning of untracked section |
C-c RET or C-c C-RET |
C-S-i |
⚡ Send everything up to the current point to F* |
C-c C-l (lax) |
C-S-l |
⚡ Send everything up to the current point to F*, in lax mode |
C-c C-b (buffer) |
C-S-b |
⚡ Send entire buffer to F* in lax mode |
C-c C-r (reload) |
C-S-r |
⚡ Reload dependencies of the current buffer and reprocess its contents (add C-u for lax mode) |
C-c C-x (exit) |
C-M-c |
⚡ Kill the F* subprocess |
C-c C-c |
C-M-S-c |
⚡ Send an interrupt signal to Z3. This (generally) interrupts the currently running verification task. |
Use M-x customize-variable RET fstar-interactive-keybinding-style RET to pick a keybinding style. The default is Proof-General; the other option is Atom. Please be aware of the current restrictions on the interactive-mode.
These keybindings are available during completion only:
Key | Action |
---|---|
C-h |
Show documentation of current completion candidate |
C-w |
Show definition of current completion candidate |
C-s |
Search among completion candidates |
Use M-x customize-variable RET fstar-enabled-modules RET to choose which parts of fstar-mode
to enable.
F*-mode recognizes and highlights certain special comments as titles: (***
and (** *
; (*+
, (**+
, and (** **
; and (*!
, (**!
, and (** ***
.
Use the following snippet:
(add-to-list 'auto-mode-alist '("\\.fsi?\\'" . fstar-mode))
Add the following line to your .emacs
:
(setq fstar-subp-prover-args '("--include" "<your-path>"))
Use C-h v fstar-subp-prover-args
for more details. If your project requires a set of flags to be passed to fstar
, it's OK to use a .dir-locals.el
to set fstar-subp-prover-args
. In that case, users can add further arguments using fstar-subp-prover-additional-args
.
F*-mode is compatible with Emacs' Tramp. To use F*-mode over tramp:
- Set
fstar-executable
andz3-executable
appropriately (if F* and Z3 are in your path on the remote machine it's enough to usefstar.exe
andz3
; otherwise, use their full paths on the remote machine — e.g.~/FStar/bin/fstar.exe
), - Open a remote file (
C-x C-f /sshx:username@remote-server: RET test.fst RET
). Processing this file should invoke a remote F* through SSH.
Use M-x fstar-selective-display-mode
to toggle selective display. In selective display mode, consecutive lines prefixed with (**)
are collapsed into a single 👻
.
fstar-mode
opens a *goals*
window as soon as an F* tactic prints out a goal. Use <prior>
and <next>
(“page up” and “page down”) to navigate that window.
F*-mode's completion uses company-mode
under the hood. Try M-x customize-group company
.
Customize the variable fstar-flycheck-checker
to pick your favorite style of real-time verification (full-buffer verification or lightweight typechecking). F*-mode's real-time checking uses flycheck-mode
under the hood: try M-x customize-group flycheck
to tweak Flycheck further.
If Emacs gets very sluggish when you open an F* file, try turning off prettification with M-x prettify-symbols-mode
. If that works, you're seeing Emacs bug 21022. Emacs 26 will include a fix; in Emacs 25, you should be able to work around it by following the font configuration instructions below.
Boxes instead of math symbols are most likely due to missing fonts. DejaVu Sans Mono, Symbola, FreeMono, STIX, Unifont, Segoe UI Symbol, Arial Unicode and Cambria Math are all good candidates. If Emacs doesn't automatically use the new fonts after a restart, the following snippet (add it to your .emacs
) should help (change Symbola
and DejaVu sans Mono
to the Unicode font you just downloaded and to your usual monospace font, respectively):
(set-fontset-font t 'unicode (font-spec :name "Symbola") nil 'prepend)
(set-fontset-font t 'greek (font-spec :name "DejaVu sans Mono") nil 'prepend)
For Emacs < 25, you'll need the following instead:
(set-fontset-font t 'unicode (font-spec :name "YOUR USUAL EMACS FONT") nil)
(set-fontset-font t 'unicode (font-spec :name "SOME FONT WITH GOOD COVERAGE AS LISTED ABOVE") nil 'append)
Use the following snippet to use XITS Math
for ∀
:
(set-fontset-font t (cons ?∀ ?∀) "XITS Math" nil 'prepend)
If you're using Emacs on Windows with Cygwin (😱), you can install windows-path.el
The short version is to do:
$ wget https://www.emacswiki.org/emacs/download/windows-path.el
Then, in your .emacs
(require 'windows-path "<path to windows-path.el>")
(windows-path-activate)
Setup MELPA as described above, then install the dependencies and clone the repo to a directory of your choice (~/.emacs.d/lisp/fstar-mode.el
for example). Optionally byte-compile fstar-mode.el
, and finally add the following to your init file:
(require 'fstar-mode "~/.emacs.d/lisp/fstar-mode.el/fstar-mode.el")
When running an F#-compiled F* fstar-mode
will complain about being unable to parse F*'s version number and assume you're running a relatively old F* (it needs to know F*'s version number to decide which features to enable). You can override this check by customizing fstar-assumed-vernum
.