Zulip Chat Archive

Stream: general

Topic: folding problems problem


view this post on Zulip 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:

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?

view this post on Zulip 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?

view this post on Zulip Bryan Gin-ge Chen (Mar 27 2019 at 22:50):

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

view this post on Zulip Scott Morrison (Mar 28 2019 at 01:15):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Gabriel Ebner (Mar 28 2019 at 11:33):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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
  995441 8957341 98107053 bad_output

view this post on Zulip Kevin Buzzard (Mar 28 2019 at 14:36):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip Gabriel Ebner (Mar 28 2019 at 14:56):

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

view this post on Zulip Kevin Buzzard (Mar 28 2019 at 15:03):

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

view this post on Zulip Mario Carneiro (Mar 28 2019 at 17:52):

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


Last updated: May 15 2021 at 23:13 UTC