Skip to content

Editor support for F*

Jump to bottom Edit New page
Kirby Linvill edited this page Jan 21, 2024 · 29 revisions

You can edit F★ code using your favourite text editor, but Emacs, Visual Studio Code, Atom, and Vim have extensions that add special support for F★, including syntax highlighting and interactive development.

Emacs

fstar-mode supports F★'s IDE protocol described below on this page, and includes support for interactive proofs, syntax highlighting, completion, type hints, documentation queries, and quick navigation.

Visual Studio Code

fstar-vscode-assistant is a Visual Studio Code extension for F*. It uses language-server protocol between a VS Code client and language server, combined with F*'s IDE protocol. It supports interactive proofs, syntax highlighting, completion, type hints, quick navigation, document formatting, etc.

Vim (discontinued, last updated Mar 2016)

VimFStar is a Vim plugin for F★ that supports interactive development and syntax highlighting.

Atom (discontinued, last updated Jun/Nov 2017)

The Atom package for F★ supports syntax highlighting via atom-fstar and interactive development via fstar-interactive.

Status: On Jan 11, 2017 it was possible to verify an F★ file through atom-script (this is not as sophisticated as the emacs mode which can verify files piece-by-piece). There was also a fork of atom-fstar here. None of these currently supports the new JSON protocol below.

Adding support for new IDEs

F★ can be started in IDE mode by passing it the --ide flag, which supersedes the legacy --in flag. Clients of the former API are encouraged to migrate (see migration notes below).

Example

>>> indicates client messages. <<< indicates F★'s response. ### are comments. For convenience responses were reformatted, but in the actual protocol each message occupies a single line.

$ fstar.exe test.fst --ide ### Start F★

### F★ immediately sends information about the protocol upon starting
<<< { "features": [ "autocomplete", "compute", "describe-protocol", "describe-repl",
                    "exit", "lookup", "lookup/documentation", "lookup/definition",
                    "pop", "peek", "push", "search" ],
      "version": 2,
      "kind": "protocol-info" }

### Let's send some code for processing:
>>> {"query-id":"1","query":"push","args":{"kind":"full","code":"module Test\n","line":1,"column":0}}
### Looks like that worked — no errors
<<< { "response": [],
      "status": "success",
      "query-id": "1",
      "kind": "response" }

### Another push
>>> {"query-id":"2","query":"push","args":{"kind":"full","code":"\nlet rec fib n =\n  if n <= 1 then 1 else fib (n - 1) + fib (n - 2)\n","line":2,"column":0}}
<<< { "kind": "response",
      "query-id": "2",
      "status": "success",
      "response": [] }

### Use starts typing, so we try a completion
>>> {"query-id":"3","query":"autocomplete","args":{"partial-symbol":"fi"}}
### Response includes the length of the match, the namespace, and the completion candidate
<<< { "response": [[2, "Test", "fib"]],
      "status": "success",
      "query-id": "3",
      "kind": "response" }

### It's easy to get more info about a symbol, too:
>>> {"query-id":"4","query":"lookup","args":{"symbol":"Test.fib","requested-info":["type","defined-at","documentation"]}}
<<< { "response": {
          "definition": null,
          "documentation": null,
          "type": "(n:int -> Tot int)",
          "defined-at": { "end": [3, 11],
                          "beg": [3, 8],
                          "fname": "<input>" },
          "name": "Test.fib" },
      "status": "success",
      "query-id": "4",
      "kind": "response" }

### If a push fails, we get errors:
>>> {"query-id":"5","query":"push","args":{"kind":"full","code":"let a = assert false\n","line":5,"column":0}}
<<< { "response": [{ "ranges": [{ "end": [5, 20],
                                  "beg": [5, 0],
                                  "fname": "<input>" }],
                     "message": "assertion failed",
                     "level": "error" }],
      "status": "failure",
      "query-id": "5",
      "kind": "response" }

Collecting a trace from emacs

One way to experiment with F*'s IDE protocol is to collect a sample trace of events from emacs when running fstar-mode.el. You can do this by adding this to your .emacs (setq fstar-subp-debug t) and then launching fstar-mode.el on a sample F* file. This will result in the trace of interactions between emacs and fstar being recorded in the *fstar-debug* buffer. For example, you will see something like this.

;;; Started F* interactive: (" path/to/fstar.exe" " ... arguments to F* ...")
{"kind":"protocol-info","version":2,"features":["autocomplete","autocomplete/context","compute","compute/reify","compute/pure-subterms","describe-protocol","describe-repl","exit","lookup","lookup/context","lookup/documentation","lookup/definition","peek","pop","push","search","segment","vfs-add","tactic-ranges","interrupt","progress"]}
;;; Complete message received: (status: nil; message: ((kind . "protocol-info") (version . 2) (features "autocomplete" "autocomplete/context" "compute" "compute/reify" "compute/pure-subterms" "describe-protocol" "describe-repl" "exit" "lookup" "lookup/context" "lookup/documentation" "lookup/definition" "peek" "pop" "push" "search" "segment" "vfs-add" "tactic-ranges" "interrupt" "progress")))
;;; [441.68ms] Feature list received
;;; Processing queue
>>> {"query-id":"1","query":"vfs-add","args":{"filename":null,"contents":"(*\n   Copyright 2021 Microsoft Research\n\n   Licensed under the Apache License, Version 2.0 (the \"License\");\n   ... ""}}
>>> {"query-id":"2","query":"push","args":{"kind":"full","code":"...","line":1,"column":0}}
{"kind":"response","query-id":"1","status":"success","response":null}
;;; Complete message received: (status: "success"; message: ((kind . "response") (query-id . "1") (status . "success") (response . :json-null)))
;;; Query "1" completed in 0.2522s
{"kind":"message","query-id":"2","level":"progress","contents":{"stage":"loading-dependency","modname":"prims"}}

The lines that begin with ">>>" are the messages sent from emacs to F*. If you save those lines only to a file (without the ">>>" prefix) and pipe it to F* launched with the arguments described on the first line of the debug output, then you can replay an interaction with F* independently of the editor. e.g, cat trace | fstar.exe --ide A.fst

High level description

F★'s IDE mode (introduced in version 0.9.4.3) is a simple JSON-based client-server protocol over text pipes. Clients send newline-terminated queries, and the F★ server responds with a mix of newline-terminated responses (one per query) and additional newline-terminated messages providing status or progress information. The current server is ordered and synchronous (at most one query can run at any time and responses are sent in order), but clients should not depend on this.

Each query is identified by a client-selected ID which the server echoes back in exactly one response and zero or more messages pertaining to that query. Certain server messages are not directly related to a query and do not include a query ID (in fact, the current implementation of the server never includes query IDs in messages).

F★ documents are sequences of individual phrases. Clients are expected to use simple heuristics or user interaction to segment the document into individual definitions, and send these sentences one by one to the F★ server using sequences of push and pop queries. A push indicates to F★ that one more sections of the buffer are ready be parsed and typechecked, and a pop undoes the effect of the last push. F★ responds to each push with a success code indicating whether the corresponding segment was correctly parsed and typechecked. If so, the client may send the next segment (clients should wait for each segment to be fully processed before sending the next one); if not, the client should indicate errors to the user and re-send an updated segment when appropriate.

The first query must be a push. (version 2 of the protocol) There are no restrictions on the first query (nonetheless, since F★ reads the whole file to load dependencies upon the first push, it is recommended to precede it with a vfs-add). Some queries (but not push) may fail with Current module unset until a module declaration is pushed.

On recent OCaml builds, clients can send F★ an interrupt signal (SIGINT) to interrupt long-running queries (currently compute and push). F★ may ignore the interrupt, or cause the currently-running query to fail early.

Message format

Client messages are all in the one form.

  • Client queries contain three mandatory fields query-id, query, and args; no other fields are recognized:

    { "query-id": "…", "query": "…", "args": { … } }
    • query-id is a client chosen, session-unique string (a perpetually increasing counter is a good choice).
    • query is a string identifying the query.
    • args is query-specific. Send {}, not null, to indicate an empty collection of args.

Server messages can take multiple formats. In all cases, future versions of the protocol may include more data; this is not considered a breaking change. All server messages contain a ""kind" field.

  • Protocol information messages can be sent at any time; one is sent right before F★ starts to listen for client queries:

    { "kind": "protocol-info", "features": [ … ], "version": … }
    • features is a list of strings indicating which features this build of F★ supports. Clients should use this list instead of F★'s version number to determine whether a feature is available.
    • version is the protocol's version number. The current version number is 1. This number is incremented every time the API is changed in backwards-incompatible ways.

  • Status messages can be sent at any time; they provide clients with feedback while F★ is busy preparing a full-fledged response. Most messages should be displayed to the user, and even an error-level message doesn't indicate that e.g. a push failed.

    { "kind": "message", "level": "…", "contents": "…" }
    • level is one of "error", "warning", "info" and "proof-state" (other values of level may be added in the future — clients should ignore unknown values).
    • contents is message-specific: see List of status messages below.
    • query-id is optional and indicates the query (if any) whose execution caused this message to be sent.

  • Response messages are sent in response to client queries (exactly one response per query). They indicate whether a query completed successfully, and which results it produced if any. Each response contains the ID of the corresponding query.

    {"kind": "response", "query-id": "…", "status": "…", "response": …}
    • query-id is a string (the one sent by the client). If status is "protocol-violation", however, the query-id field may be set to "?".
    • status is one of "success", "failure", or "protocol-violation".
    • response is query-specific.

List of features

These are part of the list returned in "protocol-info" messages:

  • Queries (these just indicate that a query is available): autocomplete; compute; describe-protocol; describe-repl; exit; lookup; pop; peek; push; search; segment; vfs-add
  • lookup/documentation; lookup/definition: indicate that lookup understand requests for documentation and definitions.
  • lookup/context; autocomplete/context: indicate that lookup and autocomplete understand the context argument.
  • tactic-ranges: indicate that proof states may contain ranges
  • interrupt: indicate that F★ will gracefully handle sigint (C-c C-c) signals

List of queries and responses

exit

Exit the current F★ subprocess. This is equivalent to sending a C-d (U+004 END OF TRANSMISSION) character. It yields a clean exit, though usually just killing the F★ subprocess is fine too (except for saving hints).

  • Query args: {}
  • status: always "success"
  • response: null
  • Example: 
    >>> { "query-id": "0", "query": "exit", "args": {} }
<<< {"kind":"response","query-id":"0","status":"success","response":null}

describe-protocol

Replay the welcome message.

  • Query args: {}
  • status: always "success"
  • response: Same as in protocol-info messages.
  • Example: 
    >>> { "query-id": "0", "query": "describe-protocol", "args": {} }
<<< { "response": {
          "features": [
              "autocomplete",
              "compute",
              "describe-protocol",
              "describe-repl",
              "exit",
              "lookup",
              "lookup/documentation",
              "lookup/definition",
              "pop",
              "peek",
              "push",
              "search"
          ],
          "version": 2
      },
      "status": "success",
      "query-id": "0",
      "kind": "response" }

describe-repl

Give information on the current state of the subprocess. Currently only loaded dependencies.

  • Query args: {}
  • status: always "success"
  • response (dictionary): Information about the current subprocess state:
    • loaded-dependencies (list of strings): Currently loaded dependencies.
    • options (list of dictionaries): All F★ options
      • name (string): Name of the option
      • value (null, bool, string, or list of the same): Value of the option; null if unset
      • default (null, bool, string, or list of the same): Default value of the option
      • documentation (string): Docs of the option
  • Example: 
    >>> { "query-id": "0", "query": "describe-repl", "args": {} }
<<< { "response": {
          "loaded-dependencies": [
              "/build/fstar/compute/ulib/FStar.String.fsti",
              "/build/fstar/compute/ulib/FStar.List.fst",
              "/build/fstar/compute/ulib/FStar.List.Tot.fst",
              "/build/fstar/compute/ulib/FStar.List.Tot.Properties.fst",
              "/build/fstar/compute/ulib/FStar.List.Tot.Base.fst",
              "/build/fstar/compute/ulib/FStar.Classical.fst",
              "/build/fstar/compute/ulib/FStar.Squash.fsti",
              "/build/fstar/compute/ulib/FStar.Char.fsti",
              "/build/fstar/compute/ulib/FStar.All.fst",
              "/build/fstar/compute/ulib/FStar.ST.fst",
              "/build/fstar/compute/ulib/FStar.Heap.fst",
              "/build/fstar/compute/ulib/FStar.TSet.fst",
              "/build/fstar/compute/ulib/FStar.PredicateExtensionality.fst",
              "/build/fstar/compute/ulib/FStar.PropositionalExtensionality.fst",
              "/build/fstar/compute/ulib/FStar.FunctionalExtensionality.fst"
          ],
          "options": [{ "documentation": "JSON-based interactive mode for IDEs",
                        "default": false,
                        "value": true,
                        "name": "ide"}, …] },
      "status": "success",
      "query-id": "0",
      "kind": "response" }

pop

Undo the last push.

  • Query args: {}
  • status: "success" if there was a segment to pop
  • response: null
  • Example: 
    >>> { "query-id": "0", "query": "pop", "args": {} }
<<< {"kind":"response","query-id":"0","status":"success","response":null}

push

Send a buffer segment to F★.

  • Query args:
    • kind (string): "lax" for quick checking (no VCs generated) or "full" for complete checking.
    • code (string): A code fragment
    • line (int), column (int): position of the beginning of the fragment in the current buffer. Consecutive pushes should correspond to consecutive buffer segments. Lines are 1-indexed; columns are 0-indexed.
  • status: "success" if F★ accepted that code fragment; "failure" otherwise
  • response (list): A collection of errors or warnings, each with:
    • level (string): One of "error", "warning", "info", "not-implemented"
    • message (string): Issue message
    • ranges (list): A list of ranges, each with:
      • fname (string): Name of file in which the issue occurred, possibly ""
      • beg (list of int): Line and column where the issue starts
      • end (list of int): Line and column where the issue ends
  • Interrupts: This query can be interrupted, except when loading dependencies. Interrupts will cause the query to fail early, returning a possibly-empty list of error messages.
  • Example: 
    >>> { "query-id": "0", "query": "push", "args": { "kind": "full", "code": "module Test\nval a : int\nlet a : nat = 1", "line": 1, "column": 0 } }
<<< { "kind" : "response",
      "query-id" : "0",
      "response" : [{ "level" : "warning",
                      "message" : "Annotation from val declaration overrides inline type annotation",
                      "ranges" : [{ "beg" : [3, 0],
                                    "end" : [3, 15],
                                    "fname" : "<input>" }] }],
      "status" : "success" }

peek

Same as push immediately followed by pop. This is useful to implement on-the-fly checking.

  • Query args: Like push, but kind can also be "syntax" to check syntax only.
  • status: Like push
  • response: Like push
  • Example: 
    >>> { "query-id": "0", "query": "peek", "args": { "kind": "lax", "code": "module Test\nval a : int\nlet a : nat = 1", "line": 1, "column": 0 } }
<<< { "kind" : "response",
      "query-id" : "0",
      "response" : [{ "level" : "warning",
                      "message" : "Annotation from val declaration overrides inline type annotation",
                      "ranges" : [{ "beg" : [3, 0],
                                    "end" : [3, 15],
                                    "fname" : "<input>" }] }],
      "status" : "success" }

auto-complete

Find completions matching a search term (commonly a prefix). Results can be improved by specifying a context — the following contexts are recognized:

  • open, e.g. open FSt|
  • include, e.g. include FS.Li|
  • let-open. e.g. let app = let open FStar.Lis| in append
  • module-alias, e.g. module A = FStar.Se|
  • set-options, e.g. #set-options "--a|bc"
  • reset-options, e.g. #reset-options "--a|bc"
  • code for all other code
  • Query args :
    • partial-symbol (string): Part of a term to be completed. The term is either a partial identifier (in code context), a partial module or namespace name (in open, include, let-open, and module-alias contexts) or an option name with leading dashes (in set-options and reset-options contexts).
    • context (optional, string, default "code"): A completion context (see above)
  • status: always success
  • response (list): A list of 3-element lists [match-length, namespace, candidate]
    • match-length (int): how far the match extends in candidate
    • namespace (string): where the match lives
    • candidate (string): a completion candidate
  • Example: 
    >>> { "query-id": "0", "query": "autocomplete", "args": { "partial-symbol": "fs" } }
<<< { "kind": "response",
      "query-id": "0",
      "status": "success",
      "response": [[2, "Prims", "fst"]]}

>>> { "query-id": "0", "query": "autocomplete", "args": { "partial-symbol": "Pr.fs" } }
<<< { "kind": "response",
      "query-id": "0",
      "status": "success",
      "response": [[8, "", "Prims.fst"]]}

lookup

Find information about an identifier.

  • Query args:
    • symbol (string): A term to get information on (see the symbol argument of the autocomplete query)
    • context (optional, string, default "code"): A completion context (see above)
    • location (optional, { column, line, filename }): where the symbol is in the file (lines are 1-indexed; columns are 0-indexed).
    • requested-info (list of string): Which fields to return (among "name", "defined-at", "documentation", "type", and "definition"). Other fields are returned as null.
  • status: "success" if the symbol was found; "failure" otherwise
  • response (dictionary):
    • "name" (string): Full name of the symbol
    • "defined-at" (dictionary): Location of the symbol's definition
      • "beg": line, column where the definition begins
      • "end": line, column where the definition ends
      • "fname": file in which the symbol was defined
    • "documentation" (string): FsDoc for this symbol
    • "type" (string): Pretty-printed type
    • "definition" (string): Pretty-printed definition
  • Example: 
    >>> { "query-id": "0", "query": "lookup",
      "args": { "symbol": "fst", "requested-info": ["name", "defined-at"] } }
<<< { "response": {
          "definition": null,
          "documentation": null,
          "type": null,
          "defined-at": {
              "end": [615, 7],
              "beg": [615, 4],
              "fname": "/build/fstar/compute/bin/../ulib/prims.fst"
          },
          "name": "Prims.fst" },
      "status": "success",
      "query-id": "0",
      "kind": "response" }

compute

Reduce a term using F★'s normalizer.

  • Query args:
    • term (string): A term to reduce
    • rules (optional, list of string, default to all rules): which reduction rules to use (one or more of "beta", "delta", "iota", "zeta")
  • status: "success" if the termed reduced successfully; "failure" otherwise
  • response: A string containing the reduced term, or an error message in case of failure
  • Interrupts: This query can be interrupted. Interrupts will cause an early "failure" to be returned.
  • Example: 
    >>> { "query-id": "0", "query": "compute", "args": { "term": "let x = (fun x -> x + 1) 1 in x + x" } }
<<< { "kind": "response", "query-id": "0", "status": "success", "response": "4" }

search

Search the current environment for functions or theorems.

  • Query args:
    • terms (string): Search terms (user-provided). No search terms parsing should happen on the client side.
  • status: "success" if results were found; "failure" otherwise
  • response (list): A list of search results, or an error message (string) if no results are found or if the search terms cannot be parsed:
    • lid: Result's ame
    • type: Result's type
  • Example: 
    >>> { "query-id": "0", "query": "search", "args": { "terms": "FStar.List.op_At FStar.List.length" } }
<<< { "response": [{ "type": "(l1:(list 'a@0) -> l2:(list 'a@1) -> Lemma …)",
                     "lid": "append_length" }],
      "status": "success",
      "query-id": "0",
      "kind": "response" }

vfs-add

Map a file into F★'s virtual file system. A vfs-add query for file a.fst with contents xyz tells F★ to assume that a.fst contains xyz ignoring the (possibly non-existent) a.fst on disk.

This query is useful to notify F★ about yet-unsaved edits, as F★ reads the whole current file (to load its dependencies) before processing the first push and before every push following a complete sequence of pops.

  • Query args:
    • filename (optional string, defaults to the current file): The path of the file to map.
    • contents (string): The contents of the file.
  • status: always "success"
  • response: null
  • Example: 
    >>> { "query-id": "1", "query": "vfs-add", "args": { "filename": null, "contents": "module Test\n" } }
<<< { "response": null,
      "status": "success",
      "query-id": "1",
      "kind": "response" }

segment

Split an F★ program into individual definitions.

  • Query args:
    • code (string): A valid F★ program.
  • status: "success" if the program could be parsed into a list of declarations; "failure" otherwise
  • response (dictionary):
    • "decls" (list of dictionaries): A list of contiguous definition ranges
      • "def_range": Range covering a declaration ("beg", "end", and "fname")
  • Example: 
    >>> { "query-id": "0", "query": "segment", "args": { "code": "let a = 1\nlet b = 2" } }
<<< { "response": { "decls": [{ "def_range": { "beg": [1, 0], "end": [1, 9], "fname": "<input>" } },
                              { "def_range": { "beg": [2, 0], "end": [2, 9], "fname": "<input>" } }] },
       "status": "success",
       "query-id": "0",
       "kind": "response" }

List of status messages

error, warning, info messages

  • contents: A string to display to the user.

proof-state

  • contents: A dictionary containing the proof state at the point of a dump, in the following format:

    • label: The string passed to dump
    • depth: Depth for tracing and debugging
    • goals and smt-goals: Lists of dictionaries containing the active goals and the goals that have been passed to the SMT solver, in the following format:
      • hyps: List of hypotheses, containing name and type
      • goal: The goal, containing witness and type
    • location: Optional field, containing location information if available (file name fname, beginning line and column list beg, ending line and column list end)

  • Example:

    {"label": "After applying f",
 "depth": 1,
 "goals": [
     {"hyps": [
         {"name": "h", "type": "Cases.p \/ Cases.q"},
         {"name": "p", "type": "Prims.pure_post Prims.unit"},
         {"name": "uu___", "type": "Prims.squash (forall (pure_result: Prims.unit). Cases.r ==> p pure_result)"}],
     "goal": {"witness": "(*?u61*) _ h p uu___933", "type": "Prims.squash (Cases.q ==> Cases.r)"}}],
 "smt-goals": [],
 "location": {"fname": "examples/tactics/Cases.fst", "beg": [20,35], "end": [20,46]}}

Migration notes

Differences between the old and the new protocol are documented in the commit message that introduced the new protocol (https://github.com/FStarLang/FStar/commit/90e901f502f8dcb3eda2e29208a699921ffa64ec). A simple port (not adding support for new features) should just require reading and writing JSON messages instead of plain text, and removing the #pop queries that used to be required after failed #pushes.

Add a custom footer
Add a custom sidebar
Clone this wiki locally