PANIC at Lean.EnvExtension.modifyState

Stream: lean4

[Snir Broshi]

link to the panic call

/--
info: PANIC at Lean.EnvExtension.modifyState Lean.Environment:1399:17: `asyncDecl` `foo.f` is outside current context foo
backtrace:
-/
#guard_msgs in
theorem foo : True := by
  let rec f (n : Nat) : Nat :=
    match n with
    | .zero => 0
    | .succ n => f n
  trivial

/--
info: Lean 4.29.0-nightly-2026-02-01
Target: x86_64-unknown-linux-gnu
-/
#guard_msgs in
#version

[Miyahara Kō]

Thank you for your report!
Can you create the issue at leanprover/lean4?

[Snir Broshi]

Miyahara Kō said:

Thank you for your report!
Can you create the issue at leanprover/lean4?

Hello, do you work for the FRO or acting in some official capacity for Lean? Because I couldn't tell from your GitHub. If you're a random contributor like me, please do not acknowledge my report, as you are not the intended target (unless of course you're able to fix this).
In any case, I've opened lean4#12268, though I find Zulip threads work better than issues for such things.

[Miyahara Kō]

I’m very sorry. I’m just a random contributor, so I’ll be more careful from now on.

[Ruben Van de Velde]

Hey Snir, I think that reaction was unnecessarily harsh. Filing an issue is the most reliable approach, even if a zulip thread sometimes works

[Miyahara Kō]

@Ruben Van de Velde
Thank you for your concern. This is just my personal speculation, but I think Snir probably didn’t intend to sound that harsh. For non-native speakers, it can be difficult to judge the tone of such messages.

[Miyahara Kō]

(I'm non-native, too.)

[Kim Morrison]

Indeed, I'd say if you're posting about an issue on Zulip, then I (as an FRO employee!) am rather hoping that someone other than me will jump in with suggestions, advice, solutions, or indeed even the instructions that you need to open issues if you don't want your request to get lost. :-)

[Snir Broshi]

Ruben Van de Velde said:

I think that reaction was unnecessarily harsh. Filing an issue is the most reliable approach, even if a zulip thread sometimes works

Sorry, I really tried to make that message sound as pleasant as possible, do you have any suggestions for the future?
I felt deceived by the "thank you for the report", the "create an issue" part is fine as long as it's clear it's not a request coming from the maintainers but rather a helpful community member (e.g. "I recommend creating an issue").

FWIW I've reported a few issues so far, and in my experience posting on Zulip has a much higher success rate than opening an issue, and is a better experience overall.

[Snir Broshi]

Kim Morrison said:

Indeed, I'd say if you're posting about an issue on Zulip, then I (as an FRO employee!) am rather hoping that someone other than me will jump in with suggestions, advice, solutions, or indeed even the instructions that you need to open issues if you don't want your request to get lost. :-)

That's why I wrote "(unless of course you're able to fix this)", which hopefully matches what you mean.
btw here's a previous report which seems related to the Zulip vs issues debate here.

[Miyahara Kō]

When I first saw this post, it only described the bug, and I wasn’t sure what you specifically wanted people to do, so I suggested creating an issue for now.
So next time, I think it would be better to first open an issue and then ask people who seem able to help to look into it.

Also, something I personally worry about is that your contributions might decrease because you’re troubled by minor communication mishaps. I sometimes have similar experiences myself.
I’m not bothered at all, so I think it’s best to forget about this and feel free to keep contributing! :smile: