LoogleView

Stream: lean4

[Marc Huisinga]

As of 0.0.162, the VS Code extension has a built-in LoogleView with unicode input support that can be opened using the 'Loogle: Search' command. Thanks to @Shreyas Srinivas for developing the Loogle Lean extension - it was very helpful for integrating this feature into the Lean VS Code extension.

Recording-2024-06-14-at-19.16.47.gif

Another result of this is that the unicode input mechanism of the VS Code extension has been factored out into a separate TypeScript component and can now be installed from NPM if you want to implement your own unicode input mechanisms that are similar to the one in VS Code. The logic of the LoogleView unicode input component has also been factored out into a separate package if you simply want to use a HTML input component that supports unicode input.

The packages can be found here:

• Unicode input logic: https://www.npmjs.com/package/@leanprover/unicode-input
• Unicode input component: https://www.npmjs.com/package/@leanprover/unicode-input-component

[Shreyas Srinivas]

Two questions: Doesn't this override the loogle lean extension's shortcut Ctrl+Shift+L?

[Shreyas Srinivas]

And is that extension still useful for its different workflow?

[Shreyas Srinivas]

I personally use it for quick inserts of defs

[Shreyas Srinivas]

One possibility is that I could integrate the quick search workflow into the vscode extension

[Eric Wieser]

Are there plans to use these unicode packages in doc-gen's search?

[Henrik Böving]

Not right now no.

[Henrik Böving]

What would you want to use them for? All of the relevant definitions that you might search for should be ASCII shouldn't they?

[Eric Wieser]

No, I often need to search for non-ascii names

[Eric Wieser]

LinearMap.mk\_2, CliffordAlgebra.\iota_sq_scalar etc

[Henrik Böving]

I see. I guess we could include it over some CDN. I would definitely want to avoid having NPM as a dependency for building doc-gen.

[Shreyas Srinivas]

Also, @Marc Huisinga and @Joachim Breitner : what's the preferrence for the loogle lean extension in general. I'd prefer to leave it as it is (maybe add unicode support in the input but nothing more).

[Marc Huisinga]

Shreyas Srinivas said:

One possibility is that I could integrate the quick search workflow into the vscode extension

I really like the quick pick dialog in principle but the fact that we can't properly make it support unicode input and the fact that it is relatively limited in terms of the available space for displaying types is a deal-breaker to me and why I went with a webview instead. The webview is certainly a bit more clunky in terms of input. I would prefer not to support multiple different ways to display loogle queries in the VS Code extension.

Shreyas Srinivas said:

Two questions: Doesn't this override the loogle lean extension's shortcut Ctrl+Shift+L?

Oh, sorry! I overlooked that the Loogle extension already had a keybind and apparently managed to choose the same one. Would you prefer me to change it to something else, or would you prefer to have the Loogle webview on Ctrl+Shift+L?

Shreyas Srinivas said:

Also, Marc Huisinga and Joachim Breitner : what's the preferrence for the loogle lean extension in general. I'd prefer to leave it as it is (maybe add unicode support in the input but nothing more).

I certainly don't mind it remaining available for people who prefer the alternative input.

[Shreyas Srinivas]

Right now, I have too much muscle memory for Ctrl + Shift + L

[Shreyas Srinivas]

Changing shortcuts on my extension would be too much breakage right now (at least for the 250 odd installed users)

[Marc Huisinga]

Ok, I'll see if I can find another good shortcut then.

[Shreyas Srinivas]

Thanks,

Also, a couple of other points:

1. the font size in the webview seems unaffected by the vscode font settings. So I get really tiny characters right now
2. The content of the webview doesn't adjust to the size of the window. Because of this and the font issue it feels too cluttered.

[Shreyas Srinivas]

I suggest folding the usage instructions by default and centering the loogle search bar vertically in the page (or at least bringing it closer to the center)

[Shreyas Srinivas]

To give you an idea of what it looks like :
Screenshot-from-2024-06-18-13-34-59.png

[Shreyas Srinivas]

To be fair, I also have this font issue in my extension. At the moment you can get the full type signature by hovering the mouse pointer over the type (vscode even staggers it nicely), but the font size is too small

[Shreyas Srinivas]

Another suggestion if I may: Could the results have some spacing between them? I tried to incorporate this by making module names appear in the second line and providing an option to turn that off. It has a nice effect on readability as in the screenshot
Screenshot-from-2024-06-18-13-42-08.png

But in a webview you might have more flexibility.

[Marc Huisinga]

The shortcut for the LoogleView will change to the Ctrl+K Ctrl+S chord.

the font size in the webview seems unaffected by the vscode font settings. So I get really tiny characters right now

Which font setting are you talking about, exactly? Regular WebView content is not supposed to be affected by your editor font size. It scales with the zoom level (like all other non-editor content in VS Code).

The content of the webview doesn't adjust to the size of the window

It does, but the max-width is too low. I'll remove it.

I suggest folding the usage instructions by default and centering the loogle search bar vertically in the page (or at least bringing it closer to the center)

I prefer it being left-aligned.

Could the results have some spacing between them?

I think that the highlighting on the link of the identifier is sufficient separation.

[Super Veridical]

Would be nice if it had "locally installed only" and "project only" modes through a locally run loogle instance. Also an ability to use it from side bar without obscuring the active tab, i.e like normal search in vscode.

[Joachim Breitner]

Random idea from my side for future work: maybe the extension could pass the list of open namespaces at the current cursor position to Loogle, so that queries don't have to qualify names. Especially when working on open Lean this would be very convenient.

[Shreyas Srinivas]

Marc Huisinga said:

Which font setting are you talking about, exactly? Regular WebView content is not supposed to be affected by your editor font size. It scales with the zoom level (like all other non-editor content in VS Code).

The editor font. But it would be nice to have a font size setting for this webview. Currently on my screen it is too small.

I prefer it being left-aligned.

I am referring to vertical alignment. Currently the search bar is too far at the top and there is a lot of clutter with the usage info. Back in the stone age of the internet, google got this right by keeping the search page simple. The usage info is nice, but if it is collapsed and unfolded optionally and the search bar looks bigger and vertically centered, then it would be much easier to use.

[Jon Eugster]

Marc Huisinga said:

Another result of this is that the unicode input mechanism of the VS Code extension has been factored out into a separate TypeScript component and can now be installed from NPM if you want to implement your own unicode input mechanisms that are similar to the one in VS Code. The logic of the LoogleView unicode input component has also been factored out into a separate package if you simply want to use a HTML input component that supports unicode input.

The packages can be found here:

• Unicode input component: https://www.npmjs.com/package/@leanprover/unicode-input-component

Thanks, @Marc Huisinga! I already successfully added this to the react app behind the NNG! One issue I have currently is that on entering a space, the cursor jumps back to the beginning of the input. This also happens on successful completion with the option eagerReplacementEnabled: true set.

I haven't minimised it yet, so I can't completely exclude that it's a problem with my setup, but I was wondering if you maybe had a small template you used for testing which I could use to create a MWE?

[Marc Huisinga]

https://github.com/leanprover/vscode-lean4/blob/79c2e39ba34fdecf545fb3f23aec2c6aa014cd88/vscode-lean4/loogleview/index.ts#L94
https://github.com/leanprover/vscode-lean4/blob/79c2e39ba34fdecf545fb3f23aec2c6aa014cd88/vscode-lean4/loogleview/static/index.html#L4

[Marc Huisinga]

My first guess without having looked at any code is that React is probably allergic to the kind of window selection mutation that is needed to ensure that the cursor is at the right position after replacing the abbreviation and when inserting underline tags (since the cursor will otherwise just reset to the start), and that you may need to work around that somehow (e.g. using effects?).

[Kim Morrison]

Asking out of complete ignorance (I still grep :-), what does "Loogle Lean" extension offer now? Can we consolidate on a single solution here, e.g. by providing notifications suggesting using the built-in Loogle view, and then deprecating the extension?

[Shreyas Srinivas]

In place search, quick insert and copy. Basically a very different UI.

[Shreyas Srinivas]

Marc Huisinga said:

Shreyas Srinivas said:

One possibility is that I could integrate the quick search workflow into the vscode extension

I really like the quick pick dialog in principle but the fact that we can't properly make it support unicode input and the fact that it is relatively limited in terms of the available space for displaying types is a deal-breaker to me and why I went with a webview instead. The webview is certainly a bit more clunky in terms of input. I would prefer not to support multiple different ways to display loogle queries in the VS Code extension.

Shreyas Srinivas said:

Two questions: Doesn't this override the loogle lean extension's shortcut Ctrl+Shift+L?

Oh, sorry! I overlooked that the Loogle extension already had a keybind and apparently managed to choose the same one. Would you prefer me to change it to something else, or would you prefer to have the Loogle webview on Ctrl+Shift+L?

Shreyas Srinivas said:

Also, Marc Huisinga and Joachim Breitner : what's the preferrence for the loogle lean extension in general. I'd prefer to leave it as it is (maybe add unicode support in the input but nothing more).

I certainly don't mind it remaining available for people who prefer the alternative input.

We discussed it here

[Marc Huisinga]

When @Joachim Breitner and I were adding Unicode input support to the Loogle website, we noticed that the Unicode input component does not work out of the box on Firefox because Firefox will insert <br> tags into contenteditable divs when adding a space.
You can fix this by adding white-space: -moz-pre-space; to the style of the contenteditable div.