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 : 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 (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?

nontrivial?

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: Dec 20 2023 at 11:08 UTC