failing to use search in VS Code

Stream: general

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kenny Lau]

2018-05-03-2.png

[Kevin Buzzard]

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

[Kenny Lau]

what does the search result look like for you?

[Kevin Buzzard]

is_group_hom.png

[Chris Hughes]

Do you have mathlib open as a folder?

[Kenny Lau]

ctrl+shift+e

[Kenny Lau]

and screenshot

[Kenny Lau]

2018-05-03-3.png

[Sebastian Ullrich]

"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

[Kevin Buzzard]

open_stuff.png

[Sebastian Ullrich]

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

[Kenny Lau]

@Kevin Buzzard could you contract all your workspace folders

[Kenny Lau]

and see if mathlib is open

[Kenny Lau]

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

[Kevin Buzzard]

I have _target and mathlib is in there I promise

[Kevin Buzzard]

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

[Kenny Lau]

hmm

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

and now it works

[Kenny Lau]

what?

[Kevin Buzzard]

now everything is closed and it works

[Kevin Buzzard]

It is completely hit-and-miss for me

[Chris Hughes]

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

[Kenny Lau]

this is very interesting

[Kevin Buzzard]

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

[Kevin Buzzard]

fine

[Kevin Buzzard]

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

[Sebastian Ullrich]

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

[Kevin Buzzard]

IT'S THE TOGGLE BUTTON

[Kenny Lau]

lmao

[Kevin Buzzard]

I can search!

[Kevin Buzzard]

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

[Kevin Buzzard]

the nightmare is over

[Kevin Buzzard]

Thanks both of you :-)

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

The problem is that I might be in a namespace

[Kevin Buzzard]

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

[Kenny Lau]

search for namespace on the file lol

[Kevin Buzzard]

which is something I don't really like doing

[Kevin Buzzard]

I don't want to start searching

[Kevin Buzzard]

I just want to know the answer

[Kevin Buzzard]

say the file uses 10 namespaces, some within others

[Kevin Buzzard]

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

[Kevin Buzzard]

I might have to move around a large file

[Kevin Buzzard]

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

[Kevin Buzzard]

This gives me the prefix

[Kevin Buzzard]

then I ctrl-Z to get rid of my edits

[Kevin Buzzard]

It strikes me as an amateurish approach

[Kenny Lau]

@Sebastian Ullrich

[Kevin Buzzard]

but mouse hover over mul doesn't do anything

[Kevin Buzzard]

and right click on mul doesn't work

[Kevin Buzzard]

"no definition found for mul"

[Kenny Lau]

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

[Kenny Lau]

ctrl+space works quite well

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Sebastian Ullrich]

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

[Reid Barton]

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]

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