lean2/doc/server.org

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

#+BEGIN_SRC
LOAD [file-name]
#+END_SRC

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

#+BEGIN_SRC
VISIT [file-name]
#+END_SRC

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

#+BEGIN_SRC
REPLACE [line-number]
[new-line]
#+END_SRC

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

#+BEGIN_SRC
INSERT [line-number]
[new-line]
#+END_SRC

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

#+BEGIN_SRC
REMOVE [line-number]
#+END_SRC

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

#+BEGIN_SRC
INFO [line-number]
#+END_SRC

This command extracts typing information associated with line
=[line-number]= (in the current file).
Lean produces a possible empty sequence of entries delimited by the lines
=-- BEGININFO= and =-- ENDINFO=.

#+BEGIN_SRC
-- BEGININFO
[entries]*
-- ENDINFO
#+END_SRC

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

#+BEGIN_SRC
-- BEGININFO
-- NAY
-- ENDINFO
#+END_SRC

where =NAY= stands for "not available yet".

A type information entry is of the form

#+BEGIN_SRC
-- TYPE|[line-number]|[column-number]
[type]
-- ACK
#+END_SRC

Information for overloaded operators and symbols is of the form

#+BEGIN_SRC
-- OVERLOAD|[line-number]|[column-number]
[overload-1]
--
...
--
[overload-n]
-- ACK
#+END_SRC

Information for synthesized placeholders is of the form

#+BEGIN_SRC
-- SYNTH|[line-number]|[column-number]
[synthesized-term]
-- ACK
#+END_SRC

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

#+BEGIN_SRC
-- SYMBOL|[line-number]|[column-number]
[symbol]
-- ACK
#+END_SRC

#+BEGIN_SRC
-- IDENTIFIER|[line-number]|[column-number]
[fully-qualified-name]
-- ACK
#+END_SRC

Here is an example of output produced by Lean

#+BEGIN_SRC
-- 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
#+END_SRC

** 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]=.

#+BEGIN_SRC
-- CHECK [line-number]
[line]
#+END_SRC

** Set configuration option

The command

#+BEGIN_SRC
-- SET
[option-name] [value]
#+END_SRC

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

#+BEGIN_SRC
-- BEGINSET
[error]?
-- ENDSET
#+END_SRC

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.

#+BEGIN_SRC
-- SET
pp.implicit true
#+END_SRC

** Eval

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

#+BEGIN_SRC
-- EVAL
[command]
#+END_SRC

This command produces the output

#+BEGIN_SRC
-- BEGINEVAL
[error]/[output]
-- ENDEVAL
#+END_SRC

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

#+BEGIN_SRC
-- EVAL
check Prop
#+END_SRC

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

#+BEGIN_SRC
-- BEGINEVAL
-- NAY
-- ENDEVAL
#+END_SRC

** Wait

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

#+BEGIN_SRC
WAIT
#+END_SRC

** Options

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

#+BEGIN_SRC
OPTIONS
#+END_SRC

The output is a sequence of entries

#+BEGIN_SRC
-- BEGINOPTIONS
[entry]*
-- ENDOPTIONS
#+END_SRC

where each entry is of the form

#+BEGIN_SRC
-- [name]|[kind]|[default-value]|[description]
#+END_SRC

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