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

460 commits

Author SHA1 Message Date
Sebastian Ullrich
191d1e7321 chore(shell/server): sync_output command for debugging 2018-03-08 10:06:09 -08:00
Leonardo de Moura
bdea7d420d chore(*): type_context ==> type_context_old 2018-03-05 12:38:24 -08:00
Sebastian Ullrich
f247363305 feat(library/time_task): print cumulative times on --profile 2018-02-19 09:13:24 -08:00
Leonardo de Moura
3771748b4c chore(library/native): remove dead code 
The deleted code was not finished, and we are going to add a new IR
and compiler.
 2018-02-07 17:29:25 -08:00
Nuno Lopes
a69541ab67 fix(msvc): crashes in getopt and read_dir 2018-02-06 10:11:10 -08:00
Nuno Lopes
36f19f1d6e fix(msvc): fix a few more compilation errors 2018-02-06 10:11:10 -08:00
Nuno Lopes
93374bb2bc fix(msvc): add a simple getopt() implementation 2018-02-06 10:11:10 -08:00
Nuno Lopes
7f920d9d37 fix(build): regression in linux build 2018-02-06 10:11:10 -08:00
Sebastian Ullrich
fe2e95def3 fix(library/module_mgr): Revert "feat(library/module_mgr): save .olean files of non-dirty .lean files in server mode" 
This reverts commit 18c2e3739a.
The change introduced a bug where a .olean file may have been saved even if
the corresponding module had produced errors during processing, as long as these
errors were not part of the current region of interest.
 2018-02-05 14:36:27 +01:00
Leonardo de Moura
1e626e382f chore(frontends/smt2): remove SMT2 frontend 2018-01-24 15:21:52 -08:00
Leonardo de Moura
0d83a74b26 fix(library/io,tests/lean): io monad command line arguments, and tests 2018-01-23 15:24:41 -08:00
Leonardo de Moura
0ad5497462 refactor(library/io): make io easier to extend and use 2018-01-23 15:03:31 -08:00
Sebastian Ullrich
18c2e3739a feat(library/module_mgr): save .olean files of non-dirty .lean files in server mode 
Note, currently there is no way for a dirty file to become non-dirty again
 2018-01-23 11:14:18 -08:00
Sebastian Ullrich
67fc899d0d feat(shell/server): sync: default "content" to file content 
This mostly simplifies debugging and testing
 2018-01-23 11:14:18 -08:00
Sebastian Ullrich
e8c057f1de refactor(library/module_mgr): simplify module loading code 2018-01-23 11:14:18 -08:00
Sebastian Ullrich
1ee945a31f fix(library): store and validate Lean version of .olean files 
Fixes #1770
 2018-01-23 11:14:18 -08:00
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