VSCode overflow?

Stream: general

[Kevin Buzzard]

If I make a file like this in VS Code:

import data.fintype

#check finset

and then (on Ubuntu) put my cursor after finset and press ctrl-space I get the usual list of possible completions. If I scroll down then it seems, according to this screenshot finset.png that everything of the form finset.blah has blah starting with a capital letter, a, b or c; then it wraps back. Surely there is more info here which I can't see? e.g. there is finset.prod.

[Bryan Gin-ge Chen]

I think the Lean server only returns the first 100 results.

[Kevin Buzzard]

So there's nothing we can do about it?

[Bryan Gin-ge Chen]

In principle it's fixable in 3.5.0c. The simplest thing to do would just be to increase the 100 here, though maybe it should be made more configurable.

[Simon Hudon]

I don’t think that’s the right way to solve this. Maybe we should drop all errors after 100

[Simon Hudon]

You never handle more than one at once anyway

[Alex J. Best]

I don't understand your comment Simon, are you talking about errors instead of code completion results?

[Simon Hudon]

Yes, that’s right. Sorry that was off topic, I misread. On emacs, the problem is that sometimes we get too many errors and I assumed it was the same with VS code

[Bryan Gin-ge Chen]

Gabriel added a workaround for the too many errors issue in VS Code back in March https://github.com/leanprover/vscode-lean/commit/89bd3dc771b2e734d8cfab04ba46cf97c72608bd

[Bryan Gin-ge Chen]

I recently noticed an option which allows you to increase (or decrease) the max number of returned completions:

import data.fintype

set_option auto_completion.max_results 1000

#check finset.

I don't know if there's a good way to incorporate this into a setting for the VS Code extension though.

[Gabriel Ebner]

Does adding -Dauto_completion.max_results=1000 as an extra command-line option work?

[Bryan Gin-ge Chen]

Looks like it does, thanks!