Mathlib 4.15 build failure on macOS Tahoe (26.1)

Stream: general

[Kelly Davis]

Decided to upgrade macOS from Sequoia (15.7) to Tahoe (26.1).

Before the upgrade Mathlib 4.15 was able to compile fine on Sequoia (15.7). After the upgrade I am met with

.
.
.
+ pushd mathlib4

~/Code/KellyJDavis/kimina-lean-server/mathlib4 ~/Code/KellyJDavis/kimina-lean-server
+ git checkout v4.15.0

HEAD is now at 9837ca9 chore: bot validates lean-toolchain on bump/v4.X.0 branches (#20478)
+ '[' mathlib4 = mathlib4 ']'
+ lake exe cache get
**info:** plausible: cloning https://github.com/leanprover-community/plausible
**info:** plausible: checking out revision '2c57364ef83406ea86d0f78ce3e342079a2fece5'
**info:** LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
**info:** LeanSearchClient: checking out revision '003ff459cdd85de551f4dcf95cdfeefe10f20531'
**info:** importGraph: cloning https://github.com/leanprover-community/import-graph
**info:** importGraph: checking out revision '9a0b533c2fbd6195df067630be18e11e4349051c'
**info:** proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
**info:** proofwidgets: checking out revision '2b000e02d50394af68cfb4770a291113d94801b5'
**info:** aesop: cloning https://github.com/leanprover-community/aesop
**info:** aesop: checking out revision '2689851f387bb2cef351e6825fe94a56a304ca13'
**info:** Qq: cloning https://github.com/leanprover-community/quote4
**info:** Qq: checking out revision 'f0c584bcb14c5adfb53079781eeea75b26ebbd32'
**info:** batteries: cloning https://github.com/leanprover-community/batteries
**info:** batteries: checking out revision 'e8dc5fc16c625fc4fe08f42d625523275ddbbb4b'
**info:** Cli: cloning https://github.com/leanprover/lean4-cli
**info:** Cli: checking out revision '0c8ea32a15a4f74143e4e1e107ba2c412adb90fd'

dyld[47471]: __DATA_CONST segment missing SG_READ_ONLY flag in /Users/kdavis/Code/KellyJDavis/kimina-lean-server/mathlib4/.lake/build/bin/cache

dyld[47471]: __DATA_CONST segment missing SG_READ_ONLY flag

It seems that macOS has become more strict with respect to __DATA_CONST sections, expecting them to be (as the name would suggest) immutable and be marked as such with SG_READ_ONLY.

__DATA_CONST sections not marked as SG_READ_ONLY seem to be is a result of using LLVM/Clang but not always the Apple linker, for example using lld.

What I did to get around this is introduce a bash function

ensure_apple_ld() {
  if [[ "$(uname -s)" != "Darwin" ]]; then
    return
  fi

  APPLE_LD_PATH=""
  if command -v xcrun >/dev/null 2>&1; then
    APPLE_LD_PATH="$(xcrun --find ld 2>/dev/null || true)"
  fi
  APPLE_LD_PATH="${APPLE_LD_PATH:-/usr/bin/ld}"

  # Ensure the linker we expose is the Apple ld64 (not lld).
  if ! "$APPLE_LD_PATH" -v 2>&1 | grep -qi "apple"; then
    echo "ERROR: Expected Apple ld64, but found $(\"$APPLE_LD_PATH\" -v 2>&1 | head -n 1)" >&2
    echo "Please install Xcode command line tools (xcode-select --install) to get ld64." >&2
    exit 1
  fi

  # Prepend the Apple ld64 bin dir in case other setup steps override PATH (e.g., elan).
  export PATH="$(dirname "$APPLE_LD_PATH"):${PATH}"
  export LD="$APPLE_LD_PATH"
  export REAL_LD64="$APPLE_LD_PATH"
  echo "Using Apple ld64 at $APPLE_LD_PATH"
}

and called it at appropriate points in my build script.

In addition I removed calls to lake exe cache get to prevent downloading improperly linked files.

This seems to have worked, but could someone (the powers that be) re-link older, downloadable cached files with the Apple linker to prevent others from downloading them and facing this problem.

PS: I need to be on Lean 4.15 as I'm working with a ML model trained on 4.15; so, upgrading wasn't an option.

[Kevin Buzzard]

I can reproduce on my mac (also on Tahoe 26.1): git checkout v4.15.0 followed by lake exe cache get fails (with an error about RBMap), and lake clean then lake exe cache get fails again (with an error about __DATA_CONST). Checking out master puts everything back to normal.

[Kim Morrison]

If I hear the combination of:

• a second person needing v4.15.0
• and someone giving me a script that does everything needed, assuming I provide it with the cache upload key

then I could do it. :-) Otherwise it seems that just zipping up the oleans that work for you and moving them around might be the simpler solution.

[Kelly Davis]

So basically a WONTFIX.

What is the first version that starts to correctly use the Apple linker?

[Kelly Davis]

I created a script to test this and the first version, starting from 4.15, that works is 4.20.

The script is should be placed in the mathlib4 repo under scripts/find-cache-readonly-fix.sh and run as

bash scripts/find-cache-readonly-fix.sh

The script itself is

#!/usr/bin/env bash

# Find the first tag from v4.15.0 onward whose `lake exe cache get` does not
# fail with the "__DATA_CONST segment missing SG_READ_ONLY flag" error.
set -euo pipefail

REPO_ROOT="/Users/kdavis/Code/leanprover-community/mathlib4"
START_TAG="v4.15.0"
TARGET_ERROR="__DATA_CONST segment missing SG_READ_ONLY flag"

# Allow overriding the log directory; otherwise use a temporary one.
WORK_DIR="${WORK_DIR:-$(mktemp -d /tmp/mathlib-cache-check-XXXXXX)}"
mkdir -p "$WORK_DIR"

cd "$REPO_ROOT"

# Remember the starting ref so we can restore it on exit.
original_ref=$(git rev-parse --abbrev-ref HEAD)
if [[ "$original_ref" == "HEAD" ]]; then
  original_ref=$(git rev-parse HEAD)
fi
restore_original() {
  git checkout -f "$original_ref" >/dev/null 2>&1 || true
}
trap restore_original EXIT

echo "Logs will be written under: $WORK_DIR"

run_attempt() {
  local log_file="$1"
  if lake exe cache get &>"$log_file"; then
    if grep -q "$TARGET_ERROR" "$log_file"; then
      return 1   # command succeeded but printed the target error
    else
      return 0   # success and no target error
    fi
  else
    if grep -q "$TARGET_ERROR" "$log_file"; then
      return 1   # failure with the target error
    else
      return 2   # failure for another reason
    fi
  fi
}

started=0
first_good_tag=""
first_good_log=""
first_good_attempt=""

for tag in $(git tag -l 'v4.*' --sort=version:refname); do
  if [[ $started -eq 0 ]]; then
    [[ "$tag" == "$START_TAG" ]] || continue
    started=1
  fi

  echo "Checking $tag"
  git checkout --quiet "$tag"

  tag_dir="$WORK_DIR/$tag"
  mkdir -p "$tag_dir"
  first_log="$tag_dir/first.log"
  second_log="$tag_dir/second.log"

  if run_attempt "$first_log"; then
    first_good_tag="$tag"
    first_good_log="$first_log"
    first_good_attempt="first"
    break
  else
    status=$?
    if [[ $status -eq 1 ]]; then
      echo "  first attempt hit target error (see $first_log)"
    else
      echo "  first attempt failed for another reason (see $first_log)"
    fi
  fi

  lake clean

  if run_attempt "$second_log"; then
    first_good_tag="$tag"
    first_good_log="$second_log"
    first_good_attempt="after clean"
    break
  else
    status=$?
    if [[ $status -eq 1 ]]; then
      echo "  second attempt hit target error (see $second_log)"
    else
      echo "  second attempt failed for another reason (see $second_log)"
    fi
  fi
done

if [[ -n "$first_good_tag" ]]; then
  echo "First tag without the target error: $first_good_tag ($first_good_attempt run)"
  echo "Log: $first_good_log"
  exit 0
else
  echo "No tag from $START_TAG onward avoided the target error."
  exit 1
fi

[Kim Morrison]

@Kelly Davis, I think saying this is a "WONTFIX" is maybe overstating it. No one has ever suggested that they provide support for old versions of Mathlib.

I manage the releases of new versions of Lean, and coordinate making sure Mathlib works on each new stable release and release candidate. But anything older than that is a community project. (e.g. you! I can help get access to the keys.) We strongly recommend that people building AIs to interact with Lean work out how to adapt to new versions frequently.

But I'm also really confused by your diagnosis above. (I didn't read closely.) How can the linker used affect the oleans? Those are cross-platform. I think actually what you want is to rebuild Lean v4.15.0, this is not actually a request about Mathlib at all?

[Kelly Davis]

Kim Morrison said:

Kelly Davis, I think saying this is a "WONTFIX" is maybe overstating it. No one has ever suggested that they provide support for old versions of Mathlib.

I guess I read (and maybe misread) your statement as a slightly snarky way of saying "WONTFIX". Sorry if this isn't the case.

We strongly recommend that people building AIs to interact with Lean work out how to adapt to new versions frequently.

Given current technology I don't think this is a realistic expectation.

With the training times involved (e.g. 1-2 months) along with the cost of training (e.g. paying for 50-200 GPUs running full-time for 1-2 months), re-training a model for each Mathlib release is not something anyone can realistically be expected to do or would really want to do.

Myself, I'm working on a personal project using existing open pre-trained models which are "pinned" to particular Mathlib versions. So the cost and time to retrain is completely out of the question.

But I'm also really confused by your diagnosis above. (I didn't read closely.) How can the linker used affect the oleans? Those are cross-platform. I think actually what you want is to rebuild Lean v4.15.0, this is not actually a request about Mathlib at all?

I don't want to re-build Lean 4.15.

Since then, I've since gotten Mathlib4.15 and my REPL's[1][2] to work with a non-rebuilt Lean 4.15 on macOS 26.1, though it was a pain. (Initially I was researching how to rollback to macOS 15. It involves a full backup, disk wipe, and system reinstall :anguish: )

For example, my "solution" for the REPL's I landed on the hack of renaming the __DATA_CONST sections to __DATA, i.e. in lakefile.lean

...
@[default_target]
lean_exe «ast-export» where
  root := `Main
  -- Enables the use of the Lean interpreter by the executable (e.g.,
  -- `runFrontend`) at the expense of increased binary size on Linux.
  -- Remove this line if you do not need such functionality.
  supportInterpreter := true
  -- Fix for macOS 26.1 + Lean 4.15-4.19-rc3: rename __DATA_CONST segment to avoid
  -- "dyld: __DATA_CONST segment missing SG_READ_ONLY flag" error when linked with lld
  moreLinkArgs := #["-Wl,-rename_segment,__DATA_CONST,__DATA"]
...

These "fixes" are not yet in the GitHub repos I referenced.

For Mathlib4.15 I build it as part of a kimina-lean-server variant.

In particular the fixed setup script so that it

1. Uses the function ensure_apple_ld() I defined above to force use of the Apple linker
2. Doesn't call lake exe cache get for macOS to force a local build

Together these seem to work, i.e. if I don't do this I get the _DATA_CONST segment missing SG_READ_ONLY flag error occurring on

/Users/kdavis/Code/KellyJDavis/kimina-lean-server/mathlib4/.lake/build/bin/cache

which seems, as far as I can see, to be mathlib4 not Lean related.

Upon such a failure, running otool -l on the that cache file confirms what the failure indicates, the _DATA_CONST segment is missing a SG_READ_ONLY flag. So it seems to me to be mathlib4 not Lean related.

PS: I agree that oleans are platform agnostic, but something is afoot. You know far more about the toolchain than I do, or ever will. So maybe these hints help find the underlying problem.

PPS: Again whatever the underlying problem was, it went away in Mathlib 4.20 but was present from 4.15 until then, another hint.

[1] https://github.com/leanprover-community/repl
[2] https://github.com/KellyJDavis/ast_export

[Kevin Buzzard]

Kelly Davis said:

With the training times involved (e.g. 1-2 months) along with the cost of training (e.g. paying for 50-200 GPUs running full-time for 1-2 months), re-training a model for each Mathlib release is not something anyone can realistically be expected to do or would really want to do.

So we have a real disconnect here between "mathlib and lean aggressively move forwards, constantly adding new features (and theorems) and tweaking old ones, and currently make little attempt to be backwards compatible" and "it costs a huge amount of money for certain mathlb-using systems to keep up". I think that moving backwards is a solution which is obviously not acceptable (for example I am not even allowed to downgrade my mac from 26.1; it is owned by my employers and it's part of the (electronically enforced) contract that I am always on the latest OS; my mac literally stops working if I don't upgrade), so perhaps one needs to think more creatively about how to move forwards? At least once a month mathlib bumps the version of Lean which it's using and this often involves merging a PR whose diff hopefully contains all the information an LLM would need about how to go from vX to vX+1. Could one create a system which attempts to bump code depending on mathlib and written by a machine trained on mathlib from one stable version of Lean to the next? This sounds like an interesting problem and also perhaps a feasible one.

[Kelly Davis]

...my mac literally stops working if I don't upgrade...

Wow they don't play around!

Your idea seems feasible, but this only solves part of the problem.

Assuming it works, this would generate a "translator" LLM that could translate, say, the training data for a "prover" LLM model, which say targets version N, to new training data set which targets version N+1.

The "prover" model targeting version N would still be targeting version N and need to be retrained for version N+1.

For "small" deltas between version N and N+1 you might be able to get away with adding a "translator" LLM as a pre-processor and post-processor to a "prover" LLM.

However, at some point you're simply going to have to "bite-the-bullet" and retrain the "prover" LLM. For example, it wouldn't be aware of definitions, theorems, tactics.... in Mathlib4 version N+1 but not in Mathlib version N; so it wouldn't be able to suggest/use them in the proofs it generates.