Emacs support for F*
Emacs Lisp Makefile
Latest commit f7b9820 Feb 24, 2017 @beurdouche beurdouche committed on GitHub Support for the 'include' keyword


MELPA Build Status

Use F* in Emacs!




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)

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:

(setq-default fstar-executable "PATH-TO-FSTAR.EXE")

From source

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")

Using the interactive mode

Please be aware of the current restrictions on the interactive-mode.

The keybindings are as follows:

Emacs Atom Action
C-c C-n C-S-n Process the next block (terminated by two empty lines)
C-c C-u or C-c C-p C-S-p Retract last block
C-c RET or C-c C-RET C-S-i Process the file up to the current point
C-c C-l C-S-l Process the next block in lax mode
C-c C-x C-M-c Kill the F* process

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.


Enabling and disabling individual F* mode components

Use M-x customize-variable RET fstar-enabled-modules RET to choose which parts of fstar-mode to enable.

In particular, you can get real-time verification (instead of interactive, Proof-General style verification), by enabling the flycheck module. You'll need to install Flycheck from MELPA.

Using F*-mode for .fsi files

Use the following snippet:

(add-to-list 'auto-mode-alist '("\\.fsi\\'" . fstar-mode))

Include non-standard libraries when using fstar-mode

Add the following line to your .emacs.

(setq fstar-subp-prover-args '("--include" "<your-path>"))

Note that under cygwin, fstar is a windows program and expects windows pathnames. For example,

(setq fstar-subp-prover-args '("--include" "E:\\FStar\\ucontrib\\Platform\\fst")

('\\' is used to escape a Windows pathname.) See fstar-subp-prover-args for more documentation.

Using F*'s bundled version of Z3

F* looks for Z3 in your system path. To use the version of Z3 included in F* binary releases instead, add the following to your .emacs:

(advice-add 'fstar-subp-start-process :around #'fstar-subp-adjust-path)

Font issues

Missing characters

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 pick up on the new fonts after a restart, the following snippet (add it to your .emacs) should help:

(set-fontset-font t 'unicode (font-spec :name "YOUR USUAL EMACS FONT") nil 'append)
(set-fontset-font t 'unicode (font-spec :name "SOME FONT WITH GOOD COVERAGE AS LISTED ABOVE") nil 'append)

Fonts for specific characters

Use the following snippet to use Symbola for only:

(set-fontset-font t (cons ?∀ ?∀) "Symbola" nil 'prepend)