std4 / Lean4 bump

Stream: mathlib4

[Scott Morrison]

I started the bump of mathlib4 to the current std4 and lean4 at #5409. There is a lot still to do on this PR. I've labelled it help-wanted.

Some of it is that material on Fin has been upstreamed, but in complicated ways changing definitions. e.g. def castLE (h : n ≤ m) : Fin n ↪o Fin m has now been taken by the plain function, so we will need to rename the order embedding.

In other files there are mysterious problems with simp, and change, and who know what else.

As we may need to continue bumping Lean4 versions to finish the port, this bump is an integral part of the porting process... :-) Boss levels were promised!

[Ruben Van de Velde]

I'll take a look for the next 10 minutes or so

[Ruben Van de Velde]

Fun: the hypothesis in Fin.pred changed from i ≠ 0 to ↑i ≠ 0

[Ruben Van de Velde]

I'm thinking it'll be best to rename the mathlib Fin declarations first, independently of the bump

[Jeremy Tan]

Scott Morrison said:

...of the porting process... :-) Boss levels were promised!

This (the porting process) is not a video game, Scott

[Kevin Buzzard]

It's a puzzle game!

[Jeremy Tan]

What I'm saying is that the analogy between playing any sort of game and the porting process is inappropriate. According to such analogy we're not playing the game, we're developing it

[Bulhwi Cha]

Let's not read too much into the analogy.

[Jeremy Tan]

Anyway !4#5584, which renames Fin-related declarations, is ready for review

[James Gallicchio]

I'm thinking for future std<-mathlib PRs we should also have matching mathlib4 PRs that make sure things compile again...

[Mario Carneiro]

What's the status of this PR? It says it depends on #5584, which looks ready for review, @Ruben Van de Velde ?

[Ruben Van de Velde]

@Jeremy Tan started messing with that pr while I was working on it, I'm not sure what the status is now

[Mario Carneiro]

it appears to be passing CI now

[Mario Carneiro]

I'm going to guess that there isn't anything more coming from him on the PR, so I think the ball is in your court

[Mario Carneiro]

The current bump draft seems to be dropping a lot of lemmas about fin definitions in favor of theorems about the *Emb versions, which I think is likely to be the wrong default. But the lemmas about these definitions should live in std, so I've started working on the upstreaming at std#173. Please feel free to jump in and work on that, as it's a big file.

[Ruben Van de Velde]

My idea was to keep the theorems saying the same thing even though std gained different definitions with the existing names. We could change that separately

[Mario Carneiro]

yeah, that will mean that mathlib will have to basically completely avoid the fin definitions and that will require a bunch of additional work to clean up later

[Mario Carneiro]

We will in almost every case want theorems either only about the non Emb version or about both

[Mario Carneiro]

Std didn't get different definitions with the same names, the new definitions are drop in replacements for the old ones in most situations, so it will probably be less text shuffling to use the new definitions

[Scott Morrison]

Currently #5409 has a merge conflict (the latest dependent PR #5715 has been merged).

[Scott Morrison]

(There is no std# linkifier. The repository is called std4, so the linkifier is std4#173.)

[Mario Carneiro]

The std PR is now ready, although there is a lot of stuff in there and maybe someone other than me could give it a review?

[Scott Morrison]

@Ruben Van de Velde, would you be able to either do the merge of master into #5409, or give approval to abandon the changes currently on #5409 to Mathlib.Data.Fin.Basic so we can start over on that file?

It would be great to resume tracking std4 and lean4, but the PR is in a borked state that is hard to work on at the moment. :-)

[Ruben Van de Velde]

@Scott Morrison I may have some time to look at it later today, but feel free to abandon anything as you see fit

[Jeremy Tan]

A better way forward is to revert all new changes to lean4 and std4, but keep the change introducing the additional config for congr that is needed for #5032

[Jeremy Tan]

Then try each reverted commit one by one to see which ones require large refactors to mathlib4

[Scott Morrison]

Jeremy, this isn't a viable approach, unfortunately. Mathlib is a downstream project, in the fortunate situation that the maintainers of its upstream projects care very much about its success. Nevertheless, we've got to sort it out in Mathlib.

[Jeremy Tan]

I'm looking at the build error log, and many of the errors are metavariable-related (or are timeouts) and in category theory files. I see no way to fix them all without yet more fixes upstream – or reversions upstream

[Scott Morrison]

We can certainly ask for fixes or reversions upstream. Perhaps I misunderstood your suggestion. Certainly it's fine if we want to manually run mathlib4 against each Lean4 commit, in order to track down the moment at which the problem occurs. But it's probably "cheaper" to do be investigating the error. (Sorry I haven't had time to look at this bump PR.)

[Sebastian Ullrich]

A pleasant surprise? http://speedcenter.informatik.kit.edu/mathlib4/run-detail/95b755a6-1aa7-4e7f-8ffa-1697ff99406c
(4% total speedup if you don't want to scroll through that wall of deltas)

[Matthew Ballard]

10% on typeclass inference

[Notification Bot]

11 messages were moved from this topic to #mathlib4 > changing algebra instance priorities by Eric Wieser.