lean2/doc/server.org

• Commands
  • Load file
  • Visit file
  • Replace line
  • Insert line
  • Remove line
  • Extracting information
  • Check line
  • Set configuration option
  • Eval
  • Wait
  • Options

Lean can process input incrementally, and extract type information. This feature is useful for implementing "intelligent" support for Lean in editors such as Emacs. It provides a convenient way to access descriptions of functions, overloaded symbols, and typing information. We must use the option --server to enable this feature.

Commands

Lean implements a simple set of commands for loading files, extracting typing information, and "replacing" lines. The commands should be sent to the standard input.

Load file

LOAD [file-name]

This command loads the Lean file named [file-name]. Lean will create a "snapshot" (aka backtracking point) after each command. Lean uses the "snapshots" to process incremental updates efficiently.

Visit file

VISIT [file-name]

Lean can keep information about multiple files. This command sets [file-name] as the "current" file. The remaining commands are all with respect to the current file. If [file-name] has not been loaded yet, then this command will load it. Some of the remaining commands apply "changes" to the current file. The LOAD command can be used to discard all these changes, and enforce the content of the file stored in file system.

Replace line

REPLACE [line-number]
[new-line]

This command replaces the line [line-number] (in the current file) with [new-line]. Lean uses the snapshots to process the request efficiently. If [line-number] is greater than the total number of lines in the lean buffer, then empty lines are introduced. The lines are indexed from 1.

Insert line

INSERT [line-number]
[new-line]

This command inserts [new-line] (in the current file) before line [line-number]. If [line-number] is greater than the total number of lines in the lean buffer, then empty lines are introduced. The lines are indexed from 1.

Remove line

REMOVE [line-number]

Remove line [line-number] (in the current file). The lines are indexed from 1. If [line-number] is greater than the total number of lines in the lean buffer, then the command is ignored.

Extracting information

INFO [line-number] [column-number]?

This command extracts typing information associated with line [line-number] (in the current file) and [column-number]. If [column-number] is not provided then (potentially) long information is not included. Lean produces a possible empty sequence of entries delimited by the lines -- BEGININFO and -- ENDINFO.

-- BEGININFO
[entries]*
-- ENDINFO

If the server is still busy processing a previously requested update, then it produces the output

-- BEGININFO
-- NAY
-- ENDINFO

where NAY stands for "not available yet".

A type information entry is of the form

-- TYPE|[line-number]|[column-number]
[type]
-- ACK

Information for overloaded operators and symbols is of the form

-- OVERLOAD|[line-number]|[column-number]
[overload-1]
--
...
--
[overload-n]
-- ACK

Information for synthesized placeholders is of the form

-- SYNTH|[line-number]|[column-number]
[synthesized-term]
-- ACK

The following two information entries provide information for Lean keywords/symbols and identifiers.

-- SYMBOL|[line-number]|[column-number]
[symbol]
-- ACK

-- IDENTIFIER|[line-number]|[column-number]
[fully-qualified-name]
-- ACK

Information about introduced coercions is of the form

-- COERCION|[line-number]|[column-number]
[coercion-application]
--
[result-type]
-- ACK

When [column-number] is provided in the INFO command, the type of terms surrounded by () is also included. The ouput has the form

-- EXTRA_TYPE|[line-number]|[column-number]
[term]
--
[type]
-- ACK

Here is an example of output produced by Lean

-- BEGININFO
-- TYPE|15|38
num
-- ACK
-- TYPE|15|40
num → num → Prop
-- ACK
-- OVERLOAD|15|42
f
--
foo.f
-- ACK
-- TYPE|15|42
num → num
-- ACK
-- TYPE|15|44
num
-- ACK
-- IDENTIFIER|15|42
foo.f
-- ACK
-- ENDINFO

Check line

As described above, several commands can be used to apply modifications to opened/visited files. These modification reflect modifications performed by the text editor. The command CHECK can be used to double check whether the text editor and Lean have the "same view" of the current file + modifications.

The following commands returns -- OK if the line [line-number] in the current file is [line]. It returns -- MISMATCH line out of range, if [line-number] is too big, and -- MISMATCH expected [lean-line] when there is a mismatch, and Lean expects [line-number] to be [lean-line].

-- CHECK [line-number]
[line]

Set configuration option

The command

-- SET
[option-name] [value]

sets a Lean options, [option-name] must be a valid Lean option. Any option that can be set using the command set_option in a '.lean' file is supported.

This command produces the output

-- BEGINSET
[error]?
-- ENDSET

where the line [error]? is printed if there are errors parsing the SET command (e.g., invalid option name).

Here is an example that forces the Lean pretty printer to display implicit arguments.

-- SET
pp.implicit true

Eval

The following command evaluates a Lean command. It has the effect of evaluating a command in the end of the current file

-- EVAL
[command]

This command produces the output

-- BEGINEVAL
[error]/[output]
-- ENDEVAL

Here is an example that executes the check command to obtain the type of Prop.

-- EVAL
check Prop

If the server is still busy processing a previously requested update, then it produces the output

-- BEGINEVAL
-- NAY
-- ENDEVAL

Wait

The following command is for debugging purposes. It blocks the server until all pending information has been computed.

WAIT

Options

The command OPTIONS display all configuration options available in Lean. It has the form

OPTIONS

The output is a sequence of entries

-- BEGINOPTIONS
[entry]*
-- ENDOPTIONS

where each entry is of the form

-- [name]|[kind]|[default-value]|[description]

The available kinds are: Bool, Int, Unsigned Int, Double, String, and S-Expressions.