Mathlib bump

Stream: FLT

[Ruben Van de Velde]

Another one at FLT#131

[Pietro Monticone]

FLT#177

[Ruben Van de Velde]

I'll take a quick look

[Pietro Monticone]

It seems a few lemmas have been ported to mathlib recently.

[Ruben Van de Velde]

@Kevin Buzzard should I delete all the module topology experiments now?

[Kevin Buzzard]

Definitely don't bump them! There's one file which contains the arguments which work and I'm in the process of porting it. I can just delete the old ones now if you like

[Ruben Van de Velde]

That would work too - HIMExperiments/FGModuleTopology.lean is the one that I got to that's failing

[Ruben Van de Velde]

(I'll wait for that)

[Kevin Buzzard]

The file we need to keep is FLT.ForMathlib.ActionTopology . All the other module topologies are now nuked.

[Kevin Buzzard]

BTW the next step in the ongoing port of FLT.ForMathlib.ActionTopology to mathlib is #18077

[Ruben Van de Velde]

FLT#179 is up

[Pietro Monticone]

The update-dependencies workflow raised an issue (FLT#182).

Opened FLT#183 to fix it.

[Pietro Monticone]

The update-dependencies workflow raised an issue (FLT#189).

Opened FLT#190 to fix it.

[Kevin Buzzard]

I want to bump mathlib to fix this problem.

I am on main locally. I fire up VS Code, click the upside-down A -> project actions -> project: update dependency -> mathlib -> proceed, and after everything has downloaded the diff for lake-manifest.json looks like this:

buzzard@buster:~/lean-projects/FLT$ git diff lake-manifest.json | cat
diff --git a/lake-manifest.json b/lake-manifest.json
index 9dbb3ba..22896e0 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "76e9ebe4176d29cb9cc89c669ab9f1ce32b33c3d",
+   "rev": "af731107d531b39cd7278c73f91c573f40340612",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "45d016d59cf45bcf8493a203e9564cfec5203d9b",
+   "rev": "93bcfd774f89d3874903cab06abfbf69f327cbd9",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7bedaed1ef024add1e171cc17706b012a9a37802",
+   "rev": "86d0d0584f5cd165353e2f8a30c455cd0e168ac2",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "0f1430e6f1193929f13905d450b2a44a54f3927e",
+   "rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "079e5ca5a630dabf441b6b74924402b266c3f748",
+   "rev": "3ebc312bace785723ab6bb304c6a102dcc55bdee",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -100,46 +100,6 @@
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
    "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/acmepjz/md4lean",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "5e95f4776be5e048364f325c7e9d619bb56fb005",
-   "name": "MD4Lean",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "b41bc9cec7f433d6e1d74ff3b59edaaf58ad2915",
-   "name": "UnicodeBasic",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/dupuisf/BibtexQuery",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "bdc2fc30b1e834b294759a5d391d83020a90058e",
-   "name": "BibtexQuery",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/doc-gen4",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "b6ae1cf11e83d972ffa363f9cdc8a2f89aaa24dc",
-   "name": "«doc-gen4»",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "FLT",
  "lakeDir": ".lake"}

In particular, this procedure has nuked md4lean, lean4-unicode-basic, BibtexQuery and doc-gen4. I only noticed after I pushed, and now I've had to revert.

Am I doing something wrong? I am desperate to get FLT working again.

[Ruben Van de Velde]

That's because doc-gen is an optional dependency. I never remember how to make lake update remember to add it, though

[Kevin Buzzard]

Does this mean that I can't update with point-and-click? I remember sometimes some kind of -Kenv=dev option but I had understood some recent message somewhere here as implying that this wasn't needed any more. I'll give it another go.

lake update -Kenv=dev mathlib?

[Kevin Buzzard]

Nope, it still nukes them (I have no idea what that option does but apparently it doesn't do this)

[Kevin Buzzard]

Aah, got it. First update lean-toolchain manually, then lake -R -Kenv=dev update.

[Kevin Buzzard]

In a few months I will ask how to do this again and you can all laugh at the old man.

[Pietro Monticone]

@Kevin Buzzard Next time you can just run the executable scripts/update_mathlib.sh.

[Kevin Buzzard]

Thanks, and apologies if you told me this already :-)

[Kim Morrison]

Can projects please please heed our repeated suggestions to stop using -R -Kenv=dev.

[Kevin Buzzard]

Well can someone make it so that I can do the point and click thing which I did above and it updates my project without it also decimating my lake-manifest.json file? I really have no understanding of what's happening or what any of these commands do, I just searched for update and doc-gen and found some mumbo-jumbo on Zulip which worked for me, but this was only because I've not been able to work on FLT for several days for reasons which I don't really understand :-( (and don't particularly want to understand unless they'll actually help me later before I forget them)

[Kim Morrison]

Yes, convince Yael and Pietro and whoever else have been super helpful setting up maths projects for people that we should remove all the reliance of -R -Kenv=dev in the ecosystem, and that if this comes at the cost of requiring a separate repo for doc-generation, then it is still overall an improvement. I've suggested this a number of times. :-)

[Yaël Dillies]

(I have seen it suggested thrice)

[Yaël Dillies]

We can do the change but I am not yet clear about how to update my workflows

[Pietro Monticone]

Ops, I have never seen such a suggestion. Sorry!

Happy to change that, but I need a bit of time to dive a bit deeper and see how to actually do it.

[Ruben Van de Velde]

Is setting up a separate repository really supposed to be the simpler approach?

[Kim Morrison]

1. Things are eventually going to change, e.g. we might have a service that handles doc-gen for all projects.
2. Another option is just making doc-gen a first class dependency.
3. It does appear likely to be simpler than dealing with everyone's confusion with lake -R...

[Rémy Degenne]

There was a suggestion somewhere of having two packages in different folders of the same github repository instead? Or did I misunderstand? That would be more convenient. Is there an example of a repository that implemented one of those changes?

[Rémy Degenne]

Here and a couple of messages below: https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Improving.20the.20Windows.20user.20experience/near/479463868

[Bhavik Mehta]

Kim Morrison said:

Can projects please please heed our repeated suggestions to stop using -R -Kenv=dev.

What is the alternative? I have no objection to switching to something simpler (I've not had confusion with lake -R, but I'll take your word that it's bad), but I have no idea what I'm meant to be using instead.

[Kim Morrison]

Please see batteries#1028 for what looks like a good model.

[Kim Morrison]

Otherwise just a second downstream repository that includes doc-gen as a standard require.

[Kim Morrison]

Obviously neither of these are great, and Mac + David are in different directions working on making this better, but I think with the current version of Lean these are both better than -R -Kenv=dev.

[Michael Rothgang]

I can volunteer to propose the "subdirectory" model, if desired. May take me until November 18/19, though.

[Kevin Buzzard]

Thank you! I'm not in a hurry, I finally understand the situation here. If the only issue with kenvdev is that it's confusing then I'm now unconfused because I've now understood have a script to do this.

[Kim Morrison]

I think the problem here is that it is confusing, people have remained in a state of confusion for a long time, and that this confusion has affected multiple projects. Seems like it might be an indication we should be using a different approach?

[Mario Carneiro]

@Kim Morrison It is all well and good to say "don't use X" but it's not effective advice unless it comes with "use Y instead". What is the proposed alternative here?

[Kim Morrison]

Kim Morrison said:

Please see batteries#1028 for what looks like a good model.

[Mario Carneiro]

can we do something to make that easier? there is a lot of code in that PR

[Mario Carneiro]

at the very least, a how to guide for users to be able to do the copy paste correctly

[Kevin Buzzard]

Mathlib got the adeles of a number field in the last 24 hours or so. I used the script to bump FLT yesterday evening and it worked fine. As far as I'm concerned the script (ie -R -Kdev=env but something is remembering this for me) is a good solution for now. If someone comes up with a PR giving a better solution I'll be happy to merge it but right now I'm happy with the status quo.

[Yaël Dillies]

Mario Carneiro said:

at the very least, a how to guide for users to be able to do the copy paste correctly

I did in fact just try and fail to adapt APAP to use that approach

[Yaël Dillies]

The other thing is that the update_mathlib.sh script automatically updates lean-toolchain, thus avoiding a variety of confusing behavior

[Ruben Van de Velde]

I'm going to look at the elliptic curve changes

[Ruben Van de Velde]

FLT#248

[Pietro Monticone]

Ruben Van de Velde said:

FLT#248

The checkdecls step failed on push to main due to the renaming of EllipticCurve to WeierstrassCurve. Pushed the fix now.

[Pietro Monticone]

A few weeks ago, I added the run_before_push.sh script here to be executed locally before pushing, specifically to help prevent issues like this.

[Pietro Monticone]

A more robust alternative could be to unify push.yml and push_pr.yml into a single blueprint.yml workflow file, where the push and PR events share all steps except for the GitHub Pages deployment. This would be the setup we adopt in the #Equational and #Infinity-Cosmos projects.

Let me know if you want that.

[Ruben Van de Velde]

I mean, if that's not what ci is for, what is?

[Pietro Monticone]

Yes, I don't know why they were not already included. In any case, I will add it later.

[Pietro Monticone]

Done FLT#249

[Kevin Buzzard]

I merged the PR because github seemed happy and then I realised later on that something was broken, but my local copy was even more broken because I had local edits and was in the middle of something, so I ended up spending several hours finishing the something (which is still not quite done). In short, I noticed the problem but wasn't in a position to fix it. So sure, let's get CI to not let these things happen!

[Kevin Buzzard]

Pietro Monticone said:

Done FLT#249

I am not really in any position to review this PR. @Ruben Van de Velde does it look OK to you? I think I'll go back to my infinite places work!

[Kim Morrison]

FLT#262 bumps to the latest Mathlib + v4.15.0-rc1 toolchain.

[Kim Morrison]

(This fails in CI at doc-gen... I'll leave this to someone who enjoys -R more than me. :-)

[Pietro Monticone]

Done.

[Ruben Van de Velde]

Do we not want an intermediate commit that matches the release tag?

[Pietro Monticone]

The release tag will be created automatically, right?

[Ruben Van de Velde]

Pointing at what, if there's no commit that uses mathlib's v4.14.0 tag?

[Pietro Monticone]

Oh, now I see what you mean. You were referring to v4.14.0, sorry.

Then yes, I think it’s better to have an intermediate commit.

[Pietro Monticone]

FLT#335 bumps to the latest Mathlib and v4.17.0-rc1 toolchain.

[Ruben Van de Velde]

Do you not want an intermediate tag for 4.16 stable?

[Pietro Monticone]

Yes, good idea. Thanks.

[Pietro Monticone]

Done FLT#337

[Pietro Monticone]

Merged both of them.

[Kevin Buzzard]

Thanks! Sorry, I'm having a busy week (two talks)

[Pietro Monticone]

FLT#350

[Ruben Van de Velde]

I had a quick look - bumping mathlib is currently broken with an issue related to ModuleCat.ofHom in preweight.fdRep (maybe due to @Anne Baanen's work?) , and an issue with HeightOneSpectrum.adicCompletion in adicCompletionComap_isModuleTopology and following (I'm guessing #22055 from @Salvatore Mercuri)

[Salvatore Mercuri]

BaseChange.lean probably needs to have K and L replaced with WithVal (v.valuation K) and WithVal (w.valuation L) resp. throughout (and maybe remove the letI's) as a result of #22055. Feel free to send any specific errors my way relating to that! Will be away from screen for the rest of today, but I can also take a look at bumping tomorrow

[Ruben Van de Velde]

I'll leave it for you tomorrow :)

[Anne Baanen]

Ruben Van de Velde said:

I had a quick look - bumping mathlib is currently broken with an issue related to ModuleCat.ofHom in preweight.fdRep (maybe due to Anne Baanen's work?)

Does it work if you replace ModuleCat.ofHom with FGModuleCat.ofHom? (What is the error precisely?)

[Ruben Van de Velde]

Apparently not:

GLnDefs.lean:288:21

(deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached
Use `set_option maxHeartbeats <num>` to set the limit.
Additional diagnostic information may be available using the `set_option diagnostics true` command.

GLnDefs.lean:287:20

failed to synthesize
  MulOneClass (FGModuleCat.of ?m.289793 (Fin w.d → ℂ) ⟶ FGModuleCat.of ?m.289793 (Fin w.d → ℂ))
Additional diagnostic information may be available using the `set_option diagnostics true` command.

GLnDefs.lean:287:20

failed to synthesize
  One (FGModuleCat.of ?m.289793 (Fin w.d → ℂ) ⟶ FGModuleCat.of ?m.289793 (Fin w.d → ℂ))
Additional diagnostic information may be available using the `set_option diagnostics true` command.

GLnDefs.lean:287:7

failed to synthesize
  Monoid (FGModuleCat.of ?m.289793 (Fin w.d → ℂ) ⟶ FGModuleCat.of ?m.289793 (Fin w.d → ℂ))
Additional diagnostic information may be available using the `set_option diagnostics true` command.

[Kim Morrison]

@Anne Baanen, just bringing this one to your attention; if it hasn't been sorted out perhaps you can suggest something?

[Anne Baanen]

Ah, I figured it out. The .ofHom is indeed the issue, but it should be removed altogether:

noncomputable def preweight.fdRep (n : ℕ) (w : preweight n) :
    FDRep ℂ (orthogonalGroup (Fin n) ℝ) where
  V := FGModuleCat.of ℂ (Fin w.d → ℂ)
  ρ := {
    toFun := fun A ↦ ModuleCat.ofHom {
      toFun := fun x ↦ (w.rho A).1 *ᵥ x
      map_add' := fun _ _ ↦ Matrix.mulVec_add ..
      map_smul' := fun _ _ ↦ by simpa using Matrix.mulVec_smul .. }
    map_one' := by aesop
    map_mul' := fun _ _ ↦ by
      simp only [obj_carrier, MonCat.mul_of, _root_.map_mul, Units.val_mul, ← Matrix.mulVec_mulVec]
      rfl }

[Salvatore Mercuri]

I've been through and fixed up the adicValuation errors locally. I'm upstreaming some fixes to mathlib in the following two PRs

• https://github.com/leanprover-community/mathlib4/pull/22488
• https://github.com/leanprover-community/mathlib4/pull/22491

[Salvatore Mercuri]

Including Anne's fix above, my repo is now building successfully. But one of the issues is instance search timeout in SMul (v.adicCompletionIntegers K) (v.adicCompletion K), so one of my local fixes is setting heartbeats to the max value (I've tried to lower the instance priority of UniformSpace.Completion.instSMul to fix it in one of the above PRs). For that it might be better to wait until #22488 is merged/resolved.

[Kevin Buzzard]

Salvatore Mercuri said:

Including Anne's fix above, my repo is now building successfully. But one of the issues is instance search timeout in SMul (v.adicCompletionIntegers K) (v.adicCompletion K), so one of my local fixes is setting heartbeats to the max value (I've tried to lower the instance priority of UniformSpace.Completion.instSMul to fix it in one of the above PRs). For that it might be better to wait until #22488 is merged/resolved.

In the old days we had problems with timeouts with things like Algebra (𝓞 K) (𝓞 K) where 𝓞 K was the ring of integers of a number field K, and this was because 𝓞 K was defined to be a Subalgebra (i.e. a term, not a type). Then we changed it to a type and the problems went away. See here for the relevant comment in Mathlib. However I see v.adicCompletionIntegers K is defined as a ValuationSubring (i.e. a subtype), and I suspect that this might be the cause of the problems. I can take a look later but my instinct is that we might want to make v.adicCompletionIntegers K into a type rather than making it as a term and coercing it to a type.

[Salvatore Mercuri]

This did remind me of the RingOfIntegers issue. I guess the issue in this case is twofold: (1) the type synonym is allowing UniformSpace.Completion.instSMul to fire in instance search when previously it did not, and (2) this is taking a long time to fail due to v.adicCompletionIntegers K being a subtype rather than a type. There are a couple of instance search traces in #22488 if that's useful. Redefining it as a type probably makes more sense then rather than lowering the instance priority of UniformSpace.Completion.instSMul (which anyway led to slightly mixed benchmarking results in the linked PR)

[Salvatore Mercuri]

By the way I noticed during the bump PR that this timeout also occurs for SMul (v.adicCompletion K) (Π (w : v.Extension B), w.1.adicCompletion L), so this problem is not restricted to adicCompletionIntegers

[Ruben Van de Velde]

Did another quick bump at FLT#392 to pick up the new lean version

[Kevin Buzzard]

@Yaël Dillies do you know why FLT.Mathlib.GroupTheory.Index is broken when I bump mathlib? The code is

open Function
open scoped Pointwise

namespace AddSubgroup
variable {G A : Type*} [Group G] [AddGroup A] [DistribMulAction G A]
-- TODO: Why does making this lemma simp make `NumberTheory.Padic.PadicIntegers` time out?
lemma index_smul (a : G) (S : AddSubgroup A) : (a • S).index = S.index :=
  index_map_of_bijective _ (MulAction.bijective _)

end AddSubgroup

and the error is

failed to synthesize
  HSMul G (AddSubgroup A) ?m.10818

Is this action no longer a thing?

[Yaël Dillies]

Add import Mathlib.Algebra.GroupWithZero.Subgroup

[Yaël Dillies]

This is fallout from #23832

[Kevin Buzzard]

Thanks!