385 lines
9 KiB
Org Mode
385 lines
9 KiB
Org Mode
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.
|
|
|
|
** Synchronize
|
|
|
|
The following command can be used to make sure the front-end application
|
|
and lean have the same "view". It resets the contents associated with current visited file/buffer.
|
|
|
|
#+BEGIN_SRC
|
|
SYNC [num]
|
|
line_1
|
|
...
|
|
line_num
|
|
#+END_SRC
|
|
|
|
** 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] [column-number]?
|
|
#+END_SRC
|
|
|
|
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=.
|
|
|
|
#+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
|
|
|
|
Information about introduced coercions is of the form
|
|
|
|
#+BEGIN_SRC
|
|
-- COERCION|[line-number]|[column-number]
|
|
[coercion-application]
|
|
--
|
|
[result-type]
|
|
-- ACK
|
|
#+END_SRC
|
|
|
|
When =[column-number]= is provided in the =INFO= command, the type of terms surrounded by =()=
|
|
is also included. The ouput has the form
|
|
|
|
#+BEGIN_SRC
|
|
-- EXTRA_TYPE|[line-number]|[column-number]
|
|
[term]
|
|
--
|
|
[type]
|
|
-- 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=.
|
|
|
|
** Find pattern
|
|
|
|
Given a sequence of characters, the command =FINDP= uses string fuzzy matching to
|
|
find declarations in the environment. The procedure uses [Bitap algorithm](http://en.wikipedia.org/wiki/Bitap_algorithm).
|
|
The approximate match is defined in terms of [Levenshtein distance](http://en.wikipedia.org/wiki/Levenshtein_distance).
|
|
The matches are sorted based on this distance.
|
|
|
|
#+BEGIN_SRC
|
|
FINDP [line-number]
|
|
[pattern]
|
|
#+END_SRC
|
|
|
|
The line number =[line-number]= is used to select the environment object that will be used to perform the search.
|
|
Only declarations in the environment are considered by =FINDP=.
|
|
The output has the following form
|
|
|
|
#+BEGIN_SRC
|
|
-- BEGINFINDP [NAY]? [STALE]?
|
|
[entries]*
|
|
-- ENDFINDP
|
|
#+END_SRC
|
|
|
|
The modifier =NAY= is included when the environment object for the given line is not available yet.
|
|
The modifier =STALE= is included to indicate that an environment object is being used, but it
|
|
does not contain the latest changes.
|
|
|
|
The entries are of the form
|
|
|
|
#+BEGIN_SRC
|
|
[name]|[type]
|
|
#+END_SRC
|
|
|
|
The types are printed without using line breaks.
|
|
The command =FINDP= is mainly used to implement auto-completion.
|
|
|
|
** Find declarations for "placeholder/goal"
|
|
|
|
A declaration may contain placeholders/goals =_=. Some of these placeholders are instantiated automatically by Lean.
|
|
Others, must be manually filled by the user. The command =FINDG= generates a sequence of declarations that may be used to
|
|
"fill" a particular placeholder. This command is only available if the declaration containing =_= is type correct, and
|
|
lean "knows" what is the expected type for =_=.
|
|
|
|
#+BEGIN_SRC
|
|
FINDG [line-number] [column-number]
|
|
[filters]*
|
|
#+END_SRC
|
|
|
|
The character at the given =[line-number]= and =[column-number]= must be a =_=.
|
|
The command also accepts a sequence of filters of the form =+[id_1]= and =-[id_2]=.
|
|
Lean will only consider declarations whose name contains =id_1= and does not contain =id_2=.
|
|
Here is an example:
|
|
|
|
#+BEGIN_SRC
|
|
FINDG 48 10
|
|
+intro -and -elim
|
|
#+END_SRC
|
|
|
|
For the command above, lean will print any declaration whose resultant type matches the type expected by =_=, and
|
|
whose name contains =intro= but does not contain =and= and =elim=.
|
|
Lean does not display "trivial" matches. We say a match is trivial if the resultant type of a declaration
|
|
matches anything.
|
|
|
|
The output produced by =FINDG= uses the same format used by =FINDP=.
|