autocomplete woes

Stream: lean4

[Kevin Buzzard]

I haven't actually written much Lean 4 code in some sense, I've been doing a lot of porting which is a different workflow to actually creating new theorems. I have now written some code though, and two things that frustrated me were no autocomplete in imports and no powerful autocomplete in lemma names. In the below screenshots I am pressing ctrl+space to switch on search, and Esc to switch it off. As can be seen, the results in Lean 3 are far more powerful than those in Lean 4.

autocomplete3.gif

autocomplete4.gif

@Sebastian Ullrich this is what I was alluding to in the other thread. Note in particular the powerful search for coprimeiff, which will potentially pick up results called ...coprime.iff... and ...coprime_iff...; I often do not know which one will be the one I'm looking for, but just writing coprimeiff searches for both. The ctrl-space search functionality is far more efficient than using the VS Code search functionality and furthermore gives far fewer false positives.

[Sebastian Ullrich]

Is it better with exact?

[Kevin Buzzard]

No, it's the same.

[Kevin Buzzard]

Nat.coprimeiff works with both rw and exact (Lean suggests things like Nat.coprime_mul_iff_left) so maybe it's something to do with namespaces.

[Sebastian Ullrich]

Oh I see, yes, Lean 4 only considers the next name component right now

[Patrick Massot]

The absence of autocompletion of import is indeed very painful.

[Kevin Buzzard]

Yeah in demos I say "OK so let's try and prove a theorem about continuous functions. Hmm, how shall we start? Let's try import continu...oh look. "

[James Gallicchio]

part of me thinks normal autocomplete isn't really made for the lean3 powerful search... maybe it would be better to have macros for searching, like search "coprime iff", that provide code actions for the search results?

[James Gallicchio]

this could allow configurability & flexibility -- maybe the search splits up words and looks for anything with all those words in any order, finding both iff_coprime and coprime_iff theorems

[James Gallicchio]

and generally when i want a powerful search (rather than autocomplete) i want something that triggers more explicitly than autocomplete (which is sometimes finicky). does anyone else have that feeling?

[Kevin Buzzard]

What I like about the ctrl-space dance is that I can do in the middle of writing a line of tactic code or term code or whatever without having to step outside of where I am (e.g. outside the middle of a 40 line proof) or do any clicking on anything etc.

[James Gallicchio]

Totally. I wonder if we can get the same interface with code actions.

[Eric Wieser]

Note the intended behavior of autocomplete is documented here: https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textDocument_completion

[Eric Wieser]

In particular:

to achieve consistency across languages and to honor different clients usually the client is responsible for filtering and sorting.

So it sounds like we should just return as many matches as possible and leave vscode to filter them

[Max Nowak 🐉]

Lean's language server is actually very hackable, and most of the semantic information is already there (I say based on limited attempts while trying to improve semantic highlighting).

[James Gallicchio]

Eric Wieser said:

So it sounds like we should just return as many matches as possible and leave vscode to filter them

it's a bit unclear from the documentation what servers should return... if the cursor is at Lean.some| should we just return all matches for Lean. or all that start with Lean.some or all that start with Lean. and have the letters s o m e?

[Julian Berman]

In VSCode I think the expectation is something like the last one -- specifically https://github.com//Microsoft/vscode/issues/15419 was open for ages it seems which is the behavior from Kevin's Lean 3 capture, and was open for like 3 years before they added an option to turn it off and not do the fuzzy matching

[James Gallicchio]

I suspect we may even want to do something like the first, ignoring user input after the dot and returning all options for that namespace. unclear what to do at top level though (keywords + top level idents + all idents in all open namespaces??? maybe if that list is cached it would be fine)

[Damiano Testa]

Autocompleting at Lean.some|, my personal preference would be:

1. exact match Lean.something;
2. within the Lean namespace, fuzzy match on the some;
3. rest of Lean namespace.

However, anything that works, trumps any of the above!

[Yaël Dillies]

While we're at it, I always found it incredibly irritating that autocompleting s.pr| gives set.prod| instead of s.prod|.

[Julian Berman]

@Damiano Testa I think most of the discussion is about what the server sends back -- the client (i.e. VSCode) can do lots of nice things once it has all the results. In nvim there are literally 10 different implementations even of just the word "fuzzy" in your number 2, because lots of people expect different sorting behavior (based on contiguous letters, based on item type, based on lots of other things which can feel very nice or very wrong, etc.). But the server has to send back enough results first to even get started

[Julian Berman]

(regardless of anything I think most people of course probably expect that if there's an exact match on what you've typed, you should get that, and if there's prefix matches on what you typed you should get those higher than other results, etc.)

[Damiano Testa]

Julian, in this discussion, the "server" is...?

[Julian Berman]

The Lean process running in the background

[Damiano Testa]

Ok, so "my" computer, right?

[Julian Berman]

Yeah both running on your computer typically

[Damiano Testa]

Ah, one is what lean passes on the the editor is the other is what the editor does with the info?

[Julian Berman]

Exactly

[Damiano Testa]

ok, this clears up some confusion!

[Damiano Testa]

I thought that server could refer to an online machine...

[Julian Berman]

Yeah it's confusing terminology, we programmers have to get back at you mathematicians somehow.

[Damiano Testa]

Anyway, just to clarify, by "fuzzy" I meant a regular expression along the lines of Lean\..*s.*o.*m.*e.*

[Damiano Testa]

I think that after an exact match, this what I would like.

[Damiano Testa]

But, in the meantime, I have to figure out what server means... and who know what other traps have you laid out for me!

[Julian Berman]

And what order do you want the results in, arbitrary? Usually it's nice if results matching Lean.som.*e ranks higher than Lean.s.*o.*m.*e if there are results that match both

[Julian Berman]

There's a nice writeup of even more hairy details in fzy's documentation

[Julian Berman]

https://github.com/jhawthorn/fzy/blob/master/ALGORITHM.md

[Damiano Testa]

I find that the fzf add-on is what I would like. Let me find a link.

[Damiano Testa]

I use this all the time and it is great!

https://github.com/junegunn/fzf

[Julian Berman]

nod -- yeah I'm aware of fzf's, cool, makes sense.

[Damiano Testa]

(although I would prefer exact matches, before going fuzzy)

[Julian Berman]

We're completely off-topic clearly, but if you haven't tried fzy I'd definitely recommend it

[Julian Berman]

I find its algorithm hugely more intuitive to my fingers than fzf's (which is described in that link)

[Damiano Testa]

with fzf, I no longer need to worry about folder structures: i simply start typing a fuzzy match and the correct file opens automatically. having this for mathlib lemmas would be awesome!

[Damiano Testa]

In fact, it may be possibleeasy to have a cheap implementation of scrubbing the lemma names from mathlib and feeding them to your favourite fuzzy finder, at least on the cli

[Yaël Dillies]

We can let the user decide on the matching algorithm, right?

[Damiano Testa]

(although, seeing the type of each lemma is invaluable and would be hard to achieve on the commandline)

[Eric Rodriguez]

i've gotten so used to fzf that fzy would probably be a step back by now, to the point i do weird stuff like RTCyEv for ring_theory/polynomial/cyclotomic/eval; but it may be worth trying fzy for a couple days...

[Eric Wieser]

Yaël Dillies said:

We can let the user decide on the matching algorithm, right?

The "user" here is vscode I think. Maybe there as settings that let you customize it?

[Kevin Buzzard]

Writing Lean 4 code now I just wrote quotientKerEquivOfSurjective and Lean complained that this doesn't exist, whereas I know it does because I just copied it from a file. It's probably in a namespace though. In Lean 3 ctrl-space tab just solved that problem immediately, it would suggest the correct fully qualified name as the first shot. I miss this feature.

[Eric Rodriguez]

Eric Wieser said:

Yaël Dillies said:

We can let the user decide on the matching algorithm, right?

The "user" here is vscode I think. Maybe there as settings that let you customize it?

don't think so

[Julian Berman]

I have no personal experience clearly but looks like there's at least one extension which mucks with it -- https://marketplace.visualstudio.com/items?itemName=cfognom.VSIntelliSenseTweaks so there seems like there may be the hooks needed to do this from extensions OK never mind that's for Visual Studio which I must say I didn't even know was still a thing.

[Eric Wieser]

Here's one that got me the other day:

import Lean

#check MetaM -- fails

Autocomplete on MetaM does not tell me that I wanted Lean.MetaM

[Sebastian Ullrich]

Isn't that the same issue as above? And, for documentation purposes, lean4#1659

[Eric Wieser]

Ah, it's exactly that issue; sorry for the noise

[Sebastien Gouezel]

Can we put a bounty on issues? Because I would be willing to put a lot on this one :-)

[Mario Carneiro]

you can upvote it

[Henrik Böving]

I've been wondering how one would implement this efficiently. Surely we cannot want to do a linear search through the entire environment and check for things that end on a word right?

[Sebastian Ullrich]

If only VS Code understood partial results, we could actually return matches as soon as we find them

[Sebastian Ullrich]

But if performance was adequate in Lean 3, it should be possible to implement in Lean 4 as well

[Mario Carneiro]

what ever happened to that fuzzy autocomplete PR?

[Mario Carneiro]

I thought this was among the things that was handled

[Mario Carneiro]

lean4#1710 seems to have been merged

[Sebastian Ullrich]

Only workspace symbols uses fuzzy matching on the entire name so far

[Mario Carneiro]

I see FuzzyMatching.lean is still there in the current version of lean but FuzzyMatching.fuzzyMatch appears to be unused outside a benchmark

[Mario Carneiro]

oh, fuzzyMatchScoreWithThreshold? is used instead

[Sebastian Ullrich]

Oh there it is: https://github.com/Kha/lean4/commit/73a46a05a48cc3b5d0ee9d7b8dea9fa46bba5b60. I ran out of time for actually testing it and refound it in my stash just now

[Sebastian Ullrich]

lean4#2351