Zulip Chat Archive

Stream: general

Topic: SEGV with irreducible attribute

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

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

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.

Johan Commelin (Aug 18 2020 at 11:51):

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

Johan Commelin (Aug 18 2020 at 11:51):

No idea why it segfaults though

Gabriel Ebner (Aug 18 2020 at 12:00):

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

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?

Gabriel Ebner (Aug 18 2020 at 12:12):


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.

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

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)

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: Aug 03 2023 at 10:10 UTC