Zulip Chat Archive

Stream: general

Topic: SEGV with irreducible attribute


view this post on Zulip Kevin Buzzard (Aug 18 2020 at 11:49):

universes u v
variable {α : Type u}

/-- Add an extra element `1` to a type -/
def with_one (α) := option α

namespace with_one

instance : monad with_one := option.monad

instance : has_one (with_one α) := none

instance : inhabited (with_one α) := 1

instance [nonempty α] : nontrivial (with_one α) := option.nontrivial

instance : has_coe_t α (with_one α) := some

attribute [irreducible] with_one

@[simp]
lemma one_ne_coe {a : α} : (1 : with_one α)  a :=
λ h, option.no_confusion h

@[simp]
lemma coe_ne_one {a : α} : (a : with_one α)  (1 : with_one α) :=
λ h, option.no_confusion h

lemma ne_one_iff_exists :  {x : with_one α}, x  1   (a : α), x = a
| 1       := ⟨λ h, false.elim $ h rfl, by { rintros a,ha h, simpa using h }
| (a : α) := ⟨λ h, a, rfl, λ h, with_one.coe_ne_one

end with_one

produces a SIGSEGV for me on Ubuntu 18.04 with Lean 3.18.4 . Can anyone else reproduce? This is pretty much directly from mathlib algebra.group.with_one except that I have added the attribute [irreducible] with_one line, possibly too early -- but I didn't expect a segfault.

view this post on Zulip Johan Commelin (Aug 18 2020 at 11:51):

You can't use option.no_confusion after marking it irreducible

view this post on Zulip Johan Commelin (Aug 18 2020 at 11:51):

No idea why it segfaults though

view this post on Zulip Gabriel Ebner (Aug 18 2020 at 12:00):

Please remove references to mathlib and file as a bug. Segfaults are always bugs.

view this post on Zulip Kevin Buzzard (Aug 18 2020 at 12:12):

I've already cleared out the mathlib imports. Can someone else confirm it's segfaulting for them?

view this post on Zulip Gabriel Ebner (Aug 18 2020 at 12:12):

nontrivial?

view this post on Zulip Shing Tak Lam (Aug 18 2020 at 12:19):

I think I've minimised it to the point where there's no mathlib imports, and commenting out any line won't segfault anymore.

variable {α : Type}

def with_one (α) := option α

instance : has_one (with_one α) := none

attribute [irreducible] with_one

lemma ne_one_iff_exists :  {x : with_one α}, x  1   (a : α), x = a
| 1       := by { using }
| (a : α) := sorry

If whatever is between the braces contains using then it crashes. Otherwise Lean just complains about unknown identifier or something else.

lean#450 . The issue title is vague since I don't really know what is going on tbh.

view this post on Zulip Kevin Buzzard (Aug 18 2020 at 12:23):

Thanks Shing. I was minimising and restarting Lean in VS Code and then when I would restart VS Code it wouldn't segfault any more -- I had got as far as I did by constantly restarting VS Code

view this post on Zulip Reid Barton (Aug 18 2020 at 12:35):

For minimizing crashes I generally test from the command line--I don't totally trust emacs to accurately report what is happening when Lean is crashing (though it does seem to generally work)

view this post on Zulip Gabriel Ebner (Aug 18 2020 at 12:36):

If you use a debug build of lean then you actually get an error message instead of a segfault. This makes it a bit easier.


Last updated: May 15 2021 at 23:13 UTC