new project setup fails

Stream: mathlib4

[Wouter Smeenk]

When I setup a new project using https://leanprover-community.github.io/install/project.html I get this error in VS code:

`/Users/wouterprivee/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/lake print-paths Init Mathlib.Topology.Basic` failed:

stderr:
info: [58/702] Building Std.Tactic.Lint.Basic
error: > LEAN_PATH=./lake-packages/proofwidgets/build/lib:./build/lib:./lake-packages/Cli/build/lib:./lake-packages/mathlib/build/lib:./lake-packages/Qq/build/lib:./lake-packages/aesop/build/lib:./lake-packages/std/build/lib DYLD_LIBRARY_PATH=./lake-packages/proofwidgets/build/lib:./build/lib:./lake-packages/Cli/build/lib:./lake-packages/mathlib/build/lib:./lake-packages/Qq/build/lib:./lake-packages/aesop/build/lib:./lake-packages/std/build/lib:./lake-packages/std/build/lib /Users/wouterprivee/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/lean -Dlinter.missingDocs=true -DwarningAsError=true ./lake-packages/std/././Std/Tactic/Lint/Basic.lean -R ./lake-packages/std/./. -o ./lake-packages/std/build/lib/Std/Tactic/Lint/Basic.olean -i ./lake-packages/std/build/lib/Std/Tactic/Lint/Basic.ilean -c ./lake-packages/std/build/ir/Std/Tactic/Lint/Basic.c
error: external command `/Users/wouterprivee/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/lean` exited with code 139

This is using on MacOS with M1 processor. Can someone help? I tried creating a new project because my old project which I tried updating has the same problem.

[Scott Morrison]

Can you try lake clean && lake exe cache get? I often get this from a broken olean file (e.g. from multiple processes writing the same file?),

[Scott Morrison]

If that doesn't work try again with lake clean && lake exe cache get!.

[Wouter Smeenk]

That does seem to work. Thanks!

I do get this:

ld64.lld: warning: directory not found for option -L/Applications/Xcode_14.2.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX13.1.sdk/usr/lib
ld64.lld: warning: /usr/lib/system/libsystem_kernel.dylib has version 13.4.0, which is newer than target minimum of 13.0.0
ld64.lld: warning: /usr/lib/system/libsystem_platform.dylib has version 13.4.0, which is newer than target minimum of 13.0.0
ld64.lld: warning: /usr/lib/system/libsystem_pthread.dylib has version 13.4.0, which is newer than target minimum of 13.0.0

[Antoine Chambert-Loir]

(i have similar error messages all the time…)

[Scott Morrison]

Me too. I've been suspecting that it's because I run a relatively old OS. (11.7.7 Big Sur!) I'm curious which macos version others who see this error are running.

[Matthew Ballard]

I’ve got them on Monterrey