Zulip Chat Archive

Stream: general

Topic: Segfault??


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip SnowFox (Oct 15 2020 at 04:38):

^^

view this post on Zulip SnowFox (Oct 15 2020 at 04:40):

I have run this previously; forgot to mention it!

view this post on Zulip SnowFox (Oct 15 2020 at 04:41):

I guess I should add my code and trace to that thread then?

view this post on Zulip SnowFox (Oct 15 2020 at 04:42):

Or a new issue and reference it as plausibly related?

view this post on Zulip Bryan Gin-ge Chen (Oct 15 2020 at 04:43):

Give me a second, I'll check with lldb.

view this post on Zulip SnowFox (Oct 15 2020 at 04:43):

Okay.

view this post on Zulip Bryan Gin-ge Chen (Oct 15 2020 at 04:45):

Yep, it's crashing in the same function.

view this post on Zulip Bryan Gin-ge Chen (Oct 15 2020 at 04:46):

Since @Koundinya Vajjha found the issue first, maybe he has an idea for a workaround?

view this post on Zulip SnowFox (Oct 15 2020 at 05:06):

Oh I already have my workaround. @q ff .. for that example.

view this post on Zulip SnowFox (Oct 15 2020 at 05:08):

In my real code that's @arith integer .., I found this because I'm using patterns to abstract away noise / focus on the relevant details.


Last updated: May 08 2021 at 03:17 UTC