F* extension for VS Code

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.

Development

After clone repository

npm ci
npm run compile

Then press F5 within VS Code.