New variable inclusion mechanism

Stream: mathlib4

[Kim Morrison]

lean#4814 will introduce a new variable inclusion mechanism, resolving lean#2452.

It's going to require a big effort to adapt Mathlib to it. I'm not ready to ask for help getting this done, because we've encountered a few problems with lean#4814 that should be fixed first. When I'm ready, I'll definitely be asking here!

In the meantime, however, there are several Mathlib PRs backporting changes to master, that I prepared while identifying these problems.

If someone could take a look and :peace_sign: or , that would be great. There will be many more of these to come.

[Kim Morrison]

#15245

[Kim Morrison]

#15246

[Kim Morrison]

#15249

[Kim Morrison]

#15255

[Sébastien Gouëzel]

I love how it forces you to fix lines like

variable (α) [Group α] [AddGroup α]

(yes, we have that in mathlib :-)

[Kim Morrison]

Just bringing across a discussion with @Floris van Doorn that I think it is easier to have here, as it is to do with how we adapt Mathlib, rather than the implementation of #4814.

I propose that during the adaptation work we:

• allow using include, but only as include ... in, or immediately after the variable statement.

I think the consensus is that in the long run we would like only have include ... in, and no section wide include.

However it is going to be less work for me (and whoever is helping do this adapation) if at first we allow the variable + include. These can then be cleaned up in parallel afterwards, rather than getting in the way of reaching a full build of Mathlib under #4814.

[Jireh Loreaux]

I think that makes sense. Hopefully we can write some automation to do that clean-up of variable + include after the fact.

[Damiano Testa]

I also agree.

[Damiano Testa]

As for the automation, it looks like the kind of adaptations would be reasonably easy to achieve. They also look similar to the adaptations that I was playing around with when removing implications between typeclass assumptions.

[Kim Morrison]

#15310

[Kim Morrison]

#15313

[Kim Morrison]

Okay, things are looking pretty good here! If anyone would like to jump in and work on fixing problems on branch#lean-pr-testing-4814, I think we can do so.

[Kim Morrison]

There's only room for one person at a time, so please do claim and unclaim here!

[Kim Morrison]

Quoting from the PR comments:

Re: looking at Mathlib on this PR. So far there are two classes of problems: typeclasses hypothesis being included which should not be (for which the new linter is really helpful), and variables which need an include.

Fixing the first class of problems requires either adding sections to bound variable [...] scopes, using variable ... in, or reordering results.

I propose that for anyone working on the Mathlib branch for this PR, we try to backport all the changes of the first form.

A reasonable workflow seems to be:

• As you make changes on lean-pr-testing-4814, any changes that use include (i.e. which will not work on master), you immediately stage.
• But any changes for excluding typeclasses hypotheses you leave unstaged.
• At suitable intervals, make a commit of the staged changes (includes) on lean-pr-testing-4814`
• Then stash the remaining changes, make a new branch off master, make a PR from it, and then merge that branch cherry-pick that commit back to lean-pr-testing-4814. (See first example of such a PR at https://github.com/leanprover-community/mathlib4/pull/15245.)

[Kim Morrison]

While actually working on the branch is only "one person at the coal face", the backporting PRs that are generated are essentially all independent, so can be reviewed in parallel / asychronously. If you make any such PRs please post them here!

[Edward van de Meent]

i noticed that in Algebra.Order.Ring.Unbundled.Basic, some lemmas use a combination of MulPosMono and PosMulMono, despite not needing to... i suppose it'd be ok to fix this by "duplicating" (modulo switching the statement/assumption) to a Right or PosMulMono namespace or something like that?

[Edward van de Meent]

the file is quite the mess when viewed on the branch :melting_face:

[Kim Morrison]

Late here, I only got as far as seeing the file is a real mess. :-) I'd suggest trying to making relatively conservative changes. We can also flag files for a second round of cleanup by a specialist later.

[Edward van de Meent]

in that case i guess i'll leave it be for now...

[Edward van de Meent]

since there really isn't a simple way to fix this

[Matthew Ballard]

Let me take a look at whittling these down on master

[Edward van de Meent]

i seem to have found a (third?) kind of problem which needs some special consideration:

some variable (h:SomeFooOrOther) would be included due to use of induction or subst (or something like that), but gets removed explicitly with clear. This raises an error in the test branch, because h no longer gets included. However, you can't make a pull to mathlib removing the clear because that changes the signature of the lemma.

example:

variable {v : Nat → Type} {P : Nat -> Sort} {a b : Nat} (useless : P b)

theorem foo (h : a = b) : a = b := by
clear useless -- removing this makes `foo`  depend on `useless`
subst h
  rfl

#check foo

I think in this case, it is appropriate to remove the clear line in the test branch but not PR it to mathlib?

[Edward van de Meent]

either that or prepend try and add a TODO

[Edward van de Meent]

or some kind of porting note

[Edward van de Meent]

i guess i'll do the first option i suggested.

[Matthew Ballard]

#15334

[Edward van de Meent]

thanks, that's large mess taken care of for now. however, i fear my point might have been missed slightly: if you add a version of pow_nonneg assuming MulPosMono rather than PosMulMono, some of the following lemmas can be made to assume exactly one of these classes rather than both.

[Matthew Ballard]

Oh, I don't think about any improvements in doing that.

[Matthew Ballard]

If you want to improve what is there, feel free to push there

[Edward van de Meent]

i think that your current branch is probably fine to go on the test-branch, as i'm not sure we want this kind of change to necessarily be merged immediately...

[Edward van de Meent]

btw, i'm done working on branch#lean-pr-testing-4814, so feel free to test your changes on it.

[Edward van de Meent]

btw, #15332 has changes i made

[Kim Morrison]

Edward van de Meent said:

I think in this case, it is appropriate to remove the clear line in the test branch but not PR it to mathlib?

Just confirming this is correct, and it's fine to push such changes (along with adding include) direct to the lean-pr-testing-4814 branch.

Thanks!

[Kim Morrison]

Matthew Ballard said:

#15334

I removed some unused arguments detected by the linter, and 'd. Thanks!

[Kim Morrison]

... and I've cherry-picked the changes over to branch#lean-pr-testing-4814

[Kim Morrison]

Edward van de Meent said:

btw, #15332 has changes i made

I've removed a stray comment, and 'd. (And cherry-pick the comment removal.)

[Kim Morrison]

I'm :working_on_it: it now.

[Kim Morrison]

@Mario Carneiro, it looks like file#Computability/TuringMachine will be a little subtle to fix on branch#lean-pr-testing-4814, because of fine-grained variation in needing [Inhabited] and [DecidableEq] instances.

Would you have a chance to have a look at it?

(We can route around it for now, as there are not a lot of downstream dependencies. I can also do it if you don't have time, but I'm a little worried of making a mess here.)

[Mario Carneiro]

ok, I'll take a look

[Kim Morrison]

(If it's possible to make changes that are backportable to master, that's great. If not, just push includes to the branch.)

[Kim Morrison]

chore: backports for leanprover/lean4#4814 (part 8) #15349

[Kim Morrison]

Still working (away from TuringMachine).

[Mario Carneiro]

I won't be able to get to it right now, maybe tomorrow

[Kim Morrison]

chore: backports for leanprover/lean4#4814 (part 9) #15352

[Kim Morrison]

This one has not been cherry-picked to lean-pr-testing-4814, because there are some incoming changes on master that will cause conflicts. I'm going to try to merge nightly-testing into lean-pr-testing-4814 first.

[Kim Morrison]

There was a bit of an outage due to branch conflicts (long story, unavoidable, we're working on it), but branch#lean-pr-testing-4814 is open for business again!

[Kim Morrison]

(Leave the file EditDistance/Defs, I know a good fix and will can do it next time I'm on this branch.)

[Kim Morrison]

Currently awaiting review is #15349

[Kim Morrison]

Okay, claiming the branch for now.

[Kim Morrison]

Now also awaiting review is #15389.

[Kim Morrison]

And a short one: #15390

[Kim Morrison]

I'm now stopping on this branch if anyone would like to push it a bit further!

[Kim Morrison]

The current "frontier", i.e. the build failures reported by lake --wfail build, is:

- Mathlib.Algebra.Order.Ring.Unbundled.Basic
- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
- Mathlib.Algebra.Ring.Subsemiring.Basic
- Mathlib.Order.CompactlyGenerated.Basic
- Mathlib.Order.Filter.Interval
- Mathlib.Topology.NhdsSet
- Mathlib.Topology.Order.Bornology
- Mathlib.Order.BooleanGenerators
- Mathlib.RingTheory.HahnSeries.Basic
- Mathlib.Data.Sym.Card
- Mathlib.Combinatorics.Colex
- Mathlib.Data.Finset.Sups
- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
- Mathlib.Combinatorics.SetFamily.FourFunctions
- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
- Mathlib.Data.List.EditDistance.Defs
- Mathlib.RingTheory.Nilpotent.Defs
- Mathlib.CategoryTheory.Sites.CoversTop
- Mathlib.Order.Interval.Finset.Fin
- Mathlib.CategoryTheory.Sites.IsSheafOneHypercover
- Mathlib.Data.Fintype.BigOperators
- Mathlib.Data.Setoid.Partition
- Mathlib.Combinatorics.SimpleGraph.Turan
- Mathlib.Topology.Maps.Basic
- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
- Mathlib.CategoryTheory.Sites.PreservesSheafification
- Mathlib.Combinatorics.SimpleGraph.Density
- Mathlib.Algebra.Module.Submodule.Map
- Mathlib.Computability.TuringMachine
- Mathlib.CategoryTheory.Limits.Final

[Kim Morrison]

Another one at #15394

[Edward van de Meent]

@Nicolas Rolland i think Kim Morrison still has the branch claimed?

[Edward van de Meent]

as indicated by the emote reaction?

[Edward van de Meent]

so please only react with that emote if you claim the branch (and no-one else is claming it)

[Kim Morrison]

Sorry, I left it claimed accidentally, but I'm back on it now.

[Kim Morrison]

I'll try to be better an unclaiming, sorry. :-(

[Edward van de Meent]

btw, i'm not sure why, but Batteries.Data.List.Pairwise locally (on the current version of the branch) fails to build for me? it throws

error: .\.\.lake/packages\batteries\.\.\Batteries\Data\List\Pairwise.lean:46:6: unknown identifier 'pairwise_iff_getElem'
error: .\.\.lake/packages\batteries\.\.\Batteries\Data\List\Pairwise.lean:46:6: tactic 'rewrite' failed, equality or iff proof expected

[Kim Morrison]

What commit appears for Batteries in your lake-manifest.json?

[Edward van de Meent]

34ce6c38752e8671d7556a30120ec6008a9a177a

[Edward van de Meent]

which does seem to be current...

[Kim Morrison]

Looks good to me

[Edward van de Meent]

yea, which is why i'm confused...

[Kim Morrison]

Try deleting .lake, then lake exe cache get again...

[Edward van de Meent]

there appears to be zero cache to download?

$ lake exe cache get
info: batteries: cloning https://github.com/leanprover-community/batteries to '.\.\.lake/packages\batteries'
info: Qq: cloning https://github.com/leanprover-community/quote4 to '.\.\.lake/packages\Qq'
info: aesop: cloning https://github.com/leanprover-community/aesop to '.\.\.lake/packages\aesop'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4 to '.\.\.lake/packages\proofwidgets'
info: importGraph: cloning https://github.com/leanprover-community/import-graph to '.\.\.lake/packages\importGraph'
info: Cli: cloning https://github.com/leanprover/lean4-cli to '.\.\.lake/packages\Cli'
Attempting to download 4874 file(s)
Downloaded: 0 file(s) [attempted 4874/4874 = 100%] (0% success)
Warning: some files were not found in the cache.
This usually means that your local checkout of mathlib4 has diverged from upstream.
If you push your commits to a branch of the mathlib4 repository, CI will build the oleans and they will be available later.
No cache files to decompress

[Kim Morrison]

That's strange. You haven't used elan override have you?

[Kim Morrison]

What commit are you at?

[Edward van de Meent]

not sure, but git status says i'm current:

$ git status
On branch lean-pr-testing-4814
Your branch is up to date with 'origin/lean-pr-testing-4814'.

nothing to commit, working tree clean

[Kim Morrison]

Oh!!

[Edward van de Meent]

98c9ccc6ca31e085e357e9cb9b6c78ea25b834db

[Kim Morrison]

elan toolchain uninstall $(<lean-toolchain)

[Edward van de Meent]

should that fix it?

[Kim Morrison]

I should have announced that: we had to update #4814 itself for compatibility with the latest nightly-testing, and I completely forgot to announce here that anyone with the old toolchain needed to run that command.

[Edward van de Meent]

ahhh

[Kim Morrison]

Then just lake exe cache get again. It will download the updated toolchain automatically.

[Kim Morrison]

Sorry about that.

[Edward van de Meent]

thanks :+1:

[Kim Morrison]

Okay, I am relinquishing the branch again!

[Edward van de Meent]

in that case i'll continue from there

[Edward van de Meent]

is it maybe useful to make variable binder updates to terms automatically include those variables? i.e. make variable (M) in ... automatically do include M in ... as well?

[Edward van de Meent]

this seems sensible to me, could someone tell me if it's feasible?

[Edward van de Meent]

or really any variable ... in ....?

[Edward van de Meent]

not just binder updates

[Kim Morrison]

Interesting, yes! @Sebastian Ullrich, do you see a problem?

[Kim Morrison]

If Mathlib could really pull off never using include, but only using include ... in (we are not attempting this for now), then we'd actually be able to drop the include command entirely in favour of variable ... in.

[Damiano Testa]

This would be very cool!

Would this create some awkwardness if you wanted to preserve a specific ordering of the hypotheses, though?

[Sebastian Ullrich]

That's a bit of a break with the usual in semantics (and because of that would require a custom implementation). I think I would prefer Floris' include (M) in, and mostly just not use variable binder updates.

[Edward van de Meent]

Sebastian Ullrich said:

That's a bit of a break with the usual in semantics

in the sense that you usually can replace it with wrapping it in a section?

[Edward van de Meent]

in that case, maybe it makes sense to make a variation on the variable command which does both?

[Edward van de Meent]

also, what are you referring to with "Floris' include (M) in"?

[Kim Morrison]

Just a reminder @Edward van de Meent to say here if/when you're done on the branch. I think in any case it's time for me to sleep here, but I will try to work on this a bunch tomorrow!

[Edward van de Meent]

Yup, i'm still working on it

[Edward van de Meent]

do we have an opinion on section variable .... as a single line? i looked through the code style doc but i couldn't find any express opinion...

[Ruben Van de Velde]

I don't think we should do it (personal opinion)

[Edward van de Meent]

that does make sense though... i imagine that forcing the newline makes some smart linting/searching possible, and there isn't a lot to be gained by making it a single line...

[Edward van de Meent]

i asked because i was surprised it was accepted at all by lean, and there are some style rules suggesting we care about line count...

[Ruben Van de Velde]

No, we care about the amount of code that goes into a single file - it's just that line count is an easy but imperfect proxy for that

[Edward van de Meent]

ok, i'm done for today! please have a look at #15406

[Mario Carneiro]

@Kim Morrison said:

Mario Carneiro, it looks like file#Computability/TuringMachine will be a little subtle to fix on branch#lean-pr-testing-4814, because of fine-grained variation in needing [Inhabited] and [DecidableEq] instances.

Would you have a chance to have a look at it?

(We can route around it for now, as there are not a lot of downstream dependencies. I can also do it if you don't have time, but I'm a little worried of making a mess here.)

Pushed a fix to the branch

[Kim Morrison]

Thanks!

[Kim Morrison]

@Mario Carneiro, I've backported that commit to master as #15422.

[Mario Carneiro]

I should mention that while making the modifications I didn't get the sense that it was making the code better/clearer. The combination of the unused variable linter and the unused variable linter means that it is not very easy to use typeclass hypotheses in variables at all anymore (more precisely, you only ever seem be able to use variable in cases where it would already be included, and unused variables lying around are problematic). I can't imagine what the algebraic hierarchy heavy files are dealing with...

[Kim Morrison]

It's mostly been better than this file. If you don't need to turn on and off particular typeclasses repeatedly it goes more smoothly.

[Kim Morrison]

The PRs (both open and closed) of backports are listed at https://github.com/leanprover-community/mathlib4/pulls?q=sort%3Aupdated-desc+is%3Apr+lean4%234814+

[Mario Carneiro]

I don't need to turn on and off hypotheses in this file

[Kim Morrison]

We're mostly past the algebraic hierarchy files, although the PRs are a complete jumble (whatever is at the frontier of lake build) rather than organised by topic/directory.

[Mario Carneiro]

the other linter made me do that

[Mario Carneiro]

it's perfectly fine to assume all of those hypotheses for the whole file, but it causes some theorems to take unused arguments

[Mario Carneiro]

the only way I seem to be able to satisfy both linters simultaneously is through this pedantic sectioning

[Kim Morrison]

Obviously there's some tradeoff here. Have a look at some of the other PRs. Frequently I've been pretty happy with the changes, especially when it forces us to avoid crazy non-localities in the variables. It's identified at least one bug with a missing Decidable instance.

[Kim Morrison]

I'm starting again on this branch.

[Kim Morrison]

@Edward van de Meent, the include hadd you added in Mathlib/Algebra/MonoidAlgebra/Degree.lean causes problems: supDegree_prod_le immediately below still has its own copy of hadd, and this cause all sorts of duplication of the arguments.

[Kim Morrison]

I'm fixing this now.

[Robert Maxton]

In Mathlib we are striving towards using variable {v} and include v only using in (i.e. variable {v} or include v is banned, you should solely use variable {v} in and include v in).

Wait, does this mean you would have to specify all your variables for every theorem in a section again? Because yes, having to do that in the bits of Mathlib where every theorem requires layers upon layers of typeclasses just to state seems ... extremely unfortunate, at least.

[Robert Maxton]

Or is the idea that you would include something in explicit or implicit binders, and all necessary instance-implicits would get pulled in?

[Kim Morrison]

@Robert Maxton, take a look at some of the PRs above. Typeclasses get pulled in automatically (indeed, even more eagerly than currently.)

[Kim Morrison]

or the desciption at lean#4814 is pretty helpful explaining the new algorithm.

[Robert Maxton]

Ahh, okay. That makes more sense. I've been going mostly off the documentation rather than the code itself

[Robert Maxton]

Kim Morrison said:

or the desciption at lean#4814 is pretty helpful explaining the new algorithm.

that also helps, thanks

[Yaël Dillies]

Sorry, I'm not sure I understand why variable {v} without the in is even problematic

[Kim Morrison]

I think that's a topic for another thread, in any case. (And I mostly agree.)

[Kim Morrison]

Another one, fairly large this time: #15427

[Kim Morrison]

As we get closer to the end of some corners of Mathlib, I may ask some specific file authors if they are able to help out on files, as Mario did for TuringMachine (thanks!). These will be files that are particularly awkward to adapt, so if you do look at this, please remember mostly it goes more smoothly. :-)

[Kim Morrison]

Summary of where we're at (absolutely no compulsion if I ping you, just I'll leave these parts til later!):

[Kim Morrison]

• variables in TuringMachine.lean #15422 has a CI failure (Perhaps @Mario Carneiro could take a look, and move the fix to lean-pr-testing-4814 if needed?)

[Kim Morrison]

• Waiting for review:

[Kim Morrison]

• #15396

[Kim Morrison]

• #15397

[Kim Morrison]

• #15406

[Kim Morrison]

• #15427

[Kim Morrison]

• #15246 is failing CI; I can get to it but if someone wants to jump in, great!

[Kim Morrison]

• @Joël Riou, perhaps you might be interested in:
  • Mathlib.CategoryTheory.Abelian.ProjectiveResolution
  • Mathlib.CategoryTheory.Triangulated.Subcategory
  • Mathlib.Algebra.Homology.HomologySequenceLemmas
  • Mathlib.Algebra.Homology.HomotopyCofiber

[Kim Morrison]

• @Jireh Loreaux perhaps you could look at
  • Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  • Mathlib.Algebra.Star.NonUnitalSubalgebra

[Kim Morrison]

• Algebraic geometers (@Dagur Asgeirsson, @Andrew Yang, @Joël Riou?) could look at
  • Mathlib.CategoryTheory.Sites.Coherent.ReflectsPrecoherent
  • Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular
  • Mathlib.CategoryTheory.Sites.DenseSubsite
  • Mathlib.CategoryTheory.Sites.LocallyInjective

[Kim Morrison]

• Otherwise, most of the "frontier" of broken stuff is in Algebra/RingTheory/Topology, and I'll continue working here.

[Joël Riou]

Kim Morrison said:

• Mathlib.CategoryTheory.Abelian.ProjectiveResolution
• Mathlib.CategoryTheory.Homology.HomotopyCofiber
• Mathlib.CategoryTheory.Triangulated.Subcategory

In principle, these 3 files are fixed.

[Kim Morrison]

Another backporting PR: #15429

[Jireh Loreaux]

I will try to look early tomorrow morning, but no promises. We're about to go out of town.

[Ruben Van de Velde]

Kim Morrison said:

Another backporting PR: #15429

Failing CI

[Kim Morrison]

Thanks, sorry, a few are. I'm still going on the main branch, and will circle back to fix the PRs. If you want to push fixes, please feel free. :-)

[Kim Morrison]

@Joël Riou, something is still wrong with:

- Mathlib.Algebra.Homology.Embedding.IsSupported
- Mathlib.Algebra.Homology.HomotopyCofiber

would you be able to take a look at these?

[Kim Morrison]

I've finished on the main branch for now if anyone would like to take over. I'll fix up all my broken backport PRs in an hour or two.

[Ruben Van de Velde]

I pushed some fixes to the backport PRs

[Kim Morrison]

Thanks!

[Joël Riou]

Kim Morrison said:

Joël Riou, something is still wrong with:

- Mathlib.Algebra.Homology.Embedding.IsSupported
- Mathlib.Algebra.Homology.HomotopyCofiber

would you be able to take a look at these?

These are fixed now.

[Andrew Yang]

Kim Morrison said:

• Mathlib.CategoryTheory.Sites.Coherent.ReflectsPrecoherent
• Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular
• Mathlib.CategoryTheory.Sites.DenseSubsite
• Mathlib.CategoryTheory.Sites.LocallyInjective

I think I've fixed them. What's the proccess then? Should I push to the branch directly?

[Kim Morrison]

Yes, you can push to the branch directly.

[Kim Morrison]

If you didn't need to also use include, then we can backport to master as well.

[Kim Morrison]

(And if you did need to use include, then I'll backport after Mathlib moves to v4.11 in the next few days: it will contain a temporary noop include.)

[Andrew Yang]

No I had to use include here and there.

[Kim Morrison]

We have a number of open PRs backporting changes. It would be great to get some eyes on these and have them in, as there are going to be many more!

[Kim Morrison]

#15429

[Kim Morrison]

#15434

[Kim Morrison]

#15431

[Kim Morrison]

#15429

[Kim Morrison]

#15422

[Kim Morrison]

#15246

[Kim Morrison]

I'm resuming work on branch#lean-pr-testing-4814

[Kim Morrison]

#15510

[Kim Morrison]

@Sébastien Gouëzel or @Floris van Doorn could I get your opinion about what to do with the nicely commented variable block at the top of file#Geometry/Manifold/ContMDiff/Defs?

[Kim Morrison]

It begins

/-! ### Definition of smooth functions between manifolds -/


variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
  -- declare a smooth manifold `M` over the pair `(E, H)`.
  {E : Type*}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) {M : Type*} [TopologicalSpace M] [ChartedSpace H M]
  [SmoothManifoldWithCorners I M]
  -- declare a smooth manifold `M'` over the pair `(E', H')`.
  {E' : Type*}
  [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type*} [TopologicalSpace H']
  (I' : ModelWithCorners 𝕜 E' H') {M' : Type*} [TopologicalSpace M'] [ChartedSpace H' M']
  [SmoothManifoldWithCorners I' M']

However I need to remove [SmoothManifoldWithCorners I M] and [SmoothManifoldWithCorners I' M'] for an initial segment of the file.

[Kim Morrison]

Anywhere else I would just remove them, and add them again when needed later, but since you've gone to the effort to document that variables command, I'm hoping you'll be able to take a look and find a way to do it and preserve the nice documentation!

[Kim Morrison]

(This is on branch#lean-pr-testing-4814)

[Kim Morrison]

I'm done for a while if anyone would like to have a go on this branch. :-) We're getting there, about 80% of the way through mathlib now.

[Kim Morrison]

Resuming...

[Kim Morrison]

Stopping for a while:

Success ✔: 4481
Warning ⚠: 18
Error   ✖: 12

[Jeremy Tan]

where do you get those numbers from?

[Edward van de Meent]

i'll have a go at it

[Edward van de Meent]

ah, i imagine it'll be useful if #where also shows which variables are include-ed...

[Edward van de Meent]

also, today i learnt that instances use def regardless of if the class is a Prop or not, resulting in include not mattering for those

[Jeremy Tan]

I'm working on Geometry.Manifold.ContMDiff.Defs and others

[Edward van de Meent]

????

[Edward van de Meent]

i have the branch claimed though?

[Jeremy Tan]

I'm still waiting for Floris

[Kevin Buzzard]

@Jeremy Tan Edward has the branch claimed. Please wait your turn.

[Kim Morrison]

Jeremy Tan said:

where do you get those numbers from?

The numbers come from my count-errors script and

lake --verbose build | count-errors

[Kim Morrison]

Another useful script I have is open-errors, which you then use as open-errors lake build, to get all files with errors or warnings opened in VSCode.

[Kim Morrison]

Oh, oops @Edward van de Meent, I have local fixes to LinearAlgebra/Matrix/PosDef.lean and AlgebraGeometry/Morphisms/Basic.lean that I forgot to commit. I just pushed PosDef after merging, and will make a backport for Morphisms/Basic

[Kim Morrison]

#15543 (and pushed to the branch)

[Edward van de Meent]

i think it'd be good for an expert to look at Mathlib/Analysis/CstarAlgebra/ContinuousFunctionalCalculus/Unital.lean... i can fix it on the branch, but it is hard to backport because the cfc_tac and cfc_cont_tac seem prone to breaking by rearranging variables and theorems...

[Edward van de Meent]

i suppose for now it might be sufficient to just push to the branch and be done with it...

[Edward van de Meent]

there seems to be a problem with importing a file using the suppress_compilation tactic? the error says failed to read file '.\.\.lake\build\lib\Mathlib\CategoryTheory\Abelian\ProjectiveResolution.olean', invalid header

[Edward van de Meent]

commenting out suppress_compilation in the file fixes it...

[Edward van de Meent]

still maybe someone should look into why this happens.

[Sebastian Ullrich]

This may mean that you have an older version of the PR toolchain than the cache, try deleting it

[Sebastian Ullrich]

By changing the file, you made sure it's not using the cached version anymore

[Edward van de Meent]

curious

[Sebastian Ullrich]

It only happens on PR branches as otherwise Lean releases are immutable

[Edward van de Meent]

let's see if that fixes it...

[Jireh Loreaux]

I can take a look at the cfc stuff now, if the branch is available. Please @ me as soon as it is and I will deal with all cfc-related stuff. I imagine it may be hard for others to deal with because of all the autoparams and some still broken things with fun_prop.

[Jireh Loreaux]

It's branch#lean-pr-testing-4814 , correct?

[Jireh Loreaux]

@Edward van de Meent do you still have this branch claimed? I wasn't quite sure from the last few messages from you.

[Edward van de Meent]

yes, i'm still working on it.

[Edward van de Meent]

ok i'm done, #15549 is a small backport. @Jireh Loreaux the branch is free

[Jireh Loreaux]

Okay, I will start here in a minute.

[Jireh Loreaux]

so under what circumstances do we backport changes exactly?

[Edward van de Meent]

i think the general idea is when the changes also work with the current version of lean...
i.e. when you have to add include, you don't backport, but changes adding sections or moving around theorems can be backported....

[Jireh Loreaux]

Probably other people can work on this branch too right now if they are not working in the CstarAlgebra folder.

[Jireh Loreaux]

I guess I'll update here as I work on new files, and I'm okay if people want to work on parallel here, as long as we claim separate files.

[Jireh Loreaux]

currently, I'm moving on to Mathlib.Algebra.Algebra.NonUnitalSubalgebra

[Jeremy Tan]

Pushing commits to the following files:

On branch lean-pr-testing-4814
Your branch is up-to-date with 'origin/lean-pr-testing-4814'.

Changes to be committed:
  (use "git restore --staged <file>..." to unstage)
    modified:   Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
    modified:   Mathlib/Algebra/DirectSum/Module.lean
    modified:   Mathlib/Geometry/Manifold/ContMDiff/Defs.lean
    modified:   Mathlib/MeasureTheory/Measure/Regular.lean

[Jireh Loreaux]

can you indicate which files you plan to pursue now?

[Jireh Loreaux]

@Jeremy Tan

[Jeremy Tan]

Algebra.DirectLimit, for a start

[Jireh Loreaux]

I'm now working on Algebra.Star.NonUnitalSubalgebra

[Floris van Doorn]

Kim Morrison said:

Sébastien Gouëzel or Floris van Doorn could I get your opinion about what to do with the nicely commented variable block at the top of file#Geometry/Manifold/ContMDiff/Defs?

Feel free to just move those variables lower and replace "smooth manifold" by "charted space" in the comments

[Jireh Loreaux]

Jireh Loreaux said:

I'm now working on Algebra.Star.NonUnitalSubalgebra

done and pushed

[Jireh Loreaux]

In case anyone felt I still had claim on the branch, consider it relinquished for now.

[Jireh Loreaux]

I have the changes to Algebra.DirectLimit. @Jeremy Tan if I don't hear from you within 30-60 minutes, i'll just push them.

[Kim Morrison]

Floris van Doorn said:

Kim Morrison said:

Sébastien Gouëzel or Floris van Doorn could I get your opinion about what to do with the nicely commented variable block at the top of file#Geometry/Manifold/ContMDiff/Defs?

Feel free to just move those variables lower and replace "smooth manifold" by "charted space" in the comments

It looks like Jeremy has tackled this file in the meantime. @Jeremy Tan, were your changes compatible with this suggestion from Floris?

[Kim Morrison]

Thanks @Edward van de Meent, @Jeremy Tan, @Jireh Loreaux for your work overnight. We're now at

Success ✔: 4521
Warning ⚠: 19
Error   ✖: 9

(with a target of about 4880).

[Kim Morrison]

I'll claim the branch again, although if anyone would like it I have lots of broken backporting PRs I can switch to!

[Jeremy Tan]

Kim Morrison said:

Jeremy Tan, were your changes compatible with this suggestion from Floris?

Yes (I had to go to bed)

[Jeremy Tan]

Which files are you working on @Kim Morrison?

[Kim Morrison]

Currently I am cleaning up existing open PRs, so if you would like to take the main branch, that would be great!

[Kim Morrison]

Note that I've just merged nightly-testing back into it

[Kim Morrison]

I think the merge went well, but there may be some breakages.

[Jeremy Tan]

In that case I've fixed up Order.Filter.AtTopBot – sure I'll take the main branch ...-testing-4814

[Kim Morrison]

Oh, I just fixed that.

[Kim Morrison]

#15574

[Jeremy Tan]

Resuming on Analysis.BoxIntegral.Partition.Filter

[Kim Morrison]

I have the fix for Mathlib.MeasureTheory.Integral.Marginal (found the problem in a backport PR)

[Jeremy Tan]

huh? is that a prerequisite to the file I just mentioned?

[Jeremy Tan]

(locally building my file while the cache is regenerated)

[Kim Morrison]

I doubt it, as Marginal had errors so you shouldn't have seen anything downstream of it.

[Kim Morrison]

Okay, I've fixed all the outstanding backport PRs, I think, and would like to return to the main branch.

[Kim Morrison]

@Jeremy Tan assuming I avoid Partition.Filter, is that okay?

[Jeremy Tan]

Kim Morrison said:

Jeremy Tan assuming I avoid Partition.Filter, is that okay?

I already fixed it in https://github.com/leanprover-community/mathlib4/commit/6f26b1701dd6f958a850594817a0d8e66ce305a5

[Jeremy Tan]

In fact there probably isn't anything more to fix there

[Jeremy Tan]

two more have been pushed. I'm just waiting for my local build to show problem files for me, fixing the earliest ones one at a time

[Kim Morrison]

Okay, that will definitely result in contention. :-)

[Kim Morrison]

Are you making backports for changes that will work on master?

[Jeremy Tan]

no, not making backports

[Kim Morrison]

Please do!

[Kim Morrison]

All these changes need review.

[Kim Morrison]

Perhaps you could pause on making further progress, and review your recent commits to see what could be made into PRs to master?

[Kim Morrison]

I'm hoping that we can get to the point that the only diff between master and lean-pr-testing-4814 are adding include and removing clear.

[Kim Morrison]

Otherwise it is going to be a nightmare to review.

[Jireh Loreaux]

I'll make backporting PRs for the stuff I changed tomorrow.

[Jeremy Tan]

Will be putting my stuff into #15577

[Jeremy Tan]

All right, all my contributions to the testing branch should now be in #15577

[Jeremy Tan]

As of latest push to the testing branch

Success ✔: 4577
Warning ⚠: 20
Error   ✖: 12

[Edward van de Meent]

@Jeremy Tan are you still working on the branch? i'd like to push some style fixes from one of the backport PRs...

[Jeremy Tan]

no

[Edward van de Meent]

ok, i pushed the fix. the branch should be free now.

[Kim Morrison]

In #15577 @Jeremy Tan has (admirably) given newly introduced sections to control the scope of variables descriptive names.

However I'd like to make sure these names are predictable and uniform to the extent possible.

Examples in #15577 are:

section RAA
variable [IsScalarTower R A A] [SMulCommClass R A A]

for which I'd suggest the best available name is actually IsScalarTower
and in a different file

section DecEqIota
variable [DecidableEq ι]

which I'd suggest is DecidableEq.

Ideally these section names would actually refer the main def enclosed, but when that isn't available or doesn't make sense, I think just the "main" typeclass name that is being turned on and off is the next best thing.

[Kim Morrison]

Opinions on this welcome.

[Edward van de Meent]

we do already have sections Module, Ring, Group, etc... so continuing that naming scheme does seem sensible

[Edward van de Meent]

however, there is a limit to this scheme, in that there may be multiple possible [IsScalarTower _ _ _] to be introduced. In such a case simply using IsScalarTower as a section name is not completely unambiguous... but it's better than nothing.

[Yaël Dillies]

What you're offering as the "next best thing" is my usual section naming practice

[Edward van de Meent]

i think it hardly happens that a section to is dedicated to a single main result, rather than it being dedicated to consequences of the same assumptions/context

[Edward van de Meent]

although that might be my inexperience with mathlib speaking

[Jeremy Tan]

@Kim Morrison done

[Kevin Buzzard]

FWIW I would always shy away from using section names which could be namespaces, because when you see End Module you don't know whether this is the end of a section or a namespace. But now you seem to be able to see which section you're in in VS Code at the top of the pane, so maybe I'll change my habits.

[Kim Morrison]

Oops, forgot to claim the branch, I'm working on it now. It is feeling like the downhill run to the end now!!

[Kim Morrison]

Thanks very much to @Sébastien Gouëzel for reviewing of all the open PRs overnight!

[Kim Morrison]

We are definitely getting closer now:

Some required builds logged failures:
- Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear
- Mathlib.Geometry.Manifold.VectorBundle.Basic
- Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm
- Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
- Mathlib.Geometry.Manifold.ContMDiffMFDeriv
- Mathlib.Geometry.Manifold.LocalDiffeomorph
- Mathlib.Geometry.Manifold.PoincareConjecture
- Mathlib.Geometry.Manifold.VectorBundle.SmoothSection
- Mathlib.MeasureTheory.Integral.IntervalAverage
- Mathlib.Probability.Kernel.CondDistrib
- Mathlib.Probability.Kernel.Condexp
- Mathlib.Analysis.BoundedVariation
- Mathlib.Analysis.BoxIntegral.Basic
- Mathlib.MeasureTheory.Integral.FundThmCalculus
- Mathlib.Algebra.Lie.Weights.RootSystem
- Mathlib.Analysis.Convolution
error: build failed
Success ✔: 4738
Warning ⚠: 9
Error   ✖: 7

[Kim Morrison]

Very close to the end, and I'm stopping for a while.

There are some open PRs that could do with a review.

Currently remaining:

Some required builds logged failures:
- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
- Mathlib.Geometry.Manifold.BumpFunction
- Mathlib.Geometry.Manifold.PartitionOfUnity
- Mathlib.Analysis.FunctionalSpaces.SobolevInequality
- Mathlib.NumberTheory.NumberField.Embeddings
- Mathlib.Analysis.Fourier.FourierTransformDeriv
- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
error: build failed
Success ✔: 4859
Warning ⚠: 5
Error   ✖: 2

and then another ~20 files hiding behind those errors.

[Jeremy Tan]

@Kim Morrison I've got mathlib, Archive and Counterexamples all building without warnings

[Jeremy Tan]

#15612 is the backport PR for my recent slate of changes

[Kim Morrison]

Just pushing some linting changes now!

[Eric Wieser]

Kevin Buzzard said:

FWIW I would always shy away from using section names which could be namespaces, because when you see End Module you don't know whether this is the end of a section or a namespace. But now you seem to be able to see which section you're in in VS Code at the top of the pane, so maybe I'll change my habits.

Is this an argument that section names should be namedLike_theorems not NamedLikeNamespaces?

[Kim Morrison]

Very minor, but: newline between section and variable, or no newline? I think no newline, but there is variation here.

[Kim Morrison]

It looks like we are ready! It is now a pretty gigantic diff on branch#lean-pr-testing-4814. I am considering the possibility that we release lean#4814 as part of a v4.11.0-rc2 (there is independently demand for this), and then move Mathlib up to this promptly.

This would avoid us carrying around this enormous diff on nightly-testing for the rest of the month.

Please voice any objections here!

[Kim Morrison]

(This would also allow proceeding with work on byAsSorry without overlapping diffs...)

[Edward van de Meent]

it could be possible some back-portable changes might have slipped in, maybe it's good to make a last check?

[Kim Morrison]

Yes, if anyone wants to inspect the lean-pr-testing-4814...master diff for more backports that would be great.

[Kim Morrison]

Also important is that we get review of the remaining five open backporting PRs: https://github.com/leanprover-community/mathlib4/pulls?q=sort%3Aupdated-desc+is%3Apr+is%3Aopen+backports+-label%3AWIP

[Jeremy Tan]

What about the mathlib tests, which are still failing?

[Kim Morrison]

I'll take a look.

[Kim Morrison]

I'm running make lint locally, I expect that will have failures too.

[Kim Morrison]

Oh, the test failures are minor, they are just differences in messages...

[Ruben Van de Velde]

It doesn't really feel like a release candidate change, but also in favour of not carrying massive diffs on nightly testing

[Edward van de Meent]

i am seeing some failed to infer instance errors in the (CI) tests though...

[Kim Morrison]

We finally have a new nightly, I'll go get that working and rebase lean#4814

[Kim Morrison]

(Noting that rc2 is going to happen anyway, so it's a question of whether to include this, not whether this warrants it by itself.)

[Kim Morrison]

Does anyone know how to do the following git magic reliably:

Make a PR to master, containing the relative diff of lean-pr-testing-4814 to nightly-testing?

[Edward van de Meent]

not reliably, no... but maybe something like this would work: new branch on nightly-testing, squash merge lean-pr-testing-4814 onto that branch, then cherry pick the merge commit onto a new branch of master, and fix any conflicts

[Edward van de Meent]

alternatively, you could try a rebase -i master on the new branch from nightly-testing (rather than a cherry pick), but there might be too many commits in-between nightly-testing and master to easily isolate the merge-commit

[Kim Morrison]

nightly-testing was just recently reset to master, so that might actually work

[Edward van de Meent]

i'm confused.

the test file dfinsupp_notation is currently failing on the branch, due to an added section in Data.DFinsupp.Basic which results in the order of parameters of DFinsupp.update changing. in principle the fix for this (slightly amending the elaborator for the notation) could be backported.

however the current version of master doesn't seem to include this added section causing it all. Worse, looking at git blame for the line, it was added in the commit "chore: backports for leanprover/lean4#4814 (part 9)" 2dba55c, however when i look at the corresponding PR(s! #15389 and #15352), this change appears to not be included... what's going on? @Kim Morrison

[Edward van de Meent]

looking into it a bit more, it seems that it originally was included in #15389 but the changes were reverted (possibly due to this exact test failing?)

[Edward van de Meent]

for what it's worth, the change in order of parameters of DFinsupp.update makes it line up with Finsupp.update, and the way to fix the test is a one-line change.

[Jireh Loreaux]

I might be able to backport a few changes, as I didn't get around to it yesterday.

[Jireh Loreaux]

What (part #?) are we on now for backports?

[Edward van de Meent]

from a quick search through the PRs, it seems the next one should be # 38?

[Jireh Loreaux]

#15618

[Kim Morrison]

Edward van de Meent said:

for what it's worth, the change in order of parameters of DFinsupp.update makes it line up with Finsupp.update, and the way to fix the test is a one-line change.

Thanks @Edward van de Meent for diagnosing this. I've changed the elaborator on lean-pr-testing-4814.

[Kim Morrison]

and backported as #15636

[Kim Morrison]

@Tomas Skrivan, would you be able to take a look at test/fun_prop_dev.lean on branch#lean-pr-testing-4814? It is (thoroughly) failing, and is currently the last problem on this branch.

(If you wanted to add whatever documentation you think would have resulted in me not bothering you about this file, that would independently be nice too. :-)

[Mario Carneiro]

Eric Wieser said:

Kevin Buzzard said:

FWIW I would always shy away from using section names which could be namespaces, because when you see End Module you don't know whether this is the end of a section or a namespace. But now you seem to be able to see which section you're in in VS Code at the top of the pane, so maybe I'll change my habits.

Is this an argument that section names should be namedLike_theorems not NamedLikeNamespaces?

I actually like to have sections «named like phrases»

[Tomas Skrivan]

Kim Morrison said:

Tomas Skrivan, would you be able to take a look at test/fun_prop_dev.lean on branch#lean-pr-testing-4814? It is (thoroughly) failing, and is currently the last problem on this branch.

(If you wanted to add whatever documentation you think would have resulted in me not bothering you about this file, that would independently be nice too. :-)

#15650 fixed

Not sure what kind of comment would help. On top of the file it says

This file is designed for development of fun_prop and does not depend on most of mathlib. It defines
two function properties Con and Lin which roughly correspond to Continuity and IsLinearMap.

The file is doing exactly that. It postulates Con and Lin and postulates all the basic theorems that continuity and linearity satisfies. After that there is a huge laundry list(in no particular order) of functions that fun_prop should be able to prove continuity or linearity of. I'm happy to improve on the file description if you have an idea what would help you to understand it.

[Edward van de Meent]

i think there might be confusion about it being a file for developement... the tactic is seemingly finished, so why is there a developement file around?

[Tomas Skrivan]

Edward van de Meent said:

i think there might be confusion about it being a file for developement... the tactic is seemingly finished, so why is there a developement file around?

It is absolutely invaluable for testing, bug fixing and adding new features. Waiting for a rebuild of a big portion of mathlib every time I modify the tactic during development is completely unfeasible.

[Edward van de Meent]

but then how is it different from the test/fun_prop.lean?

[Jireh Loreaux]

I think Tomas just explained that.

[Edward van de Meent]

ah, like so

[Jireh Loreaux]

test/fun_prop.lean tests Mathlib usage, but the development file is used for quickly testing the tactic without building Mathlib.

[Edward van de Meent]

i didn't notice that the other test files imported Mathlib stuff

[Kim Morrison]

Thanks @Tomas Skrivan. CI is failing on #15650, could you take a look?

[Tomas Skrivan]

But now it is failing on /test/DeriveToExpr.lean not on fun_prop test file

[Kim Morrison]

Oh! I didn't see that it was a PR to lean-pr-testing-4814, I assumed it was a backport change to master

[Kim Morrison]

Okay, I can take it from there. Since we're moving this stuff to nightly-testing I may just close that PR and merge directly there.

[Matthew Ballard]

Now that this has completely landed there, we should clarify the library standards with regards to use of includes. So I am revivifying this topic.

[Matthew Ballard]

Kim Morrison said:

I think the consensus is that in the long run we would like only have include ... in, and no section wide include.