Discussion: Lean FRO roadmap, year 3

Stream: general

[Michael Rothgang]

Discussion of the new FRO roadmap for year 3 #announce > Lean FRO @ 💬 can happen here

[Michael Rothgang]

I'm excited to read about a code formatter. Can you share some more details? Does that mean working on pretty-printer based formatting linters for mathlib is a bit of a waste of time now (if an auto-formatter is coming soon)?

[Michael Rothgang]

Small detail: you mention the formatter in objective 6 in the intro and deliverables, but the strategy mentions it in objective 3. Is this intentional?

[Michael Rothgang]

Michael Rothgang said:

I'm excited to read about a code formatter. Can you share some more details? Does that mean working on pretty-printer based formatting linters for mathlib is a bit of a waste of time now (if an auto-formatter is coming soon)?

To clarify: I'm very happy if the answer is "yes, you can do other things now" :-)

[Marcus Rossel]

Very exciting! Could you share more details on the following two points?

We will also unify existing rewriting tactics, such as rw and simp_rw, into a single, more intuitive and powerful rewrite tool.

A next-generation simplifier, inspired by simp but designed to scale to industrial use cases, will be engineered and released.

What are (specific) aspects which are supposed to improve with the new rewriting and simplifier tactics?

[Henrik Böving]

Michael Rothgang said:

I'm excited to read about a code formatter. Can you share some more details? Does that mean working on pretty-printer based formatting linters for mathlib is a bit of a waste of time now (if an auto-formatter is coming soon)?

Can you elaborate on the objectives of this approach? The pretty printer is, inherently due to its requirements and implementation, often incapable of producing something that is faithful to the original syntax so I don't see an obvious approach to using it for formatting hints.

[Michael Rothgang]

The objective is "reduce formatting errors in mathlib by checking for some violations automatically". If there's a tool that can be useful now without having false positives, I'm all for it. That tool need not be an auto-formatter, detecting some broken-ness already helps.
There is a mathlib linter (see #24465) which checks for whitespace in declarations, which is quite useful already. #26926 (in progress) extends this to "most of mathlib" --- deferring to the pretty-printer for most formatting, but the source code for line breaks. Not perfect by any means, but useful. #27525 (in progress) checks indentation of lean files.

[Kyle Miller]

Independent of whether or not parse+format will be the way a code formatter would be organized, please keep collecting whitespace issues with the current formatting!

Ideally the pretty printer output would be the source of truth for a neutral style, but this is still often not the case.

[Robin Arnez]

What are TotalOrd and StrictWeakOrd supposed to be?

[Robin Carlier]

The "IDE and tooling" part of the roadmap only talks about VS Code. I know lean.nvim is not an official plugin, but I really hope neovim users won't be left behind and that things will keep compatibility with other editors in mind (especially the code formatting part)

[Eric Rodriguez]

I'm sad to see that the debugger has been deprioritised and isn't on the roadmap this year either. print-like debugging isn't the greatest experience

[Chris Henson]

Robin Carlier said:

The "IDE and tooling" part of the roadmap only talks about VS Code. I know lean.nvim is not an official plugin, but I really hope neovim users won't be left behind and that things will keep compatibility with other editors in mind (especially the code formatting part)

I want to second this. I don't know the numbers, but there are definitely users like myself that exclusively use Lean via neovim. I have been very pleased in the past to see the FRO support lean.nvim and hope that this will continue. I am very excited about year three of the roadmap, especially the formatter and Verso. Thank you all for your work!

[Geoffrey Irving]

When does the new code generator land, or has it already? The roadmap says June 2025. Also, will it come with @[unbox] support?

[Henrik Böving]

The new code generator is already active and being actively improved, the bug you saw in UInt128 is because of a pass in the new code generator^^

[Geoffrey Irving]

Henrik Böving said:

The new code generator is already active and being actively improved, the bug you saw in UInt128 is because of a pass in the new code generator^^

That's exciting! I am glad I could contribute to its improvement. :)

[Ching-Tsun Chou]

Is there a place where Lean users can suggest what they would like to see in proof automation?

[Kyle Miller]

We pay attention to this Zulip @Ching-Tsun Chou, and #lean4 is a reasonable starting point for making suggestions and discussing ideas.

[Ching-Tsun Chou]

Here's one suggestion: #lean4 > Can simp find useful equations automatically?

[Ching-Tsun Chou]

I think one conclusion from the thread I forked above is that Lean tactics need much better documentations. I don't think one could learn that simp can do the sort of things that @Kyle Miller and @Aaron Liu pointed out by reading the manual. It is also very hard to really understand the manual without many examples.

[Asei Inoue]

I’m writing Lean manual with a lot of examples (but Japanese only)

https://lean-ja.github.io/lean-by-example/

[Alfredo Moreira-Rosa]

I see that there is a new do notation and async-await in the roadmap, where can i get more informations about that ?
Any chances to include coroutines (yield) instead of async-await ? it would allow different implementations of async-await on top of different async primitives (event loop vs threads). Also you don't want to enter function coloring issues that are plaging Rust (sync and async functions have to be implemented twice). So designing a proper async-await abstraction is key .

[Eric Wieser]

I'm curious about how async/await fits into Lean's monadic viewpoint; I'd internalized that we effectively already have it, with def f : m X being a more general case of async def f : X and (← f) being the generalization of await f. Is this a bad take?

[Niels Voss]

I had thought so too, with def f : Task Nat being basically a async def f : Nat. It does let you do things like f.get : Nat in a non-monadic context, so it's not as strict as, say, JavaScript, because you have the ability to stall the current thread in order to wait for tasks to finish.

[Pim Otte]

What does "MVP for the Lean Online Platform as a web-only UI solution with secure sandboxing" mean? Is this kind of like Lean4web, or does it aim to run Lean in the browser itself?

[Robin Arnez]

lean4#8003 might give a bit more information about how async/await fits into do notation and why

[Joachim Breitner]

Pim Otte schrieb:

What does "MVP for the Lean Online Platform as a web-only UI solution with secure sandboxing" mean? Is this kind of like Lean4web, or does it aim to run Lean in the browser itself?

The former

[Marc Huisinga]

Chris Henson said:

Robin Carlier said:

The "IDE and tooling" part of the roadmap only talks about VS Code. I know lean.nvim is not an official plugin, but I really hope neovim users won't be left behind and that things will keep compatibility with other editors in mind (especially the code formatting part)

I want to second this. I don't know the numbers, but there are definitely users like myself that exclusively use Lean via neovim. I have been very pleased in the past to see the FRO support lean.nvim and hope that this will continue. I am very excited about year three of the roadmap, especially the formatter and Verso. Thank you all for your work!

We are very grateful for @Julian Berman's work on the NeoVim plugin, and will definitely keep coordinating potential breaking changes to the language server with lean.nvim :-)

Generally, I'm happy to extend this level of coordination to all Lean plugins that are both being actively maintained by someone I can quickly discuss changes with and that have a sufficient level of support for Lean in particular (e.g. some level of InfoView interactivity).

As for the formatter, it will definitely be available for other plugins as well. Formatting is just a standard LSP functionality.

Michael Rothgang said:

Does that mean working on pretty-printer based formatting linters for mathlib is a bit of a waste of time now (if an auto-formatter is coming soon)?

The auto-formatter will hopefully be fully functional by the end of year 3, which is still quite a while away, so any work on formatting-related linters will certainly be beneficial until then. Whether it will obsolete all formatting-related linters that Mathlib may want isn't clear to me yet at this point.

[Michael Rothgang]

Thanks for the clarification!

[Anand Rao Tadipatri]

I'm glad to see that support for literate programming via a LaTeX-inspired DSL is on the roadmap. Is it reasonable to expect that this can be used to generate blueprints for formalization projects in the future? While the current blueprint framework is already quite fantastic and has been used successfully in many large-scale formalization projects, I think it might be nice to have the added convenience of having the informal text and the Lean code in the same file.

[Joachim Breitner]

Yes, absolutely!

[Anand Rao Tadipatri]

That's great! Also, will the TeX part of the editor have the LaTeX LSP running with features like syntax highlighting auto-complete?

[pandaman]

7. Case Studies

Description: These case studies will demonstrate Lean’s maturity and utility by applying it in real-world contexts, particularly in software and hardware verification.
Strategy: We plan to develop multiple high-impact, end-to-end case studies that showcase Lean’s strengths. Each will focus on a concrete problem and highlight both challenges and solutions.
Deliverables: Each case study will be published as a public repository, accompanied by detailed write-ups explaining the approach, methodology, and insights gained. Together, they will serve as concrete evidence of Lean’s readiness for serious applied work.

Are the existing projects in scope? I'm happy to share the experiences verifying a real-world regex implementation!

[Joachim Breitner]

We have specific projects in mind that we want to see the light of day. But independent of that, please do share your experience and let people know what went well and what not. Here on Zulip, or a blog post, or maybe a talk at the Lean workshop at ITP?

[(deleted)]

We will also release an MVP for the Lean Online Platform as a web-only UI solution with secure sandboxing

Is this lockdown mode, but in a slightly different and easier to maintain form?

[(deleted)]

Now that I think of it it's perfect. I hope this will be open source.

[(deleted)]

I'm glad that there's more attention to program verification. This is my favorite field. Recently the imperative framework has been released. And I can't wait to see what else can be achieved. The real value of Lean is in ensuring the safety and correctness of software, not just to serve as a playground for reinforcement learning.

[Michael Rothgang]

I also find Lean really useful for verifying the correctness of mathematics: despite AI flocking to that area, it can (and I presume is mostly done) by humans without AI help. Given how nice programming in Lean is, I also look forward to its software verification story improving :-)

[pandaman]

Joachim Breitner said:

We have specific projects in mind that we want to see the light of day. But independent of that, please do share your experience and let people know what went well and what not. Here on Zulip, or a blog post, or maybe a talk at the Lean workshop at ITP?

Iceland is a bit too far for me:cry:

[Joachim Breitner]

At least it's far for almost everyone on the world :-)

[Kim Morrison]

New Zealand is slightly further from Iceland than Australia. :-)

[Alfredo Moreira-Rosa]

Robin Arnez said:

lean4#8003 might give a bit more information about how async/await fits into do notation and why

Is there a discussion thread to help in the design?

[George Pîrlea]

Additionally, we are working on a counterexample generator to complement proof automation with early error detection capabilities.

Could anyone in the know expand more on what this entails? Is it just better UX around Plausible?

Not too long ago, I discussed with the Lean-SMT maintainers about reflecting SMT models back into Lean values and displaying those somehow in the InfoView. It would be great if the FRO built some generic infrastructure for us to hook into for this purpose.

[GasStationManager]

I'm also curious about what's coming for counterexample generation. It'd be great to have access to both random-input generation based and SMT based approaches. Even more powerful would be a combination of techniques, e.g. instantiating some values and then proving/disproving the remaining statement by a hammer.

(I've been experimenting with some ideas in counterexample generation for error detection in coding, see e.g. this post )

[Kim Morrison]

George Pîrlea said:

Is it just better UX around Plausible?

Take this with a grain of salt, but I think our hope is that a major overhaul of Plausible (not just UX, a complete rebuild of internals) will get us most of the way there.

[Yaël Dillies]

Historical question: Was Plausible already the result of a complete rewrite of the slimcheck internals?

[Henrik Böving]

Plausible is mostly a port of slim check back in the very early days of Lean

[Eric Wieser]

Early days of Lean 4?

[Henrik Böving]

Yes

[Patrick Massot]

Anand Rao Tadipatri said:

I'm glad to see that support for literate programming via a LaTeX-inspired DSL is on the roadmap. Is it reasonable to expect that this can be used to generate blueprints for formalization projects in the future? While the current blueprint framework is already quite fantastic and has been used successfully in many large-scale formalization projects, I think it might be nice to have the added convenience of having the informal text and the Lean code in the same file.

Since it’s 2025 already, I think the FRO should seriously investigate building things on top of Typst rather than LaTeX. It would probably be much easier anyway. The obvious downside is that currently a lot more people know LaTeX, but we are talking about long term plans here.

[metakuntyyy]

I'm really excited about the rust bindings.

[Joe Hendrix]

With regards to the do notation improvements, one request I have would be a construct for resource lifetime management (like with in Python or try-with-resources in Java) that would work with mutable variables and return like if and for.

I'm not sure of the exact design, but I'd hope this could work with functions for resource management as well as tracing and other monadic combinators. e.g., with (let f := File.open ...) do .. and with (profileM name) do`.

[Jovan Gerbscheid]

Would this also allow to return from inside something like withLocalDecl type fun fvar => do ...?

[Joe Hendrix]

I think that's theoretically feasible, but would require some changes to the withLocalDecl's interface. In Python, with is implemented using a context manager interface.

If Lean followed this approach, the idea would roughly be that a function like withLocalDecl type would need to return a value that implements an enter and exit method, and with in Lean would hide the calling of those functions.

[Eric Wieser]

I think Jovan is asking a deeper question about how to make callbacks participate in do flow control

[Eric Wieser]

Though maybe the answer is "frame everything in a way suitable for with", just as we already do for for

[Notification Bot]

8 messages were moved from this topic to #general > With notation for context managers by Eric Wieser.