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:
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:
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):
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 (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 messages, and for each message only the first characters. This should hopefully be enough error messages for everybody.
Kevin Buzzard (Mar 28 2019 at 15:03):
2^31: your error message limit. Please contact the maintainers if you would like more errors.
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