lean4-htt/src/runtime
Mac Malone 25e94f916f
feat: IO.TaskState (#4097)
Adds `IO.getTaskState` which returns the state of a `Task` in the Lean
runtime's task manager. The `TaskState` inductive has 3 constructors:
`waiting`, `running`, and `finished`. The `waiting` constructor
encompasses the waiting and queued states within the C task object
documentation, because the task object does not provide a low cost way
to distinguish these different forms of waiting. Furthermore, it seems
unlikely for consumers to wish to distinguish between these internal
states. The `running` constructor encompasses both the running and
promised states in C docs. While not ideal, the C implementation does
not provide a way to distinguish between a running `Task` and a waiting
`Promise.result` (they both have null closures).
2024-05-10 23:04:54 +00:00
..
alloc.cpp chore: fix more typos in comments 2023-10-08 14:37:34 -07:00
alloc.h
allocprof.cpp
allocprof.h
apply.cpp chore: update script/apply.lean semantics 2022-11-07 19:47:04 -08:00
apply.h fix: split libInit_shared out of libleanshared (#3421) 2024-02-22 19:16:32 +00:00
array_ref.h
buffer.h
CMakeLists.txt fix: do not dllexport symbols in core static libraries (#3601) 2024-03-15 11:58:34 +00:00
compact.cpp doc: expand an error message about compacting closures (#3627) 2024-03-07 20:02:23 +00:00
compact.h fix: split libInit_shared out of libleanshared (#3421) 2024-02-22 19:16:32 +00:00
debug.cpp
debug.h fix: split libInit_shared out of libleanshared (#3421) 2024-02-22 19:16:32 +00:00
exception.cpp
exception.h fix: split libInit_shared out of libleanshared (#3421) 2024-02-22 19:16:32 +00:00
flet.h
hash.cpp chore: replace all hashes by murmurhash 2022-12-01 20:18:14 -08:00
hash.h chore: replace all hashes by murmurhash 2022-12-01 20:18:14 -08:00
init_module.cpp fix: split libInit_shared out of libleanshared (#3421) 2024-02-22 19:16:32 +00:00
init_module.h fix: split libInit_shared out of libleanshared (#3421) 2024-02-22 19:16:32 +00:00
int64.h
interrupt.cpp feat: propagate maxHeartbeats to kernel (#4113) 2024-05-09 17:44:19 +00:00
interrupt.h feat: propagate maxHeartbeats to kernel (#4113) 2024-05-09 17:44:19 +00:00
io.cpp feat: IO.TaskState (#4097) 2024-05-10 23:04:54 +00:00
io.h fix: split libInit_shared out of libleanshared (#3421) 2024-02-22 19:16:32 +00:00
list_ref.h
load_dynlib.cpp chore: define WIN32_LEAN_AND_MEAN 2022-04-06 09:38:19 +02:00
load_dynlib.h fix: split libInit_shared out of libleanshared (#3421) 2024-02-22 19:16:32 +00:00
memory.cpp chore: put throws in separate function for debugger 2023-01-23 09:27:09 -08:00
memory.h fix: split libInit_shared out of libleanshared (#3421) 2024-02-22 19:16:32 +00:00
mpn.cpp
mpn.h
mpz.cpp feat: introduce native functions for Int.ediv / Int.emod (#3376) 2024-02-19 15:04:51 +00:00
mpz.h fix: split libInit_shared out of libleanshared (#3421) 2024-02-22 19:16:32 +00:00
mutex.cpp feat: Mutex, Condvar 2022-09-05 08:52:46 -07:00
mutex.h feat: Mutex, Condvar 2022-09-05 08:52:46 -07:00
object.cpp feat: IO.TaskState (#4097) 2024-05-10 23:04:54 +00:00
object.h feat: IO.TaskState (#4097) 2024-05-10 23:04:54 +00:00
object_ref.cpp
object_ref.h fix: split libInit_shared out of libleanshared (#3421) 2024-02-22 19:16:32 +00:00
option_ref.h
optional.h
pair_ref.h
platform.cpp feat: add internal flag lean_has_llvm_backend 2023-11-02 23:21:47 +01:00
platform.h
process.cpp feat: IO.Process.get/setCurrentDir (#4036) 2024-05-02 13:49:10 +00:00
process.h
sharecommon.cpp refactor: generalize ShareCommon to a typeclass (#1537) 2022-08-29 09:34:38 -07:00
sstream.h
stack_overflow.cpp feat: Web Assembly Build (#2599) 2023-10-04 09:04:20 +02:00
stack_overflow.h
stackinfo.cpp fix: split libInit_shared out of libleanshared (#3421) 2024-02-22 19:16:32 +00:00
stackinfo.h fix: split libInit_shared out of libleanshared (#3421) 2024-02-22 19:16:32 +00:00
string_ref.h
thread.cpp feat: thread initialization for reverse FFI (#3632) 2024-03-07 17:02:47 +00:00
thread.h feat: thread initialization for reverse FFI (#3632) 2024-03-07 17:02:47 +00:00
utf8.cpp feat: add model implementation for UTF8 enc/dec (#3961) 2024-04-22 10:24:53 +00:00
utf8.h feat: UTF-8 string validation (#3958) 2024-04-20 18:36:37 +00:00