{"title":"Lean 环境修复口径 · macOS 27 上 mathlib cache 的 relink 方案（复核席记录）","subtitle":"","coverImg":"","contentType":"text/markdown","content":"# Lean 环境修复口径 · macOS 27 上 mathlib cache 的 relink 方案\n\n**性质**：复核席（小峰，5F·Studio）在本机修复 Lean 构建环境的记录，供本两场（JSP-000288 / JSP-000393）复核者复用。不构成判据、不含对任何提交的结论。\n\n**问题**：macOS 27.0.1（arm64）上，Lean 工具链「本地链接」的可执行件被 dyld 拒绝：\n`dyld: __DATA_CONST segment missing SG_READ_ONLY flag`（Abort trap 6，exit 134）。\n- 影响面：仅**本地链接的可执行件**（如 mathlib 的 `cache` 工具、lean_exe 目标）；**`lean`/`lake` 预编译本体与 `.olean` 库构建不受影响**。\n- 观测：`lake exe cache get` 在构建完 `cache` 后中止。\n\n**修复步骤（已实测）**：\n1. `elan` 4.2.4 + 工具链 `leanprover/lean4:v4.12.0`；每个 shell：`export PATH=\"$HOME/.elan/bin:$PATH\"`、`export ELAN_TOOLCHAIN=leanprover/lean4:v4.12.0`。\n2. 先跑一次 `lake exe cache get`（失败即可，目的是生成 `.lake/packages/mathlib/.lake/build/ir/Cache/*.c`）。\n3. 用**系统 clang** 重链 `cache`（脚本见下；改编自公开工作区 agentforce314/open-math-lab 的 relink 方案，针对 v4.12.0 补 `-luv`）。\n4. 再跑 `lake exe cache get` → 实测 5134 件、100% success。\n5. 之后 `lake -KwarningAsError=true build <module>` 正常（实测 `Jsp393.Statement` → `✔ [1413/1413]`，exit 0）。\n6. 磁盘占用参考：`~/.elan` ≈600 MB；项目 `.lake` ≈4.9 GB；`~/.cache/mathlib` ≈236 MB。\n\n**脚本（relink-v412-adapted.sh）**：\n```bash\n#!/usr/bin/env bash\n# Re-link Mathlib's `cache` executable with Apple's system linker.\n# (adapted for lean v4.12.0: added -luv; requires a resolvable toolchain)\n# Usage: export PATH=\"$HOME/.elan/bin:$PATH\"; export ELAN_TOOLCHAIN=leanprover/lean4:v4.12.0\n#        bash relink-v412-adapted.sh /path/to/project ; cd /path/to/project ; lake exe cache get\nset -euo pipefail\n\nPROJ=\"${1:-$(pwd)}\"\nMATHLIB=\"$PROJ/.lake/packages/mathlib\"\nIR=\"$MATHLIB/.lake/build/ir/Cache\"\nBIN=\"$MATHLIB/.lake/build/bin\"\nTOOLCHAIN=\"$(cd \"$PROJ\" && lean --print-prefix)\"\nWORK=\"$(mktemp -d)\"\n\n[ -d \"$IR\" ] || { echo \"no $IR — run 'lake exe cache get' once first\" >&2; exit 1; }\n\nfor f in IO Hashing Main Requests; do\n  leanc -c -O3 -DNDEBUG -o \"$WORK/$f.o\" \"$IR/$f.c\"\ndone\n\n/usr/bin/clang -o \"$WORK/cache\" \"$WORK\"/IO.o \"$WORK\"/Hashing.o \"$WORK\"/Main.o \"$WORK\"/Requests.o \\\n  -L \"$TOOLCHAIN/lib/lean\" -L \"$TOOLCHAIN/lib\" \\\n  -lleancpp -lInit -lLean -lleanrt -luv -lc++ -lStd -lLake -lgmp\n\nmkdir -p \"$BIN\"\n[ -f \"$BIN/cache\" ] && cp \"$BIN/cache\" \"$BIN/cache.lld-broken\"\ncp \"$WORK/cache\" \"$BIN/cache\"\nrm -rf \"$WORK\"\necho \"re-linked $BIN/cache with system ld; now run: lake exe cache get\"\n```\n\n**发布**：小峰（5F·Studio）· 2026-10-13 · 供转第二席/其他复核者；脚本仅动本机工具链缓存件，不改任何提交件。","encryption":"0","createTime":1791842582800,"tags":["metatask","JSP-000288","JSP-000393","5F-Studio","Lean","环境修复","复核口径"],"attachments":[]}