Poll : Vscode loogle interface feedback

Stream: general

[Shreyas Srinivas]

Hello everyone,

We (cc : @Joachim Breitner and @Eric Rodriguez ) have been taking a close look at the way types are rendered, both in loogle and loogle's vscode extension. Currently loogle renders the full type signature of a given term. This includes implicit parameters (including types), typeclass instances, and the explicit parameters. The primary question is : Do users find this useful or cluttered? How should loogle show type signatures?

In relation, the extension currently renders the type signature adjacent to the term name and the module name below it. It is also possible to swap their positions. In either case, when you hover the mouse over the type signature, the full signature is visible. The goal with the current design choice was to reduce clutter, especially when users turn off module names. You can see the two variants in the two pictures in this comment. We would like to get some feedback before making decisions on this issue as well as the PR.

To this end I am creating a poll below. Please choose all your preferred options (more than one allowed).

[Shreyas Srinivas]

/poll How should loogle render types. Where should the extension render type signatures
Loogle should show only explicit parameters
Loogle should show explicit parameters and typeclass instances
Loogle should show the full type signature
The extension should show type signatures next to the term
The extension should show type signatures below the term
The extension should show truncated type signatures.

[Shreyas Srinivas]

Please feel free to add options

[Floris van Doorn]

I think all places where a declaration is printed is very cluttered (#check, mouseover pop-ups, ...). The most important information is the explicit arguments, and it is not easy to see them at a glance. But I do also want to be able to see the implicit information.

[Floris van Doorn]

On branch#show_cmd I wrote a prototype command that prints declarations in a (in my opinion) cleaner format.

#show ContDiff.of_le /- prints the following:
ContDiff.of_le (h : ContDiff 𝕜 n f) (hmn : m ≤ n) : ContDiff 𝕜 m f
implicits: {𝕜 : Type u} {E : Type uE} {F : Type uF} {f : E → F} {m n : ℕ∞}
instances: [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] -/

There are some drawbacks: for example it loses information of the order of the implicit arguments, which sometimes is important.

[Ruben Van de Velde]

I guess less important now that we have (a := a) syntax at call sites

[Floris van Doorn]

true, though that doesn't worked with unnamed arguments (mostly instances)

[Mario Carneiro]

I keep hoping that we get automated names for instance variables (ideally less crazy than the autogenerated instance declaration names)

[Mario Carneiro]

because these are at the same time the most likely to be omitted and also the most likely to want to use with (a := ...) syntax

[Yaël Dillies]

I agree with the first part of your sentence, but not the second one, Mario. The most likely to be used with (a := ...) are

• the implicit arguments to an ↔ lemma (because we do want those to be mostly implicit)
• the implicit arguments to a rewriting lemma that should be explicit but we're too lazy to change them

[Shreyas Srinivas]

One key constraint from the vscode side is that vscode's quickpick api currently doesn't allow multi-line descriptions.

[Eric Rodriguez]

Floris van Doorn said:

On branch#show_cmd I wrote a prototype command that prints declarations in a (in my opinion) cleaner format.

#show ContDiff.of_le /- prints the following:
ContDiff.of_le (h : ContDiff 𝕜 n f) (hmn : m ≤ n) : ContDiff 𝕜 m f
implicits: {𝕜 : Type u} {E : Type uE} {F : Type uF} {f : E → F} {m n : ℕ∞}
instances: [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] -/

There are some drawbacks: for example it loses information of the order of the implicit arguments, which sometimes is important.

I think this would be a really good format to show things in for Loogle. Maybe rearranging to have instances above the implicits.

[Mario Carneiro]

the implicit arguments to a rewriting lemma that should be explicit but we're too lazy to change them

I think "we're too lazy" is not a correct description here, the availability of (a := ...) syntax has changed the calculus regarding the cost/benefit of making an argument implicit

[Shreyas Srinivas]

I am currently exploiting the fact that it doesn't remove whitespaces to give a clutter free view like below (turn off module names in your vscode settings)d97401ea-27e3-4b98-aa3b-afec95cce826.png

[Yaël Dillies]

I still think rewriting lemmas have no reason to have too many implicit arguments (unless they are an ↔). Also it does happen that variable names change during a refactor.

[Eric Wieser]

Mario Carneiro said:

because these are at the same time the most likely to be omitted and also the most likely to want to use with (a := ...) syntax

It is very annoying when I want to set (inst := (_)) in a lemma, but am forced back into the @ _ _ _ _ _ _ _ dark ages because the name is inaccessible

[Sebastian Ullrich]

Just for my understanding, this is in cases where let-binding the instance locally would not be appropriate?

[Sebastian Ullrich]

I believe there was a proposal for (\f<ClassType\f> := ...) once

[Eric Wieser]

It's for the case where I don't want to work out what to let bind, and just want to pass in literally the expression (_) to find it by unification

[Sebastian Ullrich]

Oh haha, I didn't scan that as literal input. Does the :+1: mean you would be happy with that proposal in this case as well?

[Patrick Massot]

I never use the Loogle VSCode extension because it never shows the relevant information. It should open a panel instead of a drop-down menu.

[Shreyas Srinivas]

Currently loogle's API gives you the name of a term, the type signature and the name of the documentation. In the drop down menu all these things are already shown. I also construct a link to the docs which you can reach by clicking on the button I have circled with red ink here:
Screenshot-2023-12-12-152020.png

[Patrick Massot]

No, they are not shown. What is shown is ...

[Shreyas Srinivas]

I believe that soon loogle's API will also offer the documentation string. Then I will create a panel that shows you the declaration.

[Shreyas Srinivas]

Patrick Massot said:

No, they are not shown. What is shown is ...

what are you seeing?

[Patrick Massot]

Unless this changed recently.

[Shreyas Srinivas]

The documentation link has been there almost from the beginning

[Patrick Massot]

image.png
Contains no information whatsoever.

[Patrick Massot]

You can access information by clicking each link to open the doc website, but this completely defeats the purpose of the extension which was to avoid switching to a webbrowser.

[Patrick Massot]

And you need to retype the query for each new item you want to check (since no information allows you to know which item you should check out).

[Patrick Massot]

So this extension was a good idea but it is currently completely useless as far as I can see.

[Shreyas Srinivas]

1. About docs in the website : This was a decision made because there are plans from the lean4 extension to add the docs inside vscode, and it seemed wasteful to duplicate that work.
2. The extension is designed with the goal of being able to quickly insert a definition you want wherever your cursor is. But I can see that it might be nice to show a panel of some sort too. One issue is that a large number of mathlib4_docs terms especially theorems have no docstrings. So most loogle hits will have a docstring "null".

[Shreyas Srinivas]

But these are good points I should address very very soon.

[Shreyas Srinivas]

Would it be a good idea to show the whole docs block for the chosen declaration in-editor?

[Shreyas Srinivas]

@Patrick Massot : Reflecting on your suggestion, I think it makes sense to complement the search view with a panel where loogle results appear in more detail. I'll get on it and post an update soon (hopefully before the year runs out).

[Shreyas Srinivas]

But for now, if you hover your mouse over the type signature, a tooltip will show you the full type signature. This is typically what docs show for most theorems anyway.

[Shreyas Srinivas]

See :
image.png

[Shreyas Srinivas]

Longer example:
image.png

[Patrick Massot]

Oh, this is really tricky to find! It works only on the type signature, not on the name. This already makes this extension somewhat useful!

[Shreyas Srinivas]

I guess I should add more instructions and demos. You can go back to search for a new term with "Alt + <Left Arrow Key>" btw. The last term you searched or selection you made will be available.

[Eric Rodriguez]

Shreyas Srinivas said:

I guess I should add more instructions and demos. You can go back to search for a new term with "Alt + <Left Arrow Key>" btw. The last term you searched or selection you made will be available.

this hasn't been working on Mac and I didn't see where the keybindings or anything were, unless you're using a built-in hotkey

[Shreyas Srinivas]

You can get the shortcut by hovering over the back button on the search title bar

[Eric Rodriguez]

ah okay so it's a built in thing, cool

[Shreyas Srinivas]

There is a standard UI element for that. Of course one has to place the button and program its action.

[Joachim Breitner]

Floris van Doorn said:

On branch#show_cmd I wrote a prototype command that prints declarations in a (in my opinion) cleaner format.

#show ContDiff.of_le /- prints the following:
ContDiff.of_le (h : ContDiff 𝕜 n f) (hmn : m ≤ n) : ContDiff 𝕜 m f
implicits: {𝕜 : Type u} {E : Type uE} {F : Type uF} {f : E → F} {m n : ℕ∞}
instances: [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] -/

There are some drawbacks: for example it loses information of the order of the implicit arguments, which sometimes is important.

Looks nice! Ping me when that makes it to mathlib or even better std, and I'll happily use it. (Even more so if I can get the elaborated strings for implicits and instances separately, so that I can put them in separate JSON fields, so that Shreyas can display them cleverly)

[Eric Rodriguez]

One thing that may be nice as well, Shreyas, especially whilst we work out the best way to display everything, is just to add a link to the normal search page so that can be seen as well if necessary. (Or even to keep the loogle search in a more persistent fashion)

[Shreyas Srinivas]

I thought leaving the editor was the main issue with the way docs work for now. It might be much easier to open a panel that displays the hit than again redirect users to a browser window

[Yongyi Chen]

My feedback or question: How do I efficiently type queries involving Unicode symbols like ∨? Latex code doesn't work in the loogle prompt. Right now I'm resorting to copy and paste.

[Shreyas Srinivas]

This is an unimplemented feature. On the pipeline and coming soon

[Eric Rodriguez]

Yongyi Chen said:

My feedback or question: How do I efficiently type queries involving Unicode symbols like ∨? Latex code doesn't work in the loogle prompt. Right now I'm resorting to copy and paste.

For half of these I'm resorting to typing their full name

[Yongyi Chen]

Eric Rodriguez said:

For half of these I'm resorting to typing their full name

Haha, good to know!