Zulip Chat Archive

Stream: FLT-regular

Topic: Mathlib bump


Riccardo Brasca (Oct 28 2021 at 08:30):

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 (Oct 28 2021 at 08:39):

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 (Oct 28 2021 at 08:40):

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

Riccardo Brasca (Oct 28 2021 at 08:41):

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

Johan Commelin (Oct 28 2021 at 08:58):

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

Riccardo Brasca (Oct 28 2021 at 08:58):

Wow, very nice!!

Johan Commelin (Oct 28 2021 at 08:58):

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

Riccardo Brasca (Oct 28 2021 at 09:11):

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

Alex J. Best (Oct 28 2021 at 09:12):

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

Patrick Massot (Oct 28 2021 at 11:31):

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 (Oct 28 2021 at 13:47):

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 (Oct 28 2021 at 13:51):

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

Chris Birkbeck (Oct 28 2021 at 19:54):

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 (Oct 28 2021 at 20:01):

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

Chris Birkbeck (Oct 28 2021 at 20:05):

Yeah sorry I didn't read it carefully enough!

Eric Wieser (Oct 28 2021 at 22:04):

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

Riccardo Brasca (Oct 29 2021 at 11:22):

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

Eric Wieser (Nov 08 2021 at 14:12):

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 (Nov 08 2021 at 14:19):

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

Eric Wieser (Nov 08 2021 at 14:49):

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

Riccardo Brasca (Nov 08 2021 at 15:06):

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 (Nov 08 2021 at 15:28):

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

Eric Rodriguez (Nov 08 2021 at 15:28):

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

Kevin Buzzard (Nov 10 2021 at 15:24):

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 (Nov 10 2021 at 19:00):

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 (Nov 10 2021 at 20:12):

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

Johan Commelin (Nov 10 2021 at 20:12):

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 (Nov 10 2021 at 20:20):

docs#algebraic_closure for reference

Eric Wieser (Nov 10 2021 at 20:26):

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 (Nov 10 2021 at 20:27):

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

Johan Commelin (Nov 10 2021 at 20:29):

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

Kevin Buzzard (Nov 11 2021 at 10:22):

Splitting fields are also noncanonical

Kevin Buzzard (Nov 11 2021 at 10:23):

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 (Nov 13 2021 at 17:40):

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 (Nov 14 2021 at 12:12):

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 (Nov 14 2021 at 12:14):

What doesn't work specifically?

Alex J. Best (Nov 14 2021 at 12:14):

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

Eric Rodriguez (Nov 14 2021 at 12:16):

exactly that

Alex J. Best (Nov 14 2021 at 12:19):

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

Alex J. Best (Nov 14 2021 at 12:19):

Or do you use leanproject pull

Eric Rodriguez (Nov 14 2021 at 12:25):

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

Alex J. Best (Nov 14 2021 at 13:00):

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 (Nov 14 2021 at 13:04):

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

Kevin Buzzard (Nov 14 2021 at 13:58):

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 (Nov 14 2021 at 14:18):

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

Eric Wieser (Nov 14 2021 at 14:43):

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

Alex J. Best (Nov 20 2021 at 12:59):

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 (Nov 29 2021 at 11:11):

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 (Jan 12 2022 at 10:29):

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 (Jan 12 2022 at 10:44):

Good diff! You got rid of about 90 lines!

Riccardo Brasca (Jan 14 2022 at 09:37):

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 (Jan 14 2022 at 09:39):

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 (Jan 14 2022 at 09:56):

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 (Jan 14 2022 at 09:58):

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 (Jan 14 2022 at 09:59):

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

Yaël Dillies (Jan 14 2022 at 10:00):

I think I indeed am

Johan Commelin (Jan 14 2022 at 15:18):

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

Johan Commelin (Jan 14 2022 at 15:19):

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

Eric Wieser (Jan 14 2022 at 20:10):

Is docs#non_unital_non_assoc_ring to blame?

Riccardo Brasca (Jan 15 2022 at 10:43):

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

Eric Rodriguez (Jan 15 2022 at 13:18):

yes, sorry, been slow on PRing!

Eric Rodriguez (Apr 27 2022 at 16:19):

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

Eric Rodriguez (Apr 27 2022 at 16:19):

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 (Apr 27 2022 at 16:33):

Ouf this is annoying

Riccardo Brasca (Apr 27 2022 at 16:37):

Thanks for the bump

Anne Baanen (Apr 28 2022 at 09:58):

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 (Apr 28 2022 at 10:05):

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 (Apr 28 2022 at 10:55):

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

Eric Wieser (Apr 29 2022 at 20:36):

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

Eric Wieser (Apr 29 2022 at 20:37):

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 (Apr 29 2022 at 20:38):

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 (May 02 2022 at 10:50):

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

Riccardo Brasca (Oct 28 2021 at 08:30):

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 (Oct 28 2021 at 08:39):

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 (Oct 28 2021 at 08:40):

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

Riccardo Brasca (Oct 28 2021 at 08:41):

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

Johan Commelin (Oct 28 2021 at 08:58):

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

Riccardo Brasca (Oct 28 2021 at 08:58):

Wow, very nice!!

Johan Commelin (Oct 28 2021 at 08:58):

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

Riccardo Brasca (Oct 28 2021 at 09:11):

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

Alex J. Best (Oct 28 2021 at 09:12):

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

Patrick Massot (Oct 28 2021 at 11:31):

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 (Oct 28 2021 at 13:47):

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 (Oct 28 2021 at 13:51):

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

Chris Birkbeck (Oct 28 2021 at 19:54):

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 (Oct 28 2021 at 20:01):

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

Chris Birkbeck (Oct 28 2021 at 20:05):

Yeah sorry I didn't read it carefully enough!

Eric Wieser (Oct 28 2021 at 22:04):

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

Riccardo Brasca (Oct 29 2021 at 11:22):

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

Eric Wieser (Nov 08 2021 at 14:12):

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 (Nov 08 2021 at 14:19):

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

Eric Wieser (Nov 08 2021 at 14:49):

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

Riccardo Brasca (Nov 08 2021 at 15:06):

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 (Nov 08 2021 at 15:28):

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

Eric Rodriguez (Nov 08 2021 at 15:28):

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

Kevin Buzzard (Nov 10 2021 at 15:24):

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 (Nov 10 2021 at 19:00):

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 (Nov 10 2021 at 20:12):

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

Johan Commelin (Nov 10 2021 at 20:12):

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 (Nov 10 2021 at 20:20):

docs#algebraic_closure for reference

Eric Wieser (Nov 10 2021 at 20:26):

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 (Nov 10 2021 at 20:27):

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

Johan Commelin (Nov 10 2021 at 20:29):

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

Kevin Buzzard (Nov 11 2021 at 10:22):

Splitting fields are also noncanonical

Kevin Buzzard (Nov 11 2021 at 10:23):

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 (Nov 13 2021 at 17:40):

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 (Nov 14 2021 at 12:12):

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 (Nov 14 2021 at 12:14):

What doesn't work specifically?

Alex J. Best (Nov 14 2021 at 12:14):

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

Eric Rodriguez (Nov 14 2021 at 12:16):

exactly that

Alex J. Best (Nov 14 2021 at 12:19):

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

Alex J. Best (Nov 14 2021 at 12:19):

Or do you use leanproject pull

Eric Rodriguez (Nov 14 2021 at 12:25):

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

Alex J. Best (Nov 14 2021 at 13:00):

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 (Nov 14 2021 at 13:04):

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

Kevin Buzzard (Nov 14 2021 at 13:58):

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 (Nov 14 2021 at 14:18):

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

Eric Wieser (Nov 14 2021 at 14:43):

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

Alex J. Best (Nov 20 2021 at 12:59):

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 (Nov 29 2021 at 11:11):

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 (Jan 12 2022 at 10:29):

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 (Jan 12 2022 at 10:44):

Good diff! You got rid of about 90 lines!

Riccardo Brasca (Jan 14 2022 at 09:37):

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 (Jan 14 2022 at 09:39):

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 (Jan 14 2022 at 09:56):

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 (Jan 14 2022 at 09:58):

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 (Jan 14 2022 at 09:59):

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

Yaël Dillies (Jan 14 2022 at 10:00):

I think I indeed am

Johan Commelin (Jan 14 2022 at 15:18):

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

Johan Commelin (Jan 14 2022 at 15:19):

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

Eric Wieser (Jan 14 2022 at 20:10):

Is docs#non_unital_non_assoc_ring to blame?

Riccardo Brasca (Jan 15 2022 at 10:43):

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

Eric Rodriguez (Jan 15 2022 at 13:18):

yes, sorry, been slow on PRing!

Eric Rodriguez (Apr 27 2022 at 16:19):

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

Eric Rodriguez (Apr 27 2022 at 16:19):

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 (Apr 27 2022 at 16:33):

Ouf this is annoying

Riccardo Brasca (Apr 27 2022 at 16:37):

Thanks for the bump

Anne Baanen (Apr 28 2022 at 09:58):

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 (Apr 28 2022 at 10:05):

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 (Apr 28 2022 at 10:55):

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

Eric Wieser (Apr 29 2022 at 20:36):

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

Eric Wieser (Apr 29 2022 at 20:37):

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 (Apr 29 2022 at 20:38):

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 (May 02 2022 at 10:50):

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

Ruben Van de Velde (Dec 18 2023 at 10:43):

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 (Dec 18 2023 at 10:45):

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 (Dec 18 2023 at 11:18):

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 (Dec 18 2023 at 11:44):

I'm having a look.


Last updated: Dec 20 2023 at 11:08 UTC