search

leanprover-community / repl

A simple REPL for Lean 4, returning information about errors and sorries.
54 stars 13 forks source link

segfault and panic #3

Closed zhangir-azerbayev closed 1 year ago

zhangir-azerbayev commented 1 year ago

I've managed to find two instances that make the REPL crash.

The following input causes a segfault, with nothing printed to stdout or stderr. 

{ "cmd" : "import Mathlib.Algebra.Order.Ring.Abs\nimport Mathlib.Data.Nat.Order.Basic\nimport Mathlib.Tactic.Ring\n\nopen List\n\nexample (α : Type) (L M : List α) : (L ++ M ++ L).length = (M ++ L ++ L).length := by\n  rw [length_append, length_append, length_append, length_append]\n  ring" }

The following two inputs result in a PANIC. 

{ "cmd" : "import Mathlib.Algebra.Order.Ring.Abs\nimport Mathlib.Data.Nat.Order.Basic\nimport Mathlib.Tactic.Ring\n\nopen List\n\nexample (α : Type) (L M : List α) : (L ++ M ++ L).length = (M ++ L ++ L).length := by\n  rw [length_append],\n  rw [length_append, length_append]" }

{"sorries": [],
 "messages":
 [{"severity": "error",
   "pos": {"line": 7, "column": 83},
   "endPos": {"line": 8, "column": 20},
   "data":
   "unsolved goals\nα : Type\nL M : List α\n⊢ length (L ++ M) + length L = length (M ++ L ++ L)"},
  {"severity": "error",
   "pos": {"line": 8, "column": 20},
   "endPos": null,
   "data": "expected command"}],
 "env": 0}
{ "cmd" : "import Mathlib.Algebra.Order.Ring.Abs\nimport Mathlib.Data.Nat.Order.Basic\nimport Mathlib.Tactic.Ring\n\nopen List\n\nexample (α : Type) (L M : List α) : (L ++ M ++ L).length = (M ++ L ++ L).length := by\n  rw [length_append],\n  rw [length_append, length_append]" }

Which gives back

PANIC at Lean.PersistentHashMap.find! Lean.Data.PersistentHashMap:160:14: key is not in the map
backtrace:
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(lean_panic_fn+0x9e)[0x7f910ca5128e]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x347ad44)[0x7f910ca47d44]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x3478fc0)[0x7f910ca45fc0]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x347b082)[0x7f910ca48082]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x3478fc0)[0x7f910ca45fc0]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x347b082)[0x7f910ca48082]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x3478fc0)[0x7f910ca45fc0]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x347b082)[0x7f910ca48082]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x3478fc0)[0x7f910ca45fc0]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x347cb93)[0x7f910ca49b93]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x3475a01)[0x7f910ca42a01]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x347c817)[0x7f910ca49817]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x347c463)[0x7f910ca49463]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(lean_apply_4+0x6e8)[0x7f910ca5e318]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(l_Array_forInUnsafe_loop___at_Lean_Elab_Command_runLinters___spec__4+0x16c)[0x7f910aeedbcc]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Command_runLinters___lambda__1+0x1c5)[0x7f910aef0115]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(lean_apply_1+0x175)[0x7f910ca5b375]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(l_Lean_profileitIOUnsafe___rarg___lambda__1+0xe)[0x7f910a3b58de]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(l_Lean_profileitIOUnsafe___rarg___lambda__1___boxed+0xf)[0x7f910a3b5adf]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(lean_apply_1+0x149)[0x7f910ca5b349]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(lean_profileit+0x74)[0x7f910c9a2d24]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(l_Lean_profileitIOUnsafe___rarg+0x60)[0x7f910a3b5a00]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Command_runLinters+0x156)[0x7f910aef07f6]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(lean_apply_3+0x35b)[0x7f910ca5d27b]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(l_Lean_Elab_withLogging___at_Lean_Elab_Command_elabCommand___spec__2+0x52)[0x7f910aefd732]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Command_elabCommandTopLevel___lambda__2+0x8c5)[0x7f910af0be25]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Frontend_elabCommandAtFrontend+0x1d4)[0x7f910b8ae2f4]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Frontend_elabCommandAtFrontend___boxed+0x10)[0x7f910b8aeb00]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(lean_apply_1+0x175)[0x7f910ca5b375]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(l_Lean_profileitIOUnsafe___rarg___lambda__1+0xe)[0x7f910a3b58de]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(l_Lean_profileitIOUnsafe___rarg___lambda__1___boxed+0xf)[0x7f910a3b5adf]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(lean_apply_1+0x149)[0x7f910ca5b349]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(lean_profileit+0x74)[0x7f910c9a2d24]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(l_Lean_profileitIOUnsafe___rarg+0x60)[0x7f910a3b5a00]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Frontend_processCommand+0x52d)[0x7f910b8b0ecd]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Frontend_processCommands+0x52)[0x7f910b8b1a52]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(l_Lean_Elab_IO_processCommands+0xe0)[0x7f910b8b1e70]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(lean_apply_1+0x175)[0x7f910ca5b375]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x347a4e0)[0x7f910ca474e0]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x3478fc0)[0x7f910ca45fc0]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x347b082)[0x7f910ca48082]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x3478fc0)[0x7f910ca45fc0]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x347b082)[0x7f910ca48082]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x3478fc0)[0x7f910ca45fc0]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x347b082)[0x7f910ca48082]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x3478fc0)[0x7f910ca45fc0]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x347b082)[0x7f910ca48082]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x3478fc0)[0x7f910ca45fc0]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x347b082)[0x7f910ca48082]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x3478fc0)[0x7f910ca45fc0]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x347b082)[0x7f910ca48082]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x3478fc0)[0x7f910ca45fc0]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x347b082)[0x7f910ca48082]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x3478fc0)[0x7f910ca45fc0]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x347cb93)[0x7f910ca49b93]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x347c817)[0x7f910ca49817]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x347c429)[0x7f910ca49429]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(lean_apply_3+0x683)[0x7f910ca5d5a3]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x347a4e0)[0x7f910ca474e0]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x3478fc0)[0x7f910ca45fc0]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x347b082)[0x7f910ca48082]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x3478fc0)[0x7f910ca45fc0]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x347b082)[0x7f910ca48082]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x3478fc0)[0x7f910ca45fc0]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x347b082)[0x7f910ca48082]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x3478fc0)[0x7f910ca45fc0]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x347cb93)[0x7f910ca49b93]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x347c817)[0x7f910ca49817]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x347c3f4)[0x7f910ca493f4]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(lean_apply_2+0x2df)[0x7f910ca5c10f]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x347648a)[0x7f910ca4348a]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x347d039)[0x7f910ca4a039]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x3475c11)[0x7f910ca42c11]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(+0x3475047)[0x7f910ca42047]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/../lib/lean/libleanshared.so(lean_main+0x2878)[0x7f910c9406d8]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf3)[0x7f910926f083]
/home/zhangir/.elan/toolchains/leanprover--lean4---nightly/bin/lean(_start+0x25)[0x55cb034e37e5]
{"sorries": [],
 "messages":
 [{"severity": "error",
   "pos": {"line": 1, "column": 0},
   "endPos": null,
   "data":
   "invalid option declaration 'linter.unreachableTactic', option already exists"},
  {"severity": "error",
   "pos": {"line": 5, "column": 5},
   "endPos": {"line": 5, "column": 9},
   "data": "unknown namespace 'List'"},
  {"severity": "error",
   "pos": {"line": 7, "column": 39},
   "endPos": null,
   "data": "expected ')', ',' or ':'"}],
 "env": 1}
gebner commented 1 year ago

The second one is unsurprising. Importing twice is completely unsupported.

Do you have a backtrack for the first one?

zhangir-azerbayev commented 1 year ago

Note that I've added 

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"

to the lakefile.lean and ran lake update, lake clean, and lake build

zhangir-azerbayev commented 1 year ago

The second one is unsurprising. Importing twice is completely unsupported.

Do you have a backtrack for the first one?

If my understanding of the code is correct, the repl is supposed to create a new environment unless you explicitly refer to a previous environment using the "env" key.

zhangir-azerbayev commented 1 year ago

Member

For the first one, the repl crashes without printing an error message. Is there some kind of verbose mode or debugging mode I can enter to get more information?

gebner commented 1 year ago

Yes, you understand correctly. But you can only create one "initial" environment. This is a hard limitation of Lean. And we should probably give a better error message in the repl..

gebner commented 1 year ago

Member

For the first one, the repl crashes without printing an error message. Is there some kind of verbose mode or debugging mode I can enter to get more information?

You can run the repl in a debugger (like gdb)

gebner commented 1 year ago

I can't reproduce the segfault. Your first example prints the following for me:

{"sorries": [], "messages": [], "env": 0}
zhangir-azerbayev commented 1 year ago

I also can't reproduce the segfault. I have no idea what is different between when I ran it earlier today and now. I'm closing the issue. Thank you for helping out @gebner