Zulip Chat Archive

Stream: general

Topic: Segfault??

SnowFox (Oct 15 2020 at 03:22):

While refactoring some code I managed to segfault Lean. I've mostly reduced the issue.

https://gist.github.com/a3c2de85461ed212c174b62565346d1b

SnowFox (Oct 15 2020 at 03:39):

@[derive decidable_eq]
inductive T | a | b

structure bar (type : T) :=
(mode : if type = T.b then nat else bool)

inductive foo
| q {rtype} (x : bar rtype) (y : opt_param (bar rtype) 0)

namespace foo
  def z : foo → unit
  | (q (⟨tt⟩ : bar T.a) _) := ()
  | _ := ()
end foo

Bryan Gin-ge Chen (Oct 15 2020 at 04:37):

I suspect it might be the same issue as lean#52 but I haven't checked with lldb.

Bryan Gin-ge Chen (Oct 15 2020 at 04:38):

The reason for my hunch is that if I open your code with the web editor (with the convenient new button that shows up when I hover over your snippet), I get the same message:

equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
nested exception message:
cases tactic failed, it is not applicable to the given hypothesis

SnowFox (Oct 15 2020 at 04:38):

Plausible. Speaking of the playground.

equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
nested exception message:
cases tactic failed, it is not applicable to the given hypothesis