batteries icon indicating copy to clipboard operation
batteries copied to clipboard

feat: run `List (MetaM x)` asynchronously, returning an `MLList MetaM x` in the order they return.

Open kim-em opened this issue 2 years ago • 2 comments

Depends on:

  • [x] https://github.com/leanprover/std4/pull/398
  • [x] https://github.com/leanprover/std4/pull/397

Prerequisite for the hint tactic.

kim-em avatar Nov 27 '23 02:11 kim-em

(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.

kim-em avatar Dec 21 '23 02:12 kim-em

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!

kim-em avatar Jul 24 '24 05:07 kim-em