Zulip Chat Archive

Stream: general

Topic: VSCode overflow?


Kevin Buzzard (Sep 19 2019 at 22:33):

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 (Sep 19 2019 at 22:35):

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

Kevin Buzzard (Sep 19 2019 at 22:35):

So there's nothing we can do about it?

Bryan Gin-ge Chen (Sep 19 2019 at 22:52):

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 (Sep 20 2019 at 00:52):

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

Simon Hudon (Sep 20 2019 at 00:53):

You never handle more than one at once anyway

Alex J. Best (Sep 20 2019 at 00:54):

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

Simon Hudon (Sep 20 2019 at 06:09):

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 (Sep 20 2019 at 06:23):

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 (Nov 19 2019 at 19:56):

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 (Nov 19 2019 at 20:30):

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

Bryan Gin-ge Chen (Nov 19 2019 at 20:33):

Looks like it does, thanks!


Last updated: Dec 20 2023 at 11:08 UTC