multithreading in tactics?

Stream: general

[Scott Morrison]

There's no access to multithreading from inside a begin ... end block, is there?

[Scott Morrison]

library_search would love to fire off multiple tasks and just get an answer from the first one to succeed.

[Mario Carneiro]

use task

[Mario Carneiro]

I've tested it to work in tactics

[Scott Morrison]

can you fire off 10, and ask for the first completion?

[Mario Carneiro]

Not sure about nondeterministic uses though

[Mario Carneiro]

I had some proposals for nondeterminism primitives but they never landed in core AFAIK

[Scott Morrison]

It seems there's no way to get the first completion. Is this the entire API?

meta constant {u} task : Type u → Type u

namespace task

meta constant {u} get {α : Type u} (t : task α) : α
protected meta constant {u} pure {α : Type u} (t : α) : task α
protected meta constant {u v} map {α : Type u} {β : Type v} (f : α → β) (t : task α) : task β
protected meta constant {u} flatten {α : Type u} : task (task α) → task α

protected meta def {u v} bind {α : Type u} {β : Type v} (t : task α) (f : α → task β) : task β :=
task.flatten (task.map f t)

@[inline]
meta def {u} delay {α : Type u} (f : unit → α) : task α :=
task.map f (task.pure ())

end task

[Mario Carneiro]

yes, that's it. It's more powerful than my initial impression, but much less powerful than general threading

[Mario Carneiro]

remember nondeterminism + functional programming = bad

[Mario Carneiro]

But it's meta anyway so I don't really know why the kid gloves

[Mario Carneiro]

in fact this could probably just have the meta removed, it's a perfectly valid pure interface