Zulip Chat Archive

Stream: general

Topic: Building Lean 4

Edward Ayers (Apr 25 2019 at 13:22):

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

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 (Apr 25 2019 at 13:24):

It's now built successfully.

So? Can it define perfectoid spaces all by itself?

Edward Ayers (Apr 25 2019 at 13:26):

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

Edward Ayers (Apr 25 2019 at 13:27):

All the tests passed except the style check.

Gabriel Ebner (Apr 25 2019 at 13:27):

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 (Apr 25 2019 at 13:30):

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 (Apr 25 2019 at 13:55):

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

Last updated: Aug 03 2023 at 10:10 UTC