timeouts

Stream: mathlib4

[Heather Macbeth]

I was making minor edits to the file Analysis.NormedSpace.OperatorNorm when suddenly the sidebar turned red and I got the following error pop-up:

Lean server printed an error: libc++abi.dylib: terminating with uncaught
exception of type lean::heartbeat_exception: (deterministic) timeout

Is this a problem of mine locally (is there some setting I need to adjust) or a problem with mathlib?

[Heather Macbeth]

If relevant, here's the branch.

[Heather Macbeth]

... the branch seems to be compiling fine, so I guess it's an issue on my end? Anyone know what VS Code setting I might need to change?

[Mario Carneiro]

It appears a timeout exception was thrown somewhere where lean was not expecting it and the exception was not caught leading to a process crash

[Mario Carneiro]

unfortunately the error message gives basically no clue as to where that might be

[Mario Carneiro]

(this is why timeouts probably shouldn't be exceptions, since literally any code can take time and result in a timeout)

[Mario Carneiro]

your error is unlikely to be reproducible, even by you

[Eric Wieser]

If these things aren't reproducible, should the error messages include a traceback of some kind?

[Eric Wieser]

So that we stand some chance of spotting where the exception wasn't handled

[Mario Carneiro]

well, the exception "wasn't handled" at main

[Mario Carneiro]

probably not a very useful thing to report

[Heather Macbeth]

Mario Carneiro said:

your error is unlikely to be reproducible, even by you

Maybe this literal error is not reproducible, but I have tried basically the same thing (golfing in OperatorNorm using gcongr) several times in the last few weeks and hit this kind of timeout every time.

[Heather Macbeth]

In any case, on my machine I think it is reproducible? At least, I've tried twice to open the file in the state indicated in that branch and got the timeout both times ...

[Scott Morrison]

Unfortunately, I couldn't reproduce this one. (By checking out the branch timeout-operator-norm, running lake exe cache get, and opening Analysis.NormedSpace.OperatorNorm in VSCode.)

[Heather Macbeth]

That's frustrating. I just tried those steps again and got the timeout again.

[Eric Wieser]

Mario Carneiro said:

well, the exception "wasn't handled" at main

Well, arguably also at every frame up the call stack, with the interesting bits in the middle...

[Kevin Buzzard]

Could it be Heather's local VS Code settings? Heather can you reproduce on the command line?