Zulip Chat Archive

Stream: new members

Topic: better reporting from library_search

Mario Carneiro (Jun 24 2020 at 01:09):

Actually I think we should avoid the "failed" error message entirely. It's really a placeholder for actual error reporting

Mario Carneiro (Jun 24 2020 at 01:10):

In the case of library_search, it would be good if the failure message gave a lot more information, like a tutorial. Keep in mind that newbies are a major part of the user base for library_search

Jalex Stark (Jun 24 2020 at 01:17):

does the information you want to display depend on what the failed goal was?

Mario Carneiro (Jun 24 2020 at 01:19):

a basic troubleshooting guide would be good

library_search failed. If you aren't sure what to do next, you can also try library_search!, suggest, or hint. Possible reasons why library_search failed:

  • The goal should be provable by direct application of a lemma from the library. If you haven't already, try stating the theorem you want in its own lemma.

  • Sometimes the library has one version of a lemma but not a very similar version obtained by permuting arguments. Try replacing a + b with b + a, or a - b < c with a < b + c, to see if maybe the lemma exists but isn't stated quite the way you would like.

  • Make sure that you have all the side conditions for your theorem to be true. For example you won't find a - b + b = a in the library because it's false! Search for b <= a -> a - b + b = a instead.

  • If a definition you made is in the lemma, you won't find any theorems about it in the library. Try unfolding the definition using unfold my_definition

  • If all else fails, ask on https://leanprover.zulipchat.com/, and maybe we can improve the library and/or library_search for next time.

Scott Morrison (Jun 24 2020 at 02:07):

This sounds great. I'm not sure what "The goal should be provable by direct application of a lemma from the library." means though. Is this intended to remind the reader what the scope of library_search is?

Mario Carneiro (Jun 24 2020 at 02:51):

Yes, does "one-step proof" make more sense?

Mario Carneiro (Jun 24 2020 at 02:51):

That is, it's not a general decision procedure, it's not simp

Mario Carneiro (Jun 24 2020 at 02:52):

it should be thought of as a search function for the library (which hopefully the name already makes clear)

Mario Carneiro (Jun 24 2020 at 02:52):

but I can imagine someone confusing it for sledgehammer and needs to be told otherwise

Last updated: Dec 20 2023 at 11:08 UTC