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

227 commits

Author SHA1 Message Date
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
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
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
1ee945a31f fix(library): store and validate Lean version of .olean files 
Fixes #1770
 2018-01-23 11:14:18 -08: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
Gabriel Ebner
0579e68ab8 feat(library/export): add option to only export a single declaration 2017-07-14 09:49:24 +01: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
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
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
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
43a7dd8e4f fix(shell/lean): prevent deadlock 2017-03-23 08:57:56 +01:00
Gabriel Ebner
5f872912e0 refactor(shell/lean): set exit status 1 iff at least one error was reported 2017-03-23 08:57:56 +01:00
Gabriel Ebner
595cbb8fe9 refactor(*): task<T>, log_tree, cancellation_token 2017-03-23 08:57:52 +01:00
Leonardo de Moura
e6c5ba29d6 fix(library/message_builder): remove unnecessary field 
see #1473
 2017-03-22 08:23:29 -07:00
Leonardo de Moura
1da93c4d28 feat(CMakeLists, shell/lean): add -D ALPHA=ON cmake option for enabling alpha features (i.e., wip) 
@jroesch This commit also marks --compile as an alpha feature.
 2017-02-26 23:06:45 -08:00
Gabriel Ebner
61c380b534 fix(shell/lean): catch all exceptions 
Fixes #1386.
 2017-02-21 10:54:46 -08:00
Leonardo de Moura
9863755ae1 feat(shell/lean,library/smt): fix SMT2 frontend 2017-02-21 09:28:21 -08:00
Leonardo de Moura
3b28cef858 fix(shell/lean): default heartbeat should be unbounded in batch mode 2017-02-15 16:46:44 -08:00
Leonardo de Moura
01eb27d4a4 feat(util): "deterministic timeout" option 
closes #1134

see #1362

This feature is implemented using a "hearbeat" thread local counter.
We reset the counter whenever we start a new task.
The counter is incremented when:

  1- An object is allocated using small_object_allocator (e.g., VM object)
  2- An object is allocated using memory_pool (e.g., expr, level, rb_tree nodes, list cons-cells, etc)
  3- check_system(...) invocations

We check if the threshold was reached at check_system.
The option --timeout=num can be used to set the limit (in thousands).
The default is unbounded in batch mode.
In server mode, the default is 100000. We can compile the standard library with --timeout=12000

I did not perform many experiments to check how precise this counter is.
I added a new Emacs configuration setting to change the server default.

Here is the wall clock time for different values of --timeout for the
command used on issue #1134

time ../../bin/lean -j 0 --timeout=20000 loop.lean
loop.lean:1:0: error: (deterministic) timeout detected at 'expression equality test' (potential solution: increase timeout threshold)

real	0m1.070s
user	0m1.032s
sys	0m0.036s

time ../../bin/lean -j 0 --timeout=40000 loop.lean
loop.lean:1:0: error: (deterministic) timeout detected at 'expression equality test' (potential solution: increase timeout threshold)

real	0m1.777s
user	0m1.676s
sys	0m0.044s

time ../../bin/lean -j 0 --timeout=50000 loop.lean
loop.lean:1:0: error: (deterministic) timeout detected at 'expression equality test' (potential solution: increase timeout threshold)

real	0m1.985s
user	0m1.920s
sys	0m0.056s

time ../../bin/lean -j 0 --timeout=100000 loop.lean
loop.lean:1:0: error: (deterministic) timeout detected at 'expression equality test' (potential solution: increase timeout threshold)

real	0m3.587s
user	0m3.564s
sys	0m0.020s
 2017-02-07 13:56:12 -08:00
Gabriel Ebner
ea1e6bf3de feat(shell/lean): add default memory limit in server mode 2017-02-07 11:37:07 -08:00
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
Sebastian Ullrich
7040844f9a feat(frontends/lean/parser,shell): complete imports 2017-01-06 14:02:31 -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
c5e0ea2600 fix(shell/lean): make progress display work on emscripten 2016-12-31 15:16:03 +01:00
Sebastian Ullrich
8ccf28abf3 chore(*): remove old code 2016-12-27 10:07:34 -08:00
Gabriel Ebner
99fc13af98 refactor(library/module_mgr): cache olean imports as well 2016-12-20 10:15:19 -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
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
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
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