new lake gives me way too much information

Stream: mathlib4

[Scott Morrison]

It's nice that the new lake gives some progress information, but I also get a huge pile of warning:

info: stderr:
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: /Users/scott/.elan/toolchains/leanprover--lean4---nightly-2023-04-20/lib/libgmp.a(lt2-add.o) has version 12.0.0, which is newer than target minimum of 11.0.0
ld64.lld: warning: /Users/scott/.elan/toolchains/leanprover--lean4---nightly-2023-04-20/lib/libgmp.a(add_n.o) has version 12.0.0, which is newer than target minimum of 11.0.0
ld64.lld: warning: /Users/scott/.elan/toolchains/leanprover--lean4---nightly-2023-04-20/lib/libgmp.a(sub_n.o) has version 12.0.0, which is newer than target minimum of 11.0.0
ld64.lld: warning: /Users/scott/.elan/toolchains/leanprover--lean4---nightly-2023-04-20/lib/libgmp.a(lt3-add_ui.o) has version 12.0.0, which is newer than target minimum of 11.0.0
...

(and many more). Anyone know what I should do to either fix or silence these?

[Gabriel Ebner]

At least for warnings from Lean, this was completely intentional. Otherwise you could completely miss them.

[Gabriel Ebner]

I'm not sure about the xcode thing, is this something we could properly fix?

[Sebastian Ullrich]

I don't know where the first one is coming from, some impurity in clang? If otherwise it is complaining about libgmp only (which we take from Homebrew)... easiest fix might be USE_GMP=OFF?

[Scott Morrison]

Why does it generate a warning about a version being greater than than the minimum? That seems excessively strict.

[Sebastian Ullrich]

It's basically saying "you told me to generate code compatible with macOS 11+ but you also gave me a library compatible with macOS 12+ only, that's kind of fishy"

[Scott Morrison]

I see. Is there a lakefile switch / environment variable / etc to tell it to target 12+?