Call for help: Loogle in VS Code

Stream: general

[Joachim Breitner]

The loogle website is nice, and the bot a real gimmick, but it seems clear that the best UX is one where you don’t have to leave the editor while proving things.

My vague vision for this could be a key combo or button that adds a new panel to the side or bottom, with a search field highlighted. You type your query, it shows results as you type, and once you are happy you press Enter or so (maybe ↓ first a few times if it’s not the first hit) and the name is inserted into the document (or copied to the clipboard for convenient insertion). Especially a keyboard-only flow could be quite efficient and pleasant here!

I don’t think I’m the right person to do VS Code extensions (or extend existing extensions), so this is a call for help: Anyone here keen on implementing this feature? Happy to assist, advise and (I guess mostly) cheer!

Initially it might be easiest to use the JSON-API on loogle.lean-lang.org directly, eventually though it should use the #find command and cache that comes with your local mathlib installation (once that’s the case); maybe some of the code from the loogle CLI tool needs to move to mathlib (or std? or a mathlib dependency?). But that can follow later.

[Shreyas Srinivas]

I can try

[Shreyas Srinivas]

The second part could be hard. Could we add a #loogle command?

[Shreyas Srinivas]

Then it might be easier

[Yaël Dillies]

Do I get a feed of all the things people looked for in their vscode? :grinning_face_with_smiling_eyes:

[Eric Rodriguez]

Shreyas Srinivas said:

The second part could be hard. Could we add a #loogle command?

We are hoping to get it with the #find command when that is merged

[Shreyas Srinivas]

Where's the documentation for the loogle JSON API?

[Joachim Breitner]

Loogle is just a wrapper around #find (as proposed in https://github.com/leanprover-community/mathlib4/pull/6363), so that would be there. Feel free to experiment with that branch!

[Joachim Breitner]

The JSON “API” is a GET to https://loogle.lean-lang.org/json?q=Real.sin,tsum and you get JSON back. Happy to adjust if you need something else of course.

[Joachim Breitner]

Ah, I even mention this in the README at https://github.com/nomeata/loogle#web-service, so guess that counts as documentation :-D

[Shreyas Srinivas]

A follow up:
Is the output always like this: https://loogle.lean-lang.org/json?q=List+a+-%3E+List+a
Are there other fields?

Developing something that simply fetches results from loogle is _relatively_ simple. Accessing the cache when one is created might require knowing how the cache stores its information and where.

[Shreyas Srinivas]

In the long run you probably want it to be integrated with autocomplete, so you get suggestions on the spot.

[Joachim Breitner]

It's either error and suggestions, or it's hits, header and count

[Joachim Breitner]

All the cache handling would be handled by #find (via lake cache get), I'd expect a VS Code GUI that uses the local command to not worry about that.

[Shreyas Srinivas]

Does #find return a json? If not it would be much simpler to just query the online API.

[Joachim Breitner]

That's what I think too: start with the online API, and think about integration with a local installation (using a CLI tool, or a command and the LSP, or a local server) later.

[Joachim Breitner]

#find the command logs stuff to the info view, so that's obviously not great. The loogle CLI tool can return JSON.

[Patrick Massot]

Joachim, are you familiar with how this interface works in Coq and Isabelle? I'm pretty sure I saw a search panel for Coq.

[Shreyas Srinivas]

Where in coq? Which ide/extension?

[Patrick Massot]

I'm not sure, this was in 2017 during the two weeks I spent trying Coq before giving up and installing Lean.

[Patrick Massot]

It was either in CoqIDE that I tried myself of in emacs if it was when I looked at Assia using Coq.

[Joachim Breitner]

No, I'm rather ignorant here, hence the call for help.

[Joachim Breitner]

With Isabelle I remember that I found the GUI less useful than typing the command and using the info view, so I hope we can build something better :-)

[Eric Wieser]

I would guess you can have a command that opens a panel in the same style as Ctrl+P with the options populated by loogle

[Eric Wieser]

(By which I mean, https://code.visualstudio.com/api/ux-guidelines/quick-picks)

[Eric Wieser]

Though maybe a custom search sidebar makes more sense

[Joachim Breitner]

Quick pick might work well, although a sidebar would allow more interaction with the results, such as jump-to-definition. I'll let Shreyas surprise us

[Eric Wieser]

One advantage of a plain text editor is that presumably vscode can autocomplete the definition names

[Marc Huisinga]

Joachim Breitner said:

Quick pick might work well, although a sidebar would allow more interaction with the results, such as jump-to-definition. I'll let Shreyas surprise us

The disadvantage of sidebars is that you must switch away from your currently selected sidebar to use them. This is also why the future command menu is a title bar menu entry and not a sidebar. I'd personally prefer not using a sidebar for this.

[Eric Wieser]

I could imagine a sidebar being useful for having separate "name" and "identifier" search fields, so that users don't have to know the syntax

[Joachim Breitner]

The use case “I roughly know what I am looking for and want to insert it” might benefit from a quick pick, while “I need to do some serious sleuthing, and will look at types and docstrings of results and may have to refine my search a lot” more by a sidebar. Or both from the same somehow.

A structured query entry is also a good idea! (Ideally as long as it doesn't slow down the experienced user)

[Shreyas Srinivas]

You need both.

1. I am using quick pick because adding too many sidebars makes life painful, especially if someone wants to open documentation sidebars (or other windows with PDFs for example).
2. I think the solution to your second requirement is to add a link to loogle from the documentation viewer. It would naturally include the search bar on the loogle webpage

[Shreyas Srinivas]

I realized that this might be the better thread to post it. "Loogle Lean" is now available on the marketplace. Please check it out and let me know if you like the UI. The shortcut is Ctrl+Shift+L.

By default selecting a hit will insert it at your cursor position if you are working in an editor. If not, it will copy the definition to your clipboard.

[Joachim Breitner]

I'm on the road this weekend, so i can't play with it yet, but sounds great already! Please all test it and give Shreyas good feedback.

[Henrik Böving]

Just to make sure I'm not going to duplicate work: has someone here already started implementing this as a neovim telescope plugin?

[Shreyas Srinivas]

@Henrik Böving : I only put this up 12 hours ago. I am not sure loogle returns enough information yet for the previewer to be useful.

[Julian Berman]

Henrik Böving said:

Just to make sure I'm not going to duplicate work: has someone here already started implementing this as a neovim telescope plugin?

I have not yet though I certainly intended to both for Loogle and Moogle.

[Shreyas Srinivas]

If moogle has an API with docs, and they give permission, I can add moogle to my extension. Whom should I ask?

[Julian Berman]

In the Moogle thread I believe Jesse Michael Han mentioned there is (internal) efforts already to bring Moogle to VSCode. But Jesse I presume would be the one to talk to if you wanted to inquire about helping!

[Joachim Breitner]

@Shreyas Srinivas , could you add a nice User-agent to the request, possibly even with version information? It will be informative to see with which tools people use the loogle api. (Right now I think it is node-fetch.)

[Shreyas Srinivas]

I'll try to do it in the evening. At work right now.

[Joachim Breitner]

No rush!

[Joachim Breitner]

Just upgraded VS Code to give it a try. Very cool already!

I noticed that after issuing a search, it’s not possible (or not obvious how) to go back to the query and refine it. This might be the more relevant use case than filtering the results locally? Or somehow both ought to be possible. Maybe ↑ should go back to the query?
Related, I’d expect Shift-Ctrl-L and then ↑ to cycle through previous queries. I’m sure you thought about this before, so just supporting that feature request :)

[Shreyas Srinivas]

There is a back button

[Shreyas Srinivas]

But query history is a good idea. I'll try to incorporate it

[Shreyas Srinivas]

Also if you get suggestions and choose a suggestion the results for that suggestion show up

[Joachim Breitner]

Indeed, the back button goes back to “Loogle Search”, but with an empty search field.

[Shreyas Srinivas]

Okay I see what you mean

[Eric Rodriguez]

Whenever I press enter, nothing seems to happen - where should I be seeing the output?

[Eric Rodriguez]

Also, it'd be nice to have support for the same keyboard shortcuts that Lean4 has (eg \N -> blackboard bold N)

[Shreyas Srinivas]

Did you press enter in the filter hits input?

[Eric Rodriguez]

Oh, I think first one is just from me being impatient. PEBCAK :)

[Shreyas Srinivas]

Okay, i'll add Unicode support to the list of TODOs

[Shreyas Srinivas]

Does the API support this? I never tried it on the loogle webpage.

[Eric Rodriguez]

Loogle is just a wrapper around a native Lean command so I'd be surprised if it didn't

[Shreyas Srinivas]

That's not my worry. I hope the unicode stuff isn't garbled by URL encoding of requests

[Joachim Breitner]

Should work fine, and if not we can fix it :-)

[Shreyas Srinivas]

Eric Rodriguez said:

Oh, I think first one is just from me being impatient. PEBCAK :)

I think this issue is worth fixing. Users should know that the search is happening until the results arrive. The search bar shouldn't just disappear.

[Eric Rodriguez]

it'd also be nice if there'd be some way to keep results persistently! i'd be happy to help, been meaning to learn VSCode extensions for a bit - how could I contribute?

[Shreyas Srinivas]

For storage of key value pairs there is a vscode api class called Memento: https://code.visualstudio.com/api/references/vscode-api#Memento

Inside an extension a memento object is provided by the extension context. By configuring it and using the memento object it provides, you can add storage to the workspace.

The easiest way to get into vscode extension development is the Getting Started page. Following this you can play with the examples in the repository linked here. In the extension API docs, each UI item and contribution point links to an example in this repository.

I need to check if I have enabled PRs on the repository. I'll do this later in the evening and get back.

[Shreyas Srinivas]

@Joachim Breitner and @Eric Rodriguez : Version 0.06 has landed.

1. Queries are now carried around and editable as requested.
2. User agent added : vscode <version> loogle-lean <version>
3. I should have mentioned this before, Alt + ← triggers the back button

[Shreyas Srinivas]

For the next version I want to add histories and reorganize the code a bit, before it gets too big.

[Shreyas Srinivas]

I also fixed the issue where the search bar disappears too soon and well before the results arrive.

[Shreyas Srinivas]

Released 0.0.7 with some polishing:

1. In 0.0.6, retaining the term for filtering often filtered out all results giving the appearance of 0 hits even though there were some. So now if you want to modify the query, it shows up only in the query input.
2. Added better place holders. Shows number of hits.
3. Added a loading icon to reassure users that loogle is doing its thing when there are 200 hits (for example on the term Nat).

[Shreyas Srinivas]

I have been giving these updates here so that people who give me feedback are on the right version and know what's up. The changelog is also up to date, so from this point I will only post about serious updates, or updates in response to specific requests or feedback.

[Shreyas Srinivas]

Also a word about unicode: Copying and pasting in unicode actually works. It is the ability to modify inputs like \N in-place that is missing. I have to learn how the extension handles this in the first place. I'd be grateful for any help.

[Joachim Breitner]

I'd encourage you to keep posting here what's happening. It's a good way to advertise the extension, also to new users. And people can mute a topic.

[Shreyas Srinivas]

Okay. In that case I'll keep posting here. I was afraid the messages were reaching spam proportions.

[Shreyas Srinivas]

Fwiw, I think the extension may be ready for trial use by a broader audience than I initially suggested. I welcome volunteers.

[Shreyas Srinivas]

Here's the link for all new volunteers : https://marketplace.visualstudio.com/items?itemName=ShreyasSrinivas.loogle-lean

[Shreyas Srinivas]

@Marc Huisinga : Are there plans to bring mathlib4_docs into the doc view of the extension. Currently I am redirecting users to the webpage on an external browser. I'd like to open the docs within vscode, but it makes no sense for me to implement it separately if there are plans to have it in the extension already. (related: Is it just a webview opening a URL?)

[Shreyas Srinivas]

Version 0.08:

• Fixes a few code inconsistencies.
• The documentation link now takes you directly to the definition on the mathlib4_docs page, as originally intended.

Credits to @Eric Rodriguezfor this version.

[Marc Huisinga]

Shreyas Srinivas said:

Marc Huisinga : Are there plans to bring mathlib4_docs into the doc view of the extension. Currently I am redirecting users to the webpage on an external browser. I'd like to open the docs within vscode, but it makes no sense for me to implement it separately if there are plans to have it in the extension already. (related: Is it just a webview opening a URL?)

I looked into this. The DocView doesn't seem to be able to render mathlib4_docs, but VS Code's own SimpleBrowser does. In the future, I'd like to refactor the DocView entirely to use SimpleBrowser, which is when I'll also add the Mathlib docs to the DocView.

[Shreyas Srinivas]

If this very far in the future, then it probably makes sense for me to try to open mathlib4_docs in SimpleBrowser from the loogle extension for now.

[Shreyas Srinivas]

If it is a couple of weeks in the future, then maybe it doesn't

[Marc Huisinga]

I think it's OK to use SimpleBrowser for now. Since this is what I intend to refactor it for eventually anyways, you can then just change the command it calls and it should be exactly the same.