segfault on M1 on `import Mathlib.Topology.Cat.Basic`

Stream: lean4

[Jackson Walters]

I'm trying to set up Lean for the first time. I've initialized a new project using lake init <my-project> math. It is using the latest version of Lean, v4.22.0-rc3. I'm able to run a basic executable which prints "Hello, world!" and imports def hello := "world" from Basic.lean under Utils. It is using a .toml file.

I'm trying to formalize a fairly simple result about a pushout of Boolean algebras which uses the pullback in Stone spaces. I need imports like:

import Mathlib.Topology.Category.TopCat.Basic
import Mathlib.Topology.Category.TopCat.Limits.Pullbacks
import Mathlib.Topology.Category.Profinite.Basic

However, when I go to import any of these, I get a segmentation fault:

jacksonwalters@jaxmacbookair pushout_boolean_algebras % .lake/build/bin/pushout_boolean_algebras

zsh: segmentation fault  .lake/build/bin/pushout_boolean_algebras

Any help would be appreciated.

[Henrik Böving]

Can you give us a stacktrace of that segfault?

[Jackson Walters]

jacksonwalters@jaxmacbookair pushout_boolean_algebras % lldb .lake/build/bin/pushout_boolean_algebras

(lldb) target create ".lake/build/bin/pushout_boolean_algebras"

Current executable set to '/Users/jacksonwalters/Documents/GitHub/formal-math-lean/pushout_boolean_algebras/.lake/build/bin/pushout_boolean_algebras' (arm64).

(lldb) run

Process 1438 launched: '/Users/jacksonwalters/Documents/GitHub/formal-math-lean/pushout_boolean_algebras/.lake/build/bin/pushout_boolean_algebras' (arm64)

Process 1438 stopped
* thread #1, queue = 'com.apple.main-thread', stop reason = EXC_BAD_ACCESS (code=1, address=0x0)

    frame #0: 0x00000001072c6178 pushout_boolean_algebras`lean_mark_persistent + 148

pushout_boolean_algebras`lean_mark_persistent:
->  0x1072c6178 <+148>: ldr    w8, [x19]

    0x1072c617c <+152>: cbz    w8, 0x1072c6154 ; <+112>

    0x1072c6180 <+156>: str    wzr, [x19]

    0x1072c6184 <+160>: ldr    w8, [x19, #0x4]

Target 0: (pushout_boolean_algebras) stopped.

(lldb) bt
* thread #1, queue = 'com.apple.main-thread', stop reason = EXC_BAD_ACCESS (code=1, address=0x0)

  * frame #0: 0x00000001072c6178 pushout_boolean_algebras`lean_mark_persistent + 148

    frame #1: 0x000000010151bfbc pushout_boolean_algebras`initialize_Mathlib_Data_Set_Basic + 416

    frame #2: 0x000000010151c1e0 pushout_boolean_algebras`initialize_Mathlib_Data_Set_Disjoint + 140

    frame #3: 0x000000010151c99c pushout_boolean_algebras`initialize_Mathlib_Data_Set_Insert + 140

    frame #4: 0x000000010151ca74 pushout_boolean_algebras`initialize_Mathlib_Data_Set_Subsingleton + 140

    frame #5: 0x000000010153e488 pushout_boolean_algebras`initialize_Mathlib_Data_Set_Image + 272

    frame #6: 0x000000010153f334 pushout_boolean_algebras`initialize_Mathlib_Data_Set_Prod + 140

    frame #7: 0x000000010153f768 pushout_boolean_algebras`initialize_Mathlib_Data_Set_Function + 140

    frame #8: 0x0000000101540dec pushout_boolean_algebras`initialize_Mathlib_Logic_Equiv_Set + 140

    frame #9: 0x00000001015a2348 pushout_boolean_algebras`initialize_Mathlib_Order_CompleteBooleanAlgebra + 140

    frame #10: 0x00000001015a281c pushout_boolean_algebras`initialize_Mathlib_Data_Set_BooleanAlgebra + 140

    frame #11: 0x00000001015a2aac pushout_boolean_algebras`initialize_Mathlib_Data_Set_Lattice + 184

    frame #12: 0x00000001015a2b90 pushout_boolean_algebras`initialize_Mathlib_Data_Set_UnionLift + 140

    frame #13: 0x00000001018926dc pushout_boolean_algebras`initialize_Mathlib_Topology_ContinuousMap_Basic + 140

    frame #14: 0x00000001018939c8 pushout_boolean_algebras`initialize_Mathlib_Topology_Category_TopCat_Basic + 200

    frame #15: 0x0000000101893d08 pushout_boolean_algebras`initialize_Utils_Basic + 140

    frame #16: 0x000000010000093c pushout_boolean_algebras`initialize_Main + 140

    frame #17: 0x00000001000009d8 pushout_boolean_algebras`main + 36

    frame #18: 0x000000018bc1c274 dyld`start + 2840

(lldb) quit

[Cameron Zwarich]

Does this still happen with this at the top of your file?

set_option compiler.extract_closed false

[Cameron Zwarich]

Actually, never mind. That would need to be at the top of Mathlib/Data/Set/Basic.lean, which is probably a bit more annoying to test due to the compile times. I can try it out myself.

[Jackson Walters]

Okay, yes I tried adding the line to Main.lean on my end and it resulted in the same stack trace.

[SnO2WMaN]

Sorry for interrupting but Mathlib.Data.Set.Basic depends Mathlib.Order.PropInstances so this issue might be caused same reason, i think.

#mathlib4 > `import Mathlib.Order.PropInstances` causing segment fault

[Jackson Walters]

It sounds like the data structures in Lean depend on PropInstances?

For this particular construction, I'm not sure if I really need data sets [or even the local version of Lean]. I could probably get away with using the web version.

The construction begins with defining the two algebras in play, which are the countable atomless Boolean algebra and its Stone dual, the Cantor set.

The subalgebra in question is FinCof, the finite-cofinite subsets of the natural numbers whose Stone dual is the one-point compactification of the natural numbers.