Panic in nearly empty file

Stream: lean4

[Thomas Murrills]

The following panics:

import Lean

/--/

PANIC at Lean.EnvExtension.modifyState Lean.Environment:1388:15: called on async extension, must set asyncDecl in that case
backtrace:
PANIC at Lean.EnvExtension.modifyState Lean.Environment:1388:15: called on async extension, must set asyncDecl in that case
backtrace:

(duplication sic)

It seems the import is necessary. :)

[Julian Berman]

Sounds like #lean4 > panic on doc-string has risen from the dead.

[Thomas Murrills]

I thought I had seen this before somewhere! :)

[Kim Morrison]

Could you please open an issue?

[Markus Himmel]

May or may not be a duplicate of lean4#10756.