hint tactic priorities

Stream: mathlib4

[Gareth Ma]

Hi! I saw that the hint tactic got merged recently, that's very exciting. I was checking this example out:

example {P Q R: Prop} (x : P ∧ Q ∧ R ∧ R) : Q ∧ P ∧ R := by hint /- Try these: • simp_all only [and_self] -/
example {P Q R: Prop} (x : P ∧ Q ∧ R ∧ R) : Q ∧ P ∧ R := by tauto

Should there be some kind of priority system so that hint tries the light-weight tactics such as tauto first before the heavy ones e.g. simp and linarith? In the code it seems the hints are tried in arbitrary order:

def hint (stx : Syntax) : TacticM Unit := do
  let tacs := Nondet.ofList (← getHints)
  let results := tacs.filterMapM fun t : TSyntax `tactic => do
    if let some msgs ← observing? (withMessageLog (withoutInfoTrees (evalTactic t))) then
      return some (← getGoals, ← suggestion t msgs)
    else
      return none

[Gareth Ma]

This will also go nicely with parallelising the tactic

[Ruben Van de Velde]

The idea is to stop looking as soon as one of the parallel attempts succeeds, so I don't think this would be easy

[Gareth Ma]

What do you mean? You should be able to parallelise the tactics in order too

[Gareth Ma]

Also regarding the tauto example I suggested at the start, it seems the problem is simply that tauto is not registered:
Screenshot-2023-11-22-at-10.23.08.png

[Trebor Huang]

Isn't "parallelise in order" a contradiction in terms?

[Gareth Ma]

Uhh I am not a computer science expert, but I mean to assign those jobs ("test this tactic") in order to multiple processes (parallelise)

[Gareth Ma]

Like how multiprocessing.pool.Pool.imap does it, where it returns the mapped results in order. Maybe I'm being stupid here

[Ruben Van de Velde]

The point is that you try tactics A, B, C, ... at the same time, and the result you get is the first one that finishes

[Mauricio Collares]

hint is supposed to stop after the first result is returned, the PR just hasn't been merged yet

[Mauricio Collares]

But a configuration option that tries all choices and picks the simplest one, which I guess is what you're asking for, sounds reasonable

[Scott Morrison]

Yes, if someone wants to add a switch so that it returns all results, rather than stopping after finding one that closes the goal, that would be fine.

[Scott Morrison]

But for the most part, if one closes the goal I'm not sure I really care about the details. :-)

[Scott Morrison]

(Note that with Lean's Task model, there is no way to assign priorities.)

[Gareth Ma]

I was thinking more like "try tauto then <insert other lightweight tactics> then simp and linarith last" rather than "try them in arbitrary order" :tear:

[Scott Morrison]

The point of parallelisation is that they are all tried at once.

[Scott Morrison]

The price of that is that if you don't have enough cores, you have lost the ability to choose the order.

[Gareth Ma]

Ahhhhhhh right, my bad

[Jireh Loreaux]

Scott Morrison speaking of not having enough cores, can we have an option to limit the number of cores hint will use?

[Kyle Miller]

(@Gareth Ma You might have been thinking of concurrency vs parallelism. Without parallelism, it could have been that the tactics get run concurrently using a time-sharing scheme, and scheduling fast-completing tactics, ones that can complete within the time quantum, could make sense.)

[Thomas Murrills]

Hmm, aren’t there usually way more tactics to run than cores? Could we (down the road) set up a priority-ordered queue of tactics and one worker per core, each of which pops a tactic off the queue? (Is that kind of thing even possible in Lean?)

[Scott Morrison]

Currently there are 7 appearances of register_hint in Mathlib, so on the same order as number of cores.

[Scott Morrison]

It would definitely be possible to write a queue that only generates a bounded number of Tasks.

[Scott Morrison]

I think all the work would be in modifying/generalizing MLList.ofTaskList in #8435.

[Scott Morrison]

This would be great fun to write, and in fact I long ago implemented an MLList.parallelMap for exactly this: #3978

[Scott Morrison]

(I never marked it for review, so it just rotted.)

[Scott Morrison]

(Actually, the MonadTask design from #3978 is lovely, if I do say so myself, and ideally could be patched into #8435. I had completely forgotten about it.)

[Scott Morrison]

I abandoned the MLList.parallelMap implementation because the performance overhead for lots of quick tasks was punitive. However that's much less of an issue for hint, where we are more concerned about some slow running tasks, and the total number of tasks is so low that the overhead is irrelevant.

[Scott Morrison]

Nevertheless, I think limiting the number of cores that hint will use is not actually that important. :-) Implementing it would be high fun, but limited practical impact.

[Joachim Breitner]

Maybe this is taking this thread too much on a tangent, but how good is the Lean RTS with extensive use of concurrency? On Haskell, I’d not hesitate to spawn many small tasks (“green threads”) and leave the rest to the RTS. But you say that in lean I shouldn't quite do that?

[Scott Morrison]

I didn't intend to say that. My parallel map approach for MLList was slow, but my (untested) suspicion was that the overhead came more from managing the look-ahead pool than spawning and waiting on tasks.