Bug: No autocomplete on even chars

Stream: lean4

[Mac]

I think I have discovered a very hilarious bug in Lean autocompletions (at least in VSCode), but I want to sanity check myself here by asking whether anyone else can reproduce it before I create an issue. The bug is simple but weird: autocomplete is not properly triggered if an even number of characters is typed at once. That is:

#check B -- completion results on typing 'B'
#check Ba -- if typed together, no results; if typed as 'B' then after results, 'a', then results
#check Bas --  if typed together, results; if typed as 'B' then 'as', no results
#check Base -- if typed together or as 'Ba' then 'se', no results; if typed as 'B' then 'ase' or  'Bas' then 'e', results

I double checked that this behavior does not appear in VSCode Python and it does not, so I am fairly sure this is a Lean issue. However, I am still not sure if this is a universal issues or just some problem with my configuration.

[Sebastian Ullrich]

I can reproduce this in VS Code but not in Emacs

[Sebastian Ullrich]

I think VS Code is mad because we rejected the first completion request with "File changed." and refuses to send a second one. It has been noted before that our strategy around file changes does not align with what VS Code expects.

[Kevin Buzzard]

I have suffered from failure of autocompletion for years and I have never understood why; I would just do escape, ctrl-space to try again and observe that now I magically had loads of extra results. I hadn't realised until now that it was something to do with timing.

[Kevin Buzzard]

#check Ba typed quickly in mathlib gives me 3 results, and then escape, ctrl-space gives me 6 results.

[Mac]

@Sebastian Ullrich @Kevin Buzzard Oh, yeah. I should probably note here that if you have "Word Based Suggestions" in VSCode turned on, instead of no completion results as mentioned in the example above, you will instead get VSCode's default word based suggestions at those points (which will prevent any further Lean server-based completion on subsequent typing).

[Mac]

Sebastian Ullrich said:

I think VS Code is mad because we rejected the first completion request with "File changed." and refuses to send a second one. It has been noted before that our strategy around file changes does not align with what VS Code expects.

The "File changed." rejection certainly is a problem for VSCode. Any failed completion can fallback to word based suggestions and prevent subsequent completion requests. However, note that this bug is not caused simply typing more than 1 character, only even numbers (e.g., typing 3 characters in quick sequence will still work). I am a little confused as to why it would start working again for greater than 1 odd number characters if the "File changed." rejection was the only problem.

My initial suspicion was that it may have something to do with abbreviation support in VSCode interfering with the completion (i.e., the double characters were going abbreviation checking and this was somehow hampering completion requests). Turning off abbreviations by disabling Lean 4 input mode, however, did not solve the problem for me.