Zulip Chat Archive

Stream: new members

Topic: Simultaneously hint and library_search


Martin Dvořák (Oct 27 2022 at 14:22):

Would it make sense to have a command that performs hint and library_search simultaneously?

Jireh Loreaux (Oct 27 2022 at 14:39):

That sounds really expensive.

Martin Dvořák (Oct 27 2022 at 14:57):

Neither hint nor library_search uses more than half cores of my processor. What would be so expensive?

Damiano Testa (Oct 27 2022 at 15:10):

Something like this:

meta def lhint : tactic unit := `[ library_search <|> hint ]

first tries library_search showing its output if it succeeds. If library_search fails, then it does hint.

I do not know how to produce the output of both tactics, when the first one succeeds, though.

Martin Dvořák (Oct 27 2022 at 15:42):

Can I do it in parallel (two threads) please?

Martin Dvořák (Oct 27 2022 at 15:43):

As for getting the output of both tactics, I am not interested in hint when library search succeeds.

Kevin Buzzard (Oct 27 2022 at 15:45):

Given that both hint and library_search are liable to cause timeouts, won't running them in parallel just make them even less likely to succeed even when they might both succeed when run separately?

Damiano Testa (Oct 27 2022 at 16:57):

In any case, I do not know how to run the two tactics in parallel...

Martin Dvořák (Oct 27 2022 at 19:47):

Maybe I am completely wrong, but I believe that such a thing cannot me implemented inside Lean. We would probably need to run two Lean instances at the same time, which would require an external script / change in the Lean plugin for VSO. In such a case, it would probably not be worth the effort. Please, prove me wrong tho!

Alex J. Best (Oct 27 2022 at 21:21):

I believe this works:

import tactic

open tactic
open tactic.interactive

meta def lhint : tactic unit :=
do
  retrieve (async `[library_search]),
  async `[hint]

Alex J. Best (Oct 27 2022 at 21:21):

I have no idea whether what kevin says is true, but it doesn't seem clear to me that the different async threads would respect the same timeout limit

Eric Wieser (Oct 27 2022 at 22:27):

That looks wrong to me; doesn't it wait for the first task before starting the second?

Alex J. Best (Oct 27 2022 at 23:10):

Nope, if you do something like

import tactic

open tactic
open tactic.interactive

meta def lhint : tactic unit :=
do
  retrieve (async $ sleep 10000 >> `[library_search]),
  async (sleep 1000 >> `[hint])


example : 1 = 1:=
begin
lhint,
end

its quite clear that the output of the second comes first

Eric Wieser (Oct 27 2022 at 23:14):

Perhaps docs#retrieve isn't what I thought it was

Eric Wieser (Oct 27 2022 at 23:16):

I'm not at lean, but what does this do?

import tactic

open tactic
open tactic.interactive

meta def lhint : tactic unit :=
do
  X  retrieve (async $ sleep 10000 >> pure 37),
  async (sleep 1000 >> tactic.trace X)

Eric Wieser (Oct 27 2022 at 23:17):

Surely that has to run the first block to completion before the second can run?

Alex J. Best (Oct 27 2022 at 23:36):

The thing run inside async has to be an itactic (which is tactic unit) so it doesn't compile

Alex J. Best (Oct 27 2022 at 23:37):

Eric Wieser said:

Perhaps docs#tactic.retrieve isn't what I thought it was (edit: it's the tactic I can never find when I want!)

I also always have difficulty remembering the name of this (and other similar tactics) they're annoyingly hard to find

Eric Wieser (Oct 27 2022 at 23:44):

I was expecting it to have a signature like docs#tactic.run_async I think

Jireh Loreaux (Oct 28 2022 at 00:30):

@Martin Dvořák sorry, I misinterpreted. I thought you wanted some kind of combination hint + library_search that would somehow link outputs, not just run them in parallel.

Damiano Testa (Oct 28 2022 at 02:40):

I do not think that I had ever seen retrieve or async!

Why does async report its output on example, rather than on the tactic?

Damiano Testa (Oct 28 2022 at 02:42):

That is, when doing

meta def lhint : tactic unit := retrieve (async `[library_search]) >> `[hint]

example : 1 = 1 :=
begin
  lhint,
end

the outcome of library_search is on example, while the outcome of hint is on lhint. The Try this also replaces the example for library_search.


Last updated: Dec 20 2023 at 11:08 UTC