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
Replying to
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!
Replying to
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
2
2
Show replies