Building Lean 4

Stream: general

[Edward Ayers]

I thought I'd just write my experience building Lean 4 from source here. I did this on a mac.

There will probably be errors and I want to say that "we are not ready to help you build lean 4" is a completely reasonable answer to any problems I have.

git clone https://github.com/leanprover/lean4
cd lean
mkdir -p build/debug
cd build/debug
cmake -D CMAKE_BUILD_TYPE=DEBUG ../../src
make

This failed with "fatal error: 'wchar.h' file not found".
Which was fixed per https://stackoverflow.com/questions/26185978/macos-wchar-h-file-not-found

open /Library/Developer/CommandLineTools/Packages/macOS_SDK_headers_for_macOS_10.14.pkg

[ 81%] Built target lean_stage0 took a long time to finish.

It's now built successfully.

[Patrick Massot]

It's now built successfully.

So? Can it define perfectoid spaces all by itself?

[Edward Ayers]

I can't get the lean3 vscode extension to play ball with lean4 which isn't that surprising.

[Edward Ayers]

All the tests passed except the style check.

[Gabriel Ebner]

The editor tooling story is still a bit rough for Lean 4. At the moment, there is only the lean4-mode for emacs, which recompiles the whole file every single time (a bit slow) and doesn't have go-to-definition or any of the other nice features.

[Gabriel Ebner]

I wanted to work on a language server for Lean 4 (I got to a point where I could see diagnostics in vscode https://github.com/gebner/lean4/tree/server). But then I didn't have much time the last few months (I should be writing a thesis).

[Patrick Massot]

Gabriel, nobody needs to apologize for anything. All contributors of Lean already made an amazing job, and we all have much to do.