We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
lean panics on the following input:
class S (R : T u) M : R
$ ~/src/lean4/build/release/stage1/bin/lean panic.lean PANIC at Lean.Expr.fvarId! Lean.Expr:1068:14: fvar expected backtrace: /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x32e9dac)[0x7f42f7ae9dac] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_panic_fn+0xc4)[0x7f42f7aea114] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__6+0x3b)[0x7f42f645828b] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___lambda__3+0x261d)[0x7f42f645dded] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___lambda__4+0x103e)[0x7f42f645f02e] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_5+0xe93)[0x7f42f7afcae3] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Meta_withLCtx___at___private_Lean_Elab_Binders_0__Lean_Elab_Term_FunBinders_elabFunBinderViews___spec__3___rarg+0x47)[0x7f42f69b01c7] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___lambda__5+0xa8f)[0x7f42f643aa8f] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_8+0xc39)[0x7f42f7b02239] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_9+0xb88)[0x7f42f7b03c28] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Elab_Structure_0__Lean_Elab_Command_withParents___rarg+0x34)[0x7f42f641e554] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView+0x8ac)[0x7f42f646074c] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Command_elabStructure___lambda__2+0x467)[0x7f42f64650e7] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Command_elabStructure___lambda__2___boxed+0xf7)[0x7f42f6465e97] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_8+0xfe0)[0x7f42f7b025e0] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_8+0xb6a)[0x7f42f7b0216a] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Elab_Binders_0__Lean_Elab_Term_elabBindersAux_loop___rarg___boxed+0x25)[0x7f42f69c6eb5] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_8+0xb27)[0x7f42f7b02127] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_8+0xc39)[0x7f42f7b02239] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_6+0xcc2)[0x7f42f7afe5e2] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Meta_withLocalDecl___at_Lean_Elab_Term_withAuxDecl___spec__3___rarg+0x92)[0x7f42f62bd862] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Elab_Binders_0__Lean_Elab_Term_elabBinderViews_loop___rarg+0x64a)[0x7f42f69c386a] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Elab_Binders_0__Lean_Elab_Term_elabBindersAux___rarg+0x2f)[0x7f42f69c6f1f] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_7+0xd85)[0x7f42f7b00515] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Term_universeConstraintsCheckpoint___rarg+0xac)[0x7f42f629a0fc] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_7+0x93d)[0x7f42f7b000cd] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Term_withAutoBoundImplicit_loop___rarg+0x143)[0x7f42f62bdda3] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_8+0xb6a)[0x7f42f7b0216a] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_6+0xcc2)[0x7f42f7afe5e2] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Meta_withLocalDecl___at_Lean_Elab_Term_withAuxDecl___spec__3___rarg+0x92)[0x7f42f62bd862] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Term_withAutoBoundImplicit_loop___rarg+0xa2e)[0x7f42f62be68e] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Term_withAutoBoundImplicit___rarg+0x35f)[0x7f42f62bf60f] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_7+0xdd9)[0x7f42f7b00569] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Term_withLevelNames___rarg+0x1c1)[0x7f42f62b6441] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Command_elabStructure___lambda__3___boxed+0xe3)[0x7f42f64679d3] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_7+0x10d7)[0x7f42f7b00867] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Command_elabStructure___lambda__4___boxed+0xe3)[0x7f42f6467ed3] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_7+0x10d7)[0x7f42f7b00867] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_7+0xc5e)[0x7f42f7b003ee] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Command_runTermElabM___rarg___lambda__1___boxed+0x21)[0x7f42f63ea6c1] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_9+0xae7)[0x7f42f7b03b87] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Command_runTermElabM___rarg___lambda__2___boxed+0x21)[0x7f42f63eb5b1] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_8+0x9e4)[0x7f42f7b01fe4] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_7+0xd85)[0x7f42f7b00515] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Term_universeConstraintsCheckpoint___rarg+0xac)[0x7f42f629a0fc] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_7+0x93d)[0x7f42f7b000cd] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Term_withAutoBoundImplicit_loop___rarg+0x143)[0x7f42f62bdda3] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Term_withAutoBoundImplicit___rarg+0x35f)[0x7f42f62bf60f] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_7+0xdd9)[0x7f42f7b00569] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_withSaveInfoContext___at_Lean_Elab_Command_liftTermElabM___spec__1___rarg+0x2c0)[0x7f42f63e4f00] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Command_liftTermElabM___rarg___lambda__1+0x1b)[0x7f42f63e5f2b] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_7+0xdd9)[0x7f42f7b00569] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Term_TermElabM_run___rarg+0x257)[0x7f42f62990e7] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Command_liftTermElabM___rarg+0x49c)[0x7f42f63e669c] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Command_elabStructure___lambda__7+0x125)[0x7f42f6469385] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Command_elabStructure+0x8b7)[0x7f42f646a447] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_3+0x110e)[0x7f42f7af926e] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_withInfoTreeContext___at_Lean_Elab_Command_withMacroExpansion___spec__1___rarg+0x1fe)[0x7f42f63d091e] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Elab_Command_0__Lean_Elab_Command_elabCommandUsing+0x222)[0x7f42f63d1f02] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_3+0x10c6)[0x7f42f7af9226] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_3+0x10ee)[0x7f42f7af924e] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_withLogging___at_Lean_Elab_Command_elabCommand___spec__2+0x57)[0x7f42f63d5497] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Command_elabCommandTopLevel___lambda__2+0x340)[0x7f42f63ddc60] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Frontend_elabCommandAtFrontend+0x1f5)[0x7f42f6558585] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Frontend_elabCommandAtFrontend___boxed+0x16)[0x7f42f6559076] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0x13c7)[0x7f42f7af59e7] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_profileitIOUnsafe___rarg___lambda__1+0x14)[0x7f42f56f6c44] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_profileitIOUnsafe___rarg___lambda__1___boxed+0x11)[0x7f42f56f6d91] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0x1268)[0x7f42f7af5888] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_profileit+0x9f)[0x7f42f7a08b2f] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_profileitIOUnsafe___rarg+0x59)[0x7f42f56f6e29] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Frontend_processCommand+0xc0d)[0x7f42f655be6d] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Frontend_processCommands+0x5e)[0x7f42f655ccbe] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_IO_processCommands+0xf6)[0x7f42f655d1e6] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_runFrontend___lambda__2+0x33)[0x7f42f655e623] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_run_frontend+0x4de)[0x7f42f655fa5e] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x3196823)[0x7f42f7996823] /home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_main+0x29c5)[0x7f42f799a1b5] /lib/x86_64-linux-gnu/libc.so.6(+0x29d90)[0x7f42f4429d90] /lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x80)[0x7f42f4429e40] /home/dwrensha/src/lean4/build/release/stage1/bin/lean(_start+0x25)[0x560b9c666095] panic.lean:1:13: error: function expected at T term has type ?m.3 panic.lean:1:18: error: expected command
$ ~/src/lean4/build/release/stage1/bin/lean --version Lean (version 4.0.0, commit 5c7cf7657580, Release)
The text was updated successfully, but these errors were encountered:
5c74bc1
No branches or pull requests
lean panics on the following input:
The text was updated successfully, but these errors were encountered: