reenableeta !4#3414

Stream: mathlib4

[Matthew Ballard]

I (think I) yanked all occurrences of etaExperiment in this branch

[Scott Morrison]

@Matthew Ballard, when you removed all the maxHeartbeats you left in place many of the now redundant -- Porting notes. I commented on many, but I think it might be easier to just let you do another pass rather than leave excessively many review comments.

[Matthew Ballard]

Scott Morrison said:

Matthew Ballard, when you removed all the maxHeartbeats you left in place many of the now redundant -- Porting notes. I commented on many, but I think it might be easier to just let you do another pass rather than leave excessively many review comments.

Feel free to revert. Lesson: two bumps remain. Everything else can be removed.

[Matthew Ballard]

In the middle of the evening routine and might not touch things again until tomorrow morning.

[Scott Morrison]

I've cleaned up these porting notes now.

[Scott Morrison]

@Gabriel Ebner, as far as I'm concerned I think it's okay to merge !4#4009 into reenableeta.

[Scott Morrison]

For that matter, I think after doing that it's fine to just merge reenableeta, and then tomorrow we'll switch the toolchain back to the nightly. I don't think it's particularly harmful to use a custom toolchain temporarily. This will enable everyone to fix up all the branches which rely on this without having to do the dependent PR dance.

[Scott Morrison]

I got as far as reviewing through to Mathlib/LinearAlgebra/Matrix/Basis.lean on the !4#3414 branch, and am happy with the changes through to there, but am now offline for a while.

[Scott Morrison]

It would be great if someone could look through the rest.

[Scott Morrison]

We do have a lot of porting notes referencing lean4#2074, which should all be fixed up now, but I propose we do that in a second PR, after getting !4#3414 through.

[Notification Bot]

10 messages were moved here from #mathlib4 > port progress by Scott Morrison.

[Scott Morrison]

Mathlib.RingTheory.Finiteness has many messy porting notes that can be cleaned up post lean4#2210. If someone is keen to clean up, please push fixes direct to !4#3414. Otherwise, let's not wait on this file for !4#3414.

[Scott Morrison]

I'm still cleaning up comments in reenableeta. I won't name names or anything, but do please be careful doing regex modifications: A change that takes the comment

-- Porting note:
-- This is another alarming location where we need to use
-- `eta_experiment%` to elaborate a particular subterm, but having `synthInstance.etaExperiment`
-- on for the whole declaration breaks other typeclass search.

and just deletes the 3rd line is not particularly helpful. :-)

[Johan Commelin]

It builds!

[Scott Morrison]

There is further cleanup that can be done, but I'm taking the attitude that if there's any cleanup related to this PR where there is already a porting note that mentions lean4#2074, lean4#2210, or !4#3414, then we can do that cleanup later. :-)

[Mauricio Collares]

The nightly is out too

[Scott Morrison]

Okay, I have bumped !4#3414 to use the nightly, but something is seriously weird. In Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence something that should be an n + 2 is apparently now a Nat.succ n + 1 + 1.

[Scott Morrison]

I am bamboozled. This wasn't happening on Gabriel's tag, so this is some interaction with one of the other commits on leanprover/lean4:nightly-2023-05-16?

[Scott Morrison]

I have to admit that debugging 4 line simpa commands makes me want to say that ... we shouldn't have 4 line simpa commands, and this is precisely what have is for.

[Mauricio Collares]

Isn't that lean4#2146?

[Matthew Ballard]

Yeah. Similar things were already occurring with existing nightly. Not sure why it changed now in this file.

[Matthew Ballard]

Isn’t that PR merged in the most recent nightly?

[Scott Morrison]

Yes, lean4#2146 hasn't landed in master, it is coming in on !4#3414 (hopefully very soon).

[Scott Morrison]

I've fixed this issue. I left the proof "ungolfed" so its easier to understand the regression. There's a porting note.

[Scott Morrison]

https://github.com/leanprover-community/mathlib4/pull/3414/commits/ea334e44c4ca827fbf45c58fb8d6c4933d1ccb10

[Scott Morrison]

I also mentioned it back on lean4#2146.

[Jeremy Tan]

!4#3414 is merged

[Oliver Nash]

Does this mean we can now drop a bunch of:

attribute [-instance] Ring.toNonAssocRing

(and similar)?

[Matthew Ballard]

Many of those are gone now. There is still additional cleanup from other ad-hoc workarounds that are now in master.

[Oliver Nash]

OK great. A quick experiment showed me some still remain but in each case they were not necessary. I don't really have time for Lean at the moment but if they're still present in a week or so, I'll try to do some more cleanup of ad-hoc workarounds like this.

[Matthew Ballard]

Scott Morrison said:

I'm still cleaning up comments in reenableeta. I won't name names or anything, but do please be careful doing regex modifications

Apologies for leaving a mess and much thanks for cleaning it up!

[Scott Morrison]

There are four further cleanup PRs at !4#4029, !4#4031, !4#4032, !4#4033.

[Matthew Ballard]

Also !4#4028

[Matthew Ballard]

And !4#4030 too!

[Jeremy Tan]

I think we just had a three-way collision, but note that the simpNF linter still fails on !4#3651 (AffineIsometry) even with global eta

[Scott Morrison]

Looks like there will only be whitespace conflicts, however. I just delegated yours, @Jeremy Tan, please merge when you have a green dot! :-)