Passed a big milestone towards bootstrapping Lean 4 today: After grafting the old elaborator (written in C++) onto the new frontend (written in Lean) in true Frankensteinian fashion, the new frontend can now process all 2176 lines of core.lean successfully!
Conversation
Is there a place we can go to have a sneak peek at this work? Super interested to see how one goes about implementing an elaborator for Lean in Lean. :)
1
4
Not quite yet, unfortunately. Though rewriting the (term-level) elaborator in Lean is the one big task we haven't even started yet. Thus Frankenstein, for the time being.
1
3
Haha, no worries! I was actually attempting to look for the source code of your Lean parser in Lean the other day, but also couldn't find it either. Is that also a WIP?
1
2
Yes, it's all part of Lean 4. "We are currently developing Lean 4 in a new (private) repository. The Lean 4 source code will be released here when ready." :) github.com/leanprover/lean
1
3
Ahhh righto! Hehe, I'm so excited! Super interested to see what you've all learned.
Specifically atm I'm learning about in Top-Down Operator Precedence (Pratt) parsing and wondering if it's the right approach to be making. Having extensible syntax would be nice!
1
3
Yep, we're still doing Pratt parsing! Only realistic alternative I'm aware of is Isabelle's Early parsing, but having to specify a formal, context-free priority grammar is pretty far from our approach of "everything goes" parser combinators.
2
3
Replying to
Ahh, found some of your presentations which helps a bit!
- leanprover.github.io/presentations/
- leanprover.github.io/talks/vu2019.p
