SEGV with irreducible attribute

Stream: general

[Kevin Buzzard]

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.

[Johan Commelin]

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

[Johan Commelin]

No idea why it segfaults though

[Gabriel Ebner]

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

[Kevin Buzzard]

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

[Gabriel Ebner]

nontrivial?

[Shing Tak Lam]

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]

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]

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]

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.