How to read Lean 4 source code with LSP support
Posted on 2023-12-10 by ubikiumThe 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.