Editor support for F*

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

Emacs

fstar-mode supports F★'s new IDE protocol, including completion, type hints, documentation queries, and quick navigation.

Vim

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

Atom (discontinued?)

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

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": 1,
      "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" }

High level description

F★'s IDE mode (introduced in version 0.9.4.3) is a simple JSON-based client-server protocol over 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 responses are not directly to a query and do not include a query ID.

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 section of the buffer is 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 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.

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 {} to indicate an empty collection of args, not null.

Server messages can take multiple formats. In all cases, future versions of the protocol may have 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. These messages should be displayed to the user, but even an error-level message doesn't indicate that e.g. a push failed.
```
{ "kind": "message", "level": "…", "contents": "…" }
```
- level is one of "error", "warning", or "info".
- contents is a string to be displayed to the user.
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"
"lookup/documentation"; "lookup/definition": indicate that lookup understand requests for documentation and definitions.

List of queries and responses

`exit`

Exit the current F★ subprocess. This yields a clean exit, though usually just killing the F★ subprocess is fine too.

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": 1
      },
      "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): A list of currently loaded dependencies.

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"
          ]
      },
      "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

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 identifiers matching a search term (commonly a prefix).

Query args :
- partial-symbol (string): Part of an identifier name
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 symbol to get information on
- requested-info (list of string): Which fields to return (among "name", "defined-at", "documentation", "type", and "definition")
status: "success" if the symbol was found; "failure" otherwise
response (dictionary):
- "name" (string): Full name of the symbol
- "defined-at" (string): Location of the symbol's definition (see put)
- "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

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" }

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.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Editor support for F*

Emacs

Vim

Atom (discontinued?)

Adding support for new IDEs

Example

High level description

Message format

List of features

List of queries and responses

`exit`

`describe-protocol`

`describe-repl`

`pop`

`push`

`peek`

`auto-complete`

`lookup`

`compute`

`search`

Migration notes

Clone this wiki locally