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

444 commits

Author SHA1 Message Date
Sebastian Ullrich
37e2f085e4 chore(shell/CMakeLists): leanpkg integration tests 2017-12-30 19:31:55 +01:00
Sebastian Ullrich
adc0d250fc fix(shell/lean): show progress messages only when stdout is a terminal 2017-12-30 17:39:53 +01:00
Gabriel Ebner
8837ce0f31 fix(shell/lean): add missing newline 2017-08-29 16:40:04 +02:00
Mario Carneiro
f369e34bd6 chore(library/standard): remove standard.lean (unused, and confusing given stdlib) 2017-07-28 16:47:53 +01:00
Mario Carneiro
667e1e1381 fix(CMakeLists): remove executable before overwriting on windows, third try 
This one is tested to work on my machine
 2017-07-21 05:09:02 -07:00
Gabriel Ebner
17a501f024 fix(CMakeLists): remove executable before overwriting on windows, second try 
@digama0 Does this fix the problem for you?
 2017-07-21 10:03:32 +01:00
Gabriel Ebner
3943ffccfb fix(shell/CMakeLists): remove lean executable before copying 
On windows, running executables cannot be overwritten.
 2017-07-21 02:00:36 -07:00
Gabriel Ebner
0579e68ab8 feat(library/export): add option to only export a single declaration 2017-07-14 09:49:24 +01:00
Gabriel Ebner
c7928c16b3 fix(shell/server): do not cancel hole commands 
Nonterminating hole commands are caught by the timeout anyway.
Fixes #1729.
 2017-07-06 16:29:57 +02:00
Gabriel Ebner
adfa713dea fix(shell/server): report interrupted exception 2017-07-06 16:28:41 +02:00
Gabriel Ebner
08eceb6d85 fix(shell/server): fix sequence number in async responses 2017-06-29 16:43:12 +02:00
Gabriel Ebner
ee94f7688c fix(shell/lean): do not repeat progress messages 
This should fix the problem with the 4MB log limit on Travis.
 2017-06-29 13:04:27 +02:00
Gabriel Ebner
33679a11b9 feat(shell/lean,util/log_tree): show currently executing task in lean --make 
@dselsam @johoelzl This should make it easier to diagnose which proofs
time out or take a very long time.
 2017-06-27 18:48:25 +02:00
Gabriel Ebner
11be4e5faf fix(CMakeLists): increase node stack size for emscripten 2017-06-27 08:44:01 +02:00
Gabriel Ebner
437ab1fc27 feat(server): add command to get all holes in a file 2017-06-15 10:23:26 +02:00
Leonardo de Moura
7557a9e000 feat(shell/server,frontends/lean): add "hole_commands" server command 
The new command returns the list of registered/applicable hole
commands.
 2017-06-14 22:16:34 -07:00
Leonardo de Moura
7528e14e68 feat(frontends/lean,shell/server): "hole" command 2017-06-14 21:56:17 -07:00
Leonardo de Moura
c0556df2ec feat(shell/server): add "hole" server command skeleton 2017-06-14 11:44:32 -07:00
Gabriel Ebner
1e7e440951 fix(library/module_mgr): actually cancel invalidated tasks 2017-06-05 19:36:09 +02:00
Leonardo de Moura
24048c4258 fix(*): gcc 7 weird uninitialized warnings 
I think most of them are incorrect.
I didn't find a workaround for the one at json.hpp.
So, I just disabled this warning at server.cpp
 2017-05-31 18:05:03 -07:00
Gabriel Ebner
40eb5d0556 feat(library/module_mgr): skip reverse dependency rebuild if file content is unchanged 2017-05-23 11:14:30 -07:00
Gabriel Ebner
07c25338b9 feat(shell/server): add search command 2017-05-22 09:40:38 -07:00
Gabriel Ebner
28a259f2d3 refactor(shell/server): unify async response handling 2017-05-22 09:40:38 -07:00
Gabriel Ebner
acb03fb704 feat(shell): emscripten build with webassembly 2017-05-01 14:11:39 -07:00
Gabriel Ebner
3810e8950d refactor(util/lean_path,util/path): separate search path functions 2017-05-01 14:11:38 -07:00
Gabriel Ebner
d79909a1b8 refactor(util/lean_path): support leanpkg.path files 2017-05-01 14:11:38 -07:00
Gabriel Ebner
baa4c48f1f refactor(util/lean_path): explicitly pass around search path 2017-05-01 14:11:38 -07:00
Sebastian Ullrich
e9a6c544af refactor(frontends/lean/{elaborator,structure_cmd}): compile structure inheritance to nested fields 2017-04-24 19:35:15 +02:00
Gabriel Ebner
9424e6fa24 refactor(frontends/lean/definition_cmds): make profiling threshold configurable 2017-04-23 11:22:41 -07:00
Gabriel Ebner
e2fa363423 feat(library/system/io,shell/lean): add --run switch 2017-04-11 16:41:30 -07:00
Sebastian Ullrich
3c8e176fb0 fix(frontends/lean/interactive): fix info on new field notation 2017-03-31 09:40:49 -07:00
Gabriel Ebner
467e547160 fix(shell/CMakeLists): run all tests serially 2017-03-30 06:49:42 +02:00
Gabriel Ebner
3253a79e77 refactor(tests/lean/fail): use test suite runner 2017-03-30 06:04:00 +02:00
Sebastian Ullrich
678044d1d6 refactor(shell/lean): use log tree node from module_info 2017-03-30 06:04:00 +02:00
Sebastian Ullrich
4a33045b84 chore(tests/lean,shell/lean): run leantests and leanruntests in parallel 2017-03-30 06:04:00 +02:00
Gabriel Ebner
318910f99b refactor(frontends/lean/parser): store snapshots in a lazy async list 2017-03-27 14:00:53 -07:00
Gabriel Ebner
e784fad8c6 feat(shell/server,emacs): add visible lines and above checking mode 2017-03-24 09:08:17 +01:00
Leonardo de Moura
ccd9a8212a chore(shell/lean_js): compilation warning 2017-03-23 12:56:35 -07:00
Gabriel Ebner
a6f7f31e85 refactor(shell,emacs): handle different checking modes in server 2017-03-23 09:07:09 +01:00
Gabriel Ebner
9dfd8e1018 fix(shell/server): fix field completion 2017-03-23 09:03:43 +01:00
Gabriel Ebner
5e29fe227e fix(shell/server): set global ios in info and complete tasks 2017-03-23 09:03:43 +01:00
Gabriel Ebner
c7ca21625c feat(util/log_tree): annotate nodes with detail levels 2017-03-23 09:03:43 +01:00
Gabriel Ebner
d26e870aa5 chore(*): fix tests 2017-03-23 09:00:59 +01:00
Gabriel Ebner
d0cc6f16b1 fix(shell/server): remove cancellation token from snapshot 2017-03-23 09:00:59 +01:00
Gabriel Ebner
52bcfb713f fix(shell/server): also invalidate non-open files 2017-03-23 08:57:56 +01:00
Gabriel Ebner
1524979dbf feat(emacs,shell/server): add different region-of-interest options 2017-03-23 08:57:56 +01:00
Gabriel Ebner
2799375d24 chore(*): style 2017-03-23 08:57:56 +01:00
Gabriel Ebner
bbe30e1bc5 feat(library/module): only report sorry once per declaration 2017-03-23 08:57:56 +01:00
Gabriel Ebner
3eba8d3ffc refactor(util/task): do not propagate errors 2017-03-23 08:57:56 +01:00
Gabriel Ebner
43a7dd8e4f fix(shell/lean): prevent deadlock 2017-03-23 08:57:56 +01:00