Mac Sequoia 15.4 regression?

Stream: lean4

[Kevin Buzzard]

Over in #Lean for teaching > Issue with `Duper` in `The Mechanics of Proof` there is a conjecture that the following commands

git clone git@github.com:hrmacbeth/math2001.git
cd math2001
lake exe cache get
lake build Math2001.Homework.hw9

work fine on Mac OS Sequoia 15.3 (the file has sorrys in, that's the homework, but the build is error-free) but on Sequoia 15.4 (the version which I was just forcibly updated to because of my university's Ts and Cs) we get errors in the build (the gory output is in the thread and I'l post it again below). It also compiles fine on Ubuntu 24.04.

tl;dr: Heather's repo is broken on the newest macs :-/

[Kevin Buzzard]

Sequoia 15.4 errors:

[751/752] Building Math2001.Homework.hw9

error: > LEAN_PATH=./.lake/packages/std/.lake/build/lib:./.lake/packages/Qq/.lake/build/lib:./.lake/packages/aesop/.lake/build/lib:./.lake/packages/proofwidgets/.lake/build/lib:./.lake/packages/Cli/.lake/build/lib:./.lake/packages/mathlib/.lake/build/lib:./.lake/packages/Duper/.lake/build/lib:./.lake/packages/autograder/.lake/build/lib:./.lake/build/lib DYLD_LIBRARY_PATH=./.lake/packages/autograder/.lake/build/lib:./.lake/build/lib /Users/buzzard/.elan/toolchains/leanprover--lean4---v4.3.0/bin/lean -Dlinter.unusedVariables=false -DquotPrecheck=false -DwarningAsError=false -Dpp.unicode.fun=true ./././Math2001/Homework/hw9.lean -R ././. -o ./.lake/build/lib/Math2001/Homework/hw9.olean -i ./.lake/build/lib/Math2001/Homework/hw9.ilean -c ./.lake/build/ir/Math2001/Homework/hw9.c --load-dynlib=./.lake/packages/autograder/.lake/build/lib/libAutograderLib-1.dylib

error: stderr:

libc++abi: terminating due to uncaught exception of type lean::exception: error loading library, dlopen(./.lake/packages/autograder/.lake/build/lib/libAutograderLib-1.dylib, 0x0009): tried: './.lake/packages/autograder/.lake/build/lib/libAutograderLib-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), './.lake/build/lib/libAutograderLib-1.dylib' (no such file), './.lake/packages/autograder/.lake/build/lib/libAutograderLib-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), '/System/Volumes/Preboot/Cryptexes/OS./.lake/packages/autograder/.lake/build/lib/libAutograderLib-1.dylib' (no such file), '/Users/buzzard/.elan/toolchains/leanprover--lean4---v4.3.0/lib/./.lake/packages/autograder/.lake/build/lib/libAutograderLib-1.dylib' (no such file), '/Users/buzzard/.elan/toolchains/leanprover--lean4---v4.3.0/lib/lean/./.lake/packages/autograder/.lake/build/lib/libAutograderLib-1.dylib' (no such file), '/usr/lib/./.lake/packages/autograder/.lake/build/lib/libAutograderLib-1.dylib' (no such file, not in dyld cache), './.lake/packages/autograder/.lake/build/lib/libAutograderLib-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), './.lake/packages/autograder/.lake/build/lib/libAutograderLib-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), './.lake/build/lib/libAutograderLib-1.dylib' (no such file), '/Users/buzzard/crap/math2001/.lake/packages/autograder/.lake/build/lib/libAutograderLib-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), '/System/Volumes/Preboot/Cryptexes/OS/Users/buzzard/crap/math2001/.lake/packages/autograder/.lake/build/lib/libAutograderLib-1.dylib' (no such file), '/Users/buzzard/crap/math2001/.lake/packages/autograder/.lake/build/lib/libAutograderLib-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag)

error: external command /Users/buzzard/.elan/toolchains/leanprover--lean4---v4.3.0/bin/lean exited with code 134

[Jireh Loreaux]

on arch linux, that file builds for me, but lake build Math2001.«09_Sets».«02_Set_Operations» fails.
build_failure.txt

[Jireh Loreaux]

I suspect that this is due to some shared libraries being updated, especially because this repo is on the old 4.3.0.

[Jireh Loreaux]

It's been a while since I last updated arch, so I'll get the latest packages and see if the error changes (or changes locations), which I suspect it might. (EDIT: same error after updating all my packages.)

[Derek Rhodes]

Some more data points,
For mac, I upgraded to Sequoia 15.5
[err] $ lake build Math2001.Homework.hw9
[err] $ lake build Math2001.«09_Sets».«02_Set_Operations»
My debian stable box:
[ ok] $ lake build Math2001.Homework.hw9
[err] $ lake build Math2001.«09_Sets».«02_Set_Operations»

[Kevin Buzzard]

On Ubuntu 24.04 Math2001.Homework.hw9 is building for me and Math2001.«09_Sets».«02_Set_Operations» isn't (so same as Jireh's arch linux). On my 15.4 mac neither file builds; in the Set_Operations file I get an error building Duper.Order.

[Matthew Ballard]

leanprover--lean4---v4.3.0 is pretty old...

[Jireh Loreaux]

Do we think the issue is that the C libraries changed and so (an old version of) Lean's linking is borked? I don't know enough about low-level Lean to tell if I'm spewing nonsense here.

[Matthew Ballard]

That is my guess yes. When I would build lean itself, I often had things go haywire with compiling/linking after I upgraded the MacOS version.

You might be able to pass some environment variable to lake to point it at the right thing. This is something I did in the past. But the easiest fix was to nuke the repo and clone a new one.

[Matthew Ballard]

Not that I am saying nuking and restarting is a fix here.

[Matthew Ballard]

It looks like this flag was new in Feb 2024 and the toolchain dates from Nov 2023. So maybe getting it up to v4.7.0 (or even v4.6.0) would be enough to take care of this issue

[Kim Morrison]

I can't build main on my machine (other errors besides this) so couldn't help with version bumping.

[Kim Morrison]

The design of the cancel tactic, which uses a bunch of macro_rules, hoping for one to succeed, seems incompatible with some change that occurred in v4.4.0, as the errors from failed rules are now stopping the tactic, rather than just silently proceeding to the next rule.

[Derek Rhodes]

The cancel tactic is working now with v4.4.0, here's the diff

So, v4.4.0 builds with examples using the exhaust tactic commented out. Also the autograder attributes have been commented and the autograder and duper deps have been commented out in the lakefile.
https://github.com/drhodes/math2001/tree/v4.4.0

[Kim Morrison]

duper is available for v4.16.0, and lean4-autograder-main for v4.15.0, so hopefully these shouldn't be obstacles.

[Kim Morrison]

Are your fixes for cancel backwards compatible with the main branch (i.e. without bumping the toolchain)? Maybe best to make those first.

[Derek Rhodes]

Are your fixes for cancel backwards compatible with the main branch

Hi, no - the issue was that some theorem names living inside the cancel macro were changed in mathlib v4.4.0, which caused the breakage.

The macro uses a try combinator, which functions as a fallthrough trying different lemmas to close the goal, but also (a little surprising to me), from what I can tell, silently fails on the theorem name lookup and continues down to the fail case which has a more generic err message.

Though, I'll see how far I can get, I'd like to get this working up to v4.16.0.

[Derek Rhodes]

Oh, sorry, I misunderstood, just a second,
[fails] toolchain v4.3.0 / mathlib v4.4.0
[builds] toolchain v4.4.0 / mathlib v4.4.0

[Jannis Limperg]

This error (specifically: __DATA_CONST segment missing SG_READ_ONLY) also occurs on latest Lean nightly: lean4#7917

[Alok Singh]

Getting similar issue trying to build verso @David Thrane Christiansen

[Jeremy Lindsay]

Jannis Limperg said:

This error (specifically: __DATA_CONST segment missing SG_READ_ONLY) also occurs on latest Lean nightly: lean4#7917

I am also seeing __DATA_CONST segment missing SG_READ_ONLY flag when building MD4Lean.

[David Thrane Christiansen]

Thanks for the reports!

[Sebastian Ullrich]

lean#6063 has been resolved, testing using the next nightly welcome!

[Marcus Rossel]

I was also running into __DATA_CONST segment missing SG_READ_ONLY, which did work itself out by updating to nightly-2025-04-28. However, now I'm running into problems with external symbols not being found:

✖ [16/179] Building Egg.Core.Request.EGraph
trace: .> LEAN_PATH=/Users/marcus/Arbeit/lean-egg/.lake/packages/calcify/.lake/build/lib/lean:/Users/marcus/Arbeit/lean-egg/.lake/build/lib/lean /Users/marcus/.elan/toolchains/leanprover--lean4-nightly---nightly-2025-04-28/bin/lean /Users/marcus/Arbeit/lean-egg/Lean/Egg/Core/Request/EGraph.lean -R /Users/marcus/Arbeit/lean-egg/Lean -o /Users/marcus/Arbeit/lean-egg/.lake/build/lib/lean/Egg/Core/Request/EGraph.olean -i /Users/marcus/Arbeit/lean-egg/.lake/build/lib/lean/Egg/Core/Request/EGraph.ilean -c /Users/marcus/Arbeit/lean-egg/.lake/build/ir/Egg/Core/Request/EGraph.c --load-dynlib /Users/marcus/Arbeit/lean-egg/.lake/build/lib/libffi.dylib --load-dynlib /Users/marcus/Arbeit/lean-egg/.lake/build/lib/libegg_for_lean.dylib --load-dynlib /Users/marcus/Arbeit/lean-egg/.lake/build/lib/libslotted_for_lean.dylib --json
info: stderr:
libc++abi: terminating due to uncaught exception of type lean::exception: error loading library, dlopen(/Users/marcus/Arbeit/lean-egg/.lake/build/lib/libffi.dylib, 0x0009): symbol not found in flat namespace '_egg_free_egraph'
error: Lean exited with code 134

This used to just work in Lean v4.18.0 on macOS 15.3 (now I'm on 15.4). If I run nm on relevant files I get:

$ nm libffi.dylib
...
0000000000001120 T _egg_egraph_to_lean
                 U _egg_free_egraph
000000000000129c T _egraph_to_lean

$ nm libegg_for_lean.dylib
...
0000000000056978 T _egg_free_egraph

The libegg_for_lean.dylib (and the egg_free_egraph function) come from Rust, with libffi.dylib just declaring the function as extern.

Does this look more like user error, or should this continue to just work?

Lakefile for Reference

import Lake
open Lake DSL

require "nomeata" / "calcify" @ git "master"

-- Cf. https://github.com/lurk-lab/RustFFI.lean

package egg where
  srcDir := "Lean"
  -- See https://github.com/leanprover/lean4/tree/master/src/lake#github-release-builds
  preferReleaseBuild := true
  releaseRepo?       := none
  buildArchive?      := none

@[default_target]
lean_lib Egg where
  -- This enables the interpreter to run functions marked `@[extern]`.
  precompileModules := true

target importTarget pkg : System.FilePath :=
  pkg.afterBuildCacheAsync do
    let oFile := pkg.buildDir / "c" / "ffi.o"
    let srcJob ← inputTextFile <| pkg.dir / "C" / "ffi.c"
    buildFileAfterDep oFile srcJob fun srcFile => do
      let flags := #["-I", toString (← getLeanIncludeDir), "-fPIC"]
      compileO oFile srcFile flags

extern_lib ffi pkg := do
  let job ← fetch <| pkg.target ``importTarget
  let libFile := pkg.sharedLibDir / nameToStaticLib "ffi"
  buildStaticLib libFile #[job]

extern_lib egg_for_lean pkg := do
  pkg.afterBuildCacheAsync do
    let name      := nameToStaticLib "egg_for_lean"
    let srcPath   := pkg.dir / "Rust" / "Egg" / "target" / "release" / name
    let tgtPath   := pkg.sharedLibDir / name
    let traceFile := pkg.buildDir / "rust" / "egg.trace"
    let _ ← buildUnlessUpToDate? traceFile (← getTrace) traceFile do
      proc {
        cmd := "cargo",
        args := #["rustc", "--release", "--", "-C", "relocation-model=pic"],
        cwd := pkg.dir / "Rust" / "Egg"
      }
      IO.FS.createDirAll pkg.sharedLibDir
      IO.FS.writeBinFile tgtPath (← IO.FS.readBinFile srcPath)
    return pure tgtPath

extern_lib slotted_for_lean pkg := do
  pkg.afterBuildCacheAsync do
    let name := nameToStaticLib "slotted_for_lean"
    let srcPath := pkg.dir / "Rust" / "Slotted" / "target" / "release" / name
    let tgtPath := pkg.sharedLibDir / name
    let traceFile := pkg.buildDir / "rust" / "slotted.trace"
    let _ ← buildUnlessUpToDate? traceFile (← getTrace) traceFile do
      proc {
        cmd := "cargo",
        args := #["rustc", "--release", "--", "-C", "relocation-model=pic"],
        cwd := pkg.dir / "Rust" / "Slotted"
      }
      IO.FS.createDirAll pkg.sharedLibDir
      IO.FS.writeBinFile tgtPath (← IO.FS.readBinFile srcPath)
    return pure tgtPath

[Sebastian Ullrich]

It sounds like your libffi.dylib should be linking against libegg_for_lean.dylib if it uses its symbols

[Marcus Rossel]

@Sebastian Ullrich That is, update the extern_lib ffi declaration in the lakefile in some fashion?

[Marcus Rossel]

And do you have an idea of how this could have worked before, but now stopped working?

[Marcus Rossel]

Ah, it seems this is also being discussed (and fixed) in https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Multiple.20extern_lib