Segmentation Fault Splitting Files

Stream: lean4

[Eric Paul]

I am getting a segmentation fault when I split my code into two files.
It goes away when I put all the code into a single file.

Unfortunately I don't have a MWE or code to share, so I am just wondering if someone has experienced something similar before.
I'm not doing any FFI and have no dependencies.

[Eric Paul]

Actually it seems like many changes I make are causing segfaults.

Is there any general guidance for debugging this or typical suspects in Lean?

[Chris Bailey]

Your OS, lean version, editor info, and lean extension/plugin version would probably help.

[Eric Paul]

Good point, thanks for help!
Here's some information (I'm working on a mwe right now too).

OS: macOS Monterey Version 12.3
Lean version: Lean (version 4.10.0, x86_64-apple-darwin22.6.0, commit c375e19f6b65, Release)
Editor info: VS Code Version 1.92.2
Lean plugin version: v0.0.176

[Julian Berman]

Does it segfault even at the CLI?

[Eric Paul]

I'm not sure I know exactly what you mean, but this is when it happens:

I get a segfault when I run the following:

lake build; ./.lake/build/bin/test2

And get this output:

Build completed successfully.
zsh: segmentation fault  ./.lake/build/bin/test2```

[Julian Berman]

OK -- so it happens when you run lake build and then your executable?

[Julian Berman]

(If so the VSCode bits probably aren't relevant, which is what I was trying to eliminate)

[Julian Berman]

If you rm -rf .lake and then lake build, does it still segfault then?

[Eric Paul]

When I do that I still get a segfault.

Here's a MWE:

I type

1. lake new test
2. cd test
3. Modify Main.lean to have the following contents

import Lean.Data

def update (_ : Nat × Nat) (_ : Array String) (w : Lean.HashMap (Nat × Nat) (Array String)) :=
  w.insert (0,0) #[]

def test (x : String) (y : Lean.Xml.Element) (z : Lean.HashMap (Nat × Nat) (Array String)): Option (String × (Option String) × (Option String) × (Option String) × (Lean.HashMap (Nat × Nat) (Array String))) := do
  let m : Lean.Xml.Element ←
    (Array.filter
      (fun _ => false)
      (#[y]))[0]?

  let a := ((toString m).split (· = '\n')).getD 0 ""
  let b : Option String := none
  let c : Option String := none
  let d : Option String := do pure $ ""

  pure $ (a, b, c, d, update (0, x.length) #["", s!"{x}"] z)


def main : IO Unit := do
  IO.println "hi"

4. lake build
5. ./.lake/build/bin/test

[Chris Bailey]

I get the same segfault on an intel mac on 4.10.0 and 4.11.0-rc2; it has something to do with the string interpolation (s!"{x}")

[Chris Bailey]

Ok it has to be an array of length > 1 and include the string interpolation.

[Julian Berman]

It's quite fragile.

[Julian Berman]

I've minimized to...

import Lean.Data

def update (_ : Nat × Nat) (_ : Array String) (w : Lean.HashMap (Nat × Nat) (Array String)) :=
  w.insert (0,0) #[]

def test (x : String) (y : Lean.Xml.Element) (z : Lean.HashMap (Nat × Nat) (Array String)): Option (String × (Option String) × (Option String) × String × (Lean.HashMap (Nat × Nat) (Array String))) := do
  pure $ (
    ((toString (← (Array.filter (fun _ => true) #[y])[0]?)).split (· = '0')).getD 0 "",
    none,
    "",
    "",
    update (x.length, x.length) #[s!"{x}", s!"{x}"] z
  )


def main : IO Unit := pure ()

[Julian Berman]

The backtrace has gmp things in it. EDIT: maybe not.

[Eric Paul]

Yes, its fragility is what made me take so long in making a mwe. It seemed like every tiny change made a large difference.

[Eric Paul]

Thanks again for the interest and help!
This segfault has been destroying me

[Chris Bailey]

@Julian Berman Out of curiosity, what OS/lean version are you on

[Julian Berman]

Further:

import Lean.Data.HashMap

mutual
inductive Foo
| Foo (bar : Bar)

inductive Bar
| Foo (foo : Foo)
| Baz (baz : String)
end

mutual
def eToString : Foo → String
| Foo.Foo c => cToString c

def cToString : Bar → String
| Bar.Foo e => eToString e
| Bar.Baz c => c

end
instance : ToString Foo := ⟨eToString⟩
instance : ToString Bar := ⟨cToString⟩

def update (_ : Nat × Nat) (_ : Array String) (w : Lean.HashMap (Nat × Nat) (Array String)) :=
  w.insert (0,0) #[]

def test (x : String) (y : Foo) (z : Lean.HashMap (Nat × Nat) (Array String)): Option (String × (Option String) × (Option String) × String × (Lean.HashMap (Nat × Nat) (Array String))) := do
  pure $ (
    ((toString (← (Array.filter (fun _ => true) #[y])[0]?)).split (· = '0')).getD 0 "",
    none,
    "",
    "",
    update (x.length, x.length) #[s!"{x}", s!"{x}"] z
  )


def main : IO Unit := pure ()

[Julian Berman]

@Chris Bailey Also macOS -- 14.6.1 (23G93) + lean 4.11.0-rc2

[Julian Berman]

@Eric Paul I suspect what any of us have (including what you started with) is probably good enough to file a bug on the lean4 tracker, they mostly care that it doesn't have Mathlib in it I think.

[Eric Paul]

Sounds good, I can file an issue

[Eric Paul]

Here's the issue https://github.com/leanprover/lean4/issues/5188

[Henrik Böving]

Debugged and workaround available at the issue.

[Eric Paul]

The fix works, my code is running once again!
Thank you so much for the quick inspection and fix