Zulip Chat Archive
Stream: mathlib4
Topic: crash
Johan Commelin (Mar 09 2023 at 12:34):
In !4#2743 I'm seeing a very mysterious crash. I have no idea what's happening. See L550.
Mathlib/Algebra/Algebra/Subalgebra/Basic.lean crashed, likely due to a stack overflow or a bug.
Johan Commelin (Mar 09 2023 at 12:36):
libc++abi: terminating due to uncaught exception of type lean::stack_space_exception: deep recursion was detected at 'expression equality test' (potential solution: increase stack space in your system)
Johan Commelin (Mar 09 2023 at 12:41):
That file, without all the cruft:
import Mathlib.Algebra.Algebra.Basic
universe u v
/-- A subalgebra is a sub(semi)ring that includes the range of `algebra_map`. -/
structure Subalgebra (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] extends
Subsemiring A : Type v where
algebraMap_mem' : ∀ r, algebraMap R A r ∈ carrier
zero_mem' := (algebraMap R A).map_zero ▸ algebraMap_mem' 0
one_mem' := (algebraMap R A).map_one ▸ algebraMap_mem' 1
namespace Submodule
variable {R A : Type _} [CommSemiring R] [Semiring A] [Algebra R A]
variable (p : Submodule R A)
/-- A submodule containing `1` and closed under multiplication is a subalgebra. -/
def toSubalgebra (p : Submodule R A) (h_one : (1 : A) ∈ p)
(h_mul : ∀ x y, x ∈ p → y ∈ p → x * y ∈ p) : Subalgebra R A :=
{ p with
mul_mem' := _
algebraMap_mem' := _ }
end Submodule
Johan Commelin (Mar 09 2023 at 12:41):
Can someone confirm that this is a reproducible crash?
Kevin Buzzard (Mar 09 2023 at 13:01):
It crashes my Lean 4 on Ubuntu 20.04 with the same error.
Johan Commelin (Mar 09 2023 at 13:01):
Ok, thanks for checking. Then I know it's not just my setup
Johan Commelin (Mar 09 2023 at 13:23):
Aha, it's because the default arguments don't work
Johan Commelin (Mar 09 2023 at 13:23):
/-- A submodule containing `1` and closed under multiplication is a subalgebra. -/
def toSubalgebra (p : Submodule R A) (h_one : (1 : A) ∈ p)
(h_mul : ∀ x y, x ∈ p → y ∈ p → x * y ∈ p) : Subalgebra R A :=
{ p with
mul_mem' := _
zero_mem' := _
one_mem' := _
algebraMap_mem' := _ }
doesn't crash
Matthew Ballard (Mar 09 2023 at 14:53):
It would nice if autoParam failures threw more understandable errors.
Johan Commelin (Mar 09 2023 at 14:59):
and didn't require a restart of the entire file
Kevin Buzzard (Mar 09 2023 at 15:28):
It was autoparams which were causing panics in some category theory file which I ported recently and continually having to restart lean was indeed very frustrating.
Matthew Ballard (Mar 09 2023 at 15:31):
That is one of three other situations where this has arisen.
Matthew Ballard (Mar 09 2023 at 15:31):
Another one from Zulip
Matthew Ballard (Mar 09 2023 at 15:34):
Matthew Ballard (Mar 09 2023 at 15:36):
I had a similar situation happen just now in !4#2752. No crash but it didn't tell me the autoParam for sub_eq_add_neg failed.
Matthew Ballard (Mar 09 2023 at 15:36):
Previous ones were pinned on aesop but I don't think mine and Johan's are, right?
Jannis Limperg (Mar 09 2023 at 16:07):
The Aesop-related errors went away when I made sure that Aesop only succeeds if it in fact solved the goal. So my hypothesis is that Lean doesn't deal well with auto-param tactics which report success but don't solve the goal.
Matthew Ballard (Mar 09 2023 at 16:12):
My guess also
Johan Commelin (Mar 09 2023 at 16:18):
In my case it wasn't even a tactic. Just a default term.
Matthew Ballard (Mar 09 2023 at 16:20):
Same as mine but without the crash. Just a strange error.
James Gallicchio (Mar 16 2023 at 17:26):
Just encountered this error in my project without any autoparams, but it's very deep in my project and not easy to MWE :/
Last updated: Dec 20 2023 at 11:08 UTC