Interfacing with changes to core

Stream: mathlib4

[Mario Carneiro]

Joe Hendrix said:

Hi all. I have an open Lean 4 PR (lean4#3808) that removes some simp annotations ...

When testing on Mathlib, I noticed that this PR seems to weaken norm_num. That's a Mathlib tactic and out of scope for a Lean PR, but I thought I'd alert folks to the issue in case there are any changes that would help Mathlib.

I think it's not good form to be merging a PR 4 hours after bringing up a potential issue and while the issue is still being investigated

[Joe Hendrix]

Lean + Mathlib is not a mono repo.

[Mario Carneiro]

This isn't about fixing norm_num, it's about determining what the issue is and in particular whether it should be fixed in lean core or mathlib

[Mario Carneiro]

because just because the issue manifests in mathlib code doesn't mean it's a mathlib issue

[Eric Wieser]

There's also the concern that Scott's CI to test PRs against mathlib becomes useless as soon as a branch is merged that fails the CI, because then all future PRs fail CI for unrelated reasons

[Joe Hendrix]

Yeah, that framework is really brittle. We can't treat these two repos as a mono repo.

[Mario Carneiro]

Monorepo has nothing to do with it

[Mario Carneiro]

mathlib is a giant test suite for lean4 core

[Joe Hendrix]

No, it sometimes catches issues, but Lean can't rely on Mathlib as a required test suite.

[Mario Carneiro]

the thing is, we cannot let lean and mathlib diverge for any significant period of time, this is plainly an unacceptable outcome

[Mario Carneiro]

so I don't see any way around there needing to be some back and forth here

[Joe Hendrix]

It diverges quite regularly and that's necessary to make progress.

[Mario Carneiro]

no, there are ways to maintain the rate of progress without breaking mathlib and making scott put out fires daily. I hate hearing this so often when it's obviously false

[Joe Hendrix]

Prove it

[Mario Carneiro]

This is what bors does for mathlib

[Mario Carneiro]

we have a crazy rate of progress and yet master is never broken

[Joe Hendrix]

That's a single repo.

[Mario Carneiro]

The CI scott has set up is definitely capable of doing things which act effectively like bors over mathlib + lean

[Mario Carneiro]

this is entirely a 'cultural' issue with lean4 maintenance

[Joe Hendrix]

I don't believe you. I've used it and there are regularly issues that a single repo never has.

[Mario Carneiro]

I can't prove it because I have absolutely no power over the lean4 repo to demonstrate anything

[Mario Carneiro]

And lean 4 has never actually attempted to do it

[Joe Hendrix]

I've used the CI integration. It is difficult. It's easier to fixup nightly-testing in Mathlib.

[Mario Carneiro]

the current tools are not perfect, sure. They are things scott hacked together to make his job less painful

[Mario Carneiro]

that doesn't mean they can't be improved, especially if the processes respect them

[Mario Carneiro]

e.g. not merging things that will cause them to break

[Joe Hendrix]

I've also had a PR #10336 sit for months in Mathlib that would be needed to merge a Std PR. I could start hounding people about it I suppose, but it's a pain.

[Kim Morrison]

Eric Wieser said:

There's also the concern that Scott's CI to test PRs against mathlib becomes useless as soon as a branch is merged that fails the CI, because then all future PRs fail CI for unrelated reasons

I don't think this is true? If you want a Lean PR to test against mathlib, it is essential that you base it off nightly-with-mathlib, not master. Otherwise, Mathlib CI won't even run. However, if you do, it shouldn't matter what other breaking changes have landed on Lean master in the meantime.

[Eric Wieser]

Apologies, I forgot that nightly-with-mathlib existed. This only works for one PR though, right? You can't make two PRs that depend on each other.

[Notification Bot]

30 messages were moved here from #mathlib4 > simprocs and norm_num by Eric Wieser.

[Kim Morrison]

Why not? Seems like it should be fine.

[Joe Hendrix]

Yes, a workflow I use if I am worried about Mathlib is to start with nightly-with-mathlib, convince myself the Mathlib impact is managable, and then switch to Lean master so I am confident I can get a merge in.

[Mario Carneiro]

Suppose there is a mathlib performance regression when you do that. Where would that be caught?

[Eric Wieser]

Scott Morrison said:

Why not? Seems like it should be fine.

Once the first PR is rebase-merged into a mathlib-breaking master, there's no longer a commit to start your follow-up branch off.

[Kim Morrison]

Oh, I thought you meant while they were still open.

[Mario Carneiro]

does lean 4 core ever have dependent PR's? I've never seen it

[Kim Morrison]

Yes, this seems a bit theoretical for now.

[Mario Carneiro]

which is to say, the reason they don't exist is because the earlier PRs are merged first

[Joe Hendrix]

Mario Carneiro said:

Suppose there is a mathlib performance regression when you do that. Where would that be caught?

If this was addressed to my workflow, then it's correct my testing would likely only really catch performance regressions that are really significant like timeouts. Less significant ones would need to be addressed post master merge.

[Mario Carneiro]

right, and what would that process look like exactly?

[Joe Hendrix]

Probably like what is happening with the isDefEq changes right now, where Scott has been working on a MWE. Those changes positively impacted performance in one area to unblock some work, but negatively impacted Mathlib and so there's a need to investigate further.

[Mario Carneiro]

The way I see it playing out:

• Joe tests on mathlib manually, estimates that the mathlib breakage is fixable and merges.
• Scott starts working on a mathlib fix, and either does it himself or calls in the troops to help
• Either during this process or at the next benchmark run, a significant performance regression is discovered
• The performance regression is isolated to an example which implicates the original PR
• We have to try to convince core that this is actually a problem and some part of the PR needs to be fixed. Months pass.

[Joe Hendrix]

That's a harder case though since it involved such a fundamental algoithm. An easier case would some recent applyRfl changes that impacted rw_search. I ended up reolving those yesterday.

[Mario Carneiro]

the structure here is basically biasing toward the PR being merged, since it's now in master. So regressions will persist in the final product much longer this way

[Joe Hendrix]

The last time I looked into Mathlib build times (Tuesday), it looked like performance was improving over time. Is there a concrete issue currently negatively impacting Mathlib that you want addressed?

[Mario Carneiro]

No, I'm talking about the structural properties of this merging and interfacing setup between lean core and mathlib

[Mario Carneiro]

Which is to say: if there was a performance regressing PR, what are the mechanisms to prevent it from hurting end users? The answer seems to be "there are some early checks, but insufficient to catch many performance regressions; and there is a mechanism to ensure that minor regressions are not fixed quickly"

[Mario Carneiro]

whereas the answer I would prefer is "there is a mechanism to ensure that any regression our benchmark bots can pick up will never make it to end users"

[Joe Hendrix]

Let's be concrete then, this Lean 4 PR lean4#3784 was merged last week and this Mathlib nightly testing commit fixes an issue that arose from it.

[Joe Hendrix]

There mechanism to avoid impacting users is this release process itelf.

[Joe Hendrix]

No programming language project I know of promises stability if you are using nightly releases.

[Mario Carneiro]

(incidentally, Rust does)

[Mario Carneiro]

We do have a mechanism to make sure that mathlib master is never broken, and we have a firefighter working to make sure that mathlib master is working on a positive fraction of days on nightly, but when you have to fix your tests this is often a red flag and currently the feedback mechanism is weak where lean issues are surfaced in the mathlib bumps and need to be communicated back to core

[Mario Carneiro]

More often than not people just fix mathlib anyway, because what else can we do? The next nightly is coming up and we want a working version in time

[Mario Carneiro]

instead of going through some expedited "un-merging" process, they go through the regular issue tracker, meaning that they are not prioritized and regressions can make it to stable

[Mario Carneiro]

If we were instead making proper use of the lean 4 mathlib CI, we could have prepared a bump, caught the issue, and reported it back before the PR is merged, meaning that there is no fighting against the current and no firefighting because interruptions in this process will not affect all other PRs

[Mario Carneiro]

(Meanwhile, I look over on the Rust zulip and read:

Backport nominations

Note: many of these regressions were marked at P-high/P-critical since discovered by a crater run (thus impacting one of more crates we use as canary).

Gosh, I sure wish we were considering regressions in downstream libraries as priority-critical and even making backport fixes to stable in response...)

[Kim Morrison]

We tried the model of testing every PR against Mathlib. Unfortunately at first it had way too many false positives. Even after we go that sorted out (the model of rebasing everything onto nightly-with-mathlib), we decided that it was still slowing down progress far too much, and that the current model of asynchronous work on nightly-testing was better. I know it is far from perfect (believe me, I spend half my life on nightly-testing some weeks), but it's what we're doing for the forseeable future.

Adjustments to the procedure that make life easier are very welcome, but I don't see us changing the requirements for PRs to Lean master to require a Mathlib patch. It is just too slow, and requires too much coordination.

[Joe Hendrix]

I agree. I think everybody I know of involved in Lean development is interested in seeing both Lean and Mathlib succeed. It's just too time consuming to gate every PR to Lean master by a successful Mathlib build.

[Mario Carneiro]

The "un-merging" approach would allow for handling this situation better without changing the "merge first ask questions later" workflow: if any issues are detected after merging, remove it again before the next nightly and reinstate it once the issue is resolved

[Mario Carneiro]

that is, if you are going to merge fast then you should also not be shy to unmerge

[Mario Carneiro]

The important part is that there should not be a high bar to justify unmerging, it should be the first response to issues

[Joe Hendrix]

I don't think that's a viable solution to automatically unmerge is the right approach either. We may want to consider it if it's truly a bad idea, but iteration and refinement may be more efficiently lead to a better solution.

I think we should be clear that Mathlib nightly-testing is highly unstable and should not be used as a starting point for building stable things.

[Mario Carneiro]

it's not about whether it's "truly a bad idea", it's about giving time to people to review regressions without the clock ticking

[Mario Carneiro]

unmerging should in particular not be an implication that the original code was bad, ill-conceived or anything like that, only that it was implicated in an undiagnosed bug or regression and needs to be removed from the hot path

[Joe Hendrix]

Who are the end users for whom nightly testing of Mathlib is on their critical path?

[Mario Carneiro]

contributors to lean

[Mario Carneiro]

also stable releases

[Mario Carneiro]

if nightly testing is broken for a month, I think our whole system breaks down

[Joe Hendrix]

When is the last time that happened?

[Mario Carneiro]

never, because scott is on firefighting duty

[Mario Carneiro]

but we're always seemingly teetering on the edge of Bad Things

[Mario Carneiro]

and as a result there is a lot of pressure to make sure that nightly bumps go ahead, no matter how many hacks you have to put in place to do it

[Mario Carneiro]

and mathlib accumulates technical debt this way

[Mario Carneiro]

it would be much better if we had an "ABORT" button where we could say "okay these hacks are getting kind of ridiculous, let's just abandon this bump, unmerge the offending PR, and work out what's gone wrong"

[Mario Carneiro]

but there is a power imbalance here because unmerging is not a thing right now

[Mario Carneiro]

As far as I can tell, even scott doesn't have such an "ABORT" button. He can bring up unmerging later but The Bump Must Continue

[Johan Commelin]

@Joe Hendrix My feeling/impression when reading #nightly-testing is that almost every week there are some annoying issues that cost several people a lot of time. This feels like firefighting under pressure, in a real sense. People like @Scott Morrison and @Ruben Van de Velde are doing heroic efforts. But over the past weeks I have very often felt like this is absolutely not sustainable. We are relying on volunteers that reschedule large parts of their week to make sure that the bump continues.

If the bump doesn't continue, then mathlib lags behind Lean.

And then what?

[Kevin Buzzard]

As an end user with a high profile project which depends on mathlib, this discussion does concern me a little. In lean 3 friction (of a very different kind) between core and mathlib was fixed by a community fork; I can't imagine that anyone wants to go down this route again, but this attitude from the core devs might literally force it if the mathlib people ultimately can't keep the show on the road.

[Sebastian Ullrich]

Hey all, the previous months have been an exceptional period of Lean development due to broad changes to multiple repositories as part of the upstreaming efforts, necessitating changes to our approach to syncing with Mathlib partway through. This effort is now largely completed, so we expect the rate of breaking changes to revert back to previous levels going forward. Nevertheless, we are initiating internal discussions on how we can improve our processes here, both technical and organizational, for the benefit of all users of Lean.

[Kevin Buzzard]

Yes, I am very much torn by what's going on right now, because at the community meetings I always come away being super-excited about how fast core is progressing and all the great new things going into it. And then I see poor Scott drowning in #nightly-testing and I see the consequences of moving fast and breaking things: things get broken. It is very comforting to know that you feel like there's a light at the end of the tunnel here.

[Patrick Massot]

I don’t understand how the current workflow optimizes work, even if you only consider the FRO point of view. It seems to me that Scott’s life would be less stressful if changes were tested against Mathlib before merging them to core Lean. This would involve less back and forth, right?

[Jireh Loreaux]

Patrick, I think the point is that it doesn't optimize total effort required, but rather the speed with which core can make changes they deem necessary, and it's the latter that is currently taking priority.

[Patrick Massot]

Joe Hendrix said:

I've also had a PR #10336 sit for months in Mathlib that would be needed to merge a Std PR. I could start hounding people about it I suppose, but it's a pain.

PRs that have build errors are typically never looked at by maintainers. We are already overwhelmed by PRs that build. So yes, you should start hounding people if you need help to make it build.

[Yaël Dillies]

There's one exception, namely PRs that are tagged help-wanted, but this wasn't done here

[Kevin Buzzard]

Joe, the criterion that many people use when looking for mathlib PRs to review is whether the PR shows up in this list #queue .

[Kevin Buzzard]

When I last looked at this today it had over 170 PRs on it, and for me these are the priority ones.

[Joe Hendrix]

Thanks for the tips on how to address this in the future. I've reflected and decided to close #10336. That work predates some of the Std to base migrations and the benefits of nicer list folds in Std/Lean seem minor.

[Kim Morrison]

A few things to add:

[Kim Morrison]

• First, perhaps I have been handling nightly-testing incorrectly. I certainly would like assistance on this. Depending on what pace changes are coming at, work on Mathlib adaptations and reporting and dealing with Lean regressions takes between 20% and 100% of my time in a given week (fortunately 20% much more common!). There are other things that I'm trying to get done, too, and so I've been reporting what needs to be done on the nightly-testing thread in a way that encourages and hopefully enables others to assist. But perhaps the way I've done this has overemphasised a sense of urgency or even desperation. :-) Obviously there is a lot of work here, but we're getting it done.

[Kim Morrison]

• Second, it's important to remember that despite some disagreements about process, the FRO is really committed to helping Mathlib, both in its current form and hopefully during significant future growth. The FRO puts real resources into Mathlib, is happy to do so, and plans to put even more in future.

[Kim Morrison]

• Third, I think some of the perspectives in this thread treat the model of "Lean makes breaking changes, and then we sort things out on nightly-testing and negotiate regressions and changes between the repositories" as if this a broken model that is broken out of ignorance or carelessness. I really want to push back on that, and argue that it is much more "by design" than it might appear.

[Kim Morrison]

Why don't we go back to the system we briefly tried, in which every Lean PR is tested against mathlib? (Note this system is still available, and PR authors are encouraged to use it: just make sure your PR is based of nightly-with-mathlib, feel free to ping me if the system is confusing or not working, and read tags and branches for the gory details.)

[Kim Morrison]

1. This requires every contributor to Lean to deal with Mathlib on a regular basis (and in particular all FRO members). This is simply inefficient, and from an efficiency point of view it makes more sense to separate the work of advancing core functionality in Lean, and dealing with the ecosystem integration. We're not asking anyone to use nightly releases of Lean, nor the nightly-testing branch of Mathlib. They exist so that we can efficiently delegate to the work to the people with the comparative advantage doing that work. (e.g. Leo making fundamental changes to the simplifier, me working out how this affects Mathlib, and then adapting or reporting reporting regressions). We tried it, and it didn't work. We really care about making fast progress on Lean.

[Kim Morrison]

2. Mathlib is not the only user of Lean, and despite it being big and providing great coverage as a test suite (more on that later), we don't want it to win by default on questions of performance tradeoffs. We need to be able to make changes that have sufficiently high payoffs elsewhere, even if Mathlib suffers as a result. Testing everything against Mathlib potentially prevents us doing this. That said, we very much understand that Mathlib is a great indicator, and regressions in Mathlib caused by problems in Lean are very much worth fixing. A great example here is lean#3807, which provides absolutely essential performance changes in IsDefEq, enabling @Henrik Böving to implement a powerful bitblasting tactic. (This takes high level goals that can be converted to boolean problems, and then hands them off to a SAT solver. After the changes from 3807, it spends most of its time in the SAT solver and handling the certificate provided by the solver. Before those changes, it was stuck in IsDefEq.) However --- we discovered there are some fairly significant slow-downs in Mathlib as a result of this. Now, we haven't just told Mathlib to cope! Instead, I've spent much of the last week trying to minimize the issue, so we can go back to Leo and sort out a solution that will work for Henrik's project and for Mathlib. We've decided to delay the release of v4.8.0-rc1 precisely because of this problem; we aspire to monthly releases, but keeping in sync with Mathlib is more important, so until we get to the bottom of this (hopefully!!!) we're delaying.

[Kim Morrison]

3. While Mathlib has great coverage when used as a test suite for Lean, to be honest it has too thorough coverage. It is big enough that every peculiarity in a tactic, or performance quirk in a core language feature, is depended on somewhere in Mathlib! It's simply not okay to treat every such a dependence as a blocker for changing things in Lean. We need a negotiated process, handled by people who know Mathlib well, to diagnose which changes warrant changes in Mathlib (because it is being naughty!), and which changes need to go back to Lean. As above, not everyone working on Lean can or should be doing this.

[Kim Morrison]

Sorry, that was all a bit longer than I at first planned. We're trying, we really really care about the future of both Lean and Mathlib, and I hope everyone will work with us as we sort these things out. Hopefully what I've written above gives a bit more context on why we don't like the "test everything" or "unmerge anything that breaks" approaches to development. And I'm sorry if I've been alarmist about nightly-testing in the past. :-)

[Kim Morrison]

And an addendum: there are plans afoot to build "institutional funding" specifically for Mathlib that would not come through the FRO. It's a fantastic opportunity at the moment that the FRO is able to marshall and deploy resources for Lean and Mathlib, but it's really important that we think about Mathlib separately as well. If we are to grow significantly, and more importantly transform Mathlib into something that can support 100x as much formalisation as currently happens, as downstream projects, then I suspect we are going to need a combination of academic contributions, volunteers efforts, but also paid engineering time. I really hope at least some of these plans come to fruition, and regardless that everyone thinks about this issue.

[Kevin Buzzard]

One thing I take from these very long, helpful and informative messages is that you don't seem to be tearing your hair out at the current situation, which is really great to hear :-)

[Jeremy Tan]

Kim Morrison said:

2. Mathlib is not the only user of Lean, and despite it being big and providing great coverage as a test suite (more on that later), we don't want it to win by default on questions of performance tradeoffs. We need to be able to make changes that have sufficiently high payoffs elsewhere, even if Mathlib suffers as a result. Testing everything against Mathlib potentially prevents us doing this. That said, we very much understand that Mathlib is a great indicator, and regressions in Mathlib caused by problems in Lean are very much worth fixing. A great example here is lean#3807, which provides absolutely essential performance changes in IsDefEq, enabling Henrik Böving to implement a powerful bitblasting tactic. (This takes high level goals that can be converted to boolean problems, and then hands them off to a SAT solver. After the changes from 3807, it spends most of its time in the SAT solver and handling the certificate provided by the solver. Before those changes, it was stuck in IsDefEq.) However --- we discovered there are some fairly significant slow-downs in Mathlib as a result of this. Now, we haven't just told Mathlib to cope! Instead, I've spent much of the last week trying to minimize the issue, so we can go back to Leo and sort out a solution that will work for Henrik's project and for Mathlib. We've decided to delay the release of v4.8.0-rc1 precisely because of this problem; we aspire to monthly releases, but keeping in sync with Mathlib is more important, so until we get to the bottom of this (hopefully!!!) we're delaying.

I can wait, yes, but apparently you still haven't found the causes of the issues in mathlib's nightly testing after lean4#3807

[Jeremy Tan]

Is there really no way to diagnose simpNF linter failures? (That linter is in Std so I don't know what to do with it)

[Kim Morrison]

It should just be a matter of putting in a file with import Mathlib a restatement of the lemma and seeing if you can prove it by simp only [my_lemma].

[Kim Morrison]

Jeremy Tan said:

I can wait, yes, but apparently you still haven't found the causes of the issues in mathlib's nightly testing after lean4#3807

You might think about how this message comes across; hopefully it wasn't intended the way it sounds to me. Help looking at nightly-testing is always appreciated.

[Kim Morrison]

As an example, we can reproduce the simpNF error on

theorem comap_exp_cobounded : comap exp (cobounded ℂ) = comap re atTop

with:

import Mathlib

/--
error: failed to synthesize
  AddMonoidHomClass (AddGroupSeminorm ℂ) ℂ ℝ
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)
-/
#guard_msgs in
open Complex Filter Bornology in
example : comap exp (cobounded ℂ) = comap re atTop := by simp

[Kim Morrison]

I wonder if it makes sense to actually collect all these in a test file someone.

[Kim Morrison]

It makes is possible for someone who wants to diagnose them to get started faster.

[Kim Morrison]

And could also tell us if one got better (or even worse, if we add a second copy that succeeds with a higher timeout).

[Eric Wieser]

Regarding simpNF, it would be nice if we had a different version of nolint for "the linter crashes"

[Kim Morrison]

I think better than a test file would be some issues. I've made #12226 as a prototype: please let me know if this should be structured differently.

[Jeremy Tan]

Kim Morrison said:

It makes is possible for someone who wants to diagnose them to get started faster.

Still, that doesn't seem to help me fix the issue, which is what I was going for in my commit to the nightly-testing branch

[Kim Morrison]

I don't understand. Your commit removed a nolint simpNF, then the next commit added it back. What were you trying to do?

If you want to help diagnose these, you need to make examples such as those collected under https://github.com/leanprover-community/mathlib4/issues?q=is%3Aissue+is%3Aopen+sort%3Aupdated-desc+label%3Aslow-typeclass-synthesis.

Would you be interested in working on some of those? (Or adding more for other nolint simpNF attributes that don't have linked issues?)