Problem working with `number_theory/function_field.lean`

Stream: general

[Oliver Nash]

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]

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