Editor support for F*

You can edit F* code using your favourite text editor, but Emacs, Atom, and Vim have extensions that add special support for F*, including syntax highlighting and interactive development.

Emacs

fstar-mode implements support for F* programming, including

• Syntax highlighting
• Unicode rendering (with prettify-symbols-mode)
• Indentation
• Real-time verification (requires the Flycheck package)
• Interactive proofs (à la Proof-General)

fstar-mode requires Emacs 24.3 or newer, and is distributed through MELPA. Add the following to your Emacs 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, and run M-x package-refresh-contents, then M-x package-install RET fstar-mode RET. Future updates can be downloaded using M-x list-packages.

If fstar.exe is not already in your path, set the fstar-executable variable:

(set-default fstar-executable "path-to-fstar.exe")

Atom

The Atom package for F* supports syntax highlighting via atom-fstar and (Proof General style) interactive development via fstar-interactive.

Vim

VimFStar is a Vim plugin for F* that also supports interactive development and syntax highlighting.