Movement from Std to Init

Stream: batteries

[Mario Carneiro]

Joe Hendrix said:

I think this is common enough that it could go in Lean itself. I discussed the homogenous case with Scott yesterday since it was useful for a formalization of AES. Here's a link to that implementation if folks are interested and AES using it is here.

I'm not sure about it being "common enough to go in Lean" because it is mainly restricted to software verification contexts, but I also very much dislike the implication that common things should be going in lean just because they are common, because this is the beginning of the end for std.

[Joe Hendrix]

Indeed, there's been a lot of movement from Std to Init, and I think this is a good thing for most users for a few reasons.

• If you switch to using a nightly, then you have less fishing for finding the right branch to use.
• Fewer imports for tactics and definitions
• Importing Std modules don't change meaning of syntax or normal forms (e.g., core now uses same Integer division as Std/Mathlib). It also has much of the same Bool/Prop normal forms as Std and Mathlib.

It is of course possible to keep consistent normal forms across repos, but past experience has shown that's difficult.

[Notification Bot]

A message was moved here from #std4 > RFC: Arrays with fixed length by Mario Carneiro.

[Notification Bot]

A message was moved here from #std4 > RFC: Arrays with fixed length by Mario Carneiro.

[Mario Carneiro]

Joe Hendrix said:

Importing Std modules don't change meaning of syntax or normal forms (e.g., core now uses same Integer division as Std/Mathlib). It also has much of the same Bool/Prop normal forms as Std and Mathlib.

This is mainly a problem caused by the current Lean contribution rules though. When it's not possible to change upstream, downstream finds a workaround. No one likes that solution but moving parts of the downstream to upstream will not solve the problem.

[Mario Carneiro]

If you are saying that now that upstream is more responsive we won't need to use workarounds in downstream then that's great, but it's not motivation to move anything beyond the workaround itself. Moving more than that will create more opportunities for downstream to get stuck because upstream took ownership of things it isn't prepared to maintain

[François G. Dorais]

One problematic move was upstreaming @[ext] while it had major issues lean4#3643 (formerly std4#618). Luckily, I found time to migrate this issue so it's not forgotten. It was on my back burner to try to fix it in Std, it is not high priority enough for me to try to fix it in core.

[Mario Carneiro]

Fewer imports for tactics and definitions

There is also a possible undesirable side effect of this, which is that more projects will feel compelled to use prelude to stop importing too much due to the growing scope of Init. Already this has happened for the Lean package, which uses it to avoid unnecessary build dependencies. Downstream projects usually aren't building Init so this is less of an issue, but there is still a build cost for having all the modules in scope and initialized, an impact on autocomplete performance etc. Basically all the reasons why people don't like import Mathlib also apply to import Init in a world where Init tries to eat everything.

[François G. Dorais]

One possibility (but probably a bad idea?) is to have Std within core in a similar way that Lake is in core.

[François G. Dorais]

Following up on Mario's comment. I have been under the impression that Lean 4 core developers wanted to keep Init very small (after lessons from Lean 2 and Lean 3). Has this changed?

[François G. Dorais]

After the last (or next to last?) community meeting, I got the feeling that Leo wanted more components to be stable rather than small. (I'm thinking about some comments about the algebra hierarchy in Mathlib.)

[Joe Hendrix]

Keeping Init small is still a goal, but we also want good consistent normal forms of core types across Init, Std, and Mathlib.

Mario, if you are concerned about Init size, we could dig into the details. Could you elaborate on how that's impacting your work and post some more specific numbers comparing the size of the environment after import Init and import Mathlib?

[Mario Carneiro]

Keeping Init small is still a goal, but we also want good consistent normal forms of core types across Init, Std, and Mathlib.

As I've already said, the way to solve this is for Init, Std, and Mathlib to agree on what those normal forms are, and the way for that to happen is for the various maintainer groups to talk to each other about what the plans and problems are. As far as I am aware no concern of this form has been directly brought up with the mathlib maintainer team for consideration.

[Mario Carneiro]

You simply cannot unilaterally solve the problem by moving code around, you will just cause the problem to pop up somewhere else if the projects aren't on the same page.

[Eric Wieser]

Moving things between projects can potentially make the problem worse, as moving something upstream is saying "the normal form cannot be in terms of anything that is now downstream"

[Mario Carneiro]

:this: this was a major problem / reason we needed to upstream NatCast

[Joe Hendrix]

Mario Carneiro said:

You simply cannot unilaterally solve the problem by moving code around, you will just cause the problem to pop up somewhere else if the projects aren't on the same page.

What can't I do and why? Many more terms with Bool and Prop now have consistent normal forms in Lean, Std and Mathlib after lean4#3508. That was largely achieved by upstreaming lemmas + additional fixes.

Are there problems with that PR that I should be aware of? There will eventually be similar compatibility change for Nat/Int with lean4#3562 and then other theories.

[Mario Carneiro]

What can't I do and why? Many more terms with Bool and Prop now have consistent normal forms in Lean, Std and Mathlib after lean4#3508. That was largely achieved by upstreaming lemmas + additional fixes.

If you make a change that a downstream project disagrees with, it may "overrule" you and introduce different normal forms in order to solve downstream problems caused by your changes. I'm not saying that happened in this case, but the way to ensure it doesn't happen is to be open and communicative about what you are changing and why so that we can find a common solution which solves things for everyone rather than helping one project while hurting another.

[Mario Carneiro]

The situation with Int division was basically this: core had a definition of integer division which turned out to be really untenable for mathlib, and we needed to do something about it and core was not helping. So we ended up just overriding the definition downstream, first in mathlib and then upstreamed to std after it started getting the integer division lemmas and came to the same realization as mathlib regarding the untenability of using C-style division in most lemmas.

[Mario Carneiro]

This is a problem that would have been solved if the respective maintainer teams were on the same page. They eventually came around, which is why this division now lives in core where it should be. But in almost every case where you see "differing normal forms" that have been put there on purpose, you can trace the core of the issue down to a communications breakdown

[Mario Carneiro]

This is one of the reasons that when I hear "My project is to improve the consistency of normal forms" which does not involve going around and talking to lots of people, I get nervous, because that's exactly the prerequisite for coming up with a solution that will actually work and won't be "overruled" later

[Mario Carneiro]

Are there problems with that PR that I should be aware of?

I see that you made simp much more aggressively classical than before, making use of Classical.foo lemmas even when Decidable.foo lemmas could be used to similar effect (such that classical simping can be controlled by open Classical). This makes me sad, I was trying to avoid that, but I'm not really able to keep arguing on this point.

[Mario Carneiro]

(what's worse, making them global simps in core means no one can override it in downstream projects without local un-simp-ing every time)

[Mario Carneiro]

For something that is changing simp normal forms, I'm surprised it was not tested against mathlib before merging. How could you know if you made a good change without such a test? There are also no mathlib maintainers among the reviews. So from a procedural standpoint I would say that it has some warning signs. I would have liked to have a discussion about these changes in terms of what is changing and why; the PR itself is quite vague about the changes and you have to read the diff to actually see these things.

[Joe Hendrix]

Why do you assume that it was tested against Mathlib?

[Joe Hendrix]

Isn't Scott a Mathlib maintainer?

[Joe Hendrix]

Indeed, the increased use of classical was because Mathlib made those choices.

[Joe Hendrix]

I am sorry that you are disappointed in my results and how the work was performed.

[Mario Carneiro]

Joe Hendrix said:

Why do you assume that it was tested against Mathlib?

(I assume you missed a negation here.) The mathlib CI bot doesn't appear to have succeeded, and there is no comment on the post saying you tested it against mathlib.

[Mario Carneiro]

Joe Hendrix said:

Indeed, the increased use of classical was because Mathlib made those choices.

That was deliberately left as part of mathlib, along with the foo lemmas aliasing Classical.foo. Std was more agnostic about it.

[Mario Carneiro]

Joe Hendrix said:

I am sorry that you are disappointed in my results and how the work was performed.

The real question is whether it is acceptable for me to submit a PR reverting some of this. It's perfectly alright if we don't get things right on the first try, but the real issue is that core is super-scary for anyone not in the FRO to contribute to, so I don't know whether I should just despair on improvements at this point.

[Mario Carneiro]

Honestly I don't have enough information about what you did to be disappointed in the results. It was just not a topic of discussion at any point so I don't have a basis for understanding what in it is important. I just remarked on a few things I noticed while looking over it just now.

[Joe Hendrix]

Sure, if you have changes, you can submit PRs or propose them here. It would be helpful to me if you update and rerun the normal form tester with just Init and then import Mathlib". It currently lives in tests/playground/bool_exhaust_test.lean` until it is more polished.

[Mario Carneiro]

What is the normal form tester exactly?

[François G. Dorais]

I can't answer for Joe, but he did recently develop lots of "tactic checking" tools. As far as I am aware, the current pinnacle is an extremely thorough check of Bool simps. I really enjoyed glimpsing at these developments after Joe shared a link to me. Which brings us back to the core problem: why weren't these developments announced more broadly? I agree with Mario that there is indeed a serious communication issue.

[François G. Dorais]

FWIW: I don't think the FRO nor the community are to blame here. I think good communication is an issue that needs to be resolved from both sides, in different ways. I hope that both the FRO and the community will propose ideas to fix this issue.

[Joe Hendrix]

If I recall correctly, this was discussed at the last community meeting. The testing framework still needs additional development prior to more widespread usage on other theories in my opinion. It's not intentionally kept secret, but it just needs to be better.

[Leonardo de Moura]

Regarding communication:

• The monthly community meetings are available online. In the last one, we discussed the Std refactoring: https://www.youtube.com/watch?v=vb1pPkG9e-8.
  
• The Lean FRO public events are available here: https://lean-fro.org/events/. Note that we have weekly office hours.
• Our roadmap is available online: https://lean-fro.org/about/roadmap/

[Patrick Massot]

The road map and community meetings are great but they are mostly the FRO telling users what they are working on. I think Mario meant communication in the other direction, from users to the FRO. The office hours are not really about the same thing, from what I saw. They are also really nice, but mostly about teaching how to use Lean.

[Leonardo de Moura]

@Patrick Massot
Half of the community meetings led by the FRO are dedicated to Q&A sessions, where users are encouraged to ask questions and discuss their issues. Several FRO members also attend the community meetings organized by the Mathlib maintainers. Regarding the office hours, we clarified in the last announcement (https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Office.20hours/near/431167910) that questions about Lean, Std, and the roadmap are welcome. Additionally, several FRO members are very active here on Zulip.

[Patrick Massot]

All this is great, and you know I am very grateful. But moving many things from Std to Core was still a major decision that, as far as I can see, was not discussed at all with users and Std maintainers before being implemented. So I can understand that Mario is a bit worried. This decision was well explained after the fact but not discussed a priori (unless I missed some discussion). And allowing users to ask questions during meetings or office hours does not help with this. How could we know that we should have asked: do you plan to move Std to Core?

[Leonardo de Moura]

@Patrick Massot
Thank you for your feedback. I acknowledge that the transition from Std to Core was a significant move and not one that was taken lightly. I want to clarify that @David Thrane Christiansen did notify Mario before the changes were initiated and prior to the broader community announcement. At the FRO, we were fully committed to ensuring that Mathlib would be properly patched during the process. We are currently exploring strategies to minimize future disruptions for Mathlib users. Additionally, we are dedicated to making Lean a successful mainstream programming language with a diverse user base.

[Mario Carneiro]

I was indeed notified that some tactics were going to move, not really in a way which invited discussion but more of a "heads up this is happening". I have to admit that the scale turned out to be much bigger than I expected and now there isn't much left within the original purview of Std from what I can tell. Most of the things on Joe's original Std roadmap are now in an uncertain position and I don't know what will remain. Perhaps future announcements will clarify matters here, but I certainly haven't gotten the impression that I have any say over the contents of those announcements.

[Eric Wieser]

For reference, the old roadmap I can find is

The Standard Library consists of

• Declarations and lemmas on basic types.
• Common data structures with operations and lemmas.
• Type classes and other abstractions
• Operating system operations
• Tactics and commands
  • Manipulation and cleanup tactics
  • Highly automated finishing tactics

[Yaël Dillies]

• Type classes and other abstractions

sounds ultravague

[Leonardo de Moura]

Dear all,

First and foremost, I want to express my deepest gratitude for the exceptional work you have all contributed to the Lean project. Your dedication and expertise have been instrumental.

We are at a pivotal moment in the evolution of our project, and I need to share some significant changes that will impact our path forward. After thorough consideration and discussions, we have decided to rename the current Std library to Boost. This change will allow us to realign the library with its evolving nature and community expectations. The Boost library will be a space where experimental and incomplete ideas can flourish, providing a platform for innovation and exploration without the constraints imposed on the core libraries. @Scott Morrison has already discussed this decision with @Mario Carneiro .

In parallel, we will create a new Std library, more in line with the standard libraries of mainstream programming languages. Its scope has already been shared in the last community meeting. This new Std will house essential functionality, ensuring a coherent and high-quality foundation for Lean users across various domains, including mathematics, software development and verification, and AI.

We acknowledge and respect that within our community, there are diverse opinions about the development model. While some community members prefer the Bazaar style, which encourages a more decentralized and open approach, we have observed that this model has negatively affected productivity in our past experiments. Therefore, we will continue using the Cathedral model for the core Lean repository and the new Std to ensure a consistent and efficient development process. This decision comes with the responsibility of maintaining Lean's core integrity and ensuring it meets the broader community's needs effectively.

I want to assure you that the autonomy of the Boost library will be respected, and its maintainers will have significant freedom in its development and direction. The distinction between Std and Boost will enable us to cater to the different needs and expectations within our community without compromising the overall user experience.

The decision to transition pieces of Std to the core repository was driven by the necessity to enhance the user experience, particularly for those not utilizing Mathlib. We also wanted to streamline development and address the dispersion of key functionalities across various packages, which has led to inconsistencies and inefficiencies.

We are committed to supporting Mathlib and ensuring its seamless integration with every Lean 4 release. Our continuous efforts to reduce compilation times per million lines of code are a testament to this commitment. Our goal is to provide a seamless, efficient, and enjoyable experience for all Lean users, regardless of their field.

I understand that changes of this magnitude can be surprising and may lead to uncertainties. I want to open a line of dialogue for any concerns or suggestions you may have. Your input is invaluable, and while the strategic direction is a responsibility that I bear, it is essential that it resonates with and supports the community's goals and needs. Please free to use our weekly office hours and community meetings to ask questions.

Thank you for your ongoing commitment to the Lean project. I look forward to navigating these changes together and building a stronger, more vibrant community around our shared passion for Lean.

Best,
Leo

[Johan Commelin]

Just to clarify: who will be the maintainers of Std and who will be the maintainers of Boost?

[Leonardo de Moura]

@Johan Commelin Thanks for asking. The new Std will be maintained by the Lean FRO. Boost will be maintained by the community.

[Ruben Van de Velde]

I fear that in the coming years we'll find ourselves discovering poor design decisions that are much harder if not impossible to fix because they're baked into the core language rather than in an independently versioned std library. I hope I'm wrong, though

[Eric Wieser]

Another big downside of eagerly upstreaming things from Std (or soon-to-be-boost) to core is that development metaphor aside, the contribution barrier is far higher from a technical standpoint for the latter. If I check out the std repo, the vscode extension does all the work and I can just write lean code. If I checkout core then I have to build a lean binary before I can do anything.

[Shreyas Srinivas]

A cathedral model with such high barriers to contribute is likely to create the bazaar model anyway.

[Yaël Dillies]

eg the lemma names. Recently I have been littering mathlib with -- TODO: Fix name in Std. Should I rather be writing -- TODO: Get over it?

[Eric Wieser]

(the above is of course a problem solvable in other ways (like a nix cache?), but I haven't seen it raised yet)

[Henrik Böving]

I think a development model like this does already exist in other languages and works to produce acceptable results. E.g. in Rust where you have to fiddle with x.py etc. to get a libstd environment set up but the stdlib is pretty great. There is also of course C++ with its libstdc++ and boost (which this is obviously alluding to)

[Johan Commelin]

Leo's message didn't mention much about upstreaming to core, right? So maybe we should split into two threads...

[Eric Wieser]

Yes, I guess there are two points of discussion here:

• What determines the line between core and the library-formerly-known-as-Std? Is anything definitely out of scope for upstreaming?
• What's going on with the old vs new roadmap for Std, which seems to have completely diverged (I think the boost/std split answers this one)

[Kim Morrison]

Yaël Dillies said:

eg the lemma names. Recently I have been littering mathlib with -- TODO: Fix name in Std. Should I rather be writing -- TODO: Get over it?

The intentional is that the current contents of Std will largely move to Boost (with the exception of List/Array lemmas, which will be upstreamed, and HashMap, which @Markus Himmel is beginning significant new work on).

So these TODOs should mostly change to "Fix name in Boost". If they affect List/Array lemmas, then please make the PR to Lean if they've already moved. Name changes that require discussion should wait (we don't want to be drawn into bikesheds about names; my hope is that when verso is done and documentation efforts begin in earnest, we can appoint @David Thrane Christiansen as the core naming czar, empowered to unilaterally fix names. :-), but I'll merge obvious fixes.

[Kim Morrison]

The new Std will actually be largely, perhaps even completely, empty for a while! We want to make room for the FRO developed library, and want to alert everyone to our intention to develop this, sooner rather than later.

[Eric Wieser]

Is the "new Std" roadmap available anywhere in non-video format? (I know it came up in the meeting, but unlike the original roadmap, the slides don't seem to be google-indexed)

[Kim Morrison]

Nope. :-)

[Martin Dvořák]

If I understand correctly, the current content of Std will be split.
Essentials will go to Lean.
Non-essentials will go to Boost.

What will be the content of the new Std then?

[Eric Wieser]

It's in the slides of the latest monthly meeting, which I believe was recorded

[Shreyas Srinivas]

Question: Will lake update smoothly handle this transition when it happens?

[Mario Carneiro]

The main effect of the latest bump is that some imports like Std.Tactic.RCases are no longer necessary. If you get an error about a missing file after a bump try just deleting the import

[Martin Dvořák]

Is there a summary of those moved tactics somewhere?
I will update my table: https://github.com/madvorak/lean3-tactic-lean4

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Scott Morrison said:

Yaël Dillies said:

eg the lemma names. Recently I have been littering mathlib with -- TODO: Fix name in Std. Should I rather be writing -- TODO: Get over it?

The intentional is that the current contents of Std will largely move to Boost (with the exception of List/Array lemmas, which will be upstreamed, and HashMap, which Markus Himmel is beginning significant new work on).

So these TODOs should mostly change to "Fix name in Boost". If they affect List/Array lemmas, then please make the PR to Lean if they've already moved. Name changes that require discussion should wait (we don't want to be drawn into bikesheds about names; my hope is that when verso is done and documentation efforts begin in earnest, we can appoint David Thrane Christiansen as the core naming czar, empowered to unilaterally fix names. :-), but I'll merge obvious fixes.

FYI @Markus Himmel , building on Mario's invariants I had verified a sufficient number of HashMap functions to build verified software on top of. The basic model is in std4#279, and on my hard drive I have all the proofs using that model. I will assume that this is no longer relevant given the move, but if you would still like the proofs then please let me know and I can PR the rest.

[Yury G. Kudryashov]

We have both docs#Std.HashMap and docs#Lean.HashMap. Are there any differences? If no, then should we delete the Std one?

[Mario Carneiro]

The original reason for the split is because the lean one doesn't prove correctness and also wants the flexibility to change without affecting Std consumers.