Gabriel Ebner
9e7ca0a969
feat(checker): add leanchecker executable
2017-01-31 09:39:31 +01:00
Gabriel Ebner
2f07bf352c
refactor(library/standard_kernel): move standard kernel into kernel
2017-01-31 09:39:31 +01:00
Leonardo de Moura
cce88c6190
refactor(frontends/lean): interactive tactic support
...
After this commit, new interactice tactic classes can be added without
writing C++ code (see example: tests/lean/run/my_tac_class.lean).
The tactic_evaluator was simplified, and all the complexity has been
moved to tactic_notation, and lean code.
We can now inspect the intermediate states produced by the rewrite
tactic.
The function (@scope_trace _ line col thunk) can be used to position trace
messages produced by thunk. If line/col are not provided (i.e., we
just write (scope_trace thunk)), then line/col are filled with the
position of this term by the elaborator.
We can visualize the intermediate tactic states inside nested blocks
such as (try { ... })
The new infrastructure can be used to implement custom tactic_state
pretty printers.
2017-01-21 22:38:47 -08:00
Leonardo de Moura
c52be7e8c5
feat(frontends/lean,shell): autocompletion for ^.
...
@kha, I added autocompletion for ^. I try to elaborate the expression
before ^. using the local context provided by the parser.
The autocompletion only works if the type for the expression before ^. can be
inferred. This is a big limitation because this information cannot be
obtained in many cases. Here are examples that do not work:
meta def proof_for (e : expr) : smt_tactic expr :=
do cc ← to_cc_state, cc^.proof_for e
--^ does not work here
If we annotate cc with its type, it works:
meta def proof_for (e : expr) : smt_tactic expr :=
do cc : cc_state ← to_cc_state, cc^.proof_for e
--^ works
We don't have typing information on the equation lhs at
autocompletion time. So, the following will not work
private meta def mk_smt_goals_for (cfg : smt_config)
: list expr → list smt_goal → list expr → tactic (list smt_goal × list expr)
| [] sr tr := return (sr^.reverse, tr^.reverse)
--^ does not work since
| (tg::tgs) sr tr := ...
2017-01-17 19:27:59 -08:00
Gabriel Ebner
7daefedf05
chore(shell/server): remove hard limit on number of reported tasks
2017-01-17 17:10:37 -08:00
Gabriel Ebner
a230c47178
feat(util/task_queue,emacs,*): highlight running tasks with different background color
2017-01-17 17:10:37 -08:00
Sebastian Ullrich
7b049e7d55
fix(shell/server): prevent empty prefix completion for declarations
2017-01-17 16:38:00 -08:00
Sebastian Ullrich
b180c54c0e
feat(shell): move lean.js to server mode
2017-01-13 07:34:54 -08:00
Leonardo de Moura
a3c7ca1501
feat(shell/completion): do not include internal attribute names in auto completion
2017-01-11 08:40:36 -08:00
Sebastian Ullrich
83bddce900
feat(frontends/lean/info_manager,shell/server,emacs/lean-type): info: provide more metadata
...
* docs: attributes, options, identifiers
* location: attributes, imports
2017-01-11 15:29:14 +01:00
Sebastian Ullrich
82bcdebf7c
fix(shell/completion): remove duplicate completion candidates
...
VS Code does not automatically remove them
2017-01-10 14:42:48 -08:00
Leonardo de Moura
80d0b8d5f5
chore(library,shell): fix style
2017-01-10 09:00:17 -08:00
Sebastian Ullrich
3ae4d0fbee
feat(shell/completion,emacs/lean-company): provide doc string and location with completion candidate
2017-01-10 16:19:32 +01:00
Sebastian Ullrich
481a217722
feat(shell/completion): prefer exact prefix matches for all completion modes
2017-01-10 12:25:33 +01:00
Sebastian Ullrich
cc3126e944
feat(frontends/lean,library/scoped_ext,shell): complete namespaces
2017-01-10 12:25:33 +01:00
Sebastian Ullrich
fb294f4415
chore(shell/server): info: skip "record" output field if null
2017-01-10 12:25:33 +01:00
Sebastian Ullrich
3c89a79144
feat(shell/completion): sort completions alphabetically (secondary)
2017-01-10 12:25:33 +01:00
Sebastian Ullrich
b04df04120
feat(frontends/lean): rework and simplify completion parsing, enabling completion of empty prefixes
2017-01-10 12:25:33 +01:00
Sebastian Ullrich
7ef1bd1a15
chore(tests/lean/interactive): simplify input format and test full completion output
2017-01-10 12:25:33 +01:00
Leonardo de Moura
b86aef1ff0
feat(shell/completion): do not show internal declarations
2017-01-06 14:14:43 -08:00
Leonardo de Moura
44ef2f4eeb
feat(shell/completion): only filter class projections
2017-01-06 14:06:17 -08:00
Sebastian Ullrich
26e2aeec7a
feat(frontends/lean,shell): complete attributes
2017-01-06 14:02:31 -08:00
Sebastian Ullrich
2816d3a036
feat(frontends/lean,shell): complete interactive tactics
2017-01-06 14:02:31 -08:00
Sebastian Ullrich
7040844f9a
feat(frontends/lean/parser,shell): complete imports
2017-01-06 14:02:31 -08:00
Gabriel Ebner
6f8ccb5873
fix(CMakeLists): emscripten: pass compiler flags to gmp and mpfr as well
2017-01-06 01:04:36 -08:00
Gabriel Ebner
fb2ac90cf4
chore(tests/lean/fail): add tests that check for positive exit values
2017-01-05 18:09:28 -08:00
Gabriel Ebner
063130ee18
feat(kernel/environment): add function that checks whether all proofs are correct
2017-01-05 18:09:28 -08:00
Gabriel Ebner
90ab29d7a3
chore(CMakeLists): rename misleading LEAN_SERVER option
2017-01-05 18:08:59 -08:00
Gabriel Ebner
f6b8eb6821
feat(util/task_queue): lazy tasks
2017-01-04 16:30:22 -08:00
Leonardo de Moura
2e15304f05
feat(frontends/lean): add support for smt_state in the info_manager
2017-01-04 14:23:48 -08:00
Gabriel Ebner
ae7c8f4070
fix(shell/lean_js): the and_comm name is taken now
2016-12-31 15:19:58 +01:00
Gabriel Ebner
c5e0ea2600
fix(shell/lean): make progress display work on emscripten
2016-12-31 15:16:03 +01:00
Sebastian Ullrich
98398b16f3
feat(frontends/lean,shell): implement completing options
2016-12-27 21:41:02 -08:00
Sebastian Ullrich
3e2d1de21a
perf(shell/server,emacs): do not actually compute completions during preliminary 'complete' requests
2016-12-27 21:41:02 -08:00
Sebastian Ullrich
d228c24c81
feat(shell/server,emacs): autocompletion based on server-side parsing
2016-12-27 21:41:02 -08:00
Sebastian Ullrich
daf839e0d5
feat(frontends/lean,shell/server): report current goal anywhere within begin-end/by
2016-12-27 10:07:34 -08:00
Sebastian Ullrich
33ec940604
perf(shell/server): cancel previous 'info' task before starting a new one
2016-12-27 10:07:34 -08:00
Sebastian Ullrich
88adce1ec3
fix(shell/server): ignore exceptions during reparsing
2016-12-27 10:07:34 -08:00
Sebastian Ullrich
47264ef6fd
fix(shell/server,emacs/lean-flycheck): do not report tiny tasks as current
2016-12-27 10:07:34 -08:00
Sebastian Ullrich
fa44dc60cb
fix(shell/server): don't send out messages from reparsing
2016-12-27 10:07:34 -08:00
Sebastian Ullrich
5cb06ea912
perf(frontends/lean/parser): break at break_at_pos even if not on an interesting token
2016-12-27 10:07:34 -08:00
Sebastian Ullrich
8ccf28abf3
chore(*): remove old code
2016-12-27 10:07:34 -08:00
Sebastian Ullrich
c9a8c02fdc
feat(emacs,frontends/lean/parser,shell/server): more accurate info command using server-side parsing
2016-12-27 10:07:34 -08:00
Gabriel Ebner
0550d2a6ac
refactor(library/module): import all modules in a single call
2016-12-20 10:15:19 -08:00
Gabriel Ebner
99fc13af98
refactor(library/module_mgr): cache olean imports as well
2016-12-20 10:15:19 -08:00
Gabriel Ebner
23be9bc0c2
fix(shell/CMakeLists): ignore temporary emacs files
2016-12-20 10:13:58 -08:00
Gabriel Ebner
d89512b6fc
fix(util/task_queue): fix undefined behavior with null references
2016-12-15 09:48:57 -08:00
Gabriel Ebner
1963c8650f
feat(shell/server): support regions of interest consisting of multiple files
2016-12-12 12:40:40 -08:00
Gabriel Ebner
d5bca10af8
feat(shell/server,emacs): show currently executing task if even from another file
2016-12-12 12:40:40 -08:00
Gabriel Ebner
902df5d134
feat(shell/server,emacs): show list of currently running tasks
2016-12-12 12:40:40 -08:00
