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
Leonardo de Moura
58768940e3
chore(shell/server): std::make_unique is a C++14 feature
...
I got a compilation error
2016-12-06 17:22:24 -08:00
Gabriel Ebner
45d0525e52
feat(shell,emacs): new lean server protocol
2016-12-06 17:14:29 -08:00
Gabriel Ebner
61b70a71ce
refactor(shell/server): move auto-completion code to a separate file
2016-12-06 17:14:29 -08:00
Gabriel Ebner
ddf103a48d
feat(shell/server): support multiple files
2016-12-06 17:14:29 -08:00
Leonardo de Moura
378856fdb9
chore(*): comment native compiler tests
...
They do not work in all platforms.
2016-12-05 16:42:40 -08:00
Leonardo de Moura
e59515df5f
chore(*): fix style
2016-12-05 16:39:58 -08:00
Jared Roesch
e65d90ac79
feat(*): C++ code generator
...
in progress move of Lean.native to init
2016-12-05 16:11:41 -08:00
Gabriel Ebner
d5372e770f
fix(shell/lean): wait for all tasks to finish
2016-12-05 13:26:00 -08:00
Gabriel Ebner
e07cdcb063
fix(shell/lean): nicer error message for file not found
2016-12-05 13:26:00 -08:00
Gabriel Ebner
6bfbb79d6e
fix(shell/lean): add missing colon to 'A' option
2016-12-05 13:26:00 -08:00
Leonardo de Moura
a9d3f36f76
feat(util/thread,library/mt_task_queue): add lthread
2016-12-03 11:29:22 -08:00
Gabriel Ebner
26f0325e9b
fix(shell/server): do not fail if module parsing throws an exception
2016-12-02 08:47:46 -08:00
Leonardo de Moura
79d87138f0
feat(util/memory): simplify memory tracking code
2016-12-01 16:07:46 -08:00
Gabriel Ebner
ae21a6cae8
feat(shell/lean): support stdin redirection in server mode
...
This is useful if you're debugging lean-server in an IDE which cannot
redirect stdin, and also if you want to run `gdb --args lean
--server=some.file`.
2016-12-01 10:02:14 -08:00
Gabriel Ebner
000d97a9a6
fix(frontends/lean/parser): wrap snapshot in shared_ptr
2016-11-30 11:27:02 -05:00
Gabriel Ebner
c3f72ec0d8
fix(library/module_mgr): do not copy module_info
2016-11-30 11:26:59 -05:00
Leonardo de Moura
d40e97b4bc
chore(*): compilation errors, fix style, fix warnings
2016-11-29 11:35:01 -08:00
Gabriel Ebner
f756e9ed92
fix(shell/lean): set global ios
2016-11-29 11:12:44 -08:00
Gabriel Ebner
3ecfddcbd5
fix(*): fix build
2016-11-29 11:12:43 -08:00
Gabriel Ebner
e448e4e129
refactor(util/task_queue): merge module_task into task and cancel by position
2016-11-29 11:12:43 -08:00
Leonardo de Moura
0b2867d939
fix(shell/server): gcc compilation error
2016-11-29 11:12:43 -08:00
Gabriel Ebner
339ade623d
chore(shell/lean): clean up command-line arguments
2016-11-29 11:12:43 -08:00
Gabriel Ebner
a8df381d20
feat(*): parallel compilation
2016-11-29 11:12:40 -08:00
Leonardo de Moura
bd70e29926
chore(shell/leandoc): fix style
2016-11-29 10:38:22 -08:00
Leonardo de Moura
398af80584
feat(shell/leandoc): add support for "brief" description
...
This feature is similar to the one available in doxygen.
2016-11-27 21:42:05 -08:00
