Leonardo de Moura
|
d71aab5dc4
|
fix: allow bigger ctor objects
`IR/Checker.lean` is now also checking the maximum number of fields
and scalar size
|
2021-01-29 18:23:38 -08:00 |
|
Leonardo de Moura
|
4848533717
|
fix: make sure we have "heartbeats" even when `-D SMALL_ALLOC=OFF"
|
2021-01-24 19:42:45 -08:00 |
|
Sebastian Ullrich
|
4a262fbc5b
|
fix: remove auto-cancellation of IO tasks
Chained tasks were never auto-canceled, so let's be explicit everywhere
|
2020-12-30 17:03:09 +01:00 |
|
Leonardo de Moura
|
bbafaf8805
|
fix: Array.mk and Array.data externs
|
2020-12-13 11:10:01 -08:00 |
|
Leonardo de Moura
|
6a41d04827
|
fix: missing panics
|
2020-12-08 10:36:53 -08:00 |
|
Leonardo de Moura
|
a454c5e660
|
chore: lean_is_shared
|
2020-10-11 15:10:39 -07:00 |
|
Sebastian Ullrich
|
9e9a036475
|
fix: exclusive MT objects cannot be reused as-is, so never reuse them
|
2020-10-11 17:43:28 +02:00 |
|
Sebastian Ullrich
|
562c7ed5ce
|
feat: expose task priorities
|
2020-09-29 08:01:10 -07:00 |
|
Sebastian Ullrich
|
f3ab43e453
|
doc: task_object state machine
|
2020-09-14 17:57:33 +02:00 |
|
Sebastian Ullrich
|
63d60e6564
|
fix: more robust m_keep_alive implementation not reliant on RC
|
2020-09-14 17:57:33 +02:00 |
|
Sebastian Ullrich
|
469a822cc6
|
chore: checkInterrupted ~> checkCanceled, requestInterrupt ~> cancel
|
2020-09-14 17:57:33 +02:00 |
|
Sebastian Ullrich
|
77cbaa752c
|
fix: Task: make reference and -j0 semantics eager, simplify
|
2020-09-14 17:57:33 +02:00 |
|
Sebastian Ullrich
|
1782352af1
|
feat: optionally run tasks even when already cancelled
|
2020-09-14 17:57:33 +02:00 |
|
Sebastian Ullrich
|
b624b7d03f
|
chore: remove obsolete header
|
2020-08-31 11:09:27 +02:00 |
|
Sebastian Ullrich
|
c88784ef9d
|
refactor: consistent io_result_mk* naming
/cc @leodemoura
|
2020-08-31 11:08:57 +02:00 |
|
Leonardo de Moura
|
90bddeb12b
|
feat: add lean_task_get_own for implementing Task.get
|
2020-08-27 12:07:11 -07:00 |
|
Leonardo de Moura
|
6180ba6d7d
|
chore: rename ST.Ref primitives
|
2020-08-23 12:28:14 -07:00 |
|
Leonardo de Moura
|
350cf4d262
|
chore: copy runtime files to include/lean
|
2020-05-22 14:04:24 -07:00 |
|