Kevin Kappelmann

Having no clue about any of the Lean cpp infrastructure, is this something that should be fixed globally in [declaration.cpp](https://github.com/leanprover-community/lean/blob/ec1613aef1eee72e601f192b16740629c6d49690/src/kernel/declaration.cpp#L58) or locally in [checker.cpp](https://github.com/leanprover-community/lean/blob/master/src/checker/checker.cpp#L41)?

@gebner Thanks for dealing with this. I just wanted to adapt our [proving contest backend](https://github.com/maxhaslbeck/proving-contest-backends/) and think that there is still some issue. The program ```lean axiom «quot.sound : a»...

Facing the same problem

I am getting 504s as well https://wzrd.in/standalone/concat-stream@latest