Zulip Chat Archive

Stream: general

Topic: Segfault


Yury G. Kudryashov (Sep 27 2020 at 05:10):

If I add set_option old_structure_cmd true right above the definition of src#normed_ring, Lean segfaults (Linux).

Yury G. Kudryashov (Sep 27 2020 at 05:10):

I need normed_ring to become an old structure because I need a normed_comm_ring.

Floris van Doorn (Sep 27 2020 at 06:05):

I think I tried to do that too at some point:
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/C*-algebras
I never ended up doing something with that.

I think the problem is that

Should I make a PR turning normed_ring (and all other structures in the algebraic hierarchy) into something that uses old_structure_cmd?

So if you turn normed_ring into and old_structure, then you should also make all structures it depends on an old_structure. (Of course, this should not cause a segfault but an error)

Yury G. Kudryashov (Sep 27 2020 at 06:51):

Another option is to make a mixin has_mul_comm


Last updated: Dec 20 2023 at 11:08 UTC