Sebastian Ullrich
75b2b09c08
feat(library/module_mgr): 'trace.import' trace class
2018-09-12 09:14:58 -07:00
Sebastian Ullrich
62671c8b6f
fix(shell/lean): Flycheck doesn't ignore stderr
2018-09-12 08:29:21 -07:00
Sebastian Ullrich
52d4cc10ad
feat(shell/lean,lean4-mode/lean4-flycheck): use stdin for communication
...
no more `flycheck_` files
2018-09-11 16:35:25 -07:00
Sebastian Ullrich
af99f153f8
refactor(library/module{,_mgr},frontends/lean/parser): use absolute module names everywhere for identifying modules, move actual importing from parser to module_mgr
2018-09-11 13:55:25 -07:00
Sebastian Ullrich
716de48078
chore(library/module): remove loaded_module.m_env
...
It was used by `--run` only, which I guess will change quite a bit anyway
2018-09-11 13:55:25 -07:00
Sebastian Ullrich
904d7c4a88
chore(*): remove old task API and task queues
2018-09-11 13:55:25 -07:00
Sebastian Ullrich
af55cb13e7
fix(library/messages,library/init/lean/message): wrap message_log in structure, reverse in the end
2018-09-11 13:55:25 -07:00
Sebastian Ullrich
38208802c6
refactor(*): replace log_tree with simple message_log list, make module_mgr synchronous
2018-09-11 13:55:25 -07:00
Sebastian Ullrich
b3c44ec56e
chore(shell/{server,lean_js}): remove
2018-09-08 18:37:58 -07:00
Leonardo de Moura
81a694e73c
chore(frontends/lean): remove dead code
2018-09-08 15:44:49 -07:00
Leonardo de Moura
58e91559d0
feat(*): use new inductive datatype module
2018-09-06 18:09:22 -07:00
Leonardo de Moura
9626ad919c
chore(library/export): remove text export module
...
This can be implemented in Lean.
2018-06-08 13:36:36 -07:00
Leonardo de Moura
2a79da1ab6
refactor(kernel): move formatting stuff out of the kernel
2018-06-07 16:28:54 -07:00
Leonardo de Moura
c0e1d05199
chore(kernel): type_checker ==> old_type_checker
2018-06-06 16:10:40 -07:00
Leonardo de Moura
75c63ec921
refactor(*): list<name> ==> obj_list<name>
2018-05-23 15:48:43 -07:00
Leonardo de Moura
0556412f8d
refactor(*): add runtime folder
...
@kha The runtime folder includes what is needed to link a
standalone Lean program. It is still contains some unnecessary files.
We will be able to remove them after we release Lean4.
2018-05-14 14:23:56 -07: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
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
