How to read Lean 4 source code with LSP support

The problem

The Lean 4 source code is a fantastic learning material to read. Previously I just picked a file and opened it with my editor, which was set up to use lean.nvim, and it just worked, with all the infoview and jump to definition stuff. But recently, after rebasing on master, the editor errored out with the following message:

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 '/Users/[...]
info: caused by: http request returned an unsuccessful status code: 404

=> Operation failed. Exit code: 1.

The problem is due to the content of the lean-toolchain file in the Lean 4 source directory:

lean4

That is, the version manager elan reads this file, and sees that it should find the Lean version identified by lean4, so it tries to download it from the releases. However, there is no such artifact to download, so elan errors out.

The solution

After some thought, I realized that behavior is correct. Because Lean 4 is self-hosted, the specified Lean version is actually the Lean built by the content of this repository itself. I also found a discussion thread on the Lean Zulip chat and it pointed out previously it wasn’t getting the correct version before and instead falls back to the default Lean version.

So what we want here is to compile Lean 4. Following the instructions of the doc for building Lean, I started to build the nix-shell.

The solution (continued)

However, this failed with the following error:

[...]
 7/42 Test #11: test.fileclone ...................***Failed    0.95 sec
/tmp/nix-build-ccache-4.8.1.drv-1/source/test/suites/base.bash: line 556: syntax error near unexpected token `&&'
/tmp/nix-build-ccache-4.8.1.drv-1/source/test/suites/base.bash: line 556: `       && $COMPILER -E test1.c -gz >preprocessed.i 2>/dev/null \'
Compiler:         clang (/nix/store/l5dr4rvjmiybf3la6mk6gzhszrb9py3v-Toolchains/XcodeDefault.xctoolchain/bin/clang)
Compiler version: clang version 11.1.0
CUDA compiler:    not available

Running test suite fileclone.
FAILED

Test suite:     fileclone (line 32)
Test case:      Base case
Failure reason: Failed to clone
[...]

Great. Popping into the build directory with nix-shell --keep-failed, indeed the bash script base.bash was missing a line continuation mark at the end. Taking a look at the CCache repo (thank you open source!), that bug is fixed and released in 4.8.2 and 4.8.3. So the problem is that the flake lock is too old. Bumping it with nix flake update and recompile…Boom! nix shell is built successfully.

Following the Lean development doc, we can tell elan to use the freshly built artifact:

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

Now elan can correctly find lean4. That’s it. With this, I can continue to inspect the type and do small experimentations to test my understandings. Happy hacking!

diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index c1de314..fa93897 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -2820,7 +2820,8 @@ instance {α : Type u} {m : Type u → Type v} [Monad m] : Inhabited (α → m
   default := pure

 instance {α : Type u} {m : Type u → Type v} [Monad m] [Inhabited α] : Inhabited (m α) where
-  default := pure default
+  /- default := pure default -/
+  default := (default : (α → m α)) default

 instance [Monad m] : [Nonempty α] → Nonempty (m α)
   | ⟨x⟩ => ⟨pure x⟩

P.S. Based on how it was kind-of working before, I suspected that just using a recently released version of Lean is okay. But doing it the principled way is not hard either.