## Stream: general

### Topic: folding problems problem

#### Kevin Buzzard (Mar 27 2019 at 22:37):

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:

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 (Mar 27 2019 at 22:39):

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 (Mar 27 2019 at 22:50):

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

#### Scott Morrison (Mar 28 2019 at 01:15):

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

#### Scott Morrison (Mar 28 2019 at 01:15):

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 (Mar 28 2019 at 01:39):

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 (Mar 28 2019 at 02:24):

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 (Mar 28 2019 at 11:33):

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

#### Gabriel Ebner (Mar 28 2019 at 11:35):

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

#### Bryan Gin-ge Chen (Mar 28 2019 at 13:58):

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 (Mar 28 2019 at 13:59):

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

\$ wc bad_output


#### Kevin Buzzard (Mar 28 2019 at 14:36):

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

#### Kevin Buzzard (Mar 28 2019 at 14:43):

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 (Mar 28 2019 at 14:45):

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 (Mar 28 2019 at 14:45):

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

#### Gabriel Ebner (Mar 28 2019 at 14:56):

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.