news from Lean 4?

Stream: general

[Johan Commelin]

Inspired by https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/migrating.20mathlib.20to.20Lean.204/ I'm curious to know if @Sebastian Ullrich has any news to share about Lean 4. Are things going well? I think I saw a bunch of tactics in the commit log on the rss stream. And the tactic framework was one of the bigger missing pieces that remained, right?
If there's any gossip... I'm all ears

[Sebastian Ullrich]

The big thing happening in the commit log right now is Leo incrementally moving tests to the new frontend (i.e. the one with the parser and elaborator written in Lean, not C++), fixing bugs in it along the way. Moving the stdlib is next after that. This will make the actual Lean 4 language a reality instead of just a prototype used in a few select tests.

[Patrick Massot]

Yes, we clearly saw that in the last few days, lots of "moving to new frontend" which sound very good. The day when the new_frontend command will disappear will clearly be a huge milestone.