## Stream: general

### Topic: failing to use search in VS Code

#### 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:

#### 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)

#### Kevin Buzzard (May 03 2018 at 10:26):

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

#### Kevin Buzzard (May 03 2018 at 10:26):

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

#### Kevin Buzzard (May 03 2018 at 10:26):

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

2018-05-03-2.png

#### Kevin Buzzard (May 03 2018 at 10:28):

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

#### Kenny Lau (May 03 2018 at 10:28):

what does the search result look like for you?

is_group_hom.png

#### Chris Hughes (May 03 2018 at 10:30):

Do you have mathlib open as a folder?

ctrl+shift+e

and screenshot

2018-05-03-3.png

#### 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

open_stuff.png

#### Sebastian Ullrich (May 03 2018 at 10:31):

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

#### Kenny Lau (May 03 2018 at 10:32):

@Kevin Buzzard could you contract all your workspace folders

#### Kenny Lau (May 03 2018 at 10:32):

and see if mathlib is open

#### Kenny Lau (May 03 2018 at 10:32):

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

#### Kevin Buzzard (May 03 2018 at 10:33):

I have _target and mathlib is in there I promise

#### 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

hmm

#### Kevin Buzzard (May 03 2018 at 10:34):

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

#### Kevin Buzzard (May 03 2018 at 10:34):

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

and now it works

what?

#### Kevin Buzzard (May 03 2018 at 10:35):

now everything is closed and it works

#### Kevin Buzzard (May 03 2018 at 10:35):

It is completely hit-and-miss for me

#### Chris Hughes (May 03 2018 at 10:35):

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

#### Kenny Lau (May 03 2018 at 10:35):

this is very interesting

#### 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

fine

#### Kevin Buzzard (May 03 2018 at 10:36):

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

#### 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." :)

#### Kevin Buzzard (May 03 2018 at 10:38):

IT'S THE TOGGLE BUTTON

lmao

I can search!

#### 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

#### Kevin Buzzard (May 03 2018 at 10:39):

the nightmare is over

#### Kevin Buzzard (May 03 2018 at 10:39):

Thanks both of you :-)

#### Kevin Buzzard (May 03 2018 at 10:42):

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

#### Kevin Buzzard (May 03 2018 at 10:42):

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

#### Kevin Buzzard (May 03 2018 at 10:50):

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

#### Kevin Buzzard (May 03 2018 at 10:50):

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

#### 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?

#### Kevin Buzzard (May 03 2018 at 10:50):

The problem is that I might be in a namespace

#### Kevin Buzzard (May 03 2018 at 10:50):

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

#### Kenny Lau (May 03 2018 at 10:51):

search for namespace on the file lol

#### Kevin Buzzard (May 03 2018 at 10:51):

which is something I don't really like doing

#### Kevin Buzzard (May 03 2018 at 10:51):

I don't want to start searching

#### Kevin Buzzard (May 03 2018 at 10:51):

I just want to know the answer

#### Kevin Buzzard (May 03 2018 at 10:51):

say the file uses 10 namespaces, some within others

#### Kevin Buzzard (May 03 2018 at 10:51):

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

#### Kevin Buzzard (May 03 2018 at 10:51):

I might have to move around a large file

#### 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

#### Kevin Buzzard (May 03 2018 at 10:52):

This gives me the prefix

#### Kevin Buzzard (May 03 2018 at 10:52):

then I ctrl-Z to get rid of my edits

#### Kevin Buzzard (May 03 2018 at 10:52):

It strikes me as an amateurish approach

#### Kenny Lau (May 03 2018 at 10:52):

@Sebastian Ullrich

#### Kevin Buzzard (May 03 2018 at 10:52):

but mouse hover over mul doesn't do anything

#### Kevin Buzzard (May 03 2018 at 10:52):

and right click on mul doesn't work

#### Kevin Buzzard (May 03 2018 at 10:53):

"no definition found for mul"

#### 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

#### Kenny Lau (May 03 2018 at 10:53):

ctrl+space works quite well

#### Kevin Buzzard (May 03 2018 at 10:53):

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

#### Kevin Buzzard (May 03 2018 at 10:53):

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

#### 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

#### 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

#### 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