add_decl_doc panic loop

Stream: lean4

[Patrick Massot]

It seems that add_decl_doc is creating this chaos.

[Kevin Buzzard]

yeah I can reproduce

[Sebastian Ullrich]

Could you post a single stack trace (top dozen frames are usually sufficient) here?

[Patrick Massot]

I starts with

/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(+0x33adbae)[0x7f5eff893bae]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(lean_apply_1+0x420)[0x7f5eff880ac0]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(+0x33992a8)[0x7f5eff87f2a8]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(+0x339a351)[0x7f5eff880351]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(+0x338e9a5)[0x7f5eff8749a5]
/lib/x86_64-linux-gnu/libc.so.6(+0x94b43)[0x7f5efc325b43]
/lib/x86_64-linux-gnu/libc.so.6(+0x126a00)[0x7f5efc3b7a00]
PANIC at Lean.Parser.withCacheFn Lean.Parser.Types:397:4: withCacheFn: unexpected stack growth #[]
backtrace:
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(lean_panic_fn+0x9e)[0x7f5eff87672e]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(l_Lean_Parser_withCacheFn___lambda__2+0x259)[0x7f5efe62c949]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(lean_apply_2+0x5aa)[0x7f5eff88187a]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(lean_apply_2+0x5aa)[0x7f5eff88187a]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(lean_apply_2+0x136)[0x7f5eff881406]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(lean_apply_2+0x5aa)[0x7f5eff88187a]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(l_Lean_Loop_forIn_loop___at_Lean_Parser_parseCommand___spec__1___lambda__4+0x171)[0x7f5efe5c59d1]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(l_Lean_Loop_forIn_loop___at_Lean_Parser_parseCommand___spec__1+0x46f)[0x7f5efe5c620f]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(l_Lean_Parser_parseCommand+0x25e)[0x7f5efe5c73ae]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(l_Lean_Server_Snapshots_compileNextCmd+0x2a4)[0x7f5efe7bee84]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(l___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_nextCmdSnap___lambda__1+0x200)[0x7f5efe8abca0]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(l___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_nextCmdSnap+0x572)[0x7f5efe8acdd2]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(lean_apply_2+0x5f0)[0x7f5eff8818c0]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(l_IO_AsyncList_unfoldAsync_step___rarg+0x38)[0x7f5efe77f208]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(lean_apply_1+0x455)[0x7f5eff880af5]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(l_EIO_toBaseIO___rarg+0xd)[0x7f5efd056e5d]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(lean_apply_1+0x420)[0x7f5eff880ac0]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(+0x33adbae)[0x7f5eff893bae]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(lean_apply_1+0x420)[0x7f5eff880ac0]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(+0x33992a8)[0x7f5eff87f2a8]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(+0x339a351)[0x7f5eff880351]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(+0x338e9a5)[0x7f5eff8749a5]
/lib/x86_64-linux-gnu/libc.so.6(+0x94b43)[0x7f5efc325b43]
/lib/x86_64-linux-gnu/libc.so.6(+0x126a00)[0x7f5efc3b7a00]
PANIC at Lean.Parser.SyntaxStack.back Lean.Parser.Types:168:4: SyntaxStack.back: element is inaccessible
backtrace:
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(lean_panic_fn+0x9e)[0x7f5eff87672e]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(l_Lean_Parser_withCacheFn___lambda__1+0x66)[0x7f5efe62c0b6]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(l_Lean_Parser_withCacheFn___lambda__2+0x269)[0x7f5efe62c959]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(lean_apply_2+0x5aa)[0x7f5eff88187a]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(lean_apply_2+0x5aa)[0x7f5eff88187a]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(lean_apply_2+0x136)[0x7f5eff881406]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(lean_apply_2+0x5aa)[0x7f5eff88187a]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(l_Lean_Loop_forIn_loop___at_Lean_Parser_parseCommand___spec__1___lambda__4+0x171)[0x7f5efe5c59d1]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(l_Lean_Loop_forIn_loop___at_Lean_Parser_parseCommand___spec__1+0x46f)[0x7f5efe5c620f]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(l_Lean_Parser_parseCommand+0x25e)[0x7f5efe5c73ae]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(l_Lean_Server_Snapshots_compileNextCmd+0x2a4)[0x7f5efe7bee84]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(l___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_nextCmdSnap___lambda__1+0x200)[0x7f5efe8abca0]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(l___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_nextCmdSnap+0x572)[0x7f5efe8acdd2]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(lean_apply_2+0x5f0)[0x7f5eff8818c0]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(l_IO_AsyncList_unfoldAsync_step___rarg+0x38)[0x7f5efe77f208]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(lean_apply_1+0x455)[0x7f5eff880af5]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(l_EIO_toBaseIO___rarg+0xd)[0x7f5efd056e5d]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(lean_apply_1+0x420)[0x7f5eff880ac0]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(+0x33adbae)[0x7f5eff893bae]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(lean_apply_1+0x420)[0x7f5eff880ac0]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(+0x33992a8)[0x7f5eff87f2a8]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(+0x339a351)[0x7f5eff880351]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(+0x338e9a5)[0x7f5eff8749a5]
/lib/x86_64-linux-gnu/libc.so.6(+0x94b43)[0x7f5efc325b43]
/lib/x86_64-linux-gnu/libc.so.6(+0x126a00)[0x7f5efc3b7a00]
PANIC at Lean.Parser.SyntaxStack.back Lean.Parser.Types:168:4: SyntaxStack.back: element is inaccessible
backtrace:
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(lean_panic_fn+0x9e)[0x7f5eff87672e]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(l_Lean_Loop_forIn_loop___at_Lean_Parser_parseCommand___spec__1___lambda__3+0x1d5)[0x7f5efe5c54e5]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(l_Lean_Loop_forIn_loop___at_Lean_Parser_parseCommand___spec__1___lambda__4+0x25b)[0x7f5efe5c5abb]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(l_Lean_Loop_forIn_loop___at_Lean_Parser_parseCommand___spec__1+0x46f)[0x7f5efe5c620f]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(l_Lean_Parser_parseCommand+0x25e)[0x7f5efe5c73ae]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean/libleanshared.so(l_Lean_Server_Snapshots_compileNextCmd+0x2a4)[0x7f5efe7bee84]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-12-13/bin/../lib/lean

[Patrick Massot]

Here it says twice PANIC at Lean.Parser.SyntaxStack.back Lean.Parser.Types:168:4: SyntaxStack.back: element is inaccessible but later there is a great diversity of PANIC

[Sebastian Ullrich]

In the gif there is something about Lean.Environment first though?

[Patrick Massot]

I have a much better repro. In a file with no mathlib import:

/-- Test -/
add_decl_doc Nat

/-- Test -/
add_decl_doc Nat

[Patrick Massot]

This is on leanprover/lean4:nightly-2022-12-13

[Patrick Massot]

@Sebastian Ullrich should I open a Lean 4 issue or this enough?

[Sebastian Ullrich]

An issue would be great!

[Sebastian Ullrich]

But the short answer is that you may not define docstrings for external declarations

[Patrick Massot]

What do you mean by external? Defined in another file?

[Patrick Massot]

The first add_decl_doc works fine, only the second one brings the end of the world.

[Patrick Massot]

But indeed this doesn't happen in

def x : Nat := 1

/-- Test -/
add_decl_doc x

/-- Test -/
add_decl_doc x

[Sebastian Ullrich]

One add_decl_doc Nat is sufficient on my machine

[Sebastian Ullrich]

And then we return default : Environment from the panic and then everything goes sideways

[Patrick Massot]

https://github.com/leanprover/lean4/issues/1957

[Jannis Limperg]

Sebastian Ullrich said:

Not aborting on panics for general Lean programs was a conscious decision, but I'm starting to wonder whether it's the right decision for lean itself

Do you by any chance have a link to the discussion where this decision was made? I find this very strange (both for Lean programs and for Lean itself), but maybe there are good reasons I haven't considered.

[Mario Carneiro]

I agree with jannis, continuing after a panic breaks a lot of intuitions and makes it hard to use it to enforce invariants. I assume that the sense Sebastian means is that you don't want a panic somewhere to crash the server, but I think that can be handled by having a way to catch panics and recover in an IO context, specifically for use cases like a long running server that shouldn't ever crash (or at least, should have the opportunity to present failures nicely). That is also what rust panics do, although the need for unwind safety definitely complicates a lot of things

[Sebastian Ullrich]

Jannis Limperg said:

Sebastian Ullrich said:

Not aborting on panics for general Lean programs was a conscious decision, but I'm starting to wonder whether it's the right decision for lean itself

Do you by any chance have a link to the discussion where this decision was made? I find this very strange (both for Lean programs and for Lean itself), but maybe there are good reasons I haven't considered.

Unfortunately I don't recall where these discussions were held. But Leo's motivation for the default is that when we prove something about a function's output, which we think of as a total correctness property, it must not be undermined at run time by process termination from a panic.

[Sebastian Ullrich]

Mario Carneiro said:

That is also what rust panics do, although the need for unwind safety definitely complicates a lot of things

To panic safety issues add issues about correctly freeing reference counting tokens on the stack without excessive additional code generation

[Jannis Limperg]

Sebastian Ullrich said:

Unfortunately I don't recall where these discussions were held. But Leo's motivation for the default is that when we prove something about a function's output, which we think of as a total correctness property, it must not be undermined at run time by process termination from a panic.

I see, thanks! In practice, I would still much prefer that a panic!-ing function actually panics, instead of silently doing the wrong thing just in case I want to prove something about it.

Btw, would it be possible to translate panic! into an opaque value of the type instead of default? This would make it harder (though not impossible) to write bogus proofs about the branches which contain panic!. I feel like this has been discussed before, but I can't find the topic.

[James Gallicchio]

I'm regularly annoyed by this... I want my panics to crash.

[Sebastian Ullrich]

I probably should have mentioned LEAN_ABORT_ON_PANIC=1

[James Gallicchio]

I think it's a pretty good dogfooding goal for it to be feasible to rewrite the lean server to exist in an exception monad where necessary, to safely continue after an error. Thoughts?

[James Gallicchio]

(rather than using panic!)