Zulip Chat Archive

Stream: general

Topic: failing to use search in VS Code


view this post on Zulip Kevin Buzzard (May 03 2018 at 10:24):

I don't know how to search properly in VS Code. I am just doing something really stupid. I'm writing a new file, I have no imports at all, I type [group G] and it works, I type [is_group_hom f] and it doesn't. I know that is_group_hom is there somewhere. Here's my workflow:

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:26):

1) I click on the magnifying class in VS Code (with a project open which has mathlib as an import) and I search for is_group_hom. The only results I get are the instance in the file I just wrote, and two other instances in the comments in a file I'm not interested in (so in particular I can't go to this other piece of code and right click on is_group_hom)

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:26):

2) Think "I am rubbish at using VS Code search"

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:26):

3) grep the source code and find it in seconds.

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:26):

in mathlib in algebra.group. What am I doing wrong?

view this post on Zulip Kenny Lau (May 03 2018 at 10:27):

2018-05-03-2.png

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:28):

How do I tell my VS Code to look where yours is looking

view this post on Zulip Kenny Lau (May 03 2018 at 10:28):

what does the search result look like for you?

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:29):

is_group_hom.png

view this post on Zulip Chris Hughes (May 03 2018 at 10:30):

Do you have mathlib open as a folder?

view this post on Zulip Kenny Lau (May 03 2018 at 10:30):

ctrl+shift+e

view this post on Zulip Kenny Lau (May 03 2018 at 10:30):

and screenshot

view this post on Zulip Kenny Lau (May 03 2018 at 10:30):

2018-05-03-3.png

view this post on Zulip Sebastian Ullrich (May 03 2018 at 10:30):

"Also note the Use Exclude Settings and Ignore Files toggle button in the files to exclude box. The toggle determines whether to exclude files that are ignored by your .gitignore files [...]"
_target is in .gitignore

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:31):

open_stuff.png

view this post on Zulip Sebastian Ullrich (May 03 2018 at 10:31):

https://code.visualstudio.com/docs/editor/codebasics#_search-across-files

view this post on Zulip Kenny Lau (May 03 2018 at 10:32):

@Kevin Buzzard could you contract all your workspace folders

view this post on Zulip Kenny Lau (May 03 2018 at 10:32):

and see if mathlib is open

view this post on Zulip Kenny Lau (May 03 2018 at 10:32):

if not, drag mathlib into your workspace as the bottom folder and things should work fine

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:33):

I have _target and mathlib is in there I promise

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:33):

I don't understand the advanced options for file include/exclude: it just says "files to include/exclude" and then lets me type in a list of files without explaining how to ensure they are either included or excluded

view this post on Zulip Kenny Lau (May 03 2018 at 10:33):

hmm

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:34):

So I've not needed to play with included/excluded

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:34):

I have just randomly clicked around and opened some directories in the ctrl-shift-E view

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:34):

and now it works

view this post on Zulip Kenny Lau (May 03 2018 at 10:34):

what?

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:35):

now everything is closed and it works

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:35):

It is completely hit-and-miss for me

view this post on Zulip Chris Hughes (May 03 2018 at 10:35):

!scratch.lean excludes the file scratch.lean includes it

view this post on Zulip Kenny Lau (May 03 2018 at 10:35):

this is very interesting

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:35):

I now have what looks to me like exactly the same set-up, with no obvious parameters having been changed, and search works find

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:35):

fine

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:36):

There is some basic thing which I am constantly running into and not spotting.

view this post on Zulip Sebastian Ullrich (May 03 2018 at 10:36):

"Also note the Use Exclude Settings and Ignore Files toggle button in the files to exclude box." :)

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:38):

IT'S THE TOGGLE BUTTON

view this post on Zulip Kenny Lau (May 03 2018 at 10:38):

lmao

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:38):

I can search!

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:39):

I thought that was a settings button opening an empty menu. I hadn't noticed it was changing colour

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:39):

the nightmare is over

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:39):

Thanks both of you :-)

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:42):

I need to start wearing my glasses when I'm doing this stuff :-/

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:42):

I didn't even see the ! in the greyed out text. Thanks Chris.

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:50):

And here's another thing I fail at. If I open algebra/group.lean in mathlib

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:50):

I see on line 497 that there's a theorem called mul

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:50):

but that mul won't be in the root namespace, I'm pretty sure. How do I find out the full name of that function?

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:50):

The problem is that I might be in a namespace

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:50):

What I do currently is I simply edit algebra/group.lean

view this post on Zulip Kenny Lau (May 03 2018 at 10:51):

search for namespace on the file lol

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:51):

which is something I don't really like doing

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:51):

I don't want to start searching

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:51):

I just want to know the answer

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:51):

say the file uses 10 namespaces, some within others

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:51):

I have to check all their names and when they're closed

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:51):

I might have to move around a large file

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:51):

What I currently do is under the definition of mul in the file I just write #print mul

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:52):

This gives me the prefix

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:52):

then I ctrl-Z to get rid of my edits

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:52):

It strikes me as an amateurish approach

view this post on Zulip Kenny Lau (May 03 2018 at 10:52):

@Sebastian Ullrich

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:52):

but mouse hover over mul doesn't do anything

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:52):

and right click on mul doesn't work

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:53):

"no definition found for mul"

view this post on Zulip Kenny Lau (May 03 2018 at 10:53):

I mean, I'll just import that file in a sandbox and type #check mul and ctrl+space

view this post on Zulip Kenny Lau (May 03 2018 at 10:53):

ctrl+space works quite well

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:53):

My method has the advantage that I never lose sight of the theorem I want

view this post on Zulip Kevin Buzzard (May 03 2018 at 10:53):

aah that's an idea which will probably work well in many situations

view this post on Zulip Sebastian Ullrich (May 03 2018 at 10:54):

You're right, it would make sense if the definition had the same mouseover as its references

view this post on Zulip Reid Barton (May 03 2018 at 14:45):

I use emacs, but this is something I've wished for too: the ability to see at a keystroke

  • which namespaces the current location is inside
  • what variables/parameters are in scope at the current location

view this post on Zulip Reid Barton (May 03 2018 at 14:45):

I don't know if this can be implemented without extending lean


Last updated: May 13 2021 at 05:21 UTC