Commits on May 11, 2024

1. 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).
   
   (cherry picked from commit 25e94f9)

   

   tydeu authored and github-actions[bot] committed May 11, 2024
   Configuration menu

   • View commit details
   • Copy full SHA for c379445
   • Browse repository at this point

   Copy the full SHA

   c379445 View commit details

   Browse the repository at this point in the history