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.