folding problems problem

Stream: general

[Kevin Buzzard]

WARNING: this might crash VS Code. Save all important information before starting.

Ok here's the game. Type this into Lean and wait for a while for Lean to deterministic time-out.

import data.int.basic

set_option trace.class_instances true

example : has_coe ℤ ℕ := by apply_instance

Now make the "problems" panel big (NB if you don't have a problems panel, pull up on the blue bar at the bottom).
Things should look something like this:

VSCode.png

The game now is to try and fold up all the little blue information lines. You see the little ^ symbols by the blue i's? Click on one and it folds up. Now click on a few more and that's where the fun starts. How many can you manage to fold up?

[Kevin Buzzard]

I think what's going on is that VS Code is having real difficulty distinguishing the different information instances, because many of them seem to display the exact same information. @Gabriel Ebner do you know what is going on here?

[Bryan Gin-ge Chen]

Possibly related to this? https://github.com/Microsoft/vscode/issues/68235

[Scott Morrison]

No, I don't think this is the issue.

[Scott Morrison]

I have this one too. The problem is somehow that when it thinks for too long, it resets the window and reopens all the folded things.

[Bryan Gin-ge Chen]

That happens to me too, but if I manage to collapse one of the shorter messages (in the rare moments when VS code is responsive) then scroll down, some of the others have magically become collapsed as well.

[Bryan Gin-ge Chen]

For me, it seems the huge lag is triggered simply by scrolling sufficiently far down in the Problems tab. I managed to make a recording using the profiler in VS code's Chrome dev tools but I'm not able to make sense of it:
Screenshot-2019-03-27-22.20.12.png

If anyone wants the profile JSON file let me know, it's a 435 MB JSON file that ZIPs to 15 MB.

[Gabriel Ebner]

Looks like a vscode bug to me. Try to write code with fewer problems. :smile:

[Gabriel Ebner]

Hmm, this is not good at all. vscode is unresponsive even if I don't have the problems tab open.

[Bryan Gin-ge Chen]

Yeah, I can freeze up VS code by hovering over errors in this file as well. Performance profile looks like this:
Screenshot-2019-03-28-09.26.06.png

The output from the lean server for this file seems to be absurdly large. Maybe we should be truncating it?

[Bryan Gin-ge Chen]

running lean bad.lean &> bad_output from the command line yields (after some waiting) a 98 MB file:

$ wc bad_output
  995441 8957341 98107053 bad_output

[Kevin Buzzard]

Maybe the issue is simply that the file is producing too much debugging output.

[Kevin Buzzard]

import data.rat

set_option trace.class_instances true

def XYZ : has_coe ℤ ℚ := by apply_instance

Here's a better example perhaps. This code compiles quickly with no errors. It produces 14 pieces of debugging output when you click on "def". Folding them up is really hard. This doesn't crash VS Code this time, you just can't fold them.

[Kevin Buzzard]

It's not impossible though -- I've just done it, although there is a huge amount of whitespace in between some of them.

[Gabriel Ebner]

The earlier problem also has only 16 error messages, apparently one of these error message is almost 100 megabytes though...

[Gabriel Ebner]

I have put in a small workaround. The vscode extension now only displays the first $2^{13}$ messages, and for each message only the first $2^{18}$ characters. This should hopefully be enough error messages for everybody.

[Kevin Buzzard]

2^31: your error message limit. Please contact the maintainers if you would like more errors.

[Mario Carneiro]

When I hear stuff like this I'm surprised typeclass inference works at all