Help with Lean development workflow

Stream: lean4

[Mitchell Lee]

In #Is there code for X? > bdiv and bmod, it was recommended that I make a pull request to lean4. I opened a Windows Subsystem for Linux terminal, cloned the repository, and installed elan using these instructions: https://github.com/leanprover/lean4/blob/master/doc/dev/index.md. I also have all of the necessary packages (git libgmp-dev libuv1-dev cmake ccache clang) installed. However, I do not understand how to proceed from here.

• I tried running these commands from https://github.com/leanprover/lean4/blob/master/doc/dev/index.md:

# in the Lean rootdir
elan toolchain link lean4 build/release/stage1
elan toolchain link lean4-stage0 build/release/stage0

I got the error message

error: not a directory: 'build/release/stage1/bin'

• I tried running lake, and I got a strange 404 error.

info: downloading component 'lean'
Error(Download(HttpStatus(404)), State { next_error: None, backtrace: InternalBacktrace { backtrace: None } })
error: could not download nonexistent lean version `lean4`
info: caused by: could not download file from 'https://github.com/leanprover/lean4/releases/expanded_assets/lean4' to '/home/mitchell/.elan/tmp/ho258cmqpkm5v6kl_file'
info: caused by: http request returned an unsuccessful status code: 404

• I tried running cmake --preset release from https://github.com/leanprover/lean4/blob/master/doc/make/index.md, and I got the following error message:

CMake Error: The source directory "/home/mitchell/lean4/release" does not exist.
Specify --help for usage, or press the help button on the CMake GUI.

Thanks for reading.

[Jannis Limperg]

You need to follow these instructions first to get a Lean build.

[Mitchell Lee]

I know. I have already tried to follow the instructions on that page and you can see the results in my original message.

[Sebastian Ullrich]

The cmake line should work, your cmake may be too old for it

[Mitchell Lee]

You're right; it was too old. Thank you!

[Eric Wieser]

I recently added a gitpod configuration to the Lean repo, which you could try