max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
11083 commits 1 branch 0 tags 5.3 GiB
Commit graph

360 commits

Author SHA1 Message Date
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
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