Help with `nightly-testing`

Stream: general

[Kim Morrison]

(Background: mostly when I ask for help with the nightly-testing branch, it happens on private stream. Today I want to ask for help from someone who's not on that stream, so I'm moving here.)

[Kim Morrison]

Would @Kevin Kappelmann (the author), or anyone else, be able to take a look at Mathlib.Algebra.ContinuedFractions.Computation on the nightly-testing branch, and see if they can diagnose the error?

[Kim Morrison]

It is probably just that we need to explicitly simplify a let binding now (previously this happened in an uncontrollable fashion!)

[Kim Morrison]

But at the point of failure, it seems there are multiple goals (so either proof structuring has broken, or was never there?), and I'm having trouble working out what fix is required.

(Aside: long proofs are no fun for maintenance. Please write, and ask for during review, short modular proofs! :-)

[Damiano Testa]

I have not been able to debug this, but there is a field_simp prior to the failure that I think also failed to do its job. The goal at

      -- now unfold the recurrence one step and simplify both sides to arrive at the conclusion
      field_simp [compExactValue, continuantsAux_recurrence s_nth_eq ppconts_eq pconts_eq,
        nextContinuants, nextNumerator, nextDenominator]

changes from

(ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB) = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr

to

((continuantsAux (of v) n).a * ifp_n.fr + (continuantsAux (of v) (n + 1)).a) /
    ((continuantsAux (of v) n).b * ifp_n.fr + (continuantsAux (of v) (n + 1)).b) =
  if (IntFractPair.of (1 / ifp_n.fr)).fr = 0 then
    (↑⌊1 / ifp_n.fr⌋ * (continuantsAux (of v) (n + 1)).a + (continuantsAux (of v) n).a) /
      (↑⌊1 / ifp_n.fr⌋ * (continuantsAux (of v) (n + 1)).b + (continuantsAux (of v) n).b)
  else
    (↑⌊1 / ifp_n.fr⌋ * (continuantsAux (of v) (n + 1)).a + (continuantsAux (of v) n).a +
        (continuantsAux (of v) (n + 1)).a * (IntFractPair.of (1 / ifp_n.fr)).fr) /
      (↑⌊1 / ifp_n.fr⌋ * (continuantsAux (of v) (n + 1)).b + (continuantsAux (of v) n).b +
        (continuantsAux (of v) (n + 1)).b * (IntFractPair.of (1 / ifp_n.fr)).fr)

Also, on master, closing with the formatting below avoids the state with more than one goal

      rw [one_div, if_neg _, ← one_div, hfr]
      · field_simp [hA, hB]
        ac_rfl
      · rwa [inv_eq_one_div, hfr]

[Kim Morrison]

@Damiano Testa could you PR that last change to master? I'll hit merge instantly. :-)

[Damiano Testa]

#10979

[Damiano Testa]

I'll try to see if I can do some unfolding on master and try to reduce the work that the two field_simp do, but I am limited by time (it is getting late) and inability to work on nightly.

[Damiano Testa]

Scott, I tried to manually do the unfolding: #10980. My strategy was to replace lets by sets and use rw until dsimp told me that it was no longer able to simplify before each field_simp. I cannot test whether this fixes the proof on nightly-testing, though...

[Kim Morrison]

Okay, the PR adapting Mathlib to nightly-2024-02-26 is now up at https://github.com/leanprover-community/mathlib4/pull/10995.

[Kim Morrison]

(Thanks for the intense work of many over the last few days making this happen!)

[Kim Morrison]

There will still be further adaptations needed before Lean's next release candidate later this week, but this is the first time Mathlb has been in sync with Lean nightlies since the 15th, so it's progress. :-)

[Kim Morrison]

This can now use eyes!

[Kim Morrison]

• Please flag things that look wrong.
• Please fix things by pushing to the branch if you are confident!
• In practice it's best if changes get made simultaneously to this branch and to nightly-testing. (Cherry-pick?)

[Kim Morrison]

I can see already lots of things I am unhappy about. :-)

[Kim Morrison]

Note that it touches 651 files... this one is huge.

[Kim Morrison]

Something that has been useful in the past is to identify parts of the PR that could actually already be made on master. A very large fraction of the changes here do fall into that category. (All the additional arguments passed to simp, because simp no longer unfolds lets by default.)

[Kim Morrison]

We should think carefully about whether to do that now. Probably yes, but I want to be careful it doesn't cause unnecessary work.

The process would be:

• Take some subset of the changed files (which "you're sure are all only simp changes"), and make a PR to master with those changes.
• Post in this thread, get it on bors quickly.
• Once it lands in master, merge master into bump/v4.7.0 (this is always allowed), and then merge bump/v4.7.0 into bump/nightly-2024-02-26.
• The change that hit master will propagate automatically to nightly-testing, but as long as you didn't change anything when copying out of this PR, that will merge cleanly as all these changes are already there.

[Kim Morrison]

After that process, the diff that this PR displays should shrink.

[Kim Morrison]

Probably it is best to announce here if you can going to attempt such a transplant onto master.

[Kim Morrison]

Thus: I am going to see if I can backport all the changes to Counterexamples and Archive to master.

[Kim Morrison]

Okay, that seems to have worked perfectly: #10996

[Kim Morrison]

Process:

• git checkout master
• git merge --squash bump/nightly-2024-02-26
• revert all changes outside Archive and Counterexamples
• lake build Archive Counterexamples
• observe that there were some failures in Archive/Examples/IfNormalization/*, so revert those too
• lake build Archive Counterexamples :tada:
• branch, commit, push, open PR

[Kim Morrison]

Fantastic, and @Patrick Massot has sent it to bors.

I propose waiting a moment to make sure that the multi-step merge process works as expected, and assuming it does we then divide up the remaining simp changes and move them to master in a small number of PRs.

[Kim Morrison]

(Possibly just one.)

[Patrick Massot]

Do you want me to start preparing the simp changes branch?

[Patrick Massot]

git refuses to do git merge --squash bump/nightly-2024-02-26

[Patrick Massot]

That was a bad error message but it’s ok now. You first need to switch once to the bump branch.

[Kim Morrison]

@Patrick Massot, that would be amazing, thanks! I need to take a break for a bit now, so you won't be treading on my toes. :-)

[Patrick Massot]

Ok, I’ll try.

[Patrick Massot]

I need to stop and go to bed. I just opened #10999 which touches 291 files. I went until the logic folder.

[Patrick Massot]

We’ll see what see thinks of this selection.

[Patrick Massot]

It means I’ve done half the required work in one hour, that’s not too bad.

[Kim Morrison]

Great, I will review that now.

[Kim Morrison]

But first I will merge master into the bump branches.

[Kim Morrison]

Sigh, followed my own instructions, and unfortunately the diffs in Archive and Counterexamples still shows up.

[Kim Morrison]

Ahha! Forgot to push bump/v4.7.0 after merging master into it. That done, the Archive and Countexamples diffs have mostly disappeared.

[Kim Morrison]

In the end I had to revert some of the changes on Patrick's #10999.

[Kim Morrison]

Essentially, the changes where we add let bindings to simp_rw rather than simp don't work on master. Not sure why?

[Kim Morrison]

Ah: a super useful thing that someone could do on nightly-testing:

we have two regressions in pattern matching that show up in Algebra/Homology/Augment.lean (apparently independent problems, coincidentally in the same file!).

[Kim Morrison]

We need Mathlib free minimisations of these.

[Kim Morrison]

I may have a chance to work on this in about 6 hours, but not certain. If we can get minimisations today we can have them fixed in the 28 nightly, hopefully.

[Kim Morrison]

#11001 is the follow-up to Patrick's #10999, moving the rest of the simp changes that can be backported to master.

[Kim Morrison]

The PR description has a link to the diff (it is stacked on top of #10999, which is with bors now.)

[Kim Morrison]

Scott Morrison said:

I may have a chance to work on this in about 6 hours, but not certain. If we can get minimisations today we can have them fixed in the 28 nightly, hopefully.

oops, I have a minimisation of the first problem, I'll heopfully do the second one as well now.

[Johan Commelin]

Scott Morrison said:

#11001 is the follow-up to Patrick's #10999, moving the rest of the simp changes that can be backported to master.

I'll review it now.

[Johan Commelin]

@Scott Morrison I left a bunch of comments on that commit.

[Kim Morrison]

Thanks. I was not nearly as careful as I needed to be making sure only the trivial changes went in.

[Kim Morrison]

for #11001, I've just reverted all the changes the @Johan Commelin complained about.

[Kim Morrison]

Soon #10995 will be down to a manageable size, and we can do another pass looking for backportable stuff

[Kim Morrison]

and then get down to fixing the grungy stuff!

[Kim Morrison]

I've also merged master on #11001, so hopefully it is reviewable directly now.

[Kim Morrison]

Okay, asked the bot to merge if CI passes.

[Yaël Dillies]

Scott Morrison said:

Essentially, the changes where we add let bindings to simp_rw rather than simp don't work on master. Not sure why?

simp_rw already unfolds lets by default, and complains when a lemma does not simplify further

[Kim Morrison]

Of course, thanks.

[Ruben Van de Velde]

Scott Morrison said:

• Once it lands in master, merge master into bump/v4.7.0 (this is always allowed)

I tried that, but I'm "not authorized to push to this branch"

[Kim Morrison]

Interesting. I just pushed.

[Kim Morrison]

Maybe there is a branch protection rule?

[Kim Morrison]

Some attempt to parallelize here:

• Mathlib/Algebra/ContinuedFractions/Computation/CorrectnessTerminating.lean needs to be fixed, starting over. We don't want to use let __x := ..., instead we need to work out where to put the simp.
• similarly Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean
• (aside: are these continued fractions files maintainable? what should we do with them?)
• similarly, let __x := needs to be reverted in
  • Mathlib/FieldTheory/SeparableDegree.lean
  • Mathlib/LinearAlgebra/FreeModule/Norm.lean
• Mathlib/Algebra/Free.lean, I guess we could merge as is, but it would be great if someone could make a #mwe (failure to match on x * y) so we can get this fixed.
• same issue in Mathlib/Computability/RegularExpressions.lean
• Mathlib/Algebra/Homology/Augment.lean has sorries, but will be fixed upstream tomorrow
• are we worried about Mathlib/Algebra/GroupWithZero/Units/Basic.lean? Someone could see if there is a better fix, and/or try to get to the bottom of the change?
• Mathlib/LinearAlgebra/PiTensorProduct.lean and Mathlib/Order/CompactlyGenerated/Basic.lean still needs a solution: how to get aesop to unfold lets?

[Kim Morrison]

I realise that just waiting for the fix tomorrow for Algebra/Homology/Augment is not really going to work. nightly-testing is already broken again after 2024-02-27 arrived today.

[Kim Morrison]

I would really like to get this batch of fixes in, without having to add those to the mix.

[Kim Morrison]

So I think the only was we can achieve this is having sorries on bump/v4.7.0,just for Augment.

[Kim Morrison]

Not great, but the alternative is pretty unpleasant.

[Johan Commelin]

Would those sorries also be on master?

[Kim Morrison]

No.

[Kim Morrison]

Because once we fix mathlib for 2024-02-27, we will be able to move to 2024-02-28, which will contain the fixes to those sorries.

[Kim Morrison]

And Mathlib master will only ever see v4.7.0-rc1, which is NET 2024-02-29. :-)

[Johan Commelin]

ok, understood

[Johan Commelin]

Then it isn't too bad, right?

[Kim Morrison]

I need to sleep now. I've gone most of the way through #10995 (up to test/observe.lean). Besides FIXME nightly-testing notes, the list above, and comments on the PR, I am otherwise happy.

[Kim Morrison]

If anyone has time to address some of these, that would be great.

[Kim Morrison]

It's also possible to work on nightly-testing directly, to deal with the new breakages that are already there from 2024-02-27. There are breakages. I fixed one, and will look at it more tomorrow.

[Anne Baanen]

Let me start with Mathlib/FieldTheory/SeparableDegree.lean.

[Anne Baanen]

Next up: LinearAlgebra/FreeModule/Norm.lean.

[Anne Baanen]

Anne Baanen said:

Let me start with Mathlib/FieldTheory/SeparableDegree.lean.

Oops, I thought it worked on my machine. Let me try again...

[Anne Baanen]

After lunch I will see if I can do something with the continued fractions.

[Michael Stoll]

Side remark: My impression when looking at the Continued Fractions files a while ago was that they are overly "heavy" and perhaps too much inspired by CS data structure think. I think it would be good to have a more light-weight implementation of (regular) continued fractions of real numbers that is easier to use (with glue to relate it to the more general existing stuff). I did a very limited amount of that with docs#Real.convergent already, which I could extend (this would also be helpful for adding material relating Pell's Equation to continued fractions, from a recent BSc thesis of a student of mine), if there is interest/approval.
Of course, this is not very much related to the problems discussed in this thread :smile:

[Anne Baanen]

To unfold let bindings in aesop, you can write by aesop (add norm simp [f, g]).

[Yaël Dillies]

I made the same diagnosis of the continued fractions material ages ago but I think I never even tried to refactor it

[Anne Baanen]

So I think that's all from me today, the following I haven't looked at:

Scott Morrison said:

• Mathlib/Algebra/Free.lean, I guess we could merge as is, but it would be great if someone could make a #mwe (failure to match on x * y) so we can get this fixed.
• same issue in Mathlib/Computability/RegularExpressions.lean
• Mathlib/Algebra/Homology/Augment.lean has sorries, but will be fixed upstream tomorrow
• are we worried about Mathlib/Algebra/GroupWithZero/Units/Basic.lean? Someone could see if there is a better fix, and/or try to get to the bottom of the change?

[Kim Morrison]

Thank you Anne, that's great. I'll get started shortly.

[Kyle Miller]

Scott Morrison said:

Some attempt to parallelize here:

• Mathlib/Algebra/ContinuedFractions/Computation/CorrectnessTerminating.lean needs to be fixed, starting over. We don't want to use let __x := ..., instead we need to work out where to put the simp.
• similarly Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean
• (aside: are these continued fractions files maintainable? what should we do with them?)
• similarly, let __x := needs to be reverted in
  • Mathlib/FieldTheory/SeparableDegree.lean
  • Mathlib/LinearAlgebra/FreeModule/Norm.lean

I'm really confused -- I pushed all these fixes to nightly-testing hours before you sent this message.

[Kyle Miller]

Where did @Anne Baanen push their changes?

[Ruben Van de Velde]

#10995

[Kyle Miller]

OK, I think I finished merging our changes, and hopefully nightly-testing merges without conflicting.

[Kim Morrison]

Sorry about the confusion between nightly-testing and #10995. The problem we have now is that nightly-testing is already testing 2024-02-27.

[Kim Morrison]

I think it's best going forward if fixes that can be made on #10995 happen there first, and then we merge to nightly-testing.

[Kim Morrison]

(Because the other direction is not possible, as nightly-testing will accumulate changes specific to 2024-02-27 and later.)

[Kim Morrison]

I've fixed IfNormalization. The simp proofs were going a slightly different direction, and to get the automation back on track I needed to add

@[simp] theorem lookup_insert_eq_none {l : AList β} {k k' : α} {v : β k} :
    (l.insert k v).lookup k' = none ↔ (k' ≠ k) ∧ l.lookup k' = none := by

which seems reasonable enough.

[Kim Morrison]

The WithoutAesop proof still needs a bit more help after simp used to finish, but at least there's no regression in the aesop showcase now.

[Kim Morrison]

I just fixed it better, after regenerating the simp says statements. They can be confusing when fixing a proof!!

[Kim Morrison]

I'm just going through the files one by one now, and on this pass everything looks good.

[Kim Morrison]

I'm hoping we can merge soon.

[Kim Morrison]

Okay, I would like to get #10995 merged!

[Kim Morrison]

It all looks good to me. There are remaining issues, but we have fixes in for all of them, due for nightly-2024-02-28 in a few hours.

[Kim Morrison]

We nevertheless need to merge this as is (as discussed with Johan above), because there are more breakages on nightly-testing coping with 2024-02-27 that are still unresolved.

[Kim Morrison]

So, for requests from others:

#1 priority is to do the final review of this and do a squash merge (no bors necessary).
#2 priority is to find out what is breaking nightly-2024-02-27!

[Kyle Miller]

Taking a look

[Kyle Miller]

@Scott Morrison I just pushed two changes that compile locally and shouldn't change anything. Is it safe to go ahead and squash merge now, or should I wait for CI?

[Matthew Ballard]

I left some comments.

[Kim Morrison]

Thanks, @Matthew Ballard, looking now.

[Kim Morrison]

re: nightly-testing: I've minimised the issue in Mathlib/Order/Closure, and Leo is looking into it. There are many other failures!

[Matthew Ballard]

Is ZeroMorphisms not building?

[Thomas Murrills]

Mathlib/Algebra/Free.lean, I guess we could merge as is, but it would be great if someone could make a #mwe (failure to match on x * y) so we can get this fixed

This is actually due to a consumeMData fix, I think. binop% was adding metadata and bypassing the check. Nvm; see below. MWE:

import Lean

class Test (α) where test : α → α → α

infixl:50 "%&%" => Test.test
macro_rules | `($a %&% $b) => `(term|Test.test $a $b)

inductive Foo (α : Type u) where
| foo : Foo α → Foo α → Foo α

instance : Test (Foo α) := ⟨Foo.foo⟩

example : Foo α → True
| Test.test x y => trivial -- invalid pattern

example : Foo α → True
| x %&% y => trivial -- invalid pattern

macro_rules | `($a %&% $b) => `(term|binop% Test.test $a $b)

example : Foo α → True
| x %&% y => trivial -- works (and shouldn't)

[Kim Morrison]

Okay, sounds good. Shall I strip out the comments about it, then?

[Thomas Murrills]

It essentially goes with the porting note in Mathlib.Algebra.Free: the fact that match_pattern can't be added to Mul.mul here anymore is what forces us to not use the notation. Maybe call it a porting note and refer to the one above?

[Matthew Ballard]

Matthew Ballard said:

Is ZeroMorphisms not building?

Wrong branch :skull:

[Kyle Miller]

binop% doesn't add metadata, or am I mistaken?

[Thomas Murrills]

(It would be nice to have match_pattern for all of our notation anyway! We add it explicitly for addition (but nothing else) here.)

[Thomas Murrills]

Kyle Miller said:

binop% doesn't add metadata, or am I mistaken?

Ah, you might be right. My diagnosis might be too hasty; let me check.

[Kyle Miller]

binop% is special cased as a pattern: https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/PatternVar.lean#L161

[Thomas Murrills]

Hmm, interesting. So that might be a bug after all.

[Kim Morrison]

@Matthew Ballard et al, I've responded to these comments. My flag is up for merging this one again!

[Thomas Murrills]

Thomas Murrills said:

Hmm, interesting. So that might be a bug after all.

Oh, I see, it is intentional: the following check that the binop operator is necessarily registered with match_pattern anyway was added last week: https://github.com/leanprover/lean4/commit/a0089d466760122295d4b1dabe4bd3e931222415

[Kim Morrison]

@Kyle Miller, @Thomas Murrills, I think we're going to merge now, you're okay with any binop modifications happening later?

[Kyle Miller]

@Scott Morrison I'd say it's working by design.

I've looked through all the changes in the PR a couple times, and I'm happy to squash merge it.

[Kyle Miller]

Should I wait for CI, or can I do it now?

[Kim Morrison]

Let's wait for CI.

[Kim Morrison]

Leo is going to add a flag for simp (and I guess also rw) that enables the old behaviour re: instance arguments.

[Kim Morrison]

Our plan is to initially patch Mathlib just by using this flag at every error. (oooh, can I automate?)

[Kim Morrison]

These flags will end up in master, and will be a new form of debt Mathlib needs to pay down...

[Thomas Murrills]

(Btw, seeing as the binop% check is intentional, I think what we want is simply to add [match_pattern] to some (all?) of the other basic binary operators in Init.Prelude!)

[Thomas Murrills]

Thread: #lean4 > @[match_pattern] for basic binary operators

[Kyle Miller]

@Scott Morrison There are just a few errors left in tests, for rewrite search and some simp? says in test/matrix

[Thomas Murrills]

Looks like the two simp? ... says tests both have simp? inserting the Fin.isValue simproc into simp only. Interestingly, this can be removed from the simp only without affecting the state after it at all. Does this deserve a note?

[Kyle Miller]

Not sure

[Kyle Miller]

(And I just pushed fixes. Hopefully CI passes now.)

[Kyle Miller]

It's long been the case that sometimes there are simp lemmas that simp uses that aren't necessary for simp to simp, but there's nothing wrong with that. I think simprocs aren't very different in that regard.

[Kyle Miller]

It seems we're going to see a bit of noise here in the future, since Fin.isValue normalized literals to use the Lean core instance from the Mathlib one.

import Mathlib
set_option pp.all true
example (n : Fin 5) : n = 3 := by
  simp only [Fin.isValue]
  simp -- simp made no progress

[Kyle Miller]

Merged #10995 into branch#bump/v4.7.0

[Kim Morrison]

@David Renshaw I'm hoping I might be able to ask for some assistance with field_simp.

[Kim Morrison]

It is breaking on #11070.

[Kim Morrison]

This is our attempt to get Mathlib onto nightly-2024-02-29.

[Kim Morrison]

There seems to be some interaction with the field_simp discharger and the changes in lean#3523. I don't actually see a logic change in lean#3523, but it's certainly possible there is one there.

[Kim Morrison]

So far my efforts have been looking at the output of set_option trace.Meta.Tactic.simp true in in the failing test on #11070 in test/FieldSimp.lean.

[Kim Morrison]

The relevant difference in the trace is that on master we get:

[Meta.Tactic.simp.rewrite] @ne_eq:1000, 4 * x ^ 2 ≠ 0 ==> ¬4 * x ^ 2 = 0


[Meta.Tactic.simp.rewrite] @ne_eq:1000, x ^ 2 ≠ 0 ==> ¬x ^ 2 = 0


[Meta.Tactic.simp.rewrite] @pow_ne_zero:1000, x ^ 2 = 0 ==> False


[Meta.Tactic.simp.rewrite] not_false_eq_true:1000, ¬False ==> True


[Meta.Tactic.simp.rewrite] @mul_ne_zero:1000, 4 * x ^ 2 = 0 ==> False


[Meta.Tactic.simp.rewrite] not_false_eq_true:1000, ¬False ==> True


[Meta.Tactic.simp.rewrite] @div_eq_iff:1000, x * (3 * x ^ 3) ^ 2 * (2 * x) ^ 3 / (4 * x ^ 2) =
      18 * x ^ 8 ==> x * (3 * x ^ 3) ^ 2 * (2 * x) ^ 3 = 18 * x ^ 8 * (4 * x ^ 2)

(i.e. this is simp discharging the side condition of div_eq_iff, and then successfully rewriting by it)

[Kim Morrison]

where on #11070 it fails as:

[Meta.Tactic.simp.discharge] @div_eq_iff discharge ❌
      4 * x ^ 2 ≠ 0 ▼
  [rewrite] @ne_eq:1000, 4 * x ^ 2 ≠ 0 ==> ¬4 * x ^ 2 = 0
  [] @mul_ne_zero discharge ❌ max depth
        4 ≠ 0
  [unify] @eq_self:1000, failed to unify
        ?a = ?a
      with
        4 * x ^ 2 = 0
  [unify] @OfNat.ofNat_eq_ofNat:1000, failed to unify
        OfNat.ofNat ?m = OfNat.ofNat ?n
      with
        4 * x ^ 2 = 0
  [unify] @OfNat.ofNat_ne_zero:1000, failed to unify
        OfNat.ofNat ?n = 0
      with
        4 * x ^ 2 = 0
  [unify] @mul_right_eq_self:1000, failed to unify
        ?a * ?b = ?a
      with
        4 * x ^ 2 = 0
  [unify] @mul_left_eq_self:1000, failed to unify
        ?a * ?b = ?b
      with
        4 * x ^ 2 = 0
  [unify] @mul_eq_left₀:1000, failed to unify
        ?a * ?b = ?a
      with
        4 * x ^ 2 = 0
  [unify] @mul_eq_right₀:1000, failed to unify
        ?a * ?b = ?b
      with
        4 * x ^ 2 = 0
  [] @IsLeftRegular.mul_left_eq_zero_iff discharge ❌ max depth
        IsLeftRegular 4
  [] @IsRightRegular.mul_right_eq_zero_iff discharge ❌ max depth
        IsRightRegular (x ^ 2)

[Kim Morrison]

I'm only picking on David here because he did the port of field_simp to Lean 4. If anyone else would like to take a look, I think I'm stuck.

[Kim Morrison]

Adding some logInfos for the four strategies in field_simp's discharge, I see quite different behaviour on master and on #11070:

On master:

discharge 1: 4 * x ^ 2 ≠ 0
discharge 2: 4 * x ^ 2 ≠ 0
discharge 3: 4 * x ^ 2 ≠ 0
discharge 4: 4 * x ^ 2 ≠ 0
discharge 1: 4 ≠ 0
discharge 2: 4 ≠ 0
discharge 3: 4 ≠ 0
discharge 1: x ^ 2 ≠ 0
discharge 2: x ^ 2 ≠ 0
discharge 3: x ^ 2 ≠ 0
discharge 4: x ^ 2 ≠ 0
discharge 1: x ≠ 0

On #11070:

discharge 1: 4 * x ^ 2 ≠ 0
discharge 2: 4 * x ^ 2 ≠ 0
discharge 3: 4 * x ^ 2 ≠ 0
discharge 4: 4 * x ^ 2 ≠ 0
discharge 1: 4 * x ^ 2 ≠ 0
discharge 2: 4 * x ^ 2 ≠ 0
discharge 3: 4 * x ^ 2 ≠ 0
discharge 4: 4 * x ^ 2 ≠ 0

[Kyle Miller]

It looks like there are two logic changes in lean#3523.

1. now when synthesizing simp lemma args, the max discharge depth is respected
2. this line is no longer protected by a try/catch

The second change doesn't seem to be affecting the trace, but the max depth errors do seem related.

[Kim Morrison]

Yep, just got it.

[Kim Morrison]

Previously the max discharge depth was never being checked.

[Kim Morrison]

and field_simp was relying on going well past the default of 2.

[Kyle Miller]

I guess that's basically hardcoded to maxDischargeDepth : Nat := 2

[Kim Morrison]

setting it higher, everything works.

[Kim Morrison]

Thanks @Kyle Miller

[Kim Morrison]

Okay, #11070 is nearly ready to go.

There is a serious problem left over for afterwards. (Could someone adopt it at least to the extent of writing an issue?)

field_simp is a very ambitious tactic, that tries to prove that it can clear denominators. Previously it was taking advantage of essentially a bug in the simp discharging framework, so that parts of its discharging strategy were not limited by maxDischargeDepth (so it could "keep trying"), but everyone else was limited (so simp didn't waste time exploring large trees of discharges). Now the maxDischargeDepth is enforced for everyone, so to keep field_simp working we have to increase its maxDischargeDepth. That makes it extremely slow. I've kept the maxDischargeDepth to a minimum, but still there are some set_option maxHeartbeats (all with notes attached), and Archive/SolutionOfCubic.lean apparently needs an even higher depth, so has a sorried proof.

After we've merged this, someone is going to have to rewrite field_simp to make it performant.

In the meantime, we need to decide what to do in SolutionOfCubic. Could someone just patch the sorry by hand?

[Kim Morrison]

Besides this issue, I would be happy to have review / delegation on #11070.

[Johan Commelin]

Do we have a field_simp?. Is that easy to create?

[Kim Morrison]

We don't. It wouldn't be particularly hard, I guess.

[Johan Commelin]

I'll review #11070 now.

[Kim Morrison]

field_simp looks like it is set up to allow a config := {...} argument, but I just get an error about a sorry when I try to use it.

[Kim Morrison]

If that worked, we could locally set the maxDischargeDepth even higher for particularly broken invocations of field_simp (e.g. SolutionsOfCubic).

[Johan Commelin]

@Scott Morrison Could you please update the PR commit message?

[Johan Commelin]

@Scott Morrison I left a review. Just 2 more comments, on top of the outstanding ones.

[Johan Commelin]

I'm trying to get rid of that one field_simp on master, atm

[Kim Morrison]

I don't know the answers to any of the current queries. :-) They will require looking at the code and comparing to bump/v4.7.0 and/or master.

When I next have time for the Mathlib sync, I'm going to look at nightly-testing on 2024-03-01. We still have two major outstanding issues:

• the frequent crashes in VSCode, hopefully fixed with the next nightly
• the VSCode server startup time doubled (for Mathlib) between v4.5.0 and v4.6.0, (in particularly, on nightly-2024-02-01), and we need to track this down to fix it for v4.7.0-rc1.

[Johan Commelin]

@Scott Morrison I don't have caches, so I can't test on nightly-testing, but does the following work

  have hq' : q = (9 * (b / a) * (c / a) - 2 * (b / a) ^ 3 - 27 * (d / a)) / 54 := by
    rw [hq, h54]
    simp [field_simps, ha]
    ring_nf

[Johan Commelin]

Or is the simp [field_simps, ha] still too evil?

[Kim Morrison]

No, I tried quite a few variations of that, and couldn't get it to work.

[Kim Morrison]

(I've lost my cache, so haven't literally tried that, but I'm pretty sure I covered it.)

[Johan Commelin]

But there are no dischargers involved anymore...

[Johan Commelin]

So is ring_nf now the issue?

[Kim Morrison]

so the simp lemmas don't fire

[Kim Morrison]

The point is that all the lemmas in field_simps have side conditions.

[Kim Morrison]

Which need a very ... enthusiastic, let's say ... discharger.

[Johan Commelin]

Yes, but this proof no longer uses fancy dischargers

[Johan Commelin]

Just the standard one that simp uses.

[Kim Morrison]

So why do you expect that the simp lemmas in field_simps will apply?

[Kim Morrison]

I'm about 2 minutes from oleans for that file again, so I can try shortly, in any case.

[Kim Morrison]

Oh -- -you are saying that works on master?

[Johan Commelin]

Yes

[Kim Morrison]

Sorry, I'm an idiot.

[Kim Morrison]

Yes, this should work then.

[Kim Morrison]

Nothing else has changed.

[Johan Commelin]

  have hq' : q = (9 * (b / a) * (c / a) - 2 * (b / a) ^ 3 - 27 * (d / a)) / 54 := by
    rw [hq, h54]
    simp only [mul_div_assoc', div_mul_eq_mul_div, div_div, div_pow, ne_eq, OfNat.ofNat_ne_zero,
      not_false_eq_true, pow_eq_zero_iff, ha, sub_div', mul_eq_zero, or_self, div_sub', two_ne_zero,
      three_ne_zero, eq_div_iff, div_eq_iff]
    ring_nf

if you want the squeezed version

[Kim Morrison]

@Johan Commelin, that worked, and pushed.

[Johan Commelin]

So now the branch is sorry-free?

[Kim Morrison]

I think so.

[Kim Morrison]

"Just" a matter of cleaning up the mystery edits. :-)

[Michael Rothgang]

I just went over the diff again; I think the number of remaining mystery edits is very small.

[Michael Rothgang]

(There's a build error in Algebra/Homology/HomotopyCategory/DegreewiseSplit.lean.)

[Michael Rothgang]

Is help fixing the mystery edits welcome? If so, I can try.

[Johan Commelin]

Yes, please go ahead!

[Michael Rothgang]

I have fixed most of them and pushed.
Then I realised this throws away all work on CI creating olean's. (Can/should this be fixed, to at least upload the cache? At least for such PRs, this would be rather helpful. I understand that for a typical feature PR, it's not necessary.)

[Kim Morrison]

Yes, I think back in mathlib3 days we had a trick that CI would respond to the cancellation request by uploading any available oleans before shutting down, but that we no longer have this. It would be great!

[Michael Rothgang]

Did #8987 change the logic? (I could have sworn this changed somewhat recently; that PR matches my intuition.)

[Michael Rothgang]

#11079 is backporting a handful of changes to master. Not a big deal, but should be quick to merge.

[Michael Rothgang]

Michael Rothgang said:

(There's a build error in Algebra/Homology/HomotopyCategory/DegreewiseSplit.lean.)

This one is strange: it doesn't happen for me locally...

[Yaël Dillies]

Scott Morrison said:

Now the maxDischargeDepth is enforced for everyone

Why can't we have maxDischargeDepth be a setting on each simp call?

[Johan Commelin]

Scott Morrison said:

field_simp looks like it is set up to allow a config := {...} argument, but I just get an error about a sorry when I try to use it.

@Yaël Dillies It should be, but... :this:

[Yaël Dillies]

I read that message but I don't see how it's related: Scott is talking about configuring a specific field_simp call, I'm talking about configuring the simp call inside the definition of field_simp

[Michael Stoll]

Scott Morrison said:

After we've merged this, someone is going to have to rewrite field_simp to make it performant.

If somebody is going to rewrite field_simp, I would like to suggest it be written in such a way that it collects all non-zeroness requirements as side goals (or at least have this as a configurable option) instead of not normalizing terms completely when it cannot show that some denominator does not vanish. Right now, it is sometimes difficult to figure out exactly what term it needs to be non-zero, which leads to a trial-and-error loop to find out what needs to be in the context so that field_simp works as expected. With the suggestion above, the relevant conditions will be clear and can be discharged afterwards.

[Kim Morrison]

Yaël Dillies said:

I read that message but I don't see how it's related: Scott is talking about configuring a specific field_simp call, I'm talking about configuring the simp call inside the definition of field_simp

@Yaël Dillies, yes, please go ahead once this reaches master.

[Kim Morrison]

Thanks @Michael Rothgang and @Johan Commelin for the recent work, I think #11070 may be ready to go in?

[Kim Morrison]

I think I have nightly-testing almost ready on nightly-2024-03-01 (much easier bump!) so there'll be another one to follow close behind.

[Johan Commelin]

@Scott Morrison :peace_sign:

[Kim Morrison]

We haven't had a green tick yet on this, but as I'm going to bed, I'm going to optimistically set it to auto-merge-after-CI.

[Johan Commelin]

Ok, sleep tight!

[Kim Morrison]

nightly-testing is building on 2024-03-01. It's going to take at least one more nightly before the release of v4.7.0-rc1, and we want to fix the startup time regression.

[Kim Morrison]

I'll make the bump/nightly-2024-03-01 sometime over the weekend.

[Yaël Dillies]

Scott Morrison said:

Yaël Dillies said:

I read that message but I don't see how it's related: Scott is talking about configuring a specific field_simp call, I'm talking about configuring the simp call inside the definition of field_simp

Yaël Dillies, yes, please go ahead once this reaches master.

I'm not closely following (pretty busy with Part III right now :grimacing:), but somebody pings me when it's on master, I'll happily do it.

[David Renshaw]

mathlib4#11087 fixes the config elaboration issue

[David Renshaw]

That makes it possible to explicitly specify maxDischargeDepth.

[Patrick Massot]

This syntax elaboration is really cursed, we already had #8165 for the discharger syntax.

[Kim Morrison]

@Damiano Testa, just a heads up the compute_degree is nearly always broken without the backwards compatibility flag set_option tactic.skipAssignedInstances false.

Do you think you'll be able to look into this after this lands in master? (Hopefully that will be within the next day or two.)

[Damiano Testa]

I may have some time this afternoon (in approx 6-7 hours).

Just to be clear, I should look at the compute_degree failures on nightly-testing and try to solve them by only using the set_option mentioned above, if I can. Is that correct?

[Eric Rodriguez]

I think you should try fix it without flag on is what they're saying

[Damiano Testa]

Ah, ok, I think that I understand. The tactic had been "fixed" by adding the set_option, but now I should make sure that the tactic actually works, removing the need for the set_option.

Indeed this makes more sense.

[Kim Morrison]

Ooof. I thought we were close on https://github.com/leanprover-community/mathlib4/pull/11070 (this is the bump to nightly-2024-02-29), but there there are a bunch of linter errors still to go.

Any help with these much appreciated.

[Kim Morrison]

(It is not surprising I guess, that there are cases where simp is proceeding now, using an instance found by unification that otherwise at that moment couldn't be found by inference?)

[Kim Morrison]

It appears that simply removing @[simp] from everything the linter complains about, Mathlib still works. I am inclined to interpret this as the linter giving good advice, and proceed.

[Michael Rothgang]

There were two remaining errors by the simpNF linter. I pushed a fix to the first; the second (the left-hand side reduces to XYZ') one is harder: replacing the left hand side by XYZ yields an error

type mismatch
DFinsupp.sum W₀ fun a b ↦ (linearIsometryEquiv hV) ((V a) b)
has type
↥(lp G 2) : Type (max u_1 u_4)
but is expected to have type
Π₀ (i : ι), G i : Type (max u_1 u_4)

Original linter error message is

  ↑((IsHilbertSum.linearIsometryEquiv hV) (DFinsupp.sum W₀ fun i => ⇑(V i)))
to
  ↑(DFinsupp.sum W₀ fun a b => (IsHilbertSum.linearIsometryEquiv hV) ((V a) b))

[Damiano Testa]

Investigating the compute_degree issues, they all appear to be a consequence of a simp call inside it and then norm_num failures. Here are a couple of examples:

import Mathlib.Tactic.NormNum.Core
import Mathlib.GroupTheory.Subsemigroup.Basic

example :       0 < 1 := by norm_num -- works!
--set_option tactic.skipAssignedInstances false
example : max 0 0 ≤ 1 := by norm_num -- times out
example :       0 ≤ 1 := by norm_num -- times out
/-
  tactic 'simp' failed, nested error:
  (deterministic) timeout at 'whnf', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
-/

Note that the imports have been minimised:

• removing NormNum.Core means that norm_num does not exist;
• importing all the import of Semigroup.Basicinstead of Semigroup.Basic itself means that norm_num works as intended;
• uncommenting the set_option makes norm_num work.

[Damiano Testa]

Trying to minimise further, in Subsemigroup.Basic there is this lemma:

@[to_additive (attr := simp)]
theorem subsingleton_of_subsingleton [Subsingleton (Subsemigroup M)] : Subsingleton M := by
  constructor; intro x y
  have : ∀ a : M, a ∈ (⊥ : Subsemigroup M) := by simp [Subsingleton.elim (⊥ : Subsemigroup M) ⊤]
  exact absurd (this x) not_mem_bot

and removing the (attr := simp) from it, fixes the time out above. I have not tested whether this would fix the compute_degree issues, though, since I am waiting for the intermediate files to build.

[Damiano Testa]

Tested: removing the simp attribute above does not cause further breakage and "fixes" compute_degree!

[Damiano Testa]

(further breakage in the path to compute_degree, I do not know about the rest of mathlib).

[Damiano Testa]

I pushed the change to #11107. However, if this works, the relevant patch is 51da0513b468f47b974b0aa874ca730371f70416 and presumably simply cherry-picking it would fix compute_degree.

Update: mathlib built on #11107 so I added the patch to #11070.

[Damiano Testa]

Still it does not lint! However, I do not have more lean time today... Still, the compute_degree issue should be fixed!

[Michael Rothgang]

Damiano Testa said:

Still it does not lint! However, I do not have more lean time today... Still, the compute_degree issue should be fixed!

The remaining linter error is the one from this message. (I don't know how to fix that one.)

[Thomas Murrills]

I pushed a potential fix—I don't have the computing power to build everything else locally, though, so I'm using CI.

[Thomas Murrills]

I replaced the lhs with ((W₀.sum (γ := lp G 2) fun a b => hV.linearIsometryEquiv (V a b)) : ∀ i, G i). The simpNF linter says the original lhs ((hV.linearIsometryEquiv (W₀.sum fun i => V i) : ∀ i, G i)) simplifies via simp only [_root_.map_zero, implies_true, map_dfinsupp_sum] to something that's not obviously the same as what I replaced it with; to justify the change, note that the following works:

example (hV : IsHilbertSum 𝕜 G V) (W₀ : Π₀ i : ι, G i) :
  ((W₀.sum (γ := lp G 2) fun a b => hV.linearIsometryEquiv (V a b)) : ∀ i, G i) =
    (hV.linearIsometryEquiv (W₀.sum fun i => V i) : ∀ i, G i) := by
  simp only [map_dfinsupp_sum] -- I guess `_root_.map_zero`, `implies_true` were unused?
  -- closed by rfl

[Damiano Testa]

Bors took over the PR! Thank you all: my contribution has been to remove one simp attribute: pretty minimal effort compared to what everyone else did!

[Damiano Testa]

It turns out that I had fixed the issue with compute_degree, but did not push the removal of the set_options outside of test. I created #11123 where CI successfully built Mathlib, Archive and Counterexamples.

[Kim Morrison]

Okay, we are getting very close now!

[Kim Morrison]

I've created #11125, which will bring bump/v4.7.0 up to nightly-2024-03-02. The diff looks fine to me (mostly the diff is because of my perhaps ill-considered addition of protected to Nat.pow_succ).

[Kim Morrison]

If someone could delegate, I will hopefully be able to shepherd it through CI.

[Kim Morrison]

(It is possible, but I'm not promising, that nightly-2024-03-02 will become the next release candidate. I don't know of any obstacles at present, but will do a last "readiness poll". :-)

[Kim Morrison]

We again have some significant failures on Mathlib's nightly-testing branch. We are currently moving to nightly-2024-03-07, which includes lean4#3616. To be honest, at this point I don't understand how there is so much fallout from that PR, so as well as fixes to proofs, I'm also happy to hear an account of what is actually going wrong!

[Kim Morrison]

I've been pushing basic fixes to nightly-testing.

[Kim Morrison]

I'm also going to ping a few people here to ask for some assistance. I'm picking people here mostly on the basis of being authors of files --- please don't hesitate to jump in just because I'm not pinging you directly. :-)

• Mathlib/CategoryTheory/ComposableArrows has many cases where something used to work by dsimp, and no longer does. @Joël Riou?
• Mathlib/CategoryTheory/Bicategory/Functor has a timeout that I haven't investigated. We may have to unpack some proofs by aesop_cat so we can see what is going wrong. @Yuma Mizuno?
• Mathlib/Data/Sum/Intervals has a simp only proof that is failing, and I'm not sure what to either add, or blame for not working. @Yaël Dillies?
• Mathlib/Algebra/Homology/Augment looks like a failure of a Nat.rec to simplify that should, and may represent a bug introduced in lean4#3616? It might be work minimising this one if possible.
• Mathlib/Ordinal/SetTheory/Basic: Here succ_one used to be rfl, then was an unfold and simpa, and now is broken.
• Mathlib/Topology/Support: a problem with @[to_additive] and numerals. @Floris van Doorn?
• Mathlib/CategoryTheory/Abelian/InjectiveResolution: a simp only that no longer fires, while the simp times out. @Jujian Zhang?
• Mathlib/Analysis/Convex/Basic: a typeclass has gone missing? @Alexander Bentkamp or @Yury G. Kudryashov?

[Kim Morrison]

I'm away over the weekend, so won't be able to coordinate or contribute much on this thread until next Tuesday.

[Patrick Massot]

@Scott Morrison I investigated the Data/Sum/Interval one. The failure clearly comes from lean4#3508.

[Patrick Massot]

A proof the work in the testing branch is

simp only [nonempty_iff_ne_empty, Ne, sumLift₂_eq_empty, not_and_or, not_forall, exists_prop]

[Patrick Massot]

Do you want to use this proof or reconsider the Lean 4 change?

[Patrick Massot]

I guess that changing that kind of simp lemmas can explain a lot of random breakage (but I don’t claim those changes are bad, I didn’t look closely and it’s getting late here).

[Kim Morrison]

Something is not right

[Kim Morrison]

3508 landed in the previous night ly, which

[Kim Morrison]

We already have a merged addition PR for.

[Jujian Zhang]

For InjectiveResolution.lean:

lemma ofCocomplex_exactAt_succ (n : ℕ) :
    (ofCocomplex Z).ExactAt (n + 1) := by
  rw [HomologicalComplex.exactAt_iff' _ n (n + 1) (n + 1 + 1) (by simp) (by simp)]
  cases n
  all_goals
    dsimp only [ofCocomplex, CochainComplex.mk', CochainComplex.mk, CochainComplex.of, Nat.zero_eq,
      HomologicalComplex.sc', HomologicalComplex.shortComplexFunctor', eqToHom_refl, dite_eq_ite]
    simp only [Nat.reduceAdd, zero_add, ↓reduceIte, comp_id]
    apply exact_f_d

Fixes the error

[Joël Riou]

For Mathlib/CategoryTheory/ComposableArrows, I have this quick fix https://github.com/leanprover-community/mathlib4/commit/f3eeb3e5b010861f6e9efdf95de26c7282e3419d
However, I had to add a lot of simp lemmas: in order to have dsimp unfold inductive definitions involving Fin, I used to only have to take care of special cases of 0 and 1, as the bigger numbers could be handled by a simp lemma for elements ⟨i + 1, _⟩. Now it seems I would need a lemma for 2, 3, 4, etc. Then, my fix maybe not be the best solution.

[Kim Morrison]

We are way behind again.

There is some proof repair needed in Mathlib/Data/Nat/Cast/Defs.lean. Previously where succ was being produced by cases we are getting +1 (hooray!), but the fragile proof that follows which relied on this behaviour is now broken.

[Kim Morrison]

@Joël Riou, any chance you might be able to try minimizing this to show how the behaviour has changed? It does sound like we will need to get changes in Lean for this.

[Kim Morrison]

@Mario Carneiro, there are some errors in Mathlib/Computability/TMToPartrec.lean, could you take a look at these?

[Kim Morrison]

Jujian Zhang said:

For InjectiveResolution.lean:

lemma ofCocomplex_exactAt_succ (n : ℕ) :
    (ofCocomplex Z).ExactAt (n + 1) := by
  rw [HomologicalComplex.exactAt_iff' _ n (n + 1) (n + 1 + 1) (by simp) (by simp)]
  cases n
  all_goals
    dsimp only [ofCocomplex, CochainComplex.mk', CochainComplex.mk, CochainComplex.of, Nat.zero_eq,
      HomologicalComplex.sc', HomologicalComplex.shortComplexFunctor', eqToHom_refl, dite_eq_ite]
    simp only [Nat.reduceAdd, zero_add, ↓reduceIte, comp_id]
    apply exact_f_d

Fixes the error

Indeed, it does, thank you! This lemma, and indeed a lot of this file, is extremely slow.

[Kim Morrison]

Okay, these are the files that are currently broken and blocking progress.

I'm tagging for each question the listed author(s) of the file, in the hope that you might either fix the problem on nightly-testing, or ping someone else who might be able to take a look.

(These authors lists I think also demonstrate that these lists are often out of date, and we need a better system of ownership of code for maintenance problems like these.)

But please, anyone who is able, feel free to jump in on these. I've tried to say which ones are hopefully easy.

• Mathlib/Data/Sum/Interval.lean: has a simp only proof that is failing, and I'm not sure what to either add, or blame for not working. @Yaël Dillies?
• Mathlib/GroupTheory/Perm/List.lean: a failure because a fragile proof is relying on a distinction between k+1 and k.succ which has disappeared now that we have nicer handling on induction in Nat. @Yakov Pechersky? Fixed by Patrick.
• Mathlib/SetTheory/Ordinal/Basic.lean: Here succ_one used to be rfl, then was an unfold and simpa, and now is broken. @Mario Carneiro or @Floris van Doorn?
• Mathlib/Computability/TMToPartrec.lean, as above
• Mathlib/Data/Nat/Multiplicity.lean: hopefully an easy repair, Lean is getting caught up on 1 vs 0+1. @Chris Hughes
• Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean: hopefully easy, just have to be careful with +1 vs succ. @Aaron Anderson, @Jalex Stark, @Kyle Miller Fixed by Kyle.
• Mathilb/Analysis/Convex/Basic.lean: not sure what is happening here. @Alexander Bentkamp, @Yury G. Kudryashov @Yaël Dillies
• Mathlib/CategoryTheory/ComposableArrows.lean: @Joël Riou has identified that there is a problem in how dsimp is working here, but we really need a minimisation of this in order to be able to go fix it. This is potentially the most serious problem here, so anyone who can work on this: greatly appreciated. Update: for now, we've punted on this one using set_option simprocs false.

[Thomas Murrills]

(I’ll have a go at minimizing the error in ComposableArrows :working_on_it:)

[Yaël Dillies]

Sorry, really busy because it's the end of term on that side of the world. Happy to fix anything that's still broken by next monday, when I'm finally on holiday.

[Thomas Murrills]

Got a few errors in ComposableArrows, at least: the issue is lean4#3586, which introduced a simproc for Fin, and seems to lead dsimp down a different path. Using dsimp [-Fin.reduceFinMk] solves the goal. (There's still the question of why this actually leads us down a different path, though.)

[Kim Morrison]

@Thomas Murrills, thanks.

I propose for right now we add:

/-!
New `simprocs` that run even in `dsimp` have caused breakages in this file.

(e.g. `dsimp` can now simplify `2 + 3` to `5`)

For now, we just turn off simprocs in this file.
We'll soon provide finer grained options here, e.g. to turn off simprocs only in `dsimp`, etc.

*However*, hopefully it is possible to refactor the material here so that no backwards compatibility
`set_option`s are required at all
-/
set_option simprocs false

[Thomas Murrills]

(This also exposed an issue in dsimp?: it currently neglects simprocs, and put us in the funny situation of dsimp? and its suggestion working without dsimp working!)

[Kim Morrison]

@Thomas Murrills, ooh, could you open an issue for that? I think we used to have the same problem for simp, it should be easy to fix.

[Thomas Murrills]

(Also, shall I push that temporary set_option fix, or have you got it?)

[Kim Morrison]

Just pushed.

[Patrick Massot]

Is this a different issue in Mathlib/Data/Sum/Interval.lean or the one for which I posted a fix a couple of days ago?

[Kim Morrison]

Sorry Patrick, missed your message.

[Patrick Massot]

I should have pushed but I wanted to discuss the issue.

[Thomas Murrills]

Scott Morrison said:

Thomas Murrills, ooh, could you open an issue for that? I think we used to have the same problem for simp, it should be easy to fix.

lean4#3653

[Patrick Massot]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Help.20with.20.60nightly-testing.60/near/425445159

[Kim Morrison]

Yes, I responded saying that it couldn't be because of lean4#3508, because we had already adapted to that.

[Thomas Murrills]

(I'll go ahead and also submit a PR fixing lean4#3653 if that's alright—it's pretty straightforward, I think.)

[Patrick Massot]

Ok so I misunderstood where it came from, but this is still a fix.

[Kim Morrison]

I've pushed it, thanks @Patrick Massot

[Kim Morrison]

@Thomas Murrills, ping me if it tests okay, and I can merge.

[Patrick Massot]

Later today I will have a bit of time to work on other items in your list (I will first come back here to see if there are any updates).

[Patrick Massot]

I’ll work on the permutation one.

[Patrick Massot]

I have a fix but this proof is full of uses of deprecated stuff, so I’ll try to switch to undeprecated ones.

[Kyle Miller]

@Scott Morrison AdjMatrix is fixed (pushed to nightly-testing)

[Patrick Massot]

I gave up on the deprecated stuff, this corner of Mathlib really isn’t for me.

[Kyle Miller]

Is it cheating to add using Nat.rec to an induction to make it work without changing the proof?

[Kyle Miller]

That would solve Mathlib/GroupTheory/Perm/List.lean

[Patrick Massot]

I “solved” that one already.

[Kim Morrison]

@Kyle Miller, did you see my message on the other zulip about adding a backwards compatibility flag that disables custom recursors?

[Kim Morrison]

I'd sort of prefer that we explicitly use such options, to make it clearer that someone should fix the proof.

[Kim Morrison]

With using Nat.rec, it will just stay forever.

[Patrick Massot]

The FRO has a whole other Zulip?

[Patrick Massot]

I don’t understand why Kyle fixed my fix.

[Patrick Massot]

So I’ll stop wasting time and go to bed.

[Kyle Miller]

Sorry @Patrick Massot, I was working on it independently, then merged

[Thomas Murrills]

The two typeclass synthesis failures in Analysis.Complex.Basic can be fixed with a type annotation, but it's a bit odd (the new annotations are Set (ι → 𝕜) and Set (Fin 2 → 𝕜))

lemma segment_single_subset_stdSimplex (i j : ι) :
    ([Pi.single i 1 -[𝕜] Pi.single j 1] : Set (ι → 𝕜)) ⊆ stdSimplex 𝕜 ι := ...

lemma stdSimplex_fin_two :
    stdSimplex 𝕜 (Fin 2) = ([Pi.single 0 1 -[𝕜] Pi.single 1 1] : Set (Fin 2 → 𝕜)) := ...

I'd have thought the type Set (A → B) could be inferred from stdSimplex A B, which has exactly the annotated type, no inference required. Should I leave a note?

[Kim Morrison]

The notation here seems insane. Is it really [X -[k] Y]?

[Thomas Murrills]

That's what it is/was—I haven't touched that :woman_shrugging:

[Kim Morrison]

Let's at least leave a note saying something like

Adaptation note: as of `nightly-2024-03-11`, we need a type annotation here

[Kim Morrison]

and perhaps also saying "This notation seems unreasonable, and should be changed."

[Thomas Murrills]

Tweaked the note to mention both lemmas, but didn't express ire at the notation; it seems to be used quite extensively and defined in a different file dedicated entirely to it (Mathlib.Analysis.Convex.Segment) :sweat_smile:

[Kim Morrison]

Okay, I've posted about my ire about that notation separately. :-)

[Kyle Miller]

Patrick Massot said:

I “solved” that one already.

I just realized I completely missed this message. Double sorry.

[Thomas Murrills]

Fixed Mathlib/SetTheory/Ordinal/Basic.lean; didn't leave a note since there's already a porting note there complaining about the non-rfl proof. (Though we do seem to be getting further from it...)

[Thomas Murrills]

Fixed the two errors in Mathlib.Computability.TMToPartrec; changed simp only [Nat.rec] to simp only Nat.rec_zero] and simp only [Code.eval] to simp only [Nat.rec_zero, Part.bind_eq_bind]. (These changes didn't seem note(-)worthy to me, but I can leave a note if desired.)

[Thomas Murrills]

Fixed Data.Nat.Multiplicity, tweaked the existing adaptation note—it's still fairly awkward (I use norm_cast; nth_rw 2 [← zero_add 1] to get to 0 + 1 in the appropriate spot). (Maybe there's a better way?)

[Kim Morrison]

I think it's okay to be awkward as long as we leave an "adaptation note".

[Kim Morrison]

I've pushed more changes.

[Thomas Murrills]

Re: fixing dsimp?: lean4#3654 is the lean4 PR; std4#691 is the std4 adaptation PR. Both are green (but the mathlib build is waiting on std4#691).

(Hopefully mathlib4 doesn't need an adaptation once std4#691 is merged to the lean-pr-testing branch; I don't think it will, unless a test uses #guard_msgs with dsimp?.)

[Kim Morrison]

@Thomas Murrills, I merged, we should see it in the nightly in a few hours.

[Kim Morrison]

We are again down to four errors:

• Mathlib/Topology/Support.lean, as above, a problem in @[to_additive]
• Mathlib/Data/Polynomial/Derivative.lean: not my favourite sort of proof, where we do multiple cases statements, and then a long simp_rw and a long simp. Probably easy to fix, just annoying!
• Mathlib/SetTheory/Ordinal/Notation.lean: again, not my favourite proof structure (this one is even less fun, multiple cases, multiple try ... tactics connected by <;>, and unsurprisingly when something changes the subgoals remaining are scrambled!) Perhaps @Mario Carneiro, who originally wrote this proof?
• Mathlib/Data/Nat/Factorization.lean: now on recOnMul we get "code generator does not support recursor 'Nat.recOn' yet, consider using 'match ... with' and/or structural recursion". Note that I've already removed compile_inductive% Nat, as that says "already compiled Nat.rec", due to the recent changes. @Kyle Miller?

[Johan Commelin]

I wil take a look at Polynomial.Derivative

[Kyle Miller]

I fixed Data/Nat/Factorization/Basic, removing the porting note.

[Thomas Murrills]

I'm guessing that whatever's going on in Topology/Support, it involves the fact that a subterm of the to-be-additivized proof used to look like OfNat.ofNat (nat_lit 1), but now looks like OfNat.ofNat (OfNat.ofNat (α := ℕ) (nat_lit 1))

[Kyle Miller]

In Lean core, we have a @[csimp] lemma that makes Nat.rec have compiled code, but not for Nat.recOn. I guess compile_inductive% wants to define that as well as Nat.brecOn, but since the Nat.rec csimp is already defined it gives up.

[Kim Morrison]

@Eric Wieser, might you be able to look at Mathlib.LinearAlgebra.TensorProduct.Graded.Internal on nightly-testing? I'm not sure how it was intended to work.

[Kim Morrison]

@Riccardo Brasca, might you be able to look at Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral on nightly-testing? A fragile proof has broken now that Nat.rec gives us +1s rather than succs.

[Riccardo Brasca]

Sure, feel free to put a sorry there. I will have a look in about one hour

[Johan Commelin]

@Scott Morrison This works

@[simp]
theorem derivative_mul {f g : R[X]} : derivative (f * g) = derivative f * g + f * derivative g := by
  induction f using Polynomial.induction_on'
  · simp only [add_mul, map_add, add_assoc, add_left_comm, *]
  induction g using Polynomial.induction_on'
  · simp only [mul_add, map_add, add_assoc, add_left_comm, *]
  rename_i m a n b
  simp only [monomial_mul_monomial, derivative_monomial]
  simp only [mul_assoc, (Nat.cast_commute _ _).eq, Nat.cast_add, mul_add, map_add]
  cases m
  · simp only [zero_add, Nat.cast_zero, mul_zero, map_zero]
  cases n
  · simp only [add_zero, Nat.cast_zero, mul_zero, map_zero]
  rename_i m n
  simp only [Nat.add_succ_sub_one, add_tsub_cancel_right]
  rw [add_assoc, add_comm n 1]
#align polynomial.derivative_mul Polynomial.derivative_mul

[Johan Commelin]

I'll backport to mathlib

[Kim Morrison]

I've now opened the PR for the adaptations for nightly-2024-03-11, as #11314.

[Johan Commelin]

I've also pushed this to nightly-testing

[Kim Morrison]

Hopefully now we can parallelize getting this over the line.

• Review the changes there
• grep for FIXME.*nightly on this branch, and fix the remaining sorries!

[Kim Morrison]

@Johan Commelin, I'll put it direct into #11314 now.

[Johan Commelin]

The backport is #11315

[Eric Wieser]

Scott Morrison said:

Eric Wieser, might you be able to look at Mathlib.LinearAlgebra.TensorProduct.Graded.Internal on nightly-testing? I'm not sure how it was intended to work.

Possibly not for another 12 hours, depending on network connectivity

[Kim Morrison]

No problem, I think we'll have things to do. :-)

[Kim Morrison]

(In particular, nightly-testing has now moved on to nightly-2024-03-12. Std needed some changes, but so far Mathlib looks okay.)

[Michael Rothgang]

I just left a few comments on the diff.
Can the proof changes into by omega also be backported? (I won't have time for this.)

[Kim Morrison]

Michael Rothgang said:

Can the proof changes into by omega also be backported? (I won't have time for this.)

Good suggestion! Any volunteers? :-)

[Riccardo Brasca]

Should I push directly to #11314?

[Kim Morrison]

@Riccardo Brasca, yes please!

[Kim Morrison]

(I semi-regularly merge the bump/nightly-YYYY-MM-DD branches back to nightly-testing, so once the PR is open, it's best if changes go there.)

[Kim Morrison]

Michael Rothgang said:

I just left a few comments on the diff.

Dealt with, thanks.

[Riccardo Brasca]

Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral is fixed.

[Riccardo Brasca]

I have time to help with this... which file/folder can I work on?

[Eric Wieser]

I tried to help out here, but it seems that there's no cache available at all; I assume a dependency was just bumped, and my timing was bad?

[Riccardo Brasca]

The first sorry I see is in Mathlib/SetTheory/Ordinal/Notation.lean. I can fix the first error, but later it becomes a mess. Maybe an expert in the ordinal part of the library can help.

[Eric Wieser]

Looks like a cache will be ready in 5 minutes or so... just as my window of time expires!

[Michael Rothgang]

Scott Morrison said:

Michael Rothgang said:

Can the proof changes into by omega also be backported? (I won't have time for this.)

Good suggestion! Any volunteers? :-)

Filed #11318 now.

[Riccardo Brasca]

I am fixing Mathlib/Algebra/Homology/Augment.

[Riccardo Brasca]

I got absorbed by other stuff and I have to stop now, sorry :unamused:

[Kim Morrison]

@Kyle Miller, do you see what could be going on in Mathlib/Algebra/Homology/Augment.lean?

[Kim Morrison]

We are getting lots of goals with Nat.casesAuxOn that used to simplify away.

[Eric Wieser]

Scott Morrison said:

Eric Wieser, might you be able to look at Mathlib.LinearAlgebra.TensorProduct.Graded.Internal on nightly-testing? I'm not sure how it was intended to work.

I found some time; dsimp is refusing to use a rfl lemma passed to it

[Patrick Massot]

Patrick Massot said:

So I’ll stop wasting time and go to bed.

I apologize I was a bit rude in that message. But I think we really need to work on our process with those fixes sprints. This thread is not working as a coordination tool. Consider the following timeline of my messages.

• 19:53 Later today I will have a bit of time to work on other items in your list (I will first come back here to see if there are any updates).

• 21:00 I’ll work on the permutation one.

• 21:33 I have a fix but this proof is full of uses of deprecated stuff, so I’ll try to switch to undeprecated ones.

• 21:49 I “solved” that one already.

And then at 22:03 someone else pushed another fix for the same item (I wrote someone because my point is not at all to complain about them but about our process). I understand that opening issues for every file and using GitHub assignements is a bit painful. But if there is no lighter solution and we don’t want to do that then I’ll stop spending evenings fighting dependent rewrites in ugly corners of Mathlib.

[Mario Carneiro]

Fixed the issue in Mathlib/SetTheory/Ordinal/Notation.lean

[Kyle Miller]

Scott Morrison said:

Kyle Miller, do you see what could be going on in Mathlib/Algebra/Homology/Augment.lean?

It was from using by cases to define a function. On one hand it's a problem that dsimp is unaware of this alternative Nat eliminator, and on the other the function probably should have not been defined using tactics. (Pushed a fix)

[Thomas Murrills]

Patrick Massot said:

Patrick Massot said:

So I’ll stop wasting time and go to bed.

I apologize I was a bit rude in that message. But I think we really need to work on our process with those fixes sprints. This thread is not working as a coordination tool. Consider the following timeline of my messages.

• 19:53 Later today I will have a bit of time to work on other items in your list (I will first come back here to see if there are any updates).

• 21:00 I’ll work on the permutation one.

• 21:33 I have a fix but this proof is full of uses of deprecated stuff, so I’ll try to switch to undeprecated ones.

• 21:49 I “solved” that one already.

And then at 22:03 someone else pushed another fix for the same item (I wrote someone because my point is not at all to complain about them but about our process). I understand that opening issues for every file and using GitHub assignements is a bit painful. But if there is no lighter solution and we don’t want to do that then I’ll stop spending evenings fighting dependent rewrites in ugly corners of Mathlib.

Maybe each task should be its own message, and we use emojis to coordinate—before each list of tasks there could be a message saying “Please react with :working_on_it: (working_on_it) when you start to work on a task to prevent conflicts”.

(Repeating this message near each list of tasks should prevent people who are unfamiliar with the practice and haven’t read the whole thread from creating conflicts.)

[Kevin Buzzard]

If this is going to be a constant issue and source of random work, maybe it should have its own devoted stream. We could have threads for problem files and resolve them when they're compiling

[Michael Rothgang]

Another option could be to use Github tracking issues with participants claiming tasks. (The Rust project would write a bot allowing people to "claim" subtasks.) That doesn't integrate well with zulip, though.

[Ruben Van de Velde]

Sounds like pretty high overhead too

[Ruben Van de Velde]

I'll take a look at the simp says ones now

[Eric Wieser]

I think the process is a bit too chaotic and rushed for github issues to be useful

[Eric Wieser]

But a stream could well be; maybe the "resolved" feature could actually be useful for once!

[Thomas Murrills]

How about a bot that scrapes the build logs and posts to/creates topics in zulip? :eyes:

[Thomas Murrills]

(Well, if it turns out to be a lot of management overhead, at least. Although it’s contrary to my instinct, we should probably try the manual method before automating things… :) )

[Eric Wieser]

Thomas Murrills said:

How about a bot that scrapes the build logs and posts to/creates topics in zulip? :eyes:

This might be overkill, but might be a nice project for someone wanting to learn to write a Zulip bot

[Matthew Ballard]

Are all the errors from says right now?

[Ruben Van de Velde]

I wish says had a code action to update its expectations

[Ruben Van de Velde]

Yeah, I think so

[Matthew Ballard]

What is the intention here with says? It is nice to have the old simp list when things break. Is there anything more to do than make a note (mental or otherwise) and change the output?

[Ruben Van de Velde]

I'm just changing the output to match the new simp behaviour, which is mostly adding Int.reduceNeg

[Ruben Van de Velde]

Definitions that need a heartbeat bump to 800000 aren't fun to work with :/

[Matthew Ballard]

That is purely a fault of says if you are working with the one I remember

[Ruben Van de Velde]

I pushed, stepping out for a bit

[Ruben Van de Velde]

To nightly-testing; I hope this wasn't fixed in some PR branch yet

[Matthew Ballard]

I adjusted the last two says calls and it should build in CI now

[Matthew Ballard]

Now it is Archive Counterexamples and linting

[Kim Morrison]

Ah... @Ruben Van de Velde, @Matthew Ballard, sorry this wasn't clear, but it's important once we have a bump/nightly-YYYY-MM-DD branch, e.g. #11314, that all work happens there rather than on nightly-testing (with a caveat, see below).

[Kim Morrison]

The problem is that nightly-testing has already moved on to a subsequent nightly.

[Kim Morrison]

So while we can merge from #11314 to nightly-testing, we can't merge the other way.

[Matthew Ballard]

Oh sorry Scott

[Kim Morrison]

Hence the caveat is you can push changes to nightly-testing as long as they are specifically about fixes for the latest nightly, that do not work on whatever bump/nightly-YYYY-MM-DD PR is open.

[Kim Morrison]

np

[Kim Morrison]

This is not obvious, and indeed pretty difficult to coordinate clearly. We need to get better at this.

[Matthew Ballard]

I am about to appease the linter on the current nightly

[Kim Morrison]

I think in this case there is not actually anything fundamentally different in nightly-2024-03-12 (where nightly-testing is) compared to nightly-2024-03-11 (where #11314 is).

[Kim Morrison]

So I am going to attempt a squash merge and see what goes horribly wrong. :-)

[Kim Morrison]

(Also, because nightly-testing receives automatic merges from master, merging back from nightly-testing to bump/nightly-2024-03-11 is a bit scary: we need to first merge master into both bump/v4.8.0 (the target of #11314) and bump/nightly-2024-03-11 successfully.)

[Matthew Ballard]

- Found 9 errors in 186635 declarations (plus 452405 automatically generated ones) in Mathlib with 14 linters

/- The `docBlame` linter reports:
DEFINITIONS ARE MISSING DOCUMENTATION STRINGS: -/
-- Mathlib.Data.Nat.Factorization.Basic
./././Mathlib/Data/Nat/Factorization/Basic.lean:894:11: error: Nat.recOnMul.hp''.{u_1} definition missing documentation string

/- The `simpNF` linter reports:
SOME SIMP LEMMAS ARE NOT IN SIMP-NORMAL FORM.
see note [simp-normal form] for tips how to debug this.
https://leanprover-community.github.io/mathlib_docs/notes.html#simp-normal%20form -/
-- Mathlib.CategoryTheory.GradedObject
./././Mathlib/CategoryTheory/GradedObject.lean:154:1: error: CategoryTheory.GradedObject.eqToHom_apply.{w, v, u} simp can prove this:
  by simp only [@CategoryTheory.Functor.eqToHom_proj]
One of the lemmas above could be a duplicate.
If that's not the case try reordering lemmas or adding @[priority].


-- Mathlib.Data.Finset.Basic
./././Mathlib/Data/Finset/Basic.lean:2818:1: error: Finset.filter_congr_decidable.{u_1} Left-hand side does not simplify, when using the simp lemma on itself.
This usually means that it will never apply.


-- Mathlib.Data.Fintype.BigOperators
./././Mathlib/Data/Fintype/BigOperators.lean:146:1: error: Fintype.card_fun.{u_2, u_1} Left-hand side simplifies from
  Fintype.card (α → β)
to
  Fintype.card β ^ Finset.univ.card
using
  simp only [@Fintype.card_pi, @Finset.prod_const]
Try to change the left-hand side to the simplified term!


-- Mathlib.Logic.IsEmpty
./././Mathlib/Logic/IsEmpty.lean:157:1: error: isEmpty_fun.{u_2, u_1} Left-hand side simplifies from
  IsEmpty (α → β)
to
  ∃ a, IsEmpty β
using
  simp only [@isEmpty_pi]
Try to change the left-hand side to the simplified term!


/- The `simpVarHead` linter reports:
LEFT-HAND SIDE HAS VARIABLE AS HEAD SYMBOL.
Some simp lemmas have a variable as head symbol of the left-hand side (after whnfR): -/

- The `synTaut` linter reports:
THE FOLLOWING DECLARATIONS ARE SYNTACTIC TAUTOLOGIES. This usually means that they are of the form `∀ a b ... z, e₁ = e₂` where `e₁` and `e₂` are identical expressions. We call declarations of this form syntactic tautologies. Such lemmas are (mostly) useless and sometimes introduced unintentionally when proving basic facts using `rfl`, when elaboration results in a different term than the user intended. You should check that the declaration really says what you think it does. -/
-- Mathlib.Data.Multiset.Fintype
./././Mathlib/Data/Multiset/Fintype.lean:74:1: error: Multiset.coe_eq.{u_1} LHS equals RHS syntactically

/- The `unusedHavesSuffices` linter reports:
THE FOLLOWING DECLARATIONS HAVE INEFFECTUAL TERM MODE HAVE/SUFFICES BLOCKS. In the case of `have` this is a term of the form `have h := foo, bar` where `bar` does not refer to `foo`. Such statements have no effect on the generated proof, and can just be replaced by `bar`, in addition to being ineffectual, they may make unnecessary assumptions in proofs appear as if they are used. For `suffices` this is a term of the form `suffices h : foo, proof_of_goal, proof_of_foo` where `proof_of_goal` does not refer to `foo`. Such statements have no effect on the generated proof, and can just be replaced by `proof_of_goal`, in addition to being ineffectual, they may make unnecessary assumptions in proofs appear as if they are used. -/
-- Mathlib.Analysis.SpecialFunctions.Integrals
./././Mathlib/Analysis/SpecialFunctions/Integrals.lean:674:1: error: integral_sin_pow unnecessary have this : n + 2 ≠ 0
./././Mathlib/Analysis/SpecialFunctions/Integrals.lean:755:1: error: integral_cos_pow unnecessary have this : n + 2 ≠ 0

[Kim Morrison]

If anyone has suggestions about how we can make it clearer whether it is a bump PR, or the nightly-testing branch, which should be the main priority at any given moment, that would be great.

[Kim Morrison]

(The rule is very simple: if a bump PR exists, it is the priority.)

[Matthew Ballard]

Multiset.coe_eq looks like it can be removed in master but someone should sanity check me

[Kim Morrison]

Send it to CI! :-)

[Matthew Ballard]

It is chewing on it currently in a branch

[Matthew Ballard]

Finset.filter_congr_decidable is correctly flagged as never applying to itself with simp

[Kim Morrison]

I am happy to mark it as auto-merge-after-CI if you make it a PR.

[Matthew Ballard]

Nat.rec_add_one can by proven by simp now

[Matthew Ballard]

Scott Morrison said:

I am happy to mark it as auto-merge-after-CI if you make it a PR.

#11340

[Kim Morrison]

Okay, branches all in sync again now.

[Kim Morrison]

Please focus on #11314 instead of nightly-testing.

[Matthew Ballard]

Cleaned up #11340 correctly now

[Kim Morrison]

I'm close to the end of Archive and Counterexamples on #11314.

[Kim Morrison]

Okay, they are done.

[Kim Morrison]

Things still do on #11314:

(separate messages per item for emojis!)

[Kim Morrison]

• binCast_eq in Mathlib/Data/Nat/Cat/Defs.lean is sorried: hopefully straightforward: the proof used to rely on the syntactic difference between succ and +1.

[Kim Morrison]

• castNum_testBit in Mathlib/Data/Num/Lemmas.lean works, but is labelled with a FIXME, hacky proof. Perhaps can be downgraded to an adaptation note and dealt with later.

[Kim Morrison]

• Mathlib/LinearAlgebra/TensorProduct/Graded/Internal.lean has a FIXME, no longer works with dsimp, even though it is a rfl lemma.
  I propose downgrading to an adaptation note, and hoping that someone can come up with an import free minimisation, so we can get it fixed.

[Kim Morrison]

• Remaining linter issues. I think @Matthew Ballard might still be working on these? If not, could you let us know what remains?

[Ruben Van de Velde]

It's quite dangerous to have the bot in the other stream reporting on nightly-testing when that's not the branch to work on, but no harm done this time

[Kim Morrison]

Yes, I agree. How should that bot work?

[Kim Morrison]

1. It should post somewhere public!
2. Certainly the Std bot needs to post a green check mark when Std's nightly-testing comes good.
3. Perhaps it would detect if there was a PR open to the current bump/v4.8.0branch, and if so post about that branch instead?? That seems hard to set up.

[Ruben Van de Velde]

@Scott Morrison I just added the prime you removed in https://github.com/leanprover-community/mathlib4/pull/11314/commits/0b6eccda1916deb3bfc1ac937df60f422d31f3bd because it's about List.merge' (because Std added a conflicting List.merge)

[Ruben Van de Velde]

Maybe I should PR that rename now?

[Kim Morrison]

Why didn't I see a conflict?

[Kim Morrison]

Is it that on #11314 we haven't actually bump the Std dependency yet, so don't see this?

[Kim Morrison]

If so, perhaps this can be done as a PR direct to master, updating Std and doing this rename.

[Ruben Van de Velde]

https://github.com/leanprover-community/mathlib4/pull/11343 just moves mathlib's definition out of the way; we can then bump and adapt independently

[Ruben Van de Velde]

And with that I'm off to bed

[Kim Morrison]

Thanks!

[Matthew Ballard]

Sorry. Tea time. I have the linter appeased. Just need to get in the correct branch

[Kim Morrison]

@Ruben Van de Velde, I pushed a few more primes to that branch, and will merge shortly.

[Eric Rodriguez]

Scott Morrison said:

1. It should post somewhere public!
2. Certainly the Std bot needs to post a green check mark when Std's nightly-testing comes good.
3. Perhaps it would detect if there was a PR open to the current bump/v4.8.0branch, and if so post about that branch instead?? That seems hard to set up.

I think 3 is a crucial step if we are to have this setup; I think it's quite a confusing setup overall and any guidance that is bot-driven would be good. Also, I'm not sure if the nightly-testing guide is available on the public stream; on the other hand, I'm not sure if it's out of date.

[Kim Morrison]

@Eric Rodriguez, which guide did you have in mind? https://leanprover-community.github.io/contribute/tags_and_branches.html?

[Kim Morrison]

Kyle Miller said:

In Lean core, we have a @[csimp] lemma that makes Nat.rec have compiled code, but not for Nat.recOn. I guess compile_inductive% wants to define that as well as Nat.brecOn, but since the Nat.rec csimp is already defined it gives up.

@Kyle Miller, do you have a suggestion for what we should do here?

Currently test/CompileInductive.lean is failing on #11314 with

example := @Nat.recOn -- code generator does not support recursor 'Nat.recOn' yet, consider using 'match ... with' and/or structural recursion

[Kim Morrison]

Currently my idea is to just add

-- Adaptation note: nightly-2024-03-11.
-- Currently we can't run `compile_inductive% Nat`,
-- as `Nat.rec` already has a `@[csimp]` lemma.
-- However this means that we don't generated code for `Nat.recOn`.

and deal with this later.

[Matthew Ballard]

Ok, I had 5 of 9 linter failures only. I pushed to the bump branch. I will check out of the others now

[Eric Wieser]

Where is compile_inductive% defined?

[Matthew Ballard]

I have liberally applied the Adaptation note. Please feel free to remove if you are satisfied by the explanation

[Kim Morrison]

@Eric Wieser Mathlib.Util.CompileInductive

[Eric Wieser]

Does compile_def% Nat.recOn work?

[Kim Morrison]

I've fixed the tests now. I think it is only review and the linter

[Kim Morrison]

@Eric Wieser , looks like it does, thanks!

[Eric Wieser]

I think probably there's still a TODO here, as I think compile_inductive% does more than just compile rec and recOn, but I would guess that mathlib only actually cares about those two

[Kim Morrison]

Would you be able to write such a TODO?

[Eric Wieser]

Is a later nightly going to compile recOn too?

[Kim Morrison]

I'm not sure, will wait to see what Kyle says.

[Kim Morrison]

We could also just disable the warning in compile_inductive%, I guess.

[Kyle Miller]

I was trying to decide whether to put compiled versions of Nat.recOn and Nat.brecOn into core, but if we can make mathlib compile these, I'd so go with that for now.

I don't know what's the long term vision is for compiling recursors.

[Kim Morrison]

Okay, I will go with

compile_def% Nat.recOn
compile_def% Nat.brecOn

for now.

[Kyle Miller]

The reason that Nat.rec is compiled in core is that it's small hack to get Nat.recAux not be marked noncomputable

[Matthew Ballard]

Is docBlame supposed to complain about let rec’s?

[Kim Morrison]

@Matthew Ballard, just a request re: adaptation/porting notes: if they could always go before the change, rather than after, that is easier to understand.

e.g. https://github.com/leanprover-community/mathlib4/pull/11314/files#diff-8c3d7fa2ef5b966d341ccbdf4e174af7c0e7a3d599efb5b74205f1adbaa061ac

[Matthew Ballard]

Oh sorry, I thought I was but probably wasn’t careful

[Matthew Ballard]

That should satisfy the linter. Nothing worthwhile to note. Did field_simp get better?

[Matthew Ballard]

If you have a better pattern for hiding a let rec from docBlame please feel free

[Kim Morrison]

Write a comment? :-)

[Matthew Ballard]

That one was commented. In front even!

[Kim Morrison]

As far as I'm aware no one has fixed field_simp and it is still super slow because of the higher discharge depth limit.

[Matthew Ballard]

I was able to delete two have’s showing something was nonzero

[Kim Morrison]

Okay, thank you everyone!

I think #11314 is ready to go now. If anyone is available to do a final review/delegate that would be great.

[Matthew Ballard]

One sec. One more linter failure locally.

[Matthew Ballard]

Ok, that is fixed.

[Matthew Ballard]

Is it expected that exact? is timing out quite often still?

[Kim Morrison]

No, not really. :-( Examples are super helpful!

[Kim Morrison]

Matthew Ballard said:

That one was commented. In front even!

I meant a doc-string on the actual let rec

[Mario Carneiro]

reminder, the syntax for this is let rec /-- doc -/ foo := 1; bla

[Kim Morrison]

Presumably

  let rec
    /-- long doc-string -/
    foo := 1
  bla

is the right formatting for a long doc-string?

[Kim Morrison]

(I've done this in Nat/Factorization/Basic now)

[Mario Carneiro]

it's the best under the cirumstances; ideally the grammar would be fixed to allow

  /-- long doc-string -/
  let rec foo := 1
  bla

[Matthew Ballard]

Well, I at least read through the changes and they seem ok

[Kim Morrison]

Okay. I'll take it. :-)

[Kim Morrison]

@Damiano Testa, one of the tests for MoveAdd is failing in #11314. Since it doesn't seem to affect the rest of Mathlib, I have just commented it out for now, so as to not delay #11314.

Could you please investigate this test, and fix? (You can either make a PR to master if you have something that will work on both old and new Lean, or just PR to bump/v4.8.0 if the fix will be specific to new Lean.)

[Kim Morrison]

We need to do the List.merge fix in the right order:

• https://github.com/leanprover-community/mathlib4/pull/11347 is the PR which bumps masters Std dependency, and pulls in @François G. Dorais's fixes for https://github.com/leanprover/std4/pull/579.

[Kim Morrison]

• We can then merge that into #11314.

[Matthew Ballard]

Sorry, running to catch the last shuttle. I’ll look at the bloat in injective resolutions later or tomorrow

[François G. Dorais]

Sorry for the mess. I totally dropped the ball on std4#579.

[Kim Morrison]

No mess at all, it seems to have gone cleanly.

[Matthew Ballard]

#11349 fixes injective resolution

[Kim Morrison]

We've created a new stream https://leanprover.zulipchat.com/#narrow/stream/428973-nightly-testing for coordinating work on keeping Mathlib and other projects up to date with nightly releases of Lean.

[Kim Morrison]

Please join us. :-)

[Damiano Testa]

Scott Morrison said:

Damiano Testa, one of the tests for MoveAdd is failing in #11314. Since it doesn't seem to affect the rest of Mathlib, I have just commented it out for now, so as to not delay #11314.

Could you please investigate this test, and fix? (You can either make a PR to master if you have something that will work on both old and new Lean, or just PR to bump/v4.8.0 if the fix will be specific to new Lean.)

I'll investigate this!

[Michael Rothgang]

Matthew Ballard said:

#11349 fixes injective resolution

I recall (can't find right now) a fairly big regression by the bump PR, while #11349 is only half the size. Granted, #11349 landed on master - does this fix the regression on the bump branch?

[Matthew Ballard]

I didn’t benchmark but the experience in editor says most surely