vsfstar

January 26, 2020 ยท View on GitHub

A Visual Studio Code extension for F*, with support for hacking on the F* compiler baked in. Uses the Language Server Protocol to provide the following features:

  • Syntax highlighting forked from vscode-language-fstar
  • Lax-check entire file on open
  • Diagnostic reporting, with location information
  • Lax-check entire file on save
  • Go to definition
  • Hover information: type and documentation
  • Auto-complete
  • Custom include paths
  • Interactively stepping through proofs

Requires Z3 4.8.5 to be installed, and minimum F* version of 0.9.7. Configure vsfstar.path to point to the fstar.exe binary you built.

Demo