Does anyone know of a Lean book that builds up the basics from absolutely nothing, not even the Lean standard library? I'm curious about the foundations that lie just above the language.
Lean is self-hosted, so the language is written in Lean. And it's well documented. Starting from the Prelude [3], all the way up to the language server (yes, Lean ships a parser combinator library and a JSON library with the language).
One caveat is that the toolchain version of the repo is the repo itself, so you'd have to follow the development guide [4] to set it up.
Also, this is different from the standard library std4 [5], which is actually not shipped with the language, but just a normal package developed and used as the standard library.
[1]: https://leanprover.github.io/functional_programming_in_lean/
[2]: https://github.com/leanprover/lean4
[3]: https://github.com/leanprover/lean4/blob/master/src/Init/Pre...
[4]: https://github.com/leanprover/lean4/blob/master/doc/dev/inde...