OK Nevermind Lean 4 Is Kinda Bad Actually

Originally posted on Cohost. I had planned to write pwcc in Lean 4, but after these discoveries & roadblocks, I gave up on it.

---

The Binary Sizes

My “hello world but it parses command line arguments” binary was a whopping 78 megabytes, and after adding a regex library (which I haven’t yet ended up using in any codepaths that can be run) it’s 83 megabytes now. Talking to my friend this is because “no optimizations are done” and “all symbols from all transitive dependencies are exported” and “mathlib (the largest one & sort of the reason for Lean’s existence in the first place) is usually included somewhere in that chain”

The Error Messages

Because of the whole “type universe” thing it has going on, you get some very strange errors:

• returning the wrong type of Unit (there is also a universe-polymorphic PUnit)
• using the wrong level of Option.none inside an Option monad (when the return type of the outer function and the inner function belong to different type universes)

Let alone all the error messages that come up when trying to do metaprogramming stuff..

A lot of this I think is because Lean is wayyy too flexible, so errors are reported far away from where the “wrong” thing actually happened. Writing Unit -> T when it really wanted fun () => ({}: T) is not necessarily easy to debug.

The Metaprogramming

Lean 4 is supposed to have the most advanced metaprogramming in existence, and to some extent that’s true! However, because it’s so advanced, it only operates at the AST level & lacks the capabilities to insert all the ASTs it knows about. For example, I was trying to make a custom inductive datatype. In Rust, this looks something like this, and translating that to Lean syntax, you’ll get something like

macro t:ident "::=" (ids:ident),* : command => `(
  inductive $t where $[| $ids : $t]*
)

The problems with this you’ll run into:

1. macro doesn’t like arguments inside repeaters, you need to desugar to syntax + macro_rules
2. the part that the $[]* replaces isn’t a syntax category Lean recognizes

Both of these generate a similar error message (“unexpected token”) but (2) is the much more fundamental problem. If you try to desugar even more, you’ll find that you’re expected to make a syntax node of type TSyntax `Lean.Parser.Command.ctor. How do you get a syntax node of this type? Who knows!! If you fake it and try to case something that might look like it, you get bizarre error messages.

There’s another thing you can do, which is to make an elab instead of a macro, but I also could not for the life of me figure out the magic incantation to make Lean.Elab.Command.Declaration.inductDecl stop giving me errors when I tried to elabCommand one with a single constructor.

In any case, I think I will go back to Rust metaprogramming, where we operate on plain-ol’ token streams & the error messages make more sense to me