segfault at 4.15.0-rc1

[seanmcl]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• [X ] Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
  There is Segfault in a complex test case #6332 but it is not at 4.15.
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

[Clear and concise description of the issue]

Running lake build && lake exe tensorlib results in a segfault at 4.15.0-rc1 but is fine at 4.14.0.

Context

[Broader context that the issue occurred in. If there was any prior discussion on the Lean Zulip, link it here as well.]

Steps to Reproduce

1. Checkout the sm/segfault-at-4.15.0-rc1 branch: https://github.com/leanprover/TensorLib/tree/sm/segfault-at-4.15.0-rc1
2. lake build
3. lake exe tensorlib

Expected behavior:
0 exit code

Actual behavior:
segfault

Versions

[Output of #version or #eval Lean.versionString]
4.15.0-rc1

[OS version, if not using live.lean-lang.org.]
OSX 14.7.1

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[seanmcl]

I will attempt to minimize the example next week. I thought the people managing the 4.15 release may want to see this asap.

[hargoniX]

The segfault occurs in lean_alloc_small which is likely a red herring, the backtrace goes into batteries:

#0  0x000055d3aeea0030 in lean_alloc_small ()
#1  0x000055d3aa1d1d2b in l_Batteries_Linter_UnreachableTactic_initFn____x40_Batteries_Linter_UnreachableTactic___hyg_62_ ()
#2  0x000055d3aa1deda2 in initialize_Batteries_Linter_UnreachableTactic ()
#3  0x000055d3aa1f0e59 in initialize_Aesop_Frontend_Tactic ()
#4  0x000055d3aa205fcc in initialize_Aesop_Main ()
#5  0x000055d3aa2e50b0 in initialize_Aesop ()
#6  0x000055d3aa35d1e4 in initialize_TensorLib_Broadcast ()
#7  0x000055d3aa37a426 in initialize_TensorLib_Basic ()
#8  0x000055d3aa37a5b5 in initialize_TensorLib ()
#9  0x000055d3a9aca9c5 in initialize_Main ()
#10 0x000055d3a9acaa4b in main ()

[kim-em]

This minimizes to

import Lean.CoreM

open Lean Elab

partial def «elab» : CoreM Unit := do
  if h : 0 < #[].size then return ← «elab» $ #[][0]
  throwUnsupportedSyntax

def main (_args : List String) : IO UInt32 :=
  return 0

which exits with 139 under lake exe. This minimization, however, is not a change of behaviour on v4.15.0-rc1: it's been broken way back, and is a known issue.

[kim-em]

The orginally reported issue, however really is new to v4.15.0-rc1, strange.

[kim-em]

Ah, I'm an idiot, I've already encountered exactly this problem before in leanprover-community/aesop#182, and @JLimperg has fixed it in leanprover-community/aesop#183.

Hence a solution is to use the master branch of Aesop, rather than the v4.15.0-rc1 tag, i.e.

require aesop from git
  "https://github.com/leanprover-community/aesop" @ "master"

(Alternatively the v4.15.0 tag includes the bugfix too. I am tempted to force push the v4.15.0-rc1 tag to include this bug fix, but won't for now.)

[kim-em]

(Please reopen, or ping me, if this solution won't suffice.)