Gabriel Ebner
7036bec999
fix(util/cancellable): fix quadratic runtime with many children
2017-03-23 09:00:59 +01:00
Gabriel Ebner
d26e870aa5
chore(*): fix tests
2017-03-23 09:00:59 +01:00
Gabriel Ebner
cfa0f798ac
fix(util/log_tree): fix memory leak
2017-03-23 09:00:59 +01:00
Gabriel Ebner
677bf43da3
fix(library): fix various leaks
2017-03-23 09:00:59 +01:00
Gabriel Ebner
796097ec31
fix(util/log_tree): fix reference cycle between log_tree and tasks
2017-03-23 09:00:59 +01:00
Gabriel Ebner
3c515cc772
refactor(util/log_tree): use for_each
2017-03-23 09:00:59 +01:00
Gabriel Ebner
b6e79d646d
fix(util/cancellable): actually set interrupt flag
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
f85468159d
fix(library/module): prevent reference to previous versions
2017-03-23 09:00:59 +01:00
Gabriel Ebner
28c71d7dba
fix(library/mt_task_queue): do not wait on freed condition_variables
2017-03-23 09:00:59 +01:00
Gabriel Ebner
fa232a3a1a
fix(util/timer): fix valgrind warning
2017-03-23 09:00:59 +01:00
Gabriel Ebner
fa19b3c94d
fix(library/vm/vm): prevent segfault in out-of-memory conditions
2017-03-23 09:00:59 +01:00
Gabriel Ebner
901cef6629
refactor(util/thread): simplify thread life-cycle
2017-03-23 09:00:59 +01:00
Gabriel Ebner
7fc190c730
fix(mt_task_queue): fix reference cycle between closure and lthread
2017-03-23 09:00:59 +01:00
Gabriel Ebner
667d06108a
chore(*): fix clang warnings
2017-03-23 09:00:58 +01:00
Gabriel Ebner
d22bfbd12a
feat(util/debug): add version of lean_assert that also works in non-debug builds
2017-03-23 08:57:56 +01:00
Gabriel Ebner
52bcfb713f
fix(shell/server): also invalidate non-open files
2017-03-23 08:57:56 +01:00
Gabriel Ebner
5e94f63b3e
feat(library/mt_task_queue): kill all idle workers
2017-03-23 08:57:56 +01:00
Gabriel Ebner
667381b8bd
fix(library/mt_task_queue): bump_prio: handle unsubmitted tasks
2017-03-23 08:57:56 +01:00
Gabriel Ebner
823c451a51
fix(util/thread): detach unjoined threads
2017-03-23 08:57:56 +01:00
Gabriel Ebner
42288198db
fix(kernel/expr): disable caching by default
2017-03-23 08:57:56 +01:00
Gabriel Ebner
56aceae435
fix(library/mt_task_queue): ensure precondition for execute
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
a6d2e11a91
refactor(util/task): remove needs_separate_thread option
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
45820531c4
refactor(util/task): remove switch to disable priority inversion
2017-03-23 08:57:56 +01:00
Gabriel Ebner
26ba9c23a7
refactor(util/task): add eager execution
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
1182d8e7f7
fix(library/module): has_sorry: check examples
2017-03-23 08:57:56 +01:00
Gabriel Ebner
43a7dd8e4f
fix(shell/lean): prevent deadlock
2017-03-23 08:57:56 +01:00
Gabriel Ebner
2edefdcc12
fix(library/vm/vm_task): fix trace messages
2017-03-23 08:57:56 +01:00
Gabriel Ebner
10e354952b
feat(emacs): do not call auto-completion on tab
2017-03-23 08:57:56 +01:00
Gabriel Ebner
aebd18f136
feat(shell/server): only compile region of interest
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
60dd85719c
feat(library/system/io): system.io without axioms
2017-03-22 23:36:05 -07:00
Leonardo de Moura
3f42e5fbd9
chore(util/rb_tree): style
2017-03-22 08:31:48 -07:00
Corey Richardson
52f84c139b
chore(lp): don't use readdir_r on glibc
...
glibc (unfortunately) deprecated readdir_r, as their readdir is already
reentrant. Future versions of POSIX will assume readdir is reentrant,
see https://www.gnu.org/software/libc/manual/html_node/Reading_002fClosing-Directory.html
2017-03-22 08:24:55 -07:00
Leonardo de Moura
59d1b1ee2e
fix(util/rb_tree): avoid warning
...
see #1473
2017-03-22 08:24:17 -07:00
Leonardo de Moura
e6c5ba29d6
fix(library/message_builder): remove unnecessary field
...
see #1473
2017-03-22 08:23:29 -07:00
Sebastian Ullrich
da7e21696e
feat(init/meta/interactive): rw goal info on ,
2017-03-22 07:54:12 -07:00
Sebastian Ullrich
524a381f22
refactor(lean/tactic_notation): better goal info tweak on ,
2017-03-22 07:54:12 -07:00
Leonardo de Moura
c541f90d5b
fix(library/tactic/vm_monitor): compilation warning
2017-03-22 07:40:16 -07:00
Sebastian Ullrich
f9854be13f
feat(frontends/lean/parser): save id info for non-overloaded constants
2017-03-22 07:35:14 -07:00
Sebastian Ullrich
897b4f9db1
fix(frontends/lean/builtin_exprs): override scope behavior for strict quoted names
2017-03-22 07:34:50 -07:00
Sebastian Ullrich
793f0baee8
feat(library/tactic/vm_monitor): use attribute for registering VM monitors
2017-03-22 07:34:27 -07:00
Rob Lewis
2e921dd533
fix(algebra): generalize theorem
2017-03-22 07:34:01 -07:00
Leonardo de Moura
a31de3b7bc
feat(library/unification_hint): improve unification_hint matcher
...
Improvements:
- Use heuristic match explicit arguments first and then match implicit.
- Skip annotations.
- Follow metavariable assigments.
- Use is_def_eq when pattern doest not contain matching variables.
2017-03-21 10:19:34 -07:00
Leonardo de Moura
3a878bd3f4
fix(frontends/lean/interactive): compilation warning with older versions of g++
2017-03-21 08:31:16 -07:00
