leanchecker bug?

Stream: general

[Lucas Viana]

I've run leanproject up to make sure I'm up-to-date, but still the lean checker seems to do something weird with this file in VSCode. It uses high CPU and it eats memory until it freezes my computer. I'm running linux.

(warning: please be ready to kill the lean process before it freezes your computer! and be careful not to lose unsaved work!)

example : true := by trivial
#che -- (intentionally left like this)

Can someone confirm if this is a problem?

[Alex J. Best]

I can replicate this on osx, pretty weird!

[Bryan Gin-ge Chen]

Oh wow, I can confirm this is acting up in Windows too. @Gabriel Ebner

I thought it might have something to do with lean#342, but this replicates in 3.16.2 too.