Zulip Chat Archive

Stream: general

Topic: Problem working with `number_theory/function_field.lean`

Oliver Nash (May 09 2022 at 16:42):

I'm finding it essentially impossible to work on the file number_theory/function_field.lean in VS Code.

Working with up-to-date master+oleans if I start a new VS Code session and open only the file number_theory/function_field.lean, Lean pegs a few cores, eats up all 16GB of my memory, starts asking for more and never finishes.

Weirdly, following the above steps only reproduces the problem sporadically, though it happens more often than not.

The oddest thing is that there seems to be temporal hysteresis to the behaviour. Once it happens, if I close VS Code, wait a minute or so and then reopen the problem will recur. HOWEVER if I wait maybe 20 minutes then my experience suggests all will be well for a time.

Oliver Nash (May 09 2022 at 16:42):

Has anyone ever encountered behaviour like this before? Any suggestions for how to debug would be most welcome.

Last updated: Dec 20 2023 at 11:08 UTC