assertion violation hell

Stream: general

[Kevin Buzzard]

I'm trying to make an instance of add_comm_group X and every time I press a key I get an assertion violation and the VS Code window unfocuses. This is with Lean 3.5.1. I'm not sure I can minimise but does anyone have any tips as to why this might be happening?

[Bryan Gin-ge Chen]

You're probably triggering some bug in Lean. What does the assertion violation say exactly?

[Kevin Buzzard]

It's the usual line 3174 one:

Task: /home/buzzard/Encfs/Computer_languages/Lean/lean-projects/Wu_group_cohomology_M4R/src/add_subquotient/basic.lean: coe_sort.add_comm_group
m_ctx.match(e, *val2)
LEAN ASSERTION VIOLATION
File: /home/travis/build/leanprover-community/lean/src/frontends/lean/elaborator.cpp
Line: 3174

[Bryan Gin-ge Chen]

Oh, I wasn't aware that this happened frequently. Could you open an issue here? https://github.com/leanprover-community/lean/issues

[Kevin Buzzard]

It happens a fair amount to me when I am making structures. This seems to reliably trigger it for me:

import ring_theory.algebra

open function

def quot.lift
  {R : Type*} [comm_ring R]
  {A : Type*} [comm_ring A] [algebra R A]
  {B : Type*} [comm_ring B] [algebra R B]
  {C : Type*} [comm_ring C] [algebra R C]
  (f : A →ₐ[R] B) (hf : surjective f)
  (g : A →ₐ[R] C) (hfg : ∀ a : A, f a = 0 → g a = 0) :
  B →ₐ[R] C :=
{ to_fun := λ b, _,
  map_one' := _,
  map_mul' := _,
  map_zero' := _,
  map_add' := _,
  commutes' := _ }

LEAN ASSERTION VIOLATION
File: /home/travis/build/leanprover-community/lean/src/frontends/lean/elaborator.cpp
Line: 3174
Task: /home/buzzard/lean-projects/M4P33/scratch/unreachable.lean: quot.lift
m_ctx.match(e, *val2)

Does it trigger it for anyone else or is there something wrong with my set-up?

[Sebastien Gouezel]

I just tried it, and it also triggered the assertion violation for me.

[Bryan Gin-ge Chen]

I just tested your code in a 3.4.2 project and it triggered there as well.

[Kevin Buzzard]

(to give an indication as to how common it is for me, this is an independent problem from last week. I think I sometimes push the elaborator too far when making a structure)

[Bhavik Mehta]

I've had the same violation (and frustration) working with category theory structures, it seemed to happen only when I had _ in some part of a structure I was defining in term mode