Lake 4.34.0-rc2 crashes on macOS 27 (Golden Gate)

[johoelzl]

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• nightly works 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

Running lake --version on macOS 27 crashes after correctly printing the version for 4.34.0-rc2 but not for 4.33.1 or nightly.

So nightly fixes this, but I'm not sure if this fix is in the 4.34.0 release.

Steps to Reproduce

Expected behavior: Just print the version number.

Actual behavior: lake traps at the end of its execution. Here are example runs for --version:

~ % uname -sr
Darwin 27.0.0

~ % elan run leanprover/lean4:v4.33.1 lake --version 
Lake version 5.0.0-src+819816b (Lean version 4.33.1)

~ % elan run leanprover/lean4:v4.34.0-rc1 lake --version
Lake version 5.0.0-src+3447a66 (Lean version 4.34.0-rc1)
lake(27657,0x7080013000) malloc: *** error for object 0x1155c6280: pointer being freed was not allocated
lake(27657,0x7080013000) malloc: *** set a breakpoint in malloc_error_break to debug
zsh: trace trap  elan run leanprover/lean4:v4.34.0-rc1 lake --version

~ % elan run leanprover/lean4:v4.34.0-rc2 lake --version
Lake version 5.0.0-src+6a10ac8 (Lean version 4.34.0-rc2)
lake(27670,0x7080013000) malloc: *** error for object 0x1137c2280: pointer being freed was not allocated
lake(27670,0x7080013000) malloc: *** set a breakpoint in malloc_error_break to debug
zsh: trace trap  elan run leanprover/lean4:v4.34.0-rc2 lake --version

~ % elan run nightly lake --version
Lake version 5.0.0-src (Lean version 4.35.0-nightly-2026-09-08)

Versions

Lean v4.34.0-rc2
macOS 27 (Golden Gate)

Impact

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

[TwoFX]

The 4.34 RC is still on mimalloc 3.4.1, which is known to have issues on macOS. This is likely to be resolved by (the backport of) #15060.

[johoelzl]

This is closed in Lean v4.34.0