panic on doc-string

Stream: lean4

[Kim Morrison]

Here's a fun one:

import Mathlib

/-- -/

results in

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

Does anyone want to investigate this?

[Eric Wieser]

Minimized:

import Lean

/-- -/

[Eric Wieser]

So possibly no longer in the right channel :)

[Notification Bot]

This topic was moved here from #mathlib4 > panic on doc-string by Kim Morrison.

[Kim Morrison]

It's fixed already on nightly.

[Eric Wieser]

Looks like a regression in 4.23.0, so perhaps worth a backport to the next rc?

[Kim Morrison]

I haven't actually found what fixed it. I can try bisecting sometime, but not sure I'll have the time.

[Bhavik Mehta]

One of my students noticed this about 48 hours ago, so I reported it to Sebastian and it was fixed very soon after: lean4#10131

[Jovan Gerbscheid]

public meta section
def private

Still gives the same panic message

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

[Kim Morrison]

lean#11882