GitHub - FStarLang/fstar-mode.el: Emacs support for F*...

README.md

Use F* in Emacs!

Setup

F*-mode requires Emacs 24.3 or newer, and is distributed through MELPA.

1. 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)

2. 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.

3. If fstar.exe and z3 are not already in your path, set the fstar-executable and z3-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.

Spacemacs note: @kyoDralliam has a draft of a Spacemacs layer for F*. You may need to add the following to your user-init (not user-config) function for jump-to-definition to work:

(spacemacs|define-jump-handlers fstar-mode (fstar-jump-to-definition :async t))

Keybindings

⚡️ 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).

General

Navigation

Documentation, type hints, and computation

Matching

Interactive mode

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.

Tactics

In trace mode (?), <prev> and <next> also highlight the tactic that produced the goal in the source buffer.

Completion

These keybindings are available during completion only:

Advanced topics and customization

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.

Title comments

F*-mode recognizes and highlights certain special comments as titles: (*** and (** *; (*+, (**+, and (** **; and (*!, (**!, and (** ***.

Using F*-mode for F# files

Use the following snippet:

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

Including external libraries and passing custom flags to F*

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.

Editing remote F* files

F*-mode is compatible with Emacs' Tramp. To use F*-mode over tramp:

• Set fstar-executable and z3-executable appropriately (if F* and Z3 are in your path on the remote machine it's enough to use fstar.exe and z3; 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.

Hiding parts of a buffer

Use M-x fstar-selective-display-mode to toggle selective display. In selective display mode, consecutive lines prefixed with (**) are collapsed into a single ?.

Programming with tactics

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.

Completion

F*-mode's completion uses company-mode under the hood. Try M-x customize-group company.

Real-time verification

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.

Starting F*-mode from the command line

Use emacs -f fstar-debug-invocation path/to/fstar.exe …arguments file-name.fst to edit file-name.fst in F*-mode, with fstar-subp-prover-args set to …arguments and fstar-executable set to path/to/fstar.exe. This is particularly convenient when you want to diagnose an issue happening on the command line in Emacs: just prepend emacs -f fstar-debug-invocation to it.

Troubleshooting

Performance issues

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.

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

Fonts for specific characters

Use the following snippet to use XITS Math for ∀:

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

Cygwin

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)

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

Complaints about version numbers

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.

Debugging F*

The fstar-gdb command (M-x) attaches GDB to the current F* process and launches Emacs' GDB-mi interface. See https://askubuntu.com/questions/41629/ if you run into ptrace-related issues.