Addressing porting notes?

Stream: mathlib4

[Thomas Murrills]

I'm nearly finished with mono, and was wondering if I should restore the @[mono] attributes which were commented out and left with a porting note. I was about to go through and do it, but then started wondering if this would cause problems with SHA synchronization between mathlib3 and mathlib4, or if that's taken care of by automation.

In general, if a porting note becomes easy to fix in a completely unambiguous way (e.g. restoring @[mono] now that mono will be available) can it simply be fixed, or is there extra work a human has to do to make the SHA's line up? If so, what's the correct procedure?

[Jireh Loreaux]

There's no issue with SHAs because you aren't editing mathlib3 (or synchronizing a mathlib3 PR), so go ahead.

[Casavaca]

just a note, I've restored many of them. see https://github.com/leanprover-community/mathlib4/pull/2491

[Thomas Murrills]

Ok, great, I’ll rebase to master! :)

[Kevin Buzzard]

Reviving this topic and making it more general: at the mathlib meeting last Friday there was a discussion about "technical debt", part of which seemed to be "what the heck are we going to do with these thousands of porting notes?". Sometimes I run into one, saying something like

  -- porting note: in Lean 4 we need this next line for some reason
  haveI : Group G := inferInstance
  ...

and I try deleting the extra line which was added during the port, and the file compiles just fine, because there was some bug or inefficiency somewhere which has since been fixed. On the other hand I would imagine that there are still some porting notes which do apply, and do we have a plan for these? Is the idea to have issues in mathlib or core, and to add a link to the issue for every porting note which is still valid? Or did I misunderstand the plan?

[Johan Commelin]

It would already be extremely helpful to make a pass through many (all?!) porting notes, to see which ones can be removed and which ones still apply.

[Johan Commelin]

A follow-up step would be to categorize the remaining porting notes, and link them (in the code) to issues that need to be addressed.

[Kevin Buzzard]

But don't you think that we could do both steps in one pass?

[Kevin Buzzard]

One could change "porting note" to "triaged porting note" whenever one is linked to an issue

[Matthew Ballard]

I took a couple minutes to grab the first porting note ripgrep could find. #10496

[Jireh Loreaux]

@Matthew Ballard I left a comment.

[Johan Commelin]

Shall we label these PRs with some GH label?

[Johan Commelin]

porting-debt?

[Matthew Ballard]

Jireh Loreaux said:

Matthew Ballard I left a comment.

Ok, more thought that I gave it is required here. #PR reviews > #10496 address porting notes in Order.Grade

[Pietro Monticone]

There are hundreds of -- Porting note: added such as:

-- Porting note: added
instance instRingHomClass {X Y : SemiRingCat} : RingHomClass (X ⟶ Y) X Y :=
  RingHom.instRingHomClass

-- porting note: added
lemma coe_id {X : SemiRingCat} : (𝟙 X : X → X) = id := rfl

-- porting note: added
lemma coe_comp {X Y Z : SemiRingCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl

-- porting note: added
@[simp] lemma forget_map (f : X ⟶ Y) : (forget SemiRingCat).map f = (f : X → Y) := rfl

These should be among the easiest to solve, shouldn't they? How should they be interpreted exactly?

[Damiano Testa]

Presumably, if removing the corresponding lemma still builds mathlib, it should be fine to remove them!

[Matthew Ballard]

I would add the caveat that it should disproportionately slow down the build also. Though this applies mainly to instance's that were added.

[Josha Dekker]

don’t these specific porting notes just mean that they are new additions relative to the pre-porting status and adding during the porting process? So you should probably only remove the comments but leave the results in?

[Matthew Ballard]

I think it depends on the context. Often these are added because other things did not fire but that context is lost between the porting and the note

[Pietro Monticone]

Josha Dekker said:

don’t these specific porting notes just mean that they are new additions relative to the pre-porting status and adding during the porting process? So you should probably only remove the comments but leave the results in?

Yes, I was referring to the deletion of the comments -- Porting note: added, but I wasn't sure I interpreted correctly.

[Pietro Monticone]

Matthew Ballard said:

I think it depends on the context. Often these are added because other things did not fire but that context is lost between the porting and the note

Ok, so what should be the exact procedure to test the relevance of comments and / or their corresponding code chunks and the consequent possibility to remove them?

I'd be happy to help cleaning it all up.

[Matthew Ballard]

For me

• never add instances if you can avoid it. As corollary, remove them when you can (assuming you don't break things and !bench is not terrible)
• theorems and defs should probably be given some thought assuming the porting note didn't provide adequate explanation. Feel to ask here if a particular declaration is unclear.

[Matthew Ballard]

In the example above, I am guessing the first is needed because typeclass inference didn't find in Lean 4. For the last three, there is probably some more general declaration for ConcreteCategory's that should applicable but did not fire in Lean 4.

[Matthew Ballard]

When removing the porting notes, we should also be sure to collect examples of issues to document them better

[Matthew Ballard]

Eg in #10496, I vaguely remember there was an problem updating BinderInfo and declaring new things in the same line. Is there an issue for this already?

[Pietro Monticone]

Matthew Ballard said:

never add instances if you can avoid it. As corollary, remove them when you can (assuming you don't break things and !bench is not terrible)

In order to test if I can remove a given istance should I always re-build the whole project?

[Matthew Ballard]

Then comment !bench on a Github PR (for performance impact)

[Pietro Monticone]

There are also several -- Porting note: Removed: such as:

-- Porting note: Removed:
-- include G

These can be safely removed, right?

[Ruben Van de Velde]

Yes, all references to include and omit should just go

[Ruben Van de Velde]

I don't think you should remove things just because they're tagged with "added" comments

[Ruben Van de Velde]

Those were mostly to aid review of the port or to help when forward-porting later changes in mathlib3 to mathlib4

[Pietro Monticone]

Ruben Van de Velde said:

Yes, all references to include and omit should just go

I've just opened a PR (#10503) to remove a bunch of those.

[Johan Commelin]

Probably clear, but please only address one category of porting notes per PR.

[Pietro Monticone]

Johan Commelin said:

Probably clear, but please only address one category of porting notes per PR.

BTW, should have I used the chore keyword?

[I'm sorry, kind of new with this]

[Ruben Van de Velde]

Yes, that's probably better - this isn't about documentation

[Ruben Van de Velde]

We're not super pedantic about commit messages, unlike with everything else ;)

[Pietro Monticone]

Ruben Van de Velde said:

Yes, that's probably better - this isn't about documentation

Fixed. Sorry.

Ruben Van de Velde said:

We're not super pedantic about commit messages, unlike with everything else :wink:

No problem at all with pedantry :sweat_smile:

[Matthew Ballard]

#10509 looked like it might be fun but seems to have fixed itself

[Matthew Ballard]

#10510 is actually easy :)

[Dagur Asgeirsson]

Another include: #10516

[Damiano Testa]

Given the trend, I'm going to open a PR removing all the include/omit porting notes.

[Damiano Testa]

#10517 (does not include the removed include in #10510)

[Matthew Ballard]

I added comments referencing lean#2452 for the last two PRs and delegated

[Matthew Ballard]

#10557 - someone left a to-do inside a porting note. It seems fine as a to-do alone

[Pietro Monticone]

I've noticed there are hundreds of Porting note: simp can prove this such as:

-- @[simp] -- Porting note: simp can prove this
protected theorem map_smul (f : A →ₙₐ[R] B) (c : R) (x : A) : f (c • x) = c • f x :=
  map_smul _ _ _
#align non_unital_alg_hom.map_smul NonUnitalAlgHom.map_smul

-- @[simp] -- Porting note: simp can prove this
protected theorem map_add (f : A →ₙₐ[R] B) (x y : A) : f (x + y) = f x + f y :=
  map_add _ _ _
#align non_unital_alg_hom.map_add NonUnitalAlgHom.map_add

-- @[simp] -- Porting note: simp can prove this
protected theorem map_mul (f : A →ₙₐ[R] B) (x y : A) : f (x * y) = f x * f y :=
  map_mul _ _ _
#align non_unital_alg_hom.map_mul NonUnitalAlgHom.map_mul

-- @[simp] -- Porting note: simp can prove this
protected theorem map_zero (f : A →ₙₐ[R] B) : f 0 = 0 :=
  map_zero _
#align non_unital_alg_hom.map_zero NonUnitalAlgHom.map_zero

What's the best way to solve them?

[Yaël Dillies]

Remove them

[Pietro Monticone]

Yaël Dillies said:

Remove them

Thank you. I'm going to open a PR solving them.

[Eric Wieser]

Yaël Dillies said:

Remove them

The lemmas or the comments?

[Eric Wieser]

I wonder if we want a @[simp_can_prove_this] attribute that causes a lint failure if for some reason a lemma can no longer be proven by simp (prompting the user to add simp back)

[Yaël Dillies]

Eric Wieser said:

Yaël Dillies said:

Remove them

The lemmas or the comments?

The point of FunLike and the hom classes was to remove the lemmas, but you definitely can remove just the comments as a first pass.

[Eric Wieser]

To be clear, you're very specifically talking about the map_$foo lemmas with simp can prove this, not the general case of simp can prove this?

[Yaël Dillies]

Yes, the general case is not so easy to diagnose

[Eric Wieser]

One thing I'm curious about is whether making these simp lemmas anyway improves performance

[Eric Wieser]

Because in theory it would skip a typeclass search

[Johan Commelin]

@Pietro Monticone @Yaël Dillies I would like to discuss this a bit more before moving to action.

[Johan Commelin]

I think Eric Wieser's suggestion of a special attribute makes sense. And also the investigation whether maybe we want to mark them as simp anyways, with a (special/dedicated?) nolint.

[Johan Commelin]

So this will require a bit of investigating, to settle on the best solution.

[Damiano Testa]

An immediate version of the special simp-attribute could be to prove the lemma with simp.

[Damiano Testa]

You will definitely see if simp no longer proves the lemma!

[Damiano Testa]

Maybe we could have a by_simp (statement) := syntax that expands to

theorem (statement) := by simp

[Johan Commelin]

simp_lemma (statement)

[Damiano Testa]

So, simp_lemma makes me think that the result has the simp attribute. I was not going that far, I was simply thinking of "a lemma the simp proves". Either works.

[Pietro Monticone]

Damiano Testa said:

An immediate version of the special simp-attribute could be to prove the lemma with simp.

Just verified that simp proves all of them:

-- @[simp] -- Porting note: simp can prove this
protected theorem map_smul (f : A →ₙₐ[R] B) (c : R) (x : A) : f (c • x) = c • f x := by simp
--   map_smul _ _ _
-- #align non_unital_alg_hom.map_smul NonUnitalAlgHom.map_smul

-- @[simp] -- Porting note: simp can prove this
protected theorem map_add (f : A →ₙₐ[R] B) (x y : A) : f (x + y) = f x + f y := by simp
--   map_add _ _ _
-- #align non_unital_alg_hom.map_add NonUnitalAlgHom.map_add

-- @[simp] -- Porting note: simp can prove this
protected theorem map_mul (f : A →ₙₐ[R] B) (x y : A) : f (x * y) = f x * f y := by simp
--   map_mul _ _ _
-- #align non_unital_alg_hom.map_mul NonUnitalAlgHom.map_mul

-- @[simp] -- Porting note: simp can prove this
protected theorem map_zero (f : A →ₙₐ[R] B) : f 0 = 0 := by simp
--   map_zero _
-- #align non_unital_alg_hom.map_zero NonUnitalAlgHom.map_zero

[Ruben Van de Velde]

These in particular should also get a @[deprecated], I think

[Pietro Monticone]

Ruben Van de Velde said:

These in particular should also get a @[deprecated], I think

Something like this?

@[deprecated]
protected theorem map_smul (f : A →ₙₐ[R] B) (c : R) (x : A) : f (c • x) = c • f x := by simp

@[deprecated]
protected theorem map_add (f : A →ₙₐ[R] B) (x y : A) : f (x + y) = f x + f y := by simp

@[deprecated]
protected theorem map_mul (f : A →ₙₐ[R] B) (x y : A) : f (x * y) = f x * f y := by simp

@[deprecated]
protected theorem map_zero (f : A →ₙₐ[R] B) : f 0 = 0 := by simp

[Damiano Testa]

How does this look?

import Std

/-- `simp_lemma name signature` introduces a lemma called `name` with
signature `signature` and proves it with `by simp`. -/
macro dm:declModifiers "simp_lemma " id:declId sig:declSig : command =>
  `(command| $dm:declModifiers theorem $id $sig := by simp)

/-- I can have docs too! -/
simp_lemma ofCourse : True

#check ofCourse

/-- The `simpNF` linter does not complain -/
@[simp, nolint simpNF] simp_lemma not_linted : 1 + 0 = 1

[Damiano Testa]

(This implementation does not actually place the simp attribute.)

[Eric Wieser]

Damiano Testa said:

An immediate version of the special simp-attribute could be to prove the lemma with simp.

I think for these lemmas, it's helpful to have the trivial non-simp proof. If the point in the attribute is to verify that simp can still prove the lemma, by simp is not going to be a very helpful proof if in future simp is no longer capable!

[Jireh Loreaux]

I would suggest not deprecating right now. It would be nice to know if there is a significant performance hit (although we'll only know if many proofs use the specific versions) to the general versions. The best way to test this would be to deprecate all such lemmas simultaenously in one PR and bench it.

[Pietro Monticone]

Jireh Loreaux said:

The best way to test this would be to deprecate all such lemmas simultaenously in one PR and bench it.

Ok, so I 'd just need to add @[deprecated] (as in the code chunk above) in all code chunks of the form:

-- @[simp] -- Porting note: simp can prove this
theorem theorem_name (statement) := proof

and then open a PR commenting with !bench, right?

[Timo Carlin-Burns]

Why would marking them deprecated affect performance? Isn't the relevant benchmark adding back @[simp] to them and seeing if that speeds things up?

[Ruben Van de Velde]

Replacing the deprecated versions by the non-deprecated versions could be slower

[Pietro Monticone]

Opened a PR with !bench #10604

[Jireh Loreaux]

I was thinking that marking them deprecated would mean that they could no longer be used in Mathlib (which is true), but @Timo Carlin-Burns is correct; the relevant question is whether there is a speedup if we were to mark them @[simp, no lint simpNF]. Since they're not firing currently, I'm less inclined to care about this. What do you think @Eric Wieser ?

[Pietro Monticone]

Maybe we should dedicate different topics to different kinds of porting notes to make it all more readable and more efficient.

[Kevin Buzzard]

Right -- although I'm not an expert in this kind of project management, I was wondering whether one preliminary approach would be that for each "type" of porting note, a mathlib issue is created, and a preliminary procedure could be going through the library adding "see issue #12345" or whatever the relevant issue number is, to each one.

[Eric Wieser]

I think replacing -- porting note: foo with -- porting note (\#12345): foo would certainly improve the situation

[Eric Wieser]

(the \ is there to stop Zulip being annoying, we don't actually want it in the comment)

[Pietro Monticone]

Github issues or discussions?

[Eric Wieser]

Issues

[Pietro Monticone]

If it's ok I could start writing issues (maybe with porting-notes label?) for the most frequent "types" of porting notes such as:

• -- Porting note: was X ($\approx 600$ occurrences in $\approx 300$ files)
• -- Porting note: added ($\approx 600$ occurrences in $\approx 300$ files)
• -- Porting note: simp can prove this($\approx 300$ occurrences in $\approx 100$ files)
• etc.

[Damiano Testa]

Eric Wieser said:

Damiano Testa said:

An immediate version of the special simp-attribute could be to prove the lemma with simp.

I think for these lemmas, it's helpful to have the trivial non-simp proof. If the point in the attribute is to verify that simp can still prove the lemma, by simp is not going to be a very helpful proof if in future simp is no longer capable!

I thought that one of the issues was to make sure that simp kept proving the lemma. If that fails due to some refactor, then building mathlib will pick it up and the declaration can be fixed.

As for using a custom proof, that is easy to fix: the macro can take

simp_lemma name statement := proof

and expand to

example statement := by simp
theorem name statement := proof

[Thomas Murrills]

Would it make sense to collect these different porting note issues in a tracking issue or github project?

[Eric Wieser]

I think added and was X are not particularly interesting unless grouped by the thing that they added / remove

[Pietro Monticone]

Here is the issue related to simp can prove this: https://github.com/leanprover-community/mathlib4/issues/10618

[Eric Wieser]

I edited your description slightly; note that if you paste raw permalinks, you get an embedded code block

[Pietro Monticone]

Here is the associated PR adding the issue number as suggested by @Eric Wieser above.

[Kevin Buzzard]

I've reviewed and flagged the four instances which are not like the other 300 or so.

[Pietro Monticone]

Kevin Buzzard said:

I've reviewed and flagged the four instances which are not like the other 300 or so.

Have you seen these two? https://github.com/leanprover-community/mathlib4/pull/10619#issuecomment-1947480619

[Pietro Monticone]

PS: There are merge conflicts, but I don't have write permission so I can't directly resolve them.

[Kim Morrison]

Damiano Testa said:

Maybe we could have a by_simp (statement) := syntax that expands to

theorem (statement) := by simp

Please don't do this. It unnecessarily makes Mathlib a mutually unintelligible dialect of Lean. This is what attributes are for.

[Kevin Buzzard]

Pietro Monticone said:

Kevin Buzzard said:

I've reviewed and flagged the four instances which are not like the other 300 or so.

Have you seen these two? https://github.com/leanprover-community/mathlib4/pull/10619#issuecomment-1947480619

Yes, I would include those two. When we got these issues during the port, the linter would explain how to prove the lemmas using simp, and it looks like sometimes people decided to include the proofs. I don't see any reason to keep the proofs, they are easily regenerated by running simp? so you can just normalise them so they look like the others. That's my 2c anyway.

[Pietro Monticone]

Kevin Buzzard said:

Pietro Monticone said:

Kevin Buzzard said:

I've reviewed and flagged the four instances which are not like the other 300 or so.

Have you seen these two? https://github.com/leanprover-community/mathlib4/pull/10619#issuecomment-1947480619

Yes, I would include those two.

Done.

[Pietro Monticone]

In this case and this case was not necessary in mathlib seems to mean that Lean 4 does less work to see through definitional equalities when looking for instances.

I've commented the first instance out and it seems to be really needed since it returns errors, while the second one doesn't give any error when commented out.

Should I remove the porting note comment for the first instance and remove the whole second instance?

[Kevin Buzzard]

My instinct is that if you've found a porting note saying "this wasn't needed in Lean 3 but now it's needed", and it is not needed any more (because of a bugfix in Lean 4) then you should triumphantly remove it and make a PR. CI will check to see that mathlib compiles, and if the experts say "aah but we should have this thing anyway because of XYZ" then you can still remove the porting note because the reason it's there is not because of a regression (which is what we're hunting down here) but something else (and hence it has nothing to do with porting).

[Pietro Monticone]

Here is the PR: #10646.

All checks have passed.

Merged.

[Pietro Monticone]

New PR removing the was not necessary porting note comments related to instances, lemmas or tactics that seem to be really needed (i.e. return errors when commented out): #10669.

[Ruben Van de Velde]

I'm confused by your approach here. The notes are there exactly because the code is really needed, so that's not an argument to remove them. The goal of these notes was that we'd come back to them and investigate why the code is needed in lean 4 when it wasn't in lean 3 and potentially to improve lean 4 so we again wouldn't need it

[Pietro Monticone]

Oh, I see. I erroneously believed that the task of "addressing" / "solving" those porting notes entailed verifying the necessity of the associated code.

I've just closed the PR #10669 and opened the issue #10670 with related PR #10671 as above.

[Eric Wieser]

Ruben Van de Velde said:

The notes are there exactly because the code is really needed

The true version is "because the author thought the code was needed at some point in time".
Sometimes the code wasn't needed at all and stemmed from porter confusion;
sometimes it was needed when porting the file began, but became defunct by the time it was merged;
and in many cases, it was needed at the time it was first ported, but later Lean versions have made it defunct much more recently.

[Eric Wieser]

@Pietro Monticone, I don't think it's currently worth going to the trouble of filing issues for a single porting note; the ones that appear 5 or more times are probably more interesting to track

[Pietro Monticone]

Eric Wieser said:

Pietro Monticone, I don't think it's currently worth going to the trouble of filing issues for a single porting note; the ones that appear 5 or more times are probably more interesting to track

Do you think it might be a good idea to group all the “X was not necessary” under the same issue?

[Pietro Monticone]

Update

"Type"	Issue	PR	No. Results	No. Files
simp can prove / simplify this	#10618	#10619	476	186
instance was not necessary (category theory)	#10670	#10671	12	6
dsimp cannot prove this	#10675	#10676	28	13
dsimp can prove this	#10685	#10686	7	7
was rw	#10691	#10692	13	8
added to ease automation	#10688	#10689	22	15
added to speed up elaboration	#10694	#10695	6	2

[Kevin Buzzard]

Where are the thousands of other porting notes? I still have no real feeling what we're looking at here -- is it hundreds of different problems or can they be characterised into a small number of general classes?

[Yaël Dillies]

What's the point of opening both an issue and a PR?

[Eric Wieser]

The issue is the main event, the PR is just "add some references to the issue"

[Eric Wieser]

Having the PRs be self-referential would just be confusing, especially if we add extra notes to the same categorization later

[Eric Wieser]

Kevin Buzzard said:

Where are the thousands of other porting notes?

$ grep -r -h -o -e "[pP]orting note: .*" Mathlib | sort | uniq | wc -l
4654

so most of them are unique

[Matthew Ballard]

Once we have an issue, are keeping porting note in the file?

[Eric Wieser]

1066 of them are about simp

[Pietro Monticone]

I'm not at all sure what the optimal aggregation level is supposed to be.

Among the biggest clusters we can find:

• $\approx 600$ added or added for reason X or added Y or equivalent (maybe requires expert / porter judgment?)
• $\approx 400$ removed or removed for reason X or removed Y or equivalent (maybe requires expert / porter judgment?)
• $\approx 600$ was or was X that I suspect should be subcategorised to facilitate resolution

[Pietro Monticone]

Might it be that the finer the classification the easier and faster will be to solve?

[Pietro Monticone]

Consider, for example, the added keyword.

Should we categorise:

• by purpose (e.g. added to speed up elaboration, added to ease automation, etc.)?
• by topic or Mathlib folder structure (e.g. Algebra, Analysis, etc.)?
• by tactic (e.g. added simp, added rw, etc.)?
• by declaration (e.g. added lemma, added instance, etc.)?

[Richard Osborn]

I noticed that there are duplicates of le_iSup and iInf_le that may be artifacts from the port. Should these be removed? Order/CompleteLattice.lean:L826-L844

[Richard Osborn]

Seems like there are more duplicated theorems due to the removal of the ematch attribute (le_sup_left, le_sup_right, inf_le_left, inf_le_right).

[Matthew Ballard]

I see a good number (edit: ~85) of porting note: todo X where X is a task independent of the port. These should be changed to TODO ...

[Matthew Ballard]

#10697 removes one such that is not independent of porting. See the comment in the PR message for the sanity check.

[Joël Riou]

In the class "lemma was not necessary (category theory)", there are only simp/ext lemmas which could be together in the class "added to ease automation".

[Pietro Monticone]

Joël Riou said:

In the class "lemma was not necessary (category theory)", there are only simp/ext lemmas which could be together in the class "added to ease automation".

Done #10674. I closed the associated issue.

[Pietro Monticone]

"Type"	Issue	PR	No. Results	No. Files
simp can prove this	#10618	#10619	566	200
dsimp can prove this	#10685	#10686	7	7
simp cannot prove this	#10959	#10960	19	9
dsimp cannot prove this	#10675	#10676	28	13
need dsimp only	#10971	#10972	15	2
was rw	#10691	#10692	13	8
was simp	#10745	#10746	46	32
was dsimp	#10934	#10935	8	2
was tidy	#10936	#10937	10	5
added proof	#10888	#10889	8	4
added instance	#10754	#10755	50	25
added lemma	#10756	#10757	40	12
added dsimp only	#10750	#10751	14	1
added to ease automation	#10688	#10689	23	16
added to speed up elaboration	#10694	#10695	6	2
added to clean up types	#10750	#10751	14	1
removed @[nolint has_nonempty_instance]	#10927	#10929	43	27
instance was not necessary (category theory)	#10670	#10671	12	6

[Pietro Monticone]

Related PRs ready to be merged:

• #10929 classifies removed @[nolint has_nonempty_instance] notes
• #10931 fixes misspelled "porting note"
• #10930 classifies more simp can prove this notes
• #10935 classifies was dsimp or used to be dsimp notes
• #10937 classifies was tidy or used to be tidy notes
• #10959 classifies simp cannot prove this
• #10972 classifies need dsimp only

[Kevin Buzzard]

I was under the impression that there were about 8000 porting notes but when I search for them I find nearer 2000. Am I doing something wrong?

[Pietro Monticone]

Kevin Buzzard said:

I was under the impression that there were about 8000 porting notes but when I search for them I find nearer 2000. Am I doing something wrong?

We have almost 800 classified notes and about 7100 still to be classified.

@Kevin Buzzard How are you searching for them?

[Eric Wieser]

Some are upper case and some lower

[Pietro Monticone]

"Type"	Issue	PR	No. Results	No. Files
simp can prove this	#10618	#10619	566	200
dsimp can prove this	#10685	#10686	7	7
simp cannot prove this	#10959	#10960	19	9
dsimp cannot prove this	#10675	#10676	28	13
need dsimp only	#10971	#10972	15	2
was rw	#10691	#10692	13	8
was simp	#10745	#10746	46	32
was dsimp	#10934	#10935	8	2
was tidy	#10936	#10937	10	5
was decide!	#11043	#11044	17	6
added proof	#10888	#10889	8	4
added instance	#10754	#10755	50	25
added lemma	#10756	#10757	40	12
added dsimp only	#10750	#10751	14	1
added to ease automation	#10688	#10689	23	16
added to speed up elaboration	#10694	#10695	6	2
added to clean up types	#10750	#10751	14	1
removed @[nolint has_nonempty_instance]	#10927	#10929	43	27
instance was not necessary (category theory)	#10670	#10671	12	6
broken dot notation	#11036	#11038	28	4
broken proof was	#11039	#11040	13	3
broken ext	#11041	#11042	8	2

[Yaël Dillies]

I also just opened #11034

[Michael Rothgang]

Opened #11037 mimicking #11034. (And just accepted the review suggestions.)

[Richard Osborn]

Yaël Dillies said:

I also just opened #11034

Shouldn't le_sup_left' and other duplicate theorems be deprecated (or removed) in Order.Lattice? It looked like the only reason they existed was for [ematch].

[Pietro Monticone]

"Type"	Issue	PR	No. Results	No. Files
simp can prove this	#10618	#10619	567	204
dsimp can prove this	#10685	#10686	7	7
simp cannot prove this	#10959	#10960	19	9
dsimp cannot prove this	#10675	#10676	28	13
need dsimp only	#10971	#10972	15	2
was rw	#10691	#10692	13	8
was simp	#10745	#10746	46	32
was dsimp	#10934	#10935	8	2
was tidy	#10936	#10937	10	5
was decide!	#11043	#11044	17	6
was infer_instance	#11187	#11188	6	3
added proof	#10888	#10889	8	4
added instance	#10754	#10755	50	25
added lemma	#10756	#10757	114	60
added dsimp only	#10750	#10751	14	1
added to ease automation	#10688	#10689	23	16
added to speed up elaboration	#10694	#10695	6	2
added to clean up types	#10750	#10751	14	1
removed @[nolint has_nonempty_instance]	#10927	#10929	43	27
removed @[simp]	#11119	#11121	21	7
removed @[pp_nodot]	#11180	#11181	4	3
removed @[ext]	#11182	#11183	5	3
instance was not necessary (category theory)	#10670	#10671	12	6
broken dot notation	#11036	#11038	28	4
broken proof was	#11039	#11040	13	3
broken ext	#11041	#11042	8	2
cannot automatically derive	#11081	#11082	6	2
slow(er)	#11083	#11084	38	19
TODO	#11215	#11216	182	112

[Pietro Monticone]

New PRs ready to be merged:

• #11216: classifies TODO porting notes
• #11217: classifies new lemma / added lemma porting notes
• #11225: classifies rw to erw porting notes
• #11228: classifies added dsimp porting notes
• #11230: classifies deprecated porting notes

Here you can find the table updated in real-time: https://github.com/FormalMathematicsLab/mathlib4/discussions/2.

[Pietro Monticone]

Can deprecated sections such as

/-! Porting note (#11229): Deprecated section. Remove. -/
section deprecated
set_option linter.deprecated false

@[deprecated]
theorem power_bit0 (a b : Cardinal) : a ^ bit0 b = a ^ b * a ^ b :=
  power_add
#align cardinal.power_bit0 Cardinal.power_bit0

@[deprecated]
theorem power_bit1 (a b : Cardinal) : a ^ bit1 b = a ^ b * a ^ b * a := by
  rw [bit1, ← power_bit0, power_add, power_one]
#align cardinal.power_bit1 Cardinal.power_bit1

end deprecated

be removed after classification?

[Ruben Van de Velde]

We did half a job deprecating those during the port. Some of those might still be used

[Ruben Van de Velde]

It might also be useful to replace them by variants about Even and Odd

[Kim Morrison]

Unfortunately the bit stuff is hard to remove, because it keeps being used further downstream. I think the right approach is:

• trying removing something @[deprecated] about bit
• see what breaks
• if what breaks is still about bit, cancel removing the first things and remove the downstream thing instead, repeat
• if what breaks is not about bit, announce this discovery, and then see if you can provide alternative to the bit lemmas for that use site
• repeat

It's a bit painful!

[Johan Commelin]

A bit painful indeed :stuck_out_tongue_wink:

[Pietro Monticone]

Resolved and closed #11249.

[Pietro Monticone]

"Type"	Issue	PR	No. Results	No. Files
simp can prove this	#10618	#10619	567	204
dsimp can prove this	#10685	#10686	7	7
simp cannot prove this	#10959	#10960	19	9
dsimp cannot prove this	#10675	#10676	28	13
need dsimp only	#10971	#10972	15	2
was rw	#10691	#10692	13	8
was simp	#10745	#10746	46	32
was dsimp	#10934	#10935	8	2
was tidy	#10936	#10937	10	5
was decide!	#11043	#11044	17	6
was infer_instance	#11187	#11188	6	3
added proof	#10888	#10889	8	4
added instance	#10754	#10755	77	37
added theorem / lemma	#10756	#10757 / #11432	233	115
added definition	#11445	#11446	12	9
added dsimp	#11227	#11228	11	4
added dsimp only	#10750	#10751	14	1
added to ease automation	#10688	#10689	23	16
added to speed up elaboration	#10694	#10695	6	2
added to clean up types	#10750	#10751	14	1
removed @[nolint has_nonempty_instance]	#10927	#10929	43	27
removed @[simp]	#11119	#11121	21	7
removed @[pp_nodot]	#11180	#11181	19	4
removed @[ext]	#11182	#11183	5	3
instance was not necessary (category theory)	#10670	#10671	12	6
broken dot notation	#11036	#11038	36	5
broken proof was	#11039	#11040	13	3
broken ext	#11041	#11042	8	2
cannot automatically derive	#11081	#11082	6	2
slow(er)	#11083	#11084	38	19
TODO	#11215	#11216	182	112
change rw to erw	#11224	#11225	9	5
change (coe : ℤ → α) to (Int.cast : ℤ → α)	#11249	#11250	10	1
deprecated	#11229	#11230	4	2
rfl required	#11441	#11442	6	1
apply → induction	#11443	#11444	9	1

[Pietro Monticone]

PRs ready to be merged:

• #11432 classifying "new theorem" / "new lemma" porting notes
• #11433 classifying "new instance" porting notes
• #11442 classifying "rfl required" porting notes
• #11444 classifying "apply to induction" porting notes
• #11446 classifying "new definition" porting notes
• #11447 classifying "removed @[pp_nodot]" porting note

[Michael Rothgang]

#12061 and #12074 resolve a few more simp-related porting notes: in all cases, the original proof works again. I suspect this may be due to changes in 4.7.0, but haven't investigated.

[Michael Rothgang]

Status update: #12061 has been merged (thanks for the review!); #12074 is ready for review.
A few new PRs were filed (some, but not all are mine)

• #12088 and #12092 (simps-related)
• #12098: classify porting notes referencing a missing linter
• #12100, #12102: resolve one simple porting note each (about a tactic which has since been implemented)
• #12101: resolve all porting notes about "redundant binder updates"

[Johan Commelin]

Thanks so much! Most of these are now on the merge queue or bors d+.

[Michael Rothgang]

Thank you for the quick reviews. I addressed the feedback on #12074.
My github verification emails are having trouble coming through; see free to bors this yourself.

[Michael Rothgang]

A few new PRs on this theme

• #12126 and #12128 (restoring some simp-related proofs)
• #12130 (classifying porting notes about beta reduction)

[Kim Morrison]

'd #12126

[Kim Morrison]

'd #12128

[Kim Morrison]

and 'd #12130. I wonder if we might just declare victory on this one. I don't think we're expecting to change anything to remove the need for these beta_reduces.

[Eric Wieser]

(#12129 for the issue)

[Michael Rothgang]

Kim Morrison said:

'd #12128

There was a merge conflict with #12126; this was resolved and CI is green. Can somebody re-approve this one, please?

[Michael Rothgang]

(Thanks for all the fast reviews!)

[Riccardo Brasca]

Done!