Mathlib bump

Stream: FLT-regular

[Riccardo Brasca]

Can you announce here when you bump mathlib? i.e. when you do leanproject up. It's better to say it because if I do git pull and I don't realize mathlib has changed I get the orange bar if I don't fetch the oleans.

[Alex J. Best]

Sorry for any confusion, I also added the auto-bumper script, so seeing as the code now compiles it will bump itself every day without anybody manually intervening. You should always be able to see from the git pull output (if you are on command line) that the toml file was changed

[Riccardo Brasca]

Ah, I see! But what happens if the code doesn't compile with the new mathlib?

[Riccardo Brasca]

In LTE we see this all the time, it happens that making the bump is quite a lot of work.

[Johan Commelin]

@Riccardo Brasca Then the bot opens an issue, and waits until you do a manual bump.

[Riccardo Brasca]

Wow, very nice!!

[Johan Commelin]

After that it will pick up auto-bumping daily, until the bump breaks again.

[Riccardo Brasca]

@Alex J. Best Do you also know how to set up CI?

[Alex J. Best]

I'll have a go at it today :blush:!

[Patrick Massot]

Riccardo Brasca said:

Can you announce here when you bump mathlib? i.e. when you do leanproject up. It's better to say it because if I do git pull and I don't realize mathlib has changed I get the orange bar if I don't fetch the oleans.

Sounds like it's time for you to learn about leanproject pull.

[Alex J. Best]

Ok we now have CI (thanks to @bentoner, who did this for lean-liquid this wasn't too hard), olean caches can't be dowloaded yet, probably that needs some permissions setting up on the azure side, but seeing as we are still in the beginning of the project hopefully this isnt an issue for anyone already!

[Riccardo Brasca]

Thank you!! I agree we don't need olean caches for the moment.

[Chris Birkbeck]

I take it mathlib bump is just the same as doing leanproject up. In which case, I just did one and class_group.fintype_of_cyclotomic_ring is working now :)

[Riccardo Brasca]

It was working even before, I disabled the instance this morning. See my message in the topic general notation

[Chris Birkbeck]

Yeah sorry I didn't read it carefully enough!

[Eric Wieser]

I've a follow-up planned to try to fix it

[Riccardo Brasca]

The github mark is finally green! Let's try to keep it like that :sweat_smile:

[Eric Wieser]

Eric Wieser said:

I've a follow-up planned to try to fix it

I tried to fix it in #10220; but I think this diamond might be impossible to solve with the current definition of splitting_field

[Riccardo Brasca]

Don't worry! At the moment everything works for us :)

[Eric Wieser]

I worry only because it seems like a diamond that's impossible to solve, and we haven't seen those before

[Riccardo Brasca]

Well, maybe this is just an indication that the definition of splitting_field is not the good one. What is the problem? (If it's not too complicated to explain.)

[Eric Rodriguez]

he put a good note on it in that commit, I am surprised this hasn't been run into before though :/

[Eric Rodriguez]

(an "unsolvable" diamond, that is, not this specific one)

[Kevin Buzzard]

After some (in-person!) discussion with Eric W yesterday he told me that the diamond could be solved if we refactor splitting_field just to be "field spanned by roots of f in some algebraic closure of base field", and we have algebraic closures now IIRC

[Eric Wieser]

I think it would be fairer to say that I said that would work when you suggested it; I'd not even heard of algebraic closures until you brought it up!

[Johan Commelin]

Does that mean the definition will depend on the choice of an algebraic closure?

[Johan Commelin]

Also, did you check that the construction of algebraic closures doesn't use splitting fields under the hood? I wouldn't be surprised if it does.

[Eric Wieser]

docs#algebraic_closure for reference

[Eric Wieser]

Actually I'm pretty sure that won't work as the algebra structure is built with docs#ring_hom.to_algebra so has the bad default nsmul fields

[Eric Wieser]

And it looks suspiciously recursive, which is likely to run into the same problems as splitting_field

[Johan Commelin]

Algebraic closures are highly non-canonical. So I would be somewhat surprised if they solve defeq issues.

[Kevin Buzzard]

Splitting fields are also noncanonical

[Kevin Buzzard]

The construction of alg closure I know doesn't use splitting fields; conversely I've defined splitting fields via alg closure in a course before so I'm pretty sure it can be made to work

[Eric Rodriguez]

I just bumped — please all note the absolutely atrocious proof of gcd_mul_fun; does anyone see a better way to do this? I'm going to go take a walk...

[Eric Rodriguez]

is it just me, or does it sometimes feel like every time the bumper bot upgrades, it doesn't work and you have to manually bump again?

[Alex J. Best]

What doesn't work specifically?

[Alex J. Best]

I get a weird git sha not found error sometimes, but never bothered tracking it down

[Eric Rodriguez]

exactly that

[Alex J. Best]

Like if you do git pull and then leanproject get-mathlib-cache?

[Alex J. Best]

Or do you use leanproject pull

[Eric Rodriguez]

i've never tried leanproject pull if i'm honest

[Alex J. Best]

Same, its fairly new, I also am not in the habit of using it and see the same issue as you, so I was wondering if the fix is just for us to try and be in the habit of using that. Perhaps the issue is that the get-mathlib-cache command doesn't do a git fetch for the _target/deps/mathlib/ directory and thats why we get a confusing message that git cant find the sha?

[Eric Rodriguez]

that would make a lot of sense! I'll try it next time

[Kevin Buzzard]

Is the issue the same as my Nov 6 message to #condensed mathematics saying that I didn't know the workflow for bumps on that project? Sorry can't link, on mobile

[Eric Rodriguez]

I think so, yes (it was the same error message, anyways)

[Eric Wieser]

I think this might have been fixed by Patrick in an unreleased version

[Alex J. Best]

I just hit this again, and can confirm that installing the master version of mathlib-tools fixes it.
@Patrick Massot if you have time to release the new version I'm sure it will help some people out :+1:

[Riccardo Brasca]

Hi everybody, this week I have a collaborator visiting me and I will be less active than usual, but I am confident you will continue your great work :grinning:

[Riccardo Brasca]

Today's bump has been a little more annoying than usual

git diff c087cd0 --stat
 leanpkg.toml                                              |  4 ++--
 src/number_theory/cyclotomic/absolute_value.lean          | 13 +++++++------
 src/number_theory/cyclotomic/cyclotomic_units.lean        |  2 +-
 src/number_theory/cyclotomic/number_field_embeddings.lean |  1 +
 src/ready_for_mathlib/cycl_poly.lean                      | 76 ----------------------------------------------------------------------------
 src/ready_for_mathlib/discriminant.lean                   | 17 +----------------
 src/ready_for_mathlib/ne_zero.lean                        |  4 ----
 7 files changed, 12 insertions(+), 105 deletions(-)

but it is now done.

[Johan Commelin]

Good diff! You got rid of about 90 lines!

[Riccardo Brasca]

Does anyone know what happened to covariant_class ℝ≥0 ℝ≥0 has_mul.mul has_le.le? After the last bump Lean is not finding it anymore...

[Riccardo Brasca]

I am fixing it, but I don't understand what happened, for example

lemma eq_one_of_pow_eq_one {n : ℕ} (hn : 0 < n) {t : ℝ≥0} (h_pow : t ^ n = 1) : t = 1 :=
(pow_eq_one_iff hn.ne').mp h_pow

fails, but

lemma eq_one_of_pow_eq_one {n : ℕ} (hn : 0 < n) {t : ℝ≥0} (h_pow : t ^ n = 1) : t = 1 :=
(@pow_eq_one_iff _ _ _ nnreal.covariant_mul _ _ hn.ne').mp h_pow

works

[Eric Rodriguez]

yes, I was confused by this too... image.png these are the commits in between the last two bumps, but I don't see how that changed anything

[Eric Rodriguez]

data/nnreal/basic was touched twice in both of these commits, but both of these were Yael changing very small things that aren't related to covariant_mul.

[Riccardo Brasca]

@Yaël Dillies I am randomly pinging you even if you look innocent

[Yaël Dillies]

I think I indeed am

[Johan Commelin]

Same problem while bumping LTE. No idea what the problem is.

[Johan Commelin]

The instance nnreal.covariant_mul is there in nnreal.lean.

[Eric Wieser]

Is docs#non_unital_non_assoc_ring to blame?

[Riccardo Brasca]

@Eric Rodriguez Can you PR the results here? Thanks!

[Eric Rodriguez]

yes, sorry, been slow on PRing!

[Eric Rodriguez]

I've just bumped, I think something about mod_cast has changed so things aren't working so well (cf here).

[Eric Rodriguez]

I wonder if the correct way to do these sorts of things are to have stronger versions of coe, which would be like fun_like

[Riccardo Brasca]

Ouf this is annoying

[Riccardo Brasca]

Thanks for the bump

[Anne Baanen]

Eric Rodriguez said:

I wonder if the correct way to do these sorts of things are to have stronger versions of coe, which would be like fun_like

This is something I have been interested in for a bit, never had the chance to work on it yet. At least, I think we should split up the algebra class into a "scalar multiplication" part and a "canonical ring hom" part. And we could express the "canonical ring hom" part by subclassing has_coe(_t).

[Oliver Nash]

Would such a change be compatible with / make it easier to redefine algebra as:

class algebra (R A : Type*) [semiring R] [non_unital_non_assoc_semiring A] extends module R A :=
(smul_mul_assoc' : ∀ (t : R) (a b : A), (t • a) * b = t • (a * b))
(mul_smul_comm' : ∀ (t : R) (a b : A), a * (t • b) = t • (a * b))

(which has the advantage that we can use algebra to talk about non-unital and/or non-assoc algebras if we want)

[Anne Baanen]

Indeed, your redefinition would exactly be the first part that we split algebra into.

[Eric Wieser]

What's the advantage of that definition vs using the existing typeclasses described in docs#algebra?

[Eric Wieser]

Because here's one downside: using the separate typeclasses let's you relax R to a monoid (eg the units of your algebra)

[Eric Wieser]

I do agree though that there's a place for a separate "canonical ring hom" class, which would cover matrix.scalar and polynomial.C in places where the ground ring isn't commutative

[Anne Baanen]

I made a new discussion thread about "has canonical hom" in #general

[Riccardo Brasca]

Can you announce here when you bump mathlib? i.e. when you do leanproject up. It's better to say it because if I do git pull and I don't realize mathlib has changed I get the orange bar if I don't fetch the oleans.

[Alex J. Best]

Sorry for any confusion, I also added the auto-bumper script, so seeing as the code now compiles it will bump itself every day without anybody manually intervening. You should always be able to see from the git pull output (if you are on command line) that the toml file was changed

[Riccardo Brasca]

Ah, I see! But what happens if the code doesn't compile with the new mathlib?

[Riccardo Brasca]

In LTE we see this all the time, it happens that making the bump is quite a lot of work.

[Johan Commelin]

@Riccardo Brasca Then the bot opens an issue, and waits until you do a manual bump.

[Riccardo Brasca]

Wow, very nice!!

[Johan Commelin]

After that it will pick up auto-bumping daily, until the bump breaks again.

[Riccardo Brasca]

@Alex J. Best Do you also know how to set up CI?

[Alex J. Best]

I'll have a go at it today :blush:!

[Patrick Massot]

Riccardo Brasca said:

Can you announce here when you bump mathlib? i.e. when you do leanproject up. It's better to say it because if I do git pull and I don't realize mathlib has changed I get the orange bar if I don't fetch the oleans.

Sounds like it's time for you to learn about leanproject pull.

[Alex J. Best]

Ok we now have CI (thanks to @bentoner, who did this for lean-liquid this wasn't too hard), olean caches can't be dowloaded yet, probably that needs some permissions setting up on the azure side, but seeing as we are still in the beginning of the project hopefully this isnt an issue for anyone already!

[Riccardo Brasca]

Thank you!! I agree we don't need olean caches for the moment.

[Chris Birkbeck]

I take it mathlib bump is just the same as doing leanproject up. In which case, I just did one and class_group.fintype_of_cyclotomic_ring is working now :)

[Riccardo Brasca]

It was working even before, I disabled the instance this morning. See my message in the topic general notation

[Chris Birkbeck]

Yeah sorry I didn't read it carefully enough!

[Eric Wieser]

I've a follow-up planned to try to fix it

[Riccardo Brasca]

The github mark is finally green! Let's try to keep it like that :sweat_smile:

[Eric Wieser]

Eric Wieser said:

I've a follow-up planned to try to fix it

I tried to fix it in #10220; but I think this diamond might be impossible to solve with the current definition of splitting_field

[Riccardo Brasca]

Don't worry! At the moment everything works for us :)

[Eric Wieser]

I worry only because it seems like a diamond that's impossible to solve, and we haven't seen those before

[Riccardo Brasca]

Well, maybe this is just an indication that the definition of splitting_field is not the good one. What is the problem? (If it's not too complicated to explain.)

[Eric Rodriguez]

he put a good note on it in that commit, I am surprised this hasn't been run into before though :/

[Eric Rodriguez]

(an "unsolvable" diamond, that is, not this specific one)

[Kevin Buzzard]

After some (in-person!) discussion with Eric W yesterday he told me that the diamond could be solved if we refactor splitting_field just to be "field spanned by roots of f in some algebraic closure of base field", and we have algebraic closures now IIRC

[Eric Wieser]

I think it would be fairer to say that I said that would work when you suggested it; I'd not even heard of algebraic closures until you brought it up!

[Johan Commelin]

Does that mean the definition will depend on the choice of an algebraic closure?

[Johan Commelin]

Also, did you check that the construction of algebraic closures doesn't use splitting fields under the hood? I wouldn't be surprised if it does.

[Eric Wieser]

docs#algebraic_closure for reference

[Eric Wieser]

Actually I'm pretty sure that won't work as the algebra structure is built with docs#ring_hom.to_algebra so has the bad default nsmul fields

[Eric Wieser]

And it looks suspiciously recursive, which is likely to run into the same problems as splitting_field

[Johan Commelin]

Algebraic closures are highly non-canonical. So I would be somewhat surprised if they solve defeq issues.

[Kevin Buzzard]

Splitting fields are also noncanonical

[Kevin Buzzard]

The construction of alg closure I know doesn't use splitting fields; conversely I've defined splitting fields via alg closure in a course before so I'm pretty sure it can be made to work

[Eric Rodriguez]

I just bumped — please all note the absolutely atrocious proof of gcd_mul_fun; does anyone see a better way to do this? I'm going to go take a walk...

[Eric Rodriguez]

is it just me, or does it sometimes feel like every time the bumper bot upgrades, it doesn't work and you have to manually bump again?

[Alex J. Best]

What doesn't work specifically?

[Alex J. Best]

I get a weird git sha not found error sometimes, but never bothered tracking it down

[Eric Rodriguez]

exactly that

[Alex J. Best]

Like if you do git pull and then leanproject get-mathlib-cache?

[Alex J. Best]

Or do you use leanproject pull

[Eric Rodriguez]

i've never tried leanproject pull if i'm honest

[Alex J. Best]

Same, its fairly new, I also am not in the habit of using it and see the same issue as you, so I was wondering if the fix is just for us to try and be in the habit of using that. Perhaps the issue is that the get-mathlib-cache command doesn't do a git fetch for the _target/deps/mathlib/ directory and thats why we get a confusing message that git cant find the sha?

[Eric Rodriguez]

that would make a lot of sense! I'll try it next time

[Kevin Buzzard]

Is the issue the same as my Nov 6 message to #condensed mathematics saying that I didn't know the workflow for bumps on that project? Sorry can't link, on mobile

[Eric Rodriguez]

I think so, yes (it was the same error message, anyways)

[Eric Wieser]

I think this might have been fixed by Patrick in an unreleased version

[Alex J. Best]

I just hit this again, and can confirm that installing the master version of mathlib-tools fixes it.
@Patrick Massot if you have time to release the new version I'm sure it will help some people out :+1:

[Riccardo Brasca]

Hi everybody, this week I have a collaborator visiting me and I will be less active than usual, but I am confident you will continue your great work :grinning:

[Riccardo Brasca]

Today's bump has been a little more annoying than usual

git diff c087cd0 --stat
 leanpkg.toml                                              |  4 ++--
 src/number_theory/cyclotomic/absolute_value.lean          | 13 +++++++------
 src/number_theory/cyclotomic/cyclotomic_units.lean        |  2 +-
 src/number_theory/cyclotomic/number_field_embeddings.lean |  1 +
 src/ready_for_mathlib/cycl_poly.lean                      | 76 ----------------------------------------------------------------------------
 src/ready_for_mathlib/discriminant.lean                   | 17 +----------------
 src/ready_for_mathlib/ne_zero.lean                        |  4 ----
 7 files changed, 12 insertions(+), 105 deletions(-)

but it is now done.

[Johan Commelin]

Good diff! You got rid of about 90 lines!

[Riccardo Brasca]

Does anyone know what happened to covariant_class ℝ≥0 ℝ≥0 has_mul.mul has_le.le? After the last bump Lean is not finding it anymore...

[Riccardo Brasca]

I am fixing it, but I don't understand what happened, for example

lemma eq_one_of_pow_eq_one {n : ℕ} (hn : 0 < n) {t : ℝ≥0} (h_pow : t ^ n = 1) : t = 1 :=
(pow_eq_one_iff hn.ne').mp h_pow

fails, but

lemma eq_one_of_pow_eq_one {n : ℕ} (hn : 0 < n) {t : ℝ≥0} (h_pow : t ^ n = 1) : t = 1 :=
(@pow_eq_one_iff _ _ _ nnreal.covariant_mul _ _ hn.ne').mp h_pow

works

[Eric Rodriguez]

yes, I was confused by this too... image.png these are the commits in between the last two bumps, but I don't see how that changed anything

[Eric Rodriguez]

data/nnreal/basic was touched twice in both of these commits, but both of these were Yael changing very small things that aren't related to covariant_mul.

[Riccardo Brasca]

@Yaël Dillies I am randomly pinging you even if you look innocent

[Yaël Dillies]

I think I indeed am

[Johan Commelin]

Same problem while bumping LTE. No idea what the problem is.

[Johan Commelin]

The instance nnreal.covariant_mul is there in nnreal.lean.

[Eric Wieser]

Is docs#non_unital_non_assoc_ring to blame?

[Riccardo Brasca]

@Eric Rodriguez Can you PR the results here? Thanks!

[Eric Rodriguez]

yes, sorry, been slow on PRing!

[Eric Rodriguez]

I've just bumped, I think something about mod_cast has changed so things aren't working so well (cf here).

[Eric Rodriguez]

I wonder if the correct way to do these sorts of things are to have stronger versions of coe, which would be like fun_like

[Riccardo Brasca]

Ouf this is annoying

[Riccardo Brasca]

Thanks for the bump

[Anne Baanen]

Eric Rodriguez said:

I wonder if the correct way to do these sorts of things are to have stronger versions of coe, which would be like fun_like

This is something I have been interested in for a bit, never had the chance to work on it yet. At least, I think we should split up the algebra class into a "scalar multiplication" part and a "canonical ring hom" part. And we could express the "canonical ring hom" part by subclassing has_coe(_t).

[Oliver Nash]

Would such a change be compatible with / make it easier to redefine algebra as:

class algebra (R A : Type*) [semiring R] [non_unital_non_assoc_semiring A] extends module R A :=
(smul_mul_assoc' : ∀ (t : R) (a b : A), (t • a) * b = t • (a * b))
(mul_smul_comm' : ∀ (t : R) (a b : A), a * (t • b) = t • (a * b))

(which has the advantage that we can use algebra to talk about non-unital and/or non-assoc algebras if we want)

[Anne Baanen]

Indeed, your redefinition would exactly be the first part that we split algebra into.

[Eric Wieser]

What's the advantage of that definition vs using the existing typeclasses described in docs#algebra?

[Eric Wieser]

Because here's one downside: using the separate typeclasses let's you relax R to a monoid (eg the units of your algebra)

[Eric Wieser]

I do agree though that there's a place for a separate "canonical ring hom" class, which would cover matrix.scalar and polynomial.C in places where the ground ring isn't commutative

[Anne Baanen]

I made a new discussion thread about "has canonical hom" in #general

[Ruben Van de Velde]

I started a new bump at https://github.com/leanprover-community/flt-regular/pull/new/bump-2023-12-18 , but running into a number of timeouts in FltRegular/CaseII/InductionStep.lean. Also FractionalIdeal.dual seems to have been generalized a lot in upstreaming in ways that break the code that uses it, so I left the old one in place for now

[Riccardo Brasca]

I suggest to wait for #9063 to be merged before doing another bump (it fixes impliciteness of some variables). But the new timeouts are annoying.

[Ruben Van de Velde]

That will help with using FractionalIdeal.dual from mathlib, but probably not with the timeouts. If someone has time to look at those, that could be helpful

[Andrew Yang]

I'm having a look.