batteries
batteries copied to clipboard
feat: run `List (MetaM x)` asynchronously, returning an `MLList MetaM x` in the order they return.
Depends on:
- [x] https://github.com/leanprover/std4/pull/398
- [x] https://github.com/leanprover/std4/pull/397
Prerequisite for the hint tactic.
(prio := .max)seems suspicious. Why is it needed?
The prio := .max only appears on map tasks which are doing minor work after the main workload has been completed. Setting the priority higher makes it less likely that returning the final value will get stuck at the map stage behind any long-running tasks which have yet to be started.
I'm not going to work on this in the near future. If anyone would like to adopt, and think about a better design, please go ahead!