std4#399

Stream: batteries

[Kim Morrison]

Could I ping on std4#399, "run List (MetaM x) asynchronously, returning an MLList MetaM x in the order they return"?

It is a prerequisite for the hint tactic PR's as std4#395, which I would really like to get out into users' hands.

[Eric Wieser]

The effect of this will be that hint is nondeterministic, right?

[Ruben Van de Velde]

Isn't it now?

[Eric Wieser]

Right now I think it runs them in a deterministic order; the proposed change makes them run in parallel, and keep the results based on (nondeterministic) runtime; which means that writing tests for (or diagnosing issues with) hint is going to be tricky

[Ruben Van de Velde]

Ah indeed, #8435 hasn't landed yet

[Eric Wieser]

The ideal solution would be to ask for the heartbeat count of the successful task, and then have a "soft" cancellation that updates the heartbeat limit of the other tasks to not exceed the one that succeeded; but that seems like too much effort for too little gain.

[Joe Hendrix]

How many hint tactics are there typically? If there are many, hints later in the list aren't necessarily going to run until the earlier ones finish.

[Ruben Van de Velde]

Can the tests limit the number of jobs that run concurrently?

[Kim Morrison]

There are currently 7 register_hint commands in Mathlib, but likely that number will grow, although perhap not to more than 20 or so.