Lake now comes with Lean

Stream: lean4

[Mac]

I am happy to announce that the latest Lean 4 nightly 10-16 now ships with lake! :celebration:

$ elan which lake
C:\Users\Mac\.elan\toolchains\leanprover--lean4---nightly\bin\lake.exe
$ lake --version
Lake version 3.0.0-pre (Lean version 4.0.0-nightly-2021-10-16)

[Xubai Wang]

When running lake on Windows MSYS2, a bunch of errors arise during the link process, even with the simplest lake new template.

$ lake build
> LEAN_PATH=.\build\lib c:\Users\xubaiw\.elan\toolchains\leanprover--lean4---nightly-2021-10-16\bin\lean -R .\. -o .\build\lib\Foo.olean -c .\build\ir\Foo.c .\.\Foo.lean
> c:\Users\xubaiw\.elan\toolchains\leanprover--lean4---nightly-2021-10-16\bin\leanc -c -o .\build\ir\Foo.o .\build\ir\Foo.c -O3 -DNDEBUG -lstdc++
> LEAN_PATH=.\build\lib c:\Users\xubaiw\.elan\toolchains\leanprover--lean4---nightly-2021-10-16\bin\lean -R .\. -o .\build\lib\Main.olean -c .\build\ir\Main.c .\.\Main.lean
> c:\Users\xubaiw\.elan\toolchains\leanprover--lean4---nightly-2021-10-16\bin\leanc -c -o .\build\ir\Main.o .\build\ir\Main.c -O3 -DNDEBUG -lstdc++
> c:\Users\xubaiw\.elan\toolchains\leanprover--lean4---nightly-2021-10-16\bin\leanc -o .\build\bin\foo.exe .\build\ir\Foo.o .\build\ir\Main.o -lstdc++
/usr/lib/gcc/x86_64-pc-msys/10.2.0/../../../../x86_64-pc-msys/bin/ld: c:\Users\xubaiw\.elan\toolchains\leanprover--lean4---nightly-2021-10-16\lib\lean/libleanrt.a(object.cpp.obj):object.cpp:(.text+0x105): undefined reference to `std::basic_ostream<char, std::char_traits<char> >& std::__ostream_insert<char, std::char_traits<char> >(std::basic_ostream<char, std::char_traits<char> >&, char const*, long long)'
/usr/lib/gcc/x86_64-pc-msys/10.2.0/../../../../x86_64-pc-msys/bin/ld: c:\Users\xubaiw\.elan\toolchains\leanprover--lean4---nightly-2021-10-16\lib\lean/libleanrt.a(object.cpp.obj):object.cpp:(.text+0x11a): undefined reference to `std::basic_ostream<char, std::char_traits<char> >& std::__ostream_insert<char, std::char_traits<char> >(std::basic_ostream<char, std::char_traits<char> >&, char const*, long long)'
/usr/lib/gcc/x86_64-pc-msys/10.2.0/../../../../x86_64-pc-msys/bin/ld: c:\Users\xubaiw\.elan\toolchains\leanprover--lean4---nightly-2021-10-16\lib\lean/libleanrt.a(object.cpp.obj):object.cpp:(.text+0xe57): undefined reference to `operator new[](unsigned long long)'
# many more

But as both lean --run and g++ works correctly on this machine, I'm assuming Lean and c compilers are installed correctly.
Do we need some special configurations on MSYS2?

[Xubai Wang]

Since most of the errors are like undefined reference to operator new, it's very likely the problem arises from libc++, but adding -lstdc++ flag to moreLinkArgs doesn't work.

[Sebastian Ullrich]

Does/did it work with leanpkg before?

[Scott Morrison]

I've noticed previously that the build instructions given in the manual don't actually install stdc++ on some systems (e.g. a bare ubuntu machine), and you need to also apt-get install -y libstdc++-9-dev in order to run the full test suite and/or do some things with Lake.

[Xubai Wang]

Sebastian Ullrich said:

Does/did it work with leanpkg before?

Both leanpkg and leanmake fails due to the same reason, so it must be a problem of leanc.

[Xubai Wang]

Scott Morrison said:

I've noticed previously that the build instructions given in the manual don't actually install stdc++ on some systems (e.g. a bare ubuntu machine), and you need to also apt-get install -y libstdc++-9-dev in order to run the full test suite and/or do some things with Lake.

I'll try it.
Lean 4 manual doesn't mention which compiler to use, so I just use pacman -S msys/gcc.

[Scott Morrison]

@Mac, I've updated mathlib4 to use Lake on mathlib4#74.

However it's a bit annoying that we have to type lake build :oleans, rather than just lake build. mathlib4 doesn't have a main executable, and probably never will! Is there something we can do to ameliorate this, ideally in Lake, otherwise in mathlib4s lakefile?

[Scott Morrison]

@Xubai Wang, are you looking at https://leanprover.github.io/lean4/doc/make/index.html? It has instructions for building from source on windows, and gives advice on compilers.

[Scott Morrison]

Also, @Mac, to run the tests in mathlib4 I'm just using env LEAN_PATH=build/lib lean test/$*. Could you show me the lake way to do this?

[Xubai Wang]

Scott Morrison said:

Xubai Wang, are you looking at https://leanprover.github.io/lean4/doc/make/index.html? It has instructions for building from source on windows, and gives advice on compilers.

Thanks! It works now.

[Mac]

Scott Morrison said:

Mac, I've updated mathlib4 to use Lake on mathlib4#74.

However it's a bit annoying that we have to type lake build :oleans, rather than just lake build. mathlib4 doesn't have a main executable, and probably never will! Is there something we can do to ameliorate this, ideally in Lake, otherwise in mathlib4s lakefile?

Yes, you can set defaultFacet in your lakefile.lean to defaultFacet := PackageFacet.oleans.

I am also hoping to make Lake have smarter defaults in the future by making the bin target an optional configuration.

[Scott Morrison]

Thanks, I've added this setting to the mathlib4 PR: https://github.com/leanprover-community/mathlib4/pull/74.