Zulip Chat Archive

Stream: new members

Topic: noob question: vscode and LEAN_PATH


view this post on Zulip Vincent Siles (Oct 07 2019 at 11:23):

Hi ! I'm trying lean for the first time and I'm a bit lost in the std. So I'd like to use #find which requires a import tactic.find if I am correct.
I'm using vscode and I set up the lean path in vscode settings. I can confirm this works. But the import raises file 'tactic/find' not found in the LEAN_PATH. I'm not sure where to set this path, and to which destination.

view this post on Zulip Anne Baanen (Oct 07 2019 at 11:27):

The find tactic is part of mathlib, did you also set up that?

view this post on Zulip Johan Commelin (Oct 07 2019 at 11:29):

For the record: you might also be interested in library_search. It is complementary to #find.

view this post on Zulip Vincent Siles (Oct 07 2019 at 11:29):

No, I did not. I was just trying to search for some definitions/lemmas in general (like the SearchAbout or SearchPattern in Coq).

view this post on Zulip Johan Commelin (Oct 07 2019 at 11:29):

Aah, you'll need mathlib for both of them

view this post on Zulip Johan Commelin (Oct 07 2019 at 11:30):

It's a bit unfortunate... but you need mathlib for almost anything beyond the bare minimum

view this post on Zulip Vincent Siles (Oct 07 2019 at 11:30):

ok I'll look into how to install mathlib then. Thank you

view this post on Zulip Johan Commelin (Oct 07 2019 at 11:30):

And nowadays it's not so hard to set up, with pre-compiled binaries etc

view this post on Zulip Johan Commelin (Oct 07 2019 at 11:31):

There are good instructions on Github

view this post on Zulip Vincent Siles (Oct 07 2019 at 11:44):

#find and library_search seem to only search for lemmas. Can I use them to search for definitions too or is there another way ?

view this post on Zulip Johan Commelin (Oct 07 2019 at 11:48):

I think library_search will also find defs

view this post on Zulip Rob Lewis (Oct 07 2019 at 11:50):

There's no good reason to restrict #find to theorems, is there? It's a trivial change to let it match defs too.

view this post on Zulip Vincent Siles (Oct 07 2019 at 11:52):

#find bool -> _ -> _ doesn't show the and or or function. Maybe I'm not using it correctly

view this post on Zulip Rob Lewis (Oct 07 2019 at 11:54):

No, you're right, it doesn't do that right now. It only looks for theorems. But I don't know why it's implemented with that restriction.

view this post on Zulip Rob Lewis (Oct 07 2019 at 12:12):

https://github.com/leanprover-community/mathlib/pull/1512

view this post on Zulip Scott Morrison (Oct 08 2019 at 00:49):

library_search will find defs, but often it's not useful, but it finds "the boring ones" rather than the ones you want. A student here @Lucas Allen has some work he'll PR soon that shows a list of applicable lemmas/defs. I think he's busy with non-Lean stuff right now.

view this post on Zulip Vincent Siles (Oct 08 2019 at 06:57):

good to know, thank you


Last updated: May 14 2021 at 06:16 UTC