error in the SciLean build

sciLean.txt

% git clone [email protected]:lecopivo/SciLean.git
Cloning into 'SciLean'...
remote: Enumerating objects: 21713, done.
remote: Counting objects: 100% (2158/2158), done.
remote: Compressing objects: 100% (861/861), done.
remote: Total 21713 (delta 1681), reused 1608 (delta 1267), pack-reused 19555 (from 3)
Receiving objects: 100% (21713/21713), 11.59 MiB | 5.75 MiB/s, done.
Resolving deltas: 100% (15628/15628), done.

ar@MacBook-Pro-14-2025 temp % cd SciLean

ar@MacBook-Pro-14-2025 SciLean % lake exe cache get
info: mathlib: cloning https://github.com/leanprover-community/mathlib4
info: mathlib: checking out revision 'df255e235cde3ac9e4325de51cfa2bc82b7b2416'
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision '8e5cb8d424df462f84997dd68af6f40e347c3e35'
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 'ed3b856bd8893ade75cafe13e8544d4c2660f377'
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 'a4a08d92be3de00def5298059bf707c72dfd3c66'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision 'ad942fdf0b15c38bface6acbb01d63855a2519ac'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision 'f007bfe46ea8fb801ec907df9ab540054abcc5fd'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '0c8ea32a15a4f74143e4e1e107ba2c412adb90fd'
No files to download
Decompressing 5814 file(s)
Unpacked in 4406 ms
Completed successfully!

ar@MacBook-Pro-14-2025 SciLean % lake build
✖ [2663/2797] Building SciLean.Tactic.CompiledTactics
trace: .> LEAN_PATH=././.lake/packages/Cli/.lake/build/lib:././.lake/packages/batteries/.lake/build/lib:././.lake/packages/Qq/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/packages/proofwidgets/.lake/build/lib:././.lake/packages/importGraph/.lake/build/lib:././.lake/packages/LeanSearchClient/.lake/build/lib:././.lake/packages/plausible/.lake/build/lib:././.lake/packages/mathlib/.lake/build/lib:././.lake/build/lib DYLD_LIBRARY_PATH=././.lake/packages/mathlib/.lake/build/lib:././.lake/packages/batteries/.lake/build/lib:././.lake/packages/Qq/.lake/build/lib:././.lake/build/lib:././.lake/packages/aesop/.lake/build/lib /Users/ar/.elan/toolchains/leanprover--lean4---v4.15.0-rc1/bin/lean ././././SciLean/Tactic/CompiledTactics.lean -R ./././. -o ././.lake/build/lib/SciLean/Tactic/CompiledTactics.olean -i ././.lake/build/lib/SciLean/Tactic/CompiledTactics.ilean -c ././.lake/build/ir/SciLean/Tactic/CompiledTactics.c --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Linter-Header-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Linter-DocPrime-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Linter-GlobalAttributeIn-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Linter-HashCommandLinter-1.dylib --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Lint-Basic-1.dylib --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Lint-Misc-1.dylib --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-OpenPrivate-1.dylib --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Util-LibraryNote-1.dylib --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Lint-Simp-1.dylib --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Lint-TypeClass-1.dylib --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Lint-Frontend-1.dylib --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Lint-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-DeclarationNames-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Linter-Lint-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Linter-Multigoal-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Linter-OldObtain-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Linter-RefineLinter-1.dylib --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Unreachable-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Linter-UnusedTactic-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Linter-Style-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Init-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-FunProp-Decl-1.dylib --load-dynlib=././.lake/packages/Qq/.lake/build/lib/libQq-ForLean-ReduceEval-1.dylib --load-dynlib=././.lake/packages/Qq/.lake/build/lib/libQq-ForLean-ToExpr-1.dylib --load-dynlib=././.lake/packages/Qq/.lake/build/lib/libQq-Typ-1.dylib --load-dynlib=././.lake/packages/Qq/.lake/build/lib/libQq-Macro-1.dylib --load-dynlib=././.lake/packages/Qq/.lake/build/lib/libQq-Delab-1.dylib --load-dynlib=././.lake/packages/Qq/.lake/build/lib/libQq-MetaM-1.dylib --load-dynlib=././.lake/packages/Qq/.lake/build/lib/libQq-ForLean-Do-1.dylib --load-dynlib=././.lake/packages/Qq/.lake/build/lib/libQq-SortLocalDecls-1.dylib --load-dynlib=././.lake/packages/Qq/.lake/build/lib/libQq-Match-1.dylib --load-dynlib=././.lake/packages/Qq/.lake/build/lib/libQq-AssertInstancesCommute-1.dylib --load-dynlib=././.lake/packages/Qq/.lake/build/lib/libQq-1.dylib --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Util-ExtendedBinder-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Data-Set-Defs-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Attr-Register-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-PPWithUniv-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-ExtendDoc-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Lemma-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-TypeStar-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Basic-1.dylib --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-CodeAction-Attr-1.dylib --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-CodeAction-Basic-1.dylib --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-CodeAction-Deprecated-1.dylib --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Alias-1.dylib --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Logic-1.dylib --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Trans-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Data-Nat-Notation-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Data-Int-Notation-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Logic-Basic-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Logic-ExistsUnique-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-AdaptationNote-1.dylib --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-NameMapAttribute-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Eqns-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Logic-Function-Defs-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Logic-Nonempty-1.dylib --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Init-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Lean-Expr-Basic-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Core-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-SplitIfs-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Order-Defs-PartialOrder-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Order-Defs-Unbundled-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Logic-Function-Basic-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Util-CompileInductive-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Simps-NotationClass-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Data-FunLike-Basic-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-FunProp-ToBatteries-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-FunProp-Mor-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-FunProp-FunctionData-1.dylib --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-SeqFocus-1.dylib --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Classes-Order-1.dylib --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Control-ForInStep-Basic-1.dylib --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-RBMap-Basic-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-FunProp-Types-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Data-Nat-BinaryRec-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Data-String-Defs-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Data-Array-Defs-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Util-MemoFix-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Lean-Expr-ReplaceRec-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Lean-EnvExtension-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Lean-Meta-Simp-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Lean-Name-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Simps-Basic-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-ToAdditive-Frontend-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-ToAdditive-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Algebra-Group-ZeroOne-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Util-AssertExistsExt-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Util-AssertExists-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Algebra-Group-Operations-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-OfNat-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Algebra-Group-Defs-1.dylib --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Position-1.dylib --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-CodeAction-Misc-1.dylib --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-CodeAction-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Lean-Meta-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-MkIffOfInductiveProp-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Data-Sum-Basic-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Logic-Relator-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Logic-IsEmpty-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Inhabit-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Logic-Unique-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Spread-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Algebra-Group-Pi-Basic-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Lean-Meta-RefinedDiscrTree-Pi-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Lean-Meta-RefinedDiscrTree-Basic-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-FunProp-StateList-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Lean-Meta-RefinedDiscrTree-Encode-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Lean-Meta-RefinedDiscrTree-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Lean-Meta-RefinedDiscrTree-Lookup-1.dylib --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-RBMap-WF-1.dylib --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-RBMap-Alter-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-FunProp-Theorems-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-FunProp-Attr-1.dylib --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Exact-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-FunProp-Core-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-FunProp-Elab-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-FunProp-1.dylib --load-dynlib=././.lake/build/lib/libSciLean-Tactic-FunTrans-Decl-1.dylib --load-dynlib=././.lake/build/lib/libSciLean-Util-SorryProof-1.dylib --load-dynlib=././.lake/build/lib/libSciLean-Lean-Array-1.dylib --load-dynlib=././.lake/build/lib/libSciLean-Tactic-FunTrans-Theorems-1.dylib --load-dynlib=././.lake/build/lib/libSciLean-Tactic-FunTrans-Types-1.dylib --load-dynlib=././.lake/build/lib/libSciLean-Tactic-FunTrans-Core-1.dylib --load-dynlib=././.lake/build/lib/libSciLean-Tactic-FunTrans-Elab-1.dylib --load-dynlib=././.lake/build/lib/libSciLean-Tactic-FunTrans-Attr-1.dylib --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Nanos-1.dylib --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Index-DiscrTreeConfig-1.dylib --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-Array-Merge-1.dylib --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Util-UnorderedArraySet-1.dylib --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Expr-1.dylib --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-String-Basic-1.dylib --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Util-Basic-1.dylib --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-List-Init-Lemmas-1.dylib --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-List-Basic-1.dylib --load-dynlib=././.lake/packages/mathlib/.lake/build/lib/libMathlib-Lean-Expr-1.dylib --load-dynlib=././.lake/build/lib/libSciLean-Lean-Expr-1.dylib --load-dynlib=././.lake/build/lib/libSciLean-Lean-Meta-Basic-1.dylib --load-dynlib=././.lake/build/lib/libSciLean-Tactic-GTrans-MetaLCtxM-1.dylib --load-dynlib=././.lake/build/lib/libSciLean-Tactic-LSimp-Types-1.dylib --load-dynlib=././.lake/build/lib/libSciLean-Tactic-LSimp-Main-1.dylib --json
info: stderr:
libc++abi: terminating due to uncaught exception of type lean::exception: error loading library, dlopen(././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Linter-Header-1.dylib, 0x0009): tried: '././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Linter-Header-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), '././.lake/packages/batteries/.lake/build/lib/libMathlib-Tactic-Linter-Header-1.dylib' (no such file), '././.lake/packages/Qq/.lake/build/lib/libMathlib-Tactic-Linter-Header-1.dylib' (no such file), '././.lake/build/lib/libMathlib-Tactic-Linter-Header-1.dylib' (no such file), '././.lake/packages/aesop/.lake/build/lib/libMathlib-Tactic-Linter-Header-1.dylib' (no such file), '././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Linter-Header-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), '/System/Volumes/Preboot/Cryptexes/OS././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Linter-Header-1.dylib' (no such file), '/Users/ar/.elan/toolchains/leanprover--lean4---v4.15.0-rc1/lib/././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Linter-Header-1.dylib' (no such file), '/Users/ar/.elan/toolchains/leanprover--lean4---v4.15.0-rc1/lib/lean/././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Linter-Header-1.dylib' (no such file), '/usr/lib/././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Linter-Header-1.dylib' (no such file, not in dyld cache), '././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Linter-Header-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), '././.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Linter-Header-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), '././.lake/packages/batteries/.lake/build/lib/libMathlib-Tactic-Linter-Header-1.dylib' (no such file), '././.lake/packages/Qq/.lake/build/lib/libMathlib-Tactic-Linter-Header-1.dylib' (no such file), '././.lake/build/lib/libMathlib-Tactic-Linter-Header-1.dylib' (no such file), '././.lake/packages/aesop/.lake/build/lib/libMathlib-Tactic-Linter-Header-1.dylib' (no such file), '/Users/ar/r/temp/SciLean/.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Linter-Header-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), '/System/Volumes/Preboot/Cryptexes/OS/Users/ar/r/temp/SciLean/.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Linter-Header-1.dylib' (no such file), '/Users/ar/r/temp/SciLean/.lake/packages/mathlib/.lake/build/lib/libMathlib-Tactic-Linter-Header-1.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag)
error: Lean exited with code 134
Some required builds logged failures:
- SciLean.Tactic.CompiledTactics
error: build failed

ar@MacBook-Pro-14-2025 SciLean % uname -a
Darwin MacBook-Pro-14-2025.local 24.4.0 Darwin Kernel Version 24.4.0: Wed Mar 19 21:11:02 PDT 2025; root:xnu-11417.101.15~1/RELEASE_ARM64_T8132 arm64
ar@MacBook-Pro-14-2025 SciLean %