getting Lean4 working on macOS 12

Stream: new members

[Scott Buckley]

EDIT: I changed the title of this, as I now understand that it's about the OS version of my older macbook.

Sadly I broke the screen on my laptop, so I'm trying to get Lean set up on my wife's older i386 macbook pro.

Installation via the VSCode plugin got most of the way before falling over. I restarted a few times with elan self uninstall to no avail.

I tried setting up a new project via lake +v4.24.0 new my_project math as described here. Strangely, I think I got some different errors when this happened before, but the errors I get now are as below:

sjhb@PngTrs-MacBook-Pro againnn % lake +v4.24.0 new asd math
info: downloading mathlib `lean-toolchain` file
info: asd: no previous manifest, creating one from scratch
info: leanprover-community/mathlib: cloning https://github.com/leanprover-community/mathlib4
info: leanprover-community/mathlib: checking out revision '85fcdf8c425a12ae29526498ab5f9601c1f2dc5b'
info: toolchain not updated; already up-to-date
error: /Users/sjhb/repos/againnn/asd/.lake/packages/mathlib/lakefile.lean:139:5: Invalid field `baseName`: The environment does not contain `Lake.Package.baseName`
  rootPkg
has type
  Package
error: /Users/sjhb/repos/againnn/asd/.lake/packages/mathlib/lakefile.lean:139:24: Invalid field `baseName`: The environment does not contain `Lake.NPackage.baseName`
  pkg
has type
  NPackage _package.name
error: /Users/sjhb/repos/againnn/asd/.lake/packages/mathlib/lakefile.lean:145:34: Invalid field `trimAscii`: The environment does not contain `String.trimAscii`
  toolchainContent
has type
  String
error: /Users/sjhb/repos/againnn/asd/.lake/packages/mathlib/lakefile.lean:166:16: Invalid field `baseName`: The environment does not contain `Lake.NPackage.baseName`
  pkg
has type
  NPackage _package.name
error: /Users/sjhb/repos/againnn/asd/.lake/packages/mathlib/lakefile.lean:147:13: Invalid field `trimAscii`: The environment does not contain `String.trimAscii`
  toolchainContent
has type
  String
error: /Users/sjhb/repos/againnn/asd/.lake/packages/mathlib/lakefile.lean:149:29: Invalid field notation: Type of
  toolchainVersion
is not known; cannot resolve field `dropPrefix`
error: /Users/sjhb/repos/againnn/asd/.lake/packages/mathlib/lakefile.lean: package configuration has errors

If I build from VSCode, I get these errors (which is what i was getting in the terminal before - not sure what changed).

/Users/sjhb/repos/meowmeow2> lake +leanprover/lean4:stable build
✔ [2/8] Built Meowmeow2.Basic (2.0s)
✔ [3/8] Built Meowmeow2 (509ms)
✔ [4/8] Built Main (734ms)
✖ [5/8] Building Meowmeow2.Basic:c.o (3.4s)
trace: .> /Users/sjhb/.elan/toolchains/leanprover--lean4---v4.27.0/bin/clang -c -o /Users/sjhb/repos/meowmeow2/.lake/build/ir/Meowmeow2/Basic.c.o.export /Users/sjhb/repos/meowmeow2/.lake/build/ir/Meowmeow2/Basic.c -I /Users/sjhb/.elan/toolchains/leanprover--lean4---v4.27.0/include -fstack-clash-protection -fwrapv -fvisibility=hidden -Wno-unused-command-line-argument --sysroot /Users/sjhb/.elan/toolchains/leanprover--lean4---v4.27.0 -nostdinc -isystem /Users/sjhb/.elan/toolchains/leanprover--lean4---v4.27.0/include/clang -O3 -DNDEBUG -DLEAN_EXPORTING
info: stderr:
dyld[31484]: Symbol not found: (__ZNSt3__122__libcpp_verbose_abortEPKcz)
  Referenced from: '/Users/sjhb/.elan/toolchains/leanprover--lean4---v4.27.0/bin/clang'
  Expected in: '/usr/lib/libc++.1.dylib'
error: external command '/Users/sjhb/.elan/toolchains/leanprover--lean4---v4.27.0/bin/clang' exited with code 134
✖ [6/8] Building Main:c.o (2.2s)
trace: .> /Users/sjhb/.elan/toolchains/leanprover--lean4---v4.27.0/bin/clang -c -o /Users/sjhb/repos/meowmeow2/.lake/build/ir/Main.c.o.export /Users/sjhb/repos/meowmeow2/.lake/build/ir/Main.c -I /Users/sjhb/.elan/toolchains/leanprover--lean4---v4.27.0/include -fstack-clash-protection -fwrapv -fvisibility=hidden -Wno-unused-command-line-argument --sysroot /Users/sjhb/.elan/toolchains/leanprover--lean4---v4.27.0 -nostdinc -isystem /Users/sjhb/.elan/toolchains/leanprover--lean4---v4.27.0/include/clang -O3 -DNDEBUG -DLEAN_EXPORTING
info: stderr:
dyld[31492]: Symbol not found: (__ZNSt3__122__libcpp_verbose_abortEPKcz)
  Referenced from: '/Users/sjhb/.elan/toolchains/leanprover--lean4---v4.27.0/bin/clang'
  Expected in: '/usr/lib/libc++.1.dylib'
error: external command '/Users/sjhb/.elan/toolchains/leanprover--lean4---v4.27.0/bin/clang' exited with code 134
✖ [7/8] Building Meowmeow2:c.o (3.0s)
trace: .> /Users/sjhb/.elan/toolchains/leanprover--lean4---v4.27.0/bin/clang -c -o /Users/sjhb/repos/meowmeow2/.lake/build/ir/Meowmeow2.c.o.export /Users/sjhb/repos/meowmeow2/.lake/build/ir/Meowmeow2.c -I /Users/sjhb/.elan/toolchains/leanprover--lean4---v4.27.0/include -fstack-clash-protection -fwrapv -fvisibility=hidden -Wno-unused-command-line-argument --sysroot /Users/sjhb/.elan/toolchains/leanprover--lean4---v4.27.0 -nostdinc -isystem /Users/sjhb/.elan/toolchains/leanprover--lean4---v4.27.0/include/clang -O3 -DNDEBUG -DLEAN_EXPORTING
info: stderr:
dyld[31486]: Symbol not found: (__ZNSt3__122__libcpp_verbose_abortEPKcz)
  Referenced from: '/Users/sjhb/.elan/toolchains/leanprover--lean4---v4.27.0/bin/clang'
  Expected in: '/usr/lib/libc++.1.dylib'
error: external command '/Users/sjhb/.elan/toolchains/leanprover--lean4---v4.27.0/bin/clang' exited with code 134
Some required targets logged failures:
- Meowmeow2.Basic:c.o
- Main:c.o
- Meowmeow2:c.o
error: build failed
=> Operation failed. Exit code: 1.

Any ideas for how to resolve this?

[Ruben Van de Velde]

Hold on, in your first snippet you're asking for lean 4.24, but in the second you're overriding that and asking for stable (which is 4.27). How did that happen?

[Ruben Van de Velde]

The revision of mathlib you seem to have been downloading in the first snippet only works with v4.28.0-rc1, but the second snippet seems to insist on using stable = v4.27.0, so that might be an issue. But it doesn't seem like the second snippet is using mathlib at all

[Scott Buckley]

Yeah, sorry, right now I'm trying to just get anything working at all, and once I can do that I will work on mathlib. I guess the advice from the documentation is now out of date.

Yeah in vscode I tried setting up a project without mathlib but it still fails. Any advice on which docs I should follow to try to get this working?

[James E Hanson]

I get the same errors when I run lake +v4.24.0 new my_project math, but I know my lake installation works.

If you just run the following in terminal, what happens?

lake new my_project
cd my_project
lake build

[Scott Buckley]

@James E Hanson Just tried this, I get the same errors as usual:

sjhb@PngTrs-MacBook-Pro repos % lake new simp_proj123
sjhb@PngTrs-MacBook-Pro repos % cd simp_proj123
sjhb@PngTrs-MacBook-Pro simp_proj123 % lake build
info: simp_proj123: no previous manifest, creating one from scratch
info: toolchain not updated; already up-to-date
✖ [3/8] Building SimpProj123.Basic:c.o
trace: .> /Users/sjhb/.elan/toolchains/leanprover--lean4---v4.27.0/bin/clang -c -o /Users/sjhb/repos/simp_proj123/.lake/build/ir/SimpProj123/Basic.c.o.export /Users/sjhb/repos/simp_proj123/.lake/build/ir/SimpProj123/Basic.c -I /Users/sjhb/.elan/toolchains/leanprover--lean4---v4.27.0/include -fstack-clash-protection -fwrapv -fvisibility=hidden -Wno-unused-command-line-argument --sysroot /Users/sjhb/.elan/toolchains/leanprover--lean4---v4.27.0 -nostdinc -isystem /Users/sjhb/.elan/toolchains/leanprover--lean4---v4.27.0/include/clang -O3 -DNDEBUG -DLEAN_EXPORTING
info: stderr:
dyld[95691]: Symbol not found: (__ZNSt3__122__libcpp_verbose_abortEPKcz)
  Referenced from: '/Users/sjhb/.elan/toolchains/leanprover--lean4---v4.27.0/bin/clang'
  Expected in: '/usr/lib/libc++.1.dylib'
error: external command '/Users/sjhb/.elan/toolchains/leanprover--lean4---v4.27.0/bin/clang' exited with code 134
✖ [5/8] Building SimpProj123:c.o
trace: .> /Users/sjhb/.elan/toolchains/leanprover--lean4---v4.27.0/bin/clang -c -o /Users/sjhb/repos/simp_proj123/.lake/build/ir/SimpProj123.c.o.export /Users/sjhb/repos/simp_proj123/.lake/build/ir/SimpProj123.c -I /Users/sjhb/.elan/toolchains/leanprover--lean4---v4.27.0/include -fstack-clash-protection -fwrapv -fvisibility=hidden -Wno-unused-command-line-argument --sysroot /Users/sjhb/.elan/toolchains/leanprover--lean4---v4.27.0 -nostdinc -isystem /Users/sjhb/.elan/toolchains/leanprover--lean4---v4.27.0/include/clang -O3 -DNDEBUG -DLEAN_EXPORTING
info: stderr:
dyld[95733]: Symbol not found: (__ZNSt3__122__libcpp_verbose_abortEPKcz)
  Referenced from: '/Users/sjhb/.elan/toolchains/leanprover--lean4---v4.27.0/bin/clang'
  Expected in: '/usr/lib/libc++.1.dylib'
error: external command '/Users/sjhb/.elan/toolchains/leanprover--lean4---v4.27.0/bin/clang' exited with code 134
✖ [7/8] Building Main:c.o
trace: .> /Users/sjhb/.elan/toolchains/leanprover--lean4---v4.27.0/bin/clang -c -o /Users/sjhb/repos/simp_proj123/.lake/build/ir/Main.c.o.export /Users/sjhb/repos/simp_proj123/.lake/build/ir/Main.c -I /Users/sjhb/.elan/toolchains/leanprover--lean4---v4.27.0/include -fstack-clash-protection -fwrapv -fvisibility=hidden -Wno-unused-command-line-argument --sysroot /Users/sjhb/.elan/toolchains/leanprover--lean4---v4.27.0 -nostdinc -isystem /Users/sjhb/.elan/toolchains/leanprover--lean4---v4.27.0/include/clang -O3 -DNDEBUG -DLEAN_EXPORTING
info: stderr:
dyld[95774]: Symbol not found: (__ZNSt3__122__libcpp_verbose_abortEPKcz)
  Referenced from: '/Users/sjhb/.elan/toolchains/leanprover--lean4---v4.27.0/bin/clang'
  Expected in: '/usr/lib/libc++.1.dylib'
error: external command '/Users/sjhb/.elan/toolchains/leanprover--lean4---v4.27.0/bin/clang' exited with code 134
Some required targets logged failures:
- SimpProj123.Basic:c.o
- SimpProj123:c.o
- Main:c.o
error: build failed

right now i'm installing gcc to see if i can get it working that way - feels like it could be a clang problem. Any other ideas?

[Scott Buckley]

ah, brew failed to install gcc as I am using osx 12, which is the newest version this hardware supports but too old for brew etc. I'm guessing this is the key issue. I may have to try installing some older version of Lean then?

[Scott Buckley]

Ok, I think I've confirmed that this is just about the OS version (and i've updated the title to indicate this). Sadly I can't update this hardware to any newer OS version. Does anybody have any tips on how I might install any working version of lean (ideally lean4 but lean3 if needs be) and mathlib on MacOS 12?

[James E Hanson]

(deleted)

[James E Hanson]

(deleted)

[James E Hanson]

I guess you might have to try building a newer version of GCC or Clang from source if you don't have access to a package manager.

[Scott Buckley]

@James E Hanson yeah that may be the way forward, thanks for the suggestion. im trying macports too, which might get there eventually. although in the meantime, i found that i can use live.lean-lang.org, at least to play with the toy i'm playing with right now. that will get my by for the immediate at least.

this was a terrible time to damage my laptop though; im flying to vietnam in a few days, usually i'd have my laptop with me for trips like this.

[Scott Buckley]

Well, for posterity, I eventually got it working.

I was trying to get a newer c++ compiler, but I wasn't able to build llvm via brew, but I was able to install mp-clang-20 via macPorts, then I selected it using clang_select, and I was able to build a project, including with mathlib, using the following:

LEAN_CC=/opt/local/bin/clang lake new my_proj_math math
cd my_proj_math
LEAN_CC=/opt/local/bin/clang lake build

I'm sure there's a more elegant way to tell lake to use the newer version of clang, but this worked for me, and if I perform the above in the terminal before opening the project in vscode, i get proper interactive proofs in vscode (so far). I also got a number of warnings during compilation, but I'll take that for now.