The elephant in the room

Stream: condensed mathematics

[Adam Topaz]

When (and HOW) should we attempt a mathlib bump?

[Riccardo Brasca]

Is there anything smarter than creating a branch and start working on it?

[Kevin Buzzard]

A related question: let's say someone does actually do this. Then you have the same question next month, the month after, the month after that,... . When I realised we were in the analogous situation with perfectoid I just told Patrick that I was not going to spend the rest of my life bumping because as far as I was concerned we'd done what we'd set out to do. IIRC we were in exactly the same situation with perfectoid -- started on par, got behind, never caught up.

[Adam Topaz]

I think once the project is stable, keeping up with the mathlib bumps would be much easier

[Kevin Buzzard]

We got it working on 3.4.1 and then just left it. However Patrick still managed to port all the stuff he'd written to mathlib

[Adam Topaz]

One option is to do it in stages. I.e. bump to a certain past mathlib commit, and repeat until we reach mathlib master

[Filippo A. E. Nuccio]

But let's be honest: we will not keep LTE updated with mathlib forever, no?

[Kevin Buzzard]

Right that was my position with perfectoid

[Kevin Buzzard]

I didn't want it to become an albatross.

[Filippo A. E. Nuccio]

We should be serious with for_mathlib but a certain point it will stabilise to some mathlib commit and that will be it.

[Adam Topaz]

No of course not, but it might make sense to bump before we seriously start emptying the for_mathlib folder

[Filippo A. E. Nuccio]

Oh, sure, this I certainly agree 100% with.

[Riccardo Brasca]

I was about to suggest to do it in several steps, this is maybe the easiest thing to to.

[Riccardo Brasca]

We are at commit 4977fd9da637b6e0a805c1cf460c3a6b8df3f556, how old is it?

[Adam Topaz]

Pretty old

[Adam Topaz]

In mathlib terms at least

[Filippo A. E. Nuccio]

But what about the big homological algebra issue? That was the reason we stopped bumping, I think.

[Adam Topaz]

There were a few changes in category theory in mathlib that would take a lot of work to integrate in lte. We should probably try to isolate those commits

[Riccardo Brasca]

May 12th, not that old

[Riccardo Brasca]

I am trying to bump to a74298d8e95f8e203ebb906d35f89dd7ce464d74, three days later, to see what happens.

[Adam Topaz]

Here's the diff between those two commits
https://github.com/leanprover-community/mathlib/compare/4977fd9da637b6e0a805c1cf460c3a6b8df3f556...a74298d8e95f8e203ebb906d35f89dd7ce464d74

[Adam Topaz]

in case it helps!

[Riccardo Brasca]

I've created a branch minibump, but I am already stuck with errors related to ordinals in for_mathlib/pid.lean. They are caused by #14074, I will ask for some help to the author of that PR.

[Riccardo Brasca]

Maybe also @Fabian Glöckle can have a look? Everything is caused by the new ordinal.enum_iso, that replaced ordinal.typein_iso: it's in the reverse direction, so adding symm solves certain problems, but not all of them.

[Riccardo Brasca]

The only problems left in the minibump are those related to ordinal.enum_iso. I don't know anything about ordinals in mathlib, so I didn't spend too much time on it, but it shouldn't be very hard.

[Yaël Dillies]

Is that on the branch? I can fix the ordinal stuff.

[Riccardo Brasca]

Yes, in the minibump branch

[Riccardo Brasca]

The file for_mathlib/pid.lean has now three sorry.

[Riccardo Brasca]

Note that I modified line 661 from

let B : basis ords R M := basis.reindex b (ordinal.typein_iso r).to_equiv,

to

let B : basis ords R M := basis.reindex b (ordinal.enum_iso r).symm.to_equiv,

since ordinal.typein_iso was removed in #14074, but maybe there is a better modification. In any case thanks!

[Riccardo Brasca]

@Violeta Hernández I have subscribed you to this stream so you can see if Yael needs help, but feel free to unsubscribe if you want.

[Violeta Hernández]

Alright. I doubt that this change will cause much trouble - flipping equivalences isn't particularly destructive. Do tell me if anything goes awry.

[Robert Brijder]

Filippo A. E. Nuccio said:

But let's be honest: we will not keep LTE updated with mathlib forever, no?

Is there any reason why not the whole of LTE is merged into mathlib, but only the for_mathlib folder? If the whole is merged, then it is forever maintained. I mean, if later someone wants to formalize a result that depends on LTE, then that person is stuck with an old version of lean and mathlib?

[Kenny Lau]

how big is LTE?

[Adam Topaz]

Ben Toner said:

Number of lines: 90967
Number of nonblank lines: 78702
Number of nonblank lines excluding comments and docstrings: 72661

[Kenny Lau]

that is quite a number of lines

[Robert Brijder]

Kenny Lau said:

that is quite a number of lines

So, mathlib is not supposed to grow so much?

[Yaël Dillies]

Robert, I have been working on PRing my last summer internship for the past year. It was 5k lines. Now there are 2k lines left to be PRed.

[Kenny Lau]

my contributions to mathlib are only (+24,882 lines, -7,737 lines) in comparison :sweat_smile:

[Filippo A. E. Nuccio]

Robert Brijder said:

Filippo A. E. Nuccio said:

But let's be honest: we will not keep LTE updated with mathlib forever, no?

Is there any reason why not the whole of LTE is merged into mathlib, but only the for_mathlib folder? If the whole is merged, then it is forever maintained. I mean, if later someone wants to formalize a result that depends on LTE, then that person is stuck with an old version of lean and mathlib?

Well, you raise a good point. I was saying this thinking that LTE was not supposed to land in mathlib, and keeping a separate project alive, hence bumping mathlib twice a week or so, seems unfeasable.

[Adam Topaz]

I think the larger issue is that LTE has some objects that may or may not be interesting for most mathematicians but were needed for the formalization. I'm thinking of things like profinitely-filtered pseudo-normed groups

[Yaël Dillies]

mathlib is highly curated, so the PRing process is excruciatingly slow.

[Damiano Testa]

The review process is very thorough, and justly so. Moreover, very likely the statement of many PRed lemmas would change and it would take effort to make them re-match their corresponding place. It takes time.

[Filippo A. E. Nuccio]

On the other hand, I was discussing today with a colleague who was suggesting that if the whole point of mathlib is to allow to build new math in Lean, then LTE needs to be in mathlib.

[Robert Brijder]

Yaël Dillies said:

mathlib is highly curated, so the PRing process is excruciatingly slow.

I see, now I understand the reason. PRing to mathlib is just too much work. Thanks!

[Filippo A. E. Nuccio]

I think that something like identifying "basic" folders where the review process discussed by @Damiano Testa be very strict; and other folders where we can be more sloppy could give us some flexibility.

[Yaël Dillies]

One point though is that we don't need LTE in mathlib before that happens. And as far as I'm aware nobody, even in maths land, is using Scholze's result yet, right?

[Adam Topaz]

Clausen and Scholze are using it in their new lectures on complex analytic geometry

[Filippo A. E. Nuccio]

@Yaël Dillies Well, nobody is using Scholze's result yet. But I think that a full proof of some form of more general duality will develop out of their theory, and this we do not want to miss.

[Thomas Browning]

Adam Topaz said:

Clausen and Scholze are using it in their new lectures on complex analytic geometry

But they aren't using the liquid stuff, right?

[Filippo A. E. Nuccio]

Yes, to compare algebraic and analytic geometry, I think. That $\mathbb{R}$ is an analytic ring turns out to be crucial.

[Yaël Dillies]

To be clear, I am absolutely for having all projects reaching mathlib eventually! I just want to clear up priorities.

[Adam Topaz]

Right. I think the general framework of analytic rings is certainly something that should be in mathlib at some point (= probably the far future). And having examples is also important ;)

[Filippo A. E. Nuccio]

I confess that after the discussion had this morning with that colleague, I do not have a position any more. On a one side,

• If we want to follow-up with the new results by Clausen and Scholze, we need LTE in mathlib.
  But

• It will make mathlib much longer to compile; and

• We can't ask maintainers to check all the 96k lines (even if we golf them to 50k, say)

[Adam Topaz]

We also need to keep in mind that the transition to lean 4 will take time and effort

[Filippo A. E. Nuccio]

So, I'd rather go sailing on holiday for a while... :sailboat: :lol:

[Yaël Dillies]

My opinion is that we should slowly send bits to mathlib, with the hope that the most reusable ones will get priority. That will slowly erode the LTE mount.

[Kenny Lau]

yeah probably 20 PR's would be good

[Damiano Testa]

There could be periodic mathlib spriltze...

[Filippo A. E. Nuccio]

I would imagine 200, rather...

[Yaël Dillies]

Yeah I already got 4 PRs out of what I did for LTE and I did close to nothing, so...

[Filippo A. E. Nuccio]

If we consider a "normal" mathlib PR to contain an average of 100 lines of code (correct me if I am wrong); and if we consider that LTE will have 50k lines after all the golfing process; well, my math tells me we can expect 500 of them.

[Riccardo Brasca]

Filippo A. E. Nuccio said:

• We can't ask maintainers to check all the 96k lines (even if we golf them to 50k, say)

One of the point of having stuff in mathlib is that it is the person that opens a PR that is supposed to make everything OK. And when you exactly which modifications you did is much easier than doing a bump.

[Riccardo Brasca]

Also, a lot of the material in the LTE is not "mathlib-ready", and my hope is that it will be easier to maintain once it will be in mathlib.

[Riccardo Brasca]

But it is really a lot of work, I agree.

[Adam Topaz]

Again I should stress that I think the most challenging part of porting LTE (even some of the for_mathlib stuff) into mathlib will be finding the right level of generality for the various intermediate constructions and hacks that we have all over the place.

[Filippo A. E. Nuccio]

What I was trying to suggest is that as mathlib grows we might decide that the definition of "mathlib ready" will only apply to a specific part of "foundational" stuff, but that we will be more free-style on other stuff.

[Filippo A. E. Nuccio]

After all, not every math-paper undergoes the same excruciating review process of a Bourbaki volume; and, probably, rightly so.

[Riccardo Brasca]

We can start with something hopefully easy: do we really need all the files? We did something like 3 versions of the snake lemma and long exact sequences. If some of them are not used we can move them somewhere else.

[Riccardo Brasca]

In any case branch minibump is now at cfedf1d5b51096eccff25b7dd9ea8c86f4c402c8 from May 18th (and not May 15th as the commit says). There are three sorry, but we it's 6 days more recent than master.

[Junyan Xu]

What I was trying to suggest is that as mathlib grows we might decide that the definition of "mathlib ready" will only apply to a specific part of "foundational" stuff, but that we will be more free-style on other stuff.

mathlib already has an archive/ directory, and we could also add files to nolint.txt. But I think stuff in archive/ are not supposed to be used, and they also add to CI time. I think we do want things in archive/ to compile with latest mathlib; does LTE really takes much longer time to compile (per line) than mathlib? If we decide to place LTE in archive/, another main concern is whether it will add much maintenance work (to fix breakage from refactoring etc.).

[Peter Scholze]

Thomas Browning said:

Adam Topaz said:

Clausen and Scholze are using it in their new lectures on complex analytic geometry

But they aren't using the liquid stuff, right?

Oh, we absolutely are using the liquid stuff, everywhere! A better title for the course would have been "how to use liquid vector spaces to do complex geometry".

[Riccardo Brasca]

If we want to keep on doing the bump step by step, the next problematic PR is probably #13762, included in commit c9c9fa15fec7ca18e9ec97306fb8764bfe988a7e. I've started in branch bump_may_19 if someone wants to contribute.

[Adam Topaz]

I fixed one file

[Adam Topaz]

Is there a way to make lean build stop when it hits the first error?

[Riccardo Brasca]

I don't know, but it would be nice. My current strategy is quite dumb, I do leanproject build, start doing something else checking every 5 minutes or so, and if I see an error a kill the process and rerun it, to see where the first error is.

[David Michael Roberts]

I'm really curious, @Peter Scholze , why the reals are said to not be an analytic ring in Lecture 1 of Complex.pdf. I thought the point of the LTE was essentially to prove this!

[Adam Topaz]

I think they mean that it's not an analytic ring with respect to the spaces of signed Radon measures (the $\mathcal{M}_{\mathbb{R}}(S)$).

[David Michael Roberts]

Yeah, I know that it's not just the data of the underlying topological ring that is important, but it really surprised me to see such a claim with no foreshadowing that maybe one can choose other structure that does make it work.

[David Michael Roberts]

For instance, a forward pointer to Thm 3.11, where the family of p-liquid structures are given. Far be it for me to criticise, it was just felt odd.

Apologies for the OT noise!

[Riccardo Brasca]

The next file for the bump is src/for_mathlib/triangle_shift.lean. The first missing instances are fixed by

instance : add_group (discrete ℤ) :=
discrete_equiv.add_group

Then there is a bunch of errors, but I am done for today.

[Peter Scholze]

David Michael Roberts said:

I'm really curious, Peter Scholze , why the reals are said to not be an analytic ring in Lecture 1 of Complex.pdf. I thought the point of the LTE was essentially to prove this!

Ah, thanks for pointing out that the presentation is weird here! We certainly did the foreshadowing live, but somehow it got lost when writing the notes. I will add something to the first lecture.

(By the way, that the naive guess for an analytic ring structure didn't work, but only a weird patch, is one reason I was worried about this liquid stuff...)

[David Michael Roberts]

Peter Scholze said:

(By the way, that the naive guess for an analytic ring structure didn't work, but only a weird patch, is one reason I was worried about this liquid stuff...)

Oh, that's a cool bit of insight!

[Yaël Dillies]

Wait, @Riccardo Brasca, do you still need help on minibump?

[Yaël Dillies]

I was having cache troubles yesterday so couldn't actually do anything.

[Riccardo Brasca]

I didn't touch the pid.lean file. You can work on it in bump_may_19, you need mathlib cache of course, but you can ignore the rest of LTE.

[Violeta Hernández]

Is it just the enum_iso thing? If so, I can do the bump

[Riccardo Brasca]

If pid.lean compiles it is enough

[Violeta Hernández]

I think I see an issue

[Violeta Hernández]

image.png The way I wrote to_fun on enum_iso causes def-eq problems

[Violeta Hernández]

Replacing it with the fix on #15454 seems to help unbreak things

[Riccardo Brasca]

A temporary solution, for the LTE, is to redefine the old typein_iso or whatever it was, and use it until we get to current mathlib (not so soon I am afraid)

[Riccardo Brasca]

At least CI will be happy

[Violeta Hernández]

https://github.com/leanprover-community/lean-liquid/pull/89

[Violeta Hernández]

I just added the new enum_iso to the file

[Violeta Hernández]

It's almost identical to the old one except it doesn't use pattern matching

[Violeta Hernández]

I hope my ordinal code doesn't cause further trouble

[Riccardo Brasca]

Oh, I didn't realize you're not allowed to push, I sent you an invitation. Can you push directly to the minibump branch? (not to master). Thanks!

[Johan Commelin]

@Riccardo Brasca @Yaël Dillies @Violeta Hernández Thanks for working on this mathlib bump!

[Riccardo Brasca]

I don't understand why the linter is failing here. The error is just

/home/runner/work/_temp/e3ecbc93-eeba-4fcc-8917-c5dda939d11c.sh: line 2:  1881 Killed                  lean --run scripts/lint_project.lean

[Johan Commelin]

Hmm, no idea either. @Floris van Doorn you are our linter expert. Do you think you could help us?

[Floris van Doorn]

I haven't seen that error before, but googling exit code 137 suggest that it is an out-of-memory issue.

[Eric Wieser]

I think that can sometimes be caused by a simp or instance loop

[Riccardo Brasca]

In any case at least it compiles. Concerning the next bump, in branch bump_may_19, there is src/for_mathlib/triangle_shift.lean that I am not able to fix if someone is interested. All the changes come from #13762

[Johan Commelin]

I think that might be the hardest bump. Once we figure out how we want to fix the shift stuff, the rest is "certainly doable".

[Johan Commelin]

@Riccardo Brasca Is one of the two bump-branches now in a mergeable state?

[Johan Commelin]

I lost track...

[Riccardo Brasca]

minibump compiles. I've opened https://github.com/leanprover-community/lean-liquid/pull/90 to check if CI is working, but there the linter problem we don't understand.

[Johan Commelin]

Aah, gotcha

[Riccardo Brasca]

It also says thm95 is not sorry free, let me check

[Andrew Yang]

I don't think the shift stuff would be that hard to fix; we just need to explicitly write it out when coercing Z to discrete Z?

[Andrew Yang]

I think I can attempt on it if nobody is trying now.

[Riccardo Brasca]

I am not working on it.

[Johan Commelin]

@Andrew Yang If you want to help there, that would be great!

[Ben Toner]

Riccardo Brasca said:

It also says thm95 is not sorry free, let me check

Sorry, that's meant to be liquid_tensor_experiment not thm95 (I missed one substitution; pull request submitted) and in any case it seems to have crashed rather than concluding there are sorries.

[Ben Toner]

Riccardo Brasca said:

minibump compiles. I've opened https://github.com/leanprover-community/lean-liquid/pull/90 to check if CI is working, but there the linter problem we don't understand.

In this run, the linter failed to download the oleans built in the previous step. If the linter and sorry-checker have to do their checking without oleans, they're more likely to run of memory, which looks like what happened.

I'll figure out why it sometimes fails to download the build.

(This comment was wrong.)

[Andrew Yang]

bump_may_19 should now compile.

[Johan Commelin]

Wow! That's really helpful!

[Johan Commelin]

I was really scared of the shift-bump.

[Johan Commelin]

Please make a PR. And let's hope that CI plays along nicely.

[Adam Topaz]

This is great!

[Ben Toner]

I was wrong above about the CI not downloading the oleans. Something else is going wrong in linting and sorry-checking.

[Adam Topaz]

I think the next big hurdle in bumping is the recent changes to universe parameters in finite limits and colimits.

[Riccardo Brasca]

I've created https://github.com/leanprover-community/lean-liquid/pull/94

[Yaël Dillies]

I've cleaned up for_mathlib.pid on my way to bumping it. Where should such a cleanup go? Should I open a PR to master?

[Johan Commelin]

Yes please!

[Riccardo Brasca]

It is already compiling in https://github.com/leanprover-community/lean-liquid/pull/94

[Riccardo Brasca]

You can maybe check to see which modification looks better, but I guess it not so important

[Riccardo Brasca]

I am fixing some other files in that PR, so it will not compile, but hopefully it will soon do

[Yaël Dillies]

I mean that I did stuff for the bump, but it's actually orthogonal to the bump.

[Riccardo Brasca]

Ah sorry, then yes!

[Riccardo Brasca]

I am done for today, but the next error in https://github.com/leanprover-community/lean-liquid/pull/94 is in for_mathlib/derived/ext_coproducts.lean.

[Johan Commelin]

Thanks for all your help

[Ben Toner]

Re. the CI issues, I'm out of lean-time for today but here's what I learnt.

I've been building the minibump branch (commit ba555ce).

On a machine with 32 cores and 64 GB, everything builds fine and then linting works fine too.

We're clearly under memory pressure on CI as some builds crash at random times.

So building on beefier machines would probably fix things.

The confusing thing is that sometimes the build appears to work but the oleans that come out don't match the ones built on the high-memory machine. Some of them match those I get on the machine with 64 GB, some of them are unchanged from the cache we started with (from master) and some are different from both. Maybe we're going out-of-memory half-way through the build (silently; the build appears to be successful) and we're left with oleans from wherever we got up to?? Then the linting starts with the wrong oleans and eventually goes out-of-memory itself.

Anyway, the problem is with the building, not the linting, whatever it looks like in CI.

I didn't investigate what is causing the build to need more memory.

[Eric Wieser]

Note that in mathlib we sometimes have to run lean twice to get accurate oleans

[Ben Toner]

Yeah, the first thing I tried was to run lean three times! Anyway, I checked and the build on the 64 GB machine of ba555ce is stable after running lean once.

[Ben Toner]

More on the CI failure: The project has been getting bigger over the last two months but, because we cache builds, we haven't had to build it from scratch since the time you stopped bumping mathlib.

Usually the cache from a version of the project with an older mathlib is not helpful, so when you did try to bump mathlib, that was the first time in two months that we've built the project without the benefit of a cache.

If I try to build master in CI without the benefit of a cache, the build fails in a similar way to how it fails on the minibump branch. This suggests that it's building from scratch that's the problem, rather than some issue in the newer version of mathlib.

So maybe something specific was added in the last two months that is causing memory problems, but maybe it's just that the project's grown and there's not actually a problem that's easily identifiable. Do the experts have opinions on how much memory the build should be using?

As a temporary fix, I've bumped swap on the build machines from 4 GB to 10 GB (which is about as high as it can reasonably go, since the disk is 14 GB; this commit is currently only on the minibump branch), which might get things going again. It's running now, but I have to go to bed before it'll finish (or time out).

[Kevin Buzzard]

My understanding is that this build has succeeded?

[Johan Commelin]

@Ben Toner Thanks so much for debugging this. Your analysis makes a lot of sense!

[Johan Commelin]

I think we should merge your change into bump_may_19. That's the mathlib bump that has a PR attached to it.

[Johan Commelin]

@Riccardo Brasca did you cherry-pick Ben's commit onto your branch?

[Ben Toner]

I've added my changes to bump_may_19 (cc. @Riccardo Brasca).

[Ben Toner]

I made a separate pull request to get the CI improvements on master. Alternatively you'll get them when you merge bump_may_19.

[Riccardo Brasca]

Thanks! The failure in bump_may_19 is genuine, and I am not sure I understand how to fix it.

[Johan Commelin]

@Riccardo Brasca You are now talking about the error in ext_coproducts? Not some random CI error, right?

[Johan Commelin]

I'm building this branch now

[Riccardo Brasca]

Yep

[Johan Commelin]

Ok, my compile got there. So I'll work on them now.

[Johan Commelin]

ext_coproducts builds again

[Johan Commelin]

single_coproducts done

[Johan Commelin]

Fixed a whole bunch of other files. Still going.

[Johan Commelin]

I pushed wip on QprimeFP. It's almost done.

[Adam Topaz]

Let me know when it builds. I'll merge that PR in a heartbeat

[Johan Commelin]

I have to do something else for ~ 1hr

[Adam Topaz]

What's the next file that needs fixing?

[Riccardo Brasca]

QprimeFP is done

[Riccardo Brasca]

Let me see what happens next

[Johan Commelin]

I'm back

[Johan Commelin]

@Riccardo Brasca How's it looking?

[Riccardo Brasca]

I am waiting, for some reason my computer is very slow

[Johan Commelin]

Heat wave?

[Filippo A. E. Nuccio]

I am also trying to do something but my pc is very slow.

[Filippo A. E. Nuccio]

On which branch are you working, @Riccardo Brasca ?

[Riccardo Brasca]

OK, the next one is src/Lbar/ext_aux4.lean, it should be easy.

[Riccardo Brasca]

The branch is bump_may_19

[Adam Topaz]

Oh boy, we're at the Lbar/ext_foo files! The end is in sight!

[Riccardo Brasca]

Its projective_resolution.lean: is_zero_iff_forall_zero that it is super slow

[Johan Commelin]

That doesn't sound like it ought to be slow.

[Riccardo Brasca]

Ah, maybe it's literally taking forever...

[Johan Commelin]

Are there { tidy } proofs in there?

[Johan Commelin]

I had to replace those in projective_resolution_module.lean

[Riccardo Brasca]

yes, it's their fault

[Johan Commelin]

You can probably copy-pasta what I did in that other file

[Adam Topaz]

If tidy has to try rcases, it usually ends up being too slow. You could use clever rintros, rcases or ext with rcases paterns to help it along.

[Adam Topaz]

And with how discrete was changed, I can imagine that there is some rcases step missing.

[Johan Commelin]

I think we need to teach tidy to do cases on foo : discrete X

[Adam Topaz]

you can do local attribute [tidy] tactic.case_bash but that slows things WAY down

[Filippo A. E. Nuccio]

Riccardo Brasca said:

The branch is bump_may_19

Is it normal that if I work on minibump then after 2/3 minutes I can work, but master takes forever to open any file?

[Riccardo Brasca]

it's done

[Riccardo Brasca]

Note that minibump is completely superseded by the other branch

[Filippo A. E. Nuccio]

But I ended up triying some out of dispair...

[Johan Commelin]

@Filippo A. E. Nuccio Those branches use different mathlibs, so you'll need to fetch mathlib caches

[Johan Commelin]

And your LTE oleans will also change

[Johan Commelin]

So I'm not surprised that this causes headaches

[Filippo A. E. Nuccio]

Oh right. I did not think at the different mathlib's. Let me try to get all straight.

[Johan Commelin]

Riccardo Brasca said:

it's done

Do you mean the entire bump? Or just that file?

[Riccardo Brasca]

The file

[Riccardo Brasca]

Looking for the next error

[Filippo A. E. Nuccio]

I suppose that running leanproject get-mathlib-cache would update mathlib to the latest mathlib, and this I do not want, right? And that the script fetch_olean_cahce only updates LTE's ones...

[Riccardo Brasca]

leanproject get-mathlib-cache should do the right thing, it takes mathlib as indicated in leanpkg.toml

[Riccardo Brasca]

but then you have to recompile all the project, there is no cache for nonmaster branch

[Riccardo Brasca]

at least not yet

[Filippo A. E. Nuccio]

but if I work in master I should have no problems, then.

[Riccardo Brasca]

Yep, in master you can use script/get_cache.sh

[Filippo A. E. Nuccio]

Let me try again, I suspect that the 42 degrees we have today in Italy don't help my laptop... :sweat:

[Riccardo Brasca]

The bump compiles for me.

[Johan Commelin]

Nice!

[Johan Commelin]

Let's hope it passes CI!

[Riccardo Brasca]

Mmm, CI failed

[Riccardo Brasca]

With a mysterious error

[Riccardo Brasca]

https://github.com/leanprover-community/lean-liquid/runs/7412687246?check_suite_focus=true

[Riccardo Brasca]

I've relaunched it

[Johan Commelin]

Hmm, it got an error again

[Adam Topaz]

It looks like it's still building?

[Johan Commelin]

https://github.com/leanprover-community/lean-liquid/runs/7412687246?check_suite_focus=true#step:10:27

[Adam Topaz]

https://github.com/leanprover-community/lean-liquid/runs/7415897270?check_suite_focus=true

[Johan Commelin]

Ooh, that's a different run

[Johan Commelin]

Ooh wait... lol

[Johan Commelin]

I should learn to read messages in order.

[Ben Toner]

date: extra operand ‘%T’
Starting build at
Try 'date --help' for more information.

That's my typo, sorry - https://github.com/leanprover-community/lean-liquid/pull/100. Doesn't affect anything.

/home/runner/work/_temp/9430b2ea-94d9-4500-b5f7-bc4ab48a1515.sh: line 6:  2229 Killed                  lean --json --make src
      2230 Done                    | python scripts/detect_errors.py

That's the OOM killer. Guess the extra swap isn't enough.

[Ben Toner]

So lean goes out of memory on a machine with 7 GB RAM and 10 GB swap. Can you please ask the experts if that is reasonable for a project of this size?

[Ben Toner]

To add more colour to that question, I'm asking for help because it's unclear to me if the next step should be

1. try to figure out if we're doing something wrong that causes memory usage to be high; or
2. figure out how to deal with the fact that the project now needs more memory to build.

[Mauricio Collares]

Mathlib compiles with -T150000 to cause a timeout in case of too many allocations. Would that be useful for debugging here?

[Mauricio Collares]

I definitely get timeouts compiling with -T150000 locally. A higher number might be better, as long as the OOM killer doesn't kick in.

/home/collares/lean-liquid/src/for_mathlib/AddCommGroup/explicit_limits.lean:16:9: error: (deterministic) timeout
/home/collares/lean-liquid/src/for_mathlib/AddCommGroup/explicit_limits.lean:16:11: error: (deterministic) timeout
/home/collares/lean-liquid/src/for_mathlib/pullbacks.lean:123:2: error: (deterministic) timeout
/home/collares/lean-liquid/src/for_mathlib/pullbacks.lean:62:41: error: (deterministic) timeout
...

[Adam Topaz]

FWIW, my settings in VScode are 16G memory and 400000 time limit, and I'm quite sure that can handle anything in the repo.

[Adam Topaz]

Where does that python script come from?

[Filippo A. E. Nuccio]

BTW Adam: do you manage to have these VSCode settings not to be uploaded in git? Did you manually add json to gitignore?

[Adam Topaz]

Honestly I have no clue where vscode stores these settings. I suppose I changed them globally so it shouldn't be in the repo itself.

[Filippo A. E. Nuccio]

The problem is that AFAIU workshop settings overwrite user settings, and the workshop ones are shared on a git repo.

[Filippo A. E. Nuccio]

But if you tell me you managed to, I will try to do the same myself.

[Adam Topaz]

Oh I see. I only use vscode for Lean (and emacs for everything else), so I don't mind setting all of my settings globally :)

[Ben Toner]

Mauricio Collares said:

Mathlib compiles with -T150000 to cause a timeout in case of too many allocations. Would that be useful for debugging here?

Thanks!! I've started two builds in CI with -T200000 (since you already tested -T150000 locally) and -T400000.

[Ben Toner]

Adam Topaz said:

Where does that python script come from?

Which Python script? This one?

[Adam Topaz]

Oh yes, that's the one. I'm just trying to understand the CI script

[Mauricio Collares]

Ben Toner said:

Thanks!! I've started two builds in CI with -T200000 (since you already tested -T150000 locally) and -T400000.

Then perhaps I should mention that I tested -T150000 only on the bump_may_19 branch, because Lean decides to rebuild a lot of mathlib when I test lean-liquid master here (yes, even after leanproject get-m).

[Mauricio Collares]

(deleted)

[Adam Topaz]

@Ben Toner what are the problematic declarations? Maybe I can try to speed them up (if that helps)? (sorry, I pinged the wrong person, I meant to ping @Mauricio Collares !)

[Ben Toner]

For now, the ones @Mauricio Collares mentions above. Then whatever turns up here in a couple of hours, if those builds do fail with deterministic timeouts.

[Adam Topaz]

Well... I'm still trying to build the branch, so don't hold your breath!

[Adam Topaz]

The branch built successfully on my machine with the same command that's used in the CI script. I merged master (which includes Ben's typo fix) to the bump branch. Let's hope that CI is finally happy!

[Mauricio Collares]

The problem, as I understand it, is that the CI machine runs out of memory but doesn't give a detailed error message, so fixing the OOM is hard. If your machine has a lot of memory, that might not be a problem locally. Adding -T200000 provides clues of what things need to be optimized to make it fit into the CI memory budget (the CI run triggered by Ben shows at least one timeout with this flag). But I'm hoping it works!

[Ben Toner]

Okay, progress! (Thanks @Mauricio Collares!) There are deterministic timeouts in CI even with -T400000.

[Adam Topaz]

I tried speeding up some of the proofs that were causing timeouts. I hope this helps!

[Johan Commelin]

I can confirm that the branch also builds on my machine. How do we get it past CI?

[Johan Commelin]

Can we bundle up our locally built oleans and push those to the shared storage (I know this is a pretty ugly hack).

[Johan Commelin]

I pushed a commit bumping the swap size to 14. Let's see if that helps.

[Johan Commelin]

Answer: nope
https://github.com/leanprover-community/lean-liquid/runs/7424346509?check_suite_focus=true#step:15:38

[Johan Commelin]

Scott helped us use the Hoskinson runners, which have a lot more juice. Things are looking good now!

[Johan Commelin]

It looks like everything worked except pushing to Azure: https://github.com/leanprover-community/lean-liquid/runs/7424647087?check_suite_focus=true

[Johan Commelin]

It seems to be hanging on that step?

[Johan Commelin]

I'm too impatient. It worked

[Riccardo Brasca]

Do we know why it is so slower?

[Riccardo Brasca]

https://github.com/leanprover-community/lean-liquid/pull/94 is green!

[Eric Wieser]

Quick, merge it!

[Riccardo Brasca]

It's merged.

[Riccardo Brasca]

Let's try one week later.

[Johan Commelin]

Maybe we should take slightly bigger steps now?

[Johan Commelin]

I think we can take 2 or 3 weeks in one go.

[Johan Commelin]

@Riccardo Brasca Did you already start a new branch?

[Riccardo Brasca]

Yes, I can publish it if you want. Nothing special at the moment.

[Johan Commelin]

Yes, please post the branch name, if only to prevent people from starting a competing branch

[Riccardo Brasca]

https://github.com/leanprover-community/lean-liquid/pull/103
the branch is bump_june_10

[Riccardo Brasca]

I am stopping to work at the bump. The first error is now in condensed/exact .

[Johan Commelin]

Oww, that one seems pretty nasty.

[Adam Topaz]

What's the mathlib change that makes this bad?

[Johan Commelin]

Je ne sais pas

[Johan Commelin]

It doesn't look like cospan_ext ever changed: https://mathlib-changelog.org/def/category_theory.limits.cospan_ext

[Riccardo Brasca]

Adam Topaz said:

I think the next big hurdle in bumping is the recent changes to universe parameters in finite limits and colimits.

This is later, isn't it?

[Adam Topaz]

I'm trying to look into the error for this bump, but I have to build first.

[Johan Commelin]

I think fetch_olean_cache should now work!

[Adam Topaz]

it's doing something!

[Adam Topaz]

The issue is in docs#category_theory.limits.cospan_comp_iso and the issue is here: https://github.com/leanprover-community/mathlib/pull/14351

[Adam Topaz]

The composition with with walking_cospan_functor was removed in a later PR #15067 but that is the one that generalizes a bunch of universes

[Adam Topaz]

A temporary fix is to use docs#category_theory.limits.diagram_iso_cospan as well, but we will have to modify this again when we go to the next bump

[Adam Topaz]

I'll push the temporary fix. I hope this doesn't cause build issues in other places, but I guess we'll see!

[Adam Topaz]

BTW, it's possible that the diagram_iso_cospan will be harmless later on... I guess we shall see :)

[Johan Commelin]

@Adam Topaz Can you leave a comment near the code describing this diagnosis?

[Johan Commelin]

And thanks for debugging!

[Adam Topaz]

I wrote this in the code itself

 -- This next line can be removed later if/when we generalize universe parameters in finite (co)limits
  refine _ ≪≫ (diagram_iso_cospan _).symm,

[Adam Topaz]

Honestly, I'm a little scared of bumping past #15067 :scared:

[Johan Commelin]

I think that on a system with enough RAM to have two clones open at the same time, it should be doable.

[Riccardo Brasca]

After this bump is done we can maybe try the PR immediately before #15067, so later we can concentrate on it.

[Riccardo Brasca]

It should compile now

[Johan Commelin]

Ooh, that went fast! Cool!

[Johan Commelin]

I'm starting on bump_jul_03

[Riccardo Brasca]

Are you working on it? I have some time now.

[Johan Commelin]

Sorry, I was gone for lunch

[Johan Commelin]

Now I'm back. How about you?

[Riccardo Brasca]

Let me push what I've done.

[Riccardo Brasca]

I am fixing col_exact, hopefully the errors are easy to fix since it's a pain to work with that file.

[Riccardo Brasca]

OK, it should be done and pushed.

[Riccardo Brasca]

I am stopping for at least half an hour

[Johan Commelin]

Okido, I'll take over

[Johan Commelin]

Riccardo Brasca said:

I am fixing col_exact, hopefully the errors are easy to fix since it's a pain to work with that file.

Yes, this might be the most painful file in the entire project.

[Johan Commelin]

I fixed two more files. We're converging towards the end of this bump :sweat_smile:

[Johan Commelin]

Qprime_isoms.lean is done

[Johan Commelin]

It's done!

[Johan Commelin]

Shall we start the universe-bump on top of this one?

[Johan Commelin]

I'm starting on bump-universes

[Adam Topaz]

Can someone reproduce the following?

leanproject get lean-liquid:bump-universes
cd lean-liquid_bump-universes
leanproject build

And lean starts compiling mathlib.

[Eric Rodriguez]

is it https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.22saving.20olean.22.3F?

[Adam Topaz]

Yeah, that might be the issue. In any case, it looks like only a few files had to be compiled in mathlib, so it's not all that bad

[Adam Topaz]

I must say that I am quite unhappy now with the decision to make the universe parameters in diagrams for all finite (co)limits be 0.
What happens, for example, when you have a category C : Type u and category.{v} C which has all products (which means all limits indexed by discrete X where X : Type v), and now you want to identify the binary product with a product over a two-element type?

[Adam Topaz]

Another one: Suppose I know that a functor F from C to D preserves limits of shape J whenever C has all limits of shape J. How can I deduce that F preserves finite limits if C has all finite limits?

[Adam Topaz]

Do I now have to prove that F preserves limits of shape J for both J : Type v and J : Type 0?

I'm frustrated

[Johan Commelin]

Hmmz, shouldn't there be generic instances for that?

[Johan Commelin]

I understand your frustration.

[Johan Commelin]

I really wonder whether Lean should have extra support for quantifying over universes less than a fixed universe u.

[Johan Commelin]

We can already model this using max u v, so it wouldn't increase the strength (or even the amount of computations) of the kernel. But max u v doesn't scale from a UI point of view.

[Adam Topaz]

yeah I found preserves_finite_limits_of_preserves_finite_limits_of_size

[Adam Topaz]

Still, it feels like this change didn't really make anything easier!

[Johan Commelin]

@Adam Topaz Do you think we should forgo this bump, and "fix" mathlib first?

[Adam Topaz]

I don't know. But here is another issue: The stuff in category_theory/limits/concrete.lean was never generalized.

[Johan Commelin]

Ouch! That's annoying.

[Adam Topaz]

actually, maybe that file is okay (I got it to work in LTE), but it involved introducing new instances

[Adam Topaz]

docs#category_theory.Sheaf.is_sheaf_of_is_limit needs to be generalized as well

[Andrew Yang]

@Adam Topaz We have docs#category_theory.limits.is_limit.cone_points_iso_of_equivalence which should be useful.

[Andrew Yang]

I could try and bump it myself as well. Since I reviewed that refactor, some responsibility of the frustration might be on me. :sweat_smile:

[Adam Topaz]

@Andrew Yang if you want to take a look at for_mathlib/abelian_sheaves/main in the bump-universes branch, that would be helpful! It's just a silly proof (essentially just that limits commute with limits at the end of the day) that doesn't quite generalize with what's in mathlib

[Andrew Yang]

The building is slower than I thought, and it is late in my timezone. I'll have a thorough look at it tomorrow.

[Adam Topaz]

I fixed all the files up to (and including) the ExtrDisc equivalence, which I think is the most challenging part of this mathlib bump. There is still more work to do though, but I think we will get there soon.

[Johan Commelin]

I fixed one more file

[Johan Commelin]

@Andrew Yang if you want to hack on this, go ahead! I'll keep my hands off my keyboard (-;

[Johan Commelin]

I pushed what I did. There's a sorry in thm95/col_exact.lean

[Johan Commelin]

I pushed whatever I did. I'm gone for ~3 hrs

[Riccardo Brasca]

I am having a look

[Riccardo Brasca]

I also have to stop (without having fixed one single error :unamused: )

[Andrew Yang]

I'll try to fix some stuff in for_mathlib now.

[Johan Commelin]

@Andrew Yang did you already fix ab4.lean?

[Andrew Yang]

Yes. I can push what I have now.

[Johan Commelin]

Thanks. Then I'll start looking at breen_deligne/.

[Johan Commelin]

Which was completely broken and didn't even know whatAB4 meant.

[Andrew Yang]

Pushed. I'm working on for_mathlib/AddCommGroup/tensor now.

[Johan Commelin]

Do we have a "resize" instance for

reflects_colimit.{0 0 u+1 u+1 u+2 u+2} (functor.empty.{0 u+1 u+2} (Condensed.{u u+1 u+2} Ab.{u+1})) FF

[Johan Commelin]

I want to deduce this .{0 0} case from the .{u+1 u+1} case.

[Andrew Yang]

It should be reflects_colimits_of_size_shrink.{0 u+1 0 u+1} FF, I think.

[Johan Commelin]

Thanks, I'll try.

[Johan Commelin]

That worked. I fixed 3 files and pushed.

[Johan Commelin]

condensed/filtered_colimits seems to be quite a nightmare.

[Johan Commelin]

@Andrew Yang how is the tensor file going?

[Andrew Yang]

It should (hopefully) be almost done. I had to generalize the universe of for_mathlib/AddCommGroup.lean and we are missing a universe polymorphic has_biproducts_of_shape_of_has_finite_biproducts.

[Andrew Yang]

for_mathlib should be all fixed if lean didn't lie to me

[Johan Commelin]

I'm working on condensed/acyclic

[Johan Commelin]

done, and now I need to go

[Adam Topaz]

I fixed condesed/filtered_colimits.

[Adam Topaz]

What a mess!

[Johan Commelin]

Wow! I had 3 attempts that all failed

[Adam Topaz]

It looks like pseudo_normed_group/Qprime is the next pain in the ***.

I wonder whether it would be easier to revert Pow to how it was before this attempted bump (i.e. defined as biproducts over ulifts of fin n as opposed to fin n itself). There is an instance missing, but I think this would make Qprime easier to handle.

[Adam Topaz]

Adam Topaz said:

It looks like pseudo_normed_group/Qprime is the next pain in the ***.

I wonder whether it would be easier to revert Pow to how it was before this attempted bump (i.e. defined as biproducts over ulifts of fin n as opposed to fin n itself). There is an instance missing, but I think this would make Qprime easier to handle.

Scratch that... pseudo_normed_group/Qprime.lean is now fixed.

[Adam Topaz]

I think the branch will actually build with my latest commit. There may still be some linting remaining though

[Adam Topaz]

There was one slightly concerning thing that came up that I will mention here, just so that we (maybe) remember it in the future.
One of the last errors that came up in this branch was a maximum TC depth error in Lbra/ext in the decl condensify_iso_extend.
Adding the following instance fixed the issue, but there is probably some TC loop. What I don't know is whether the loop comes from mathlib, or from mathlib together will all of the hacky instances we have all over the place in LTE (I suppose the latter is more likely).

I mentioned a brief comment in the following:
https://github.com/leanprover-community/lean-liquid/blob/615ffdbfee74760114a2c98b92287ccf7eb9ae1d/src/Lbar/ext.lean#L44
In case anyone has time to help diagnose, if the := {} on line 47 of the file in the link above is replaced with := by apply_instance, the same error should show up.

[Johan Commelin]

I'm starting the mathlib bump to mathlib master.

[Johan Commelin]

I'm not going to rename pseudo_normed_group to pseudo_normed_add_comm_group for now.

[Yaël Dillies]

Is pseudo_normed_group pseudo in the same sense as pseudo_metric_space?

[Andrew Yang]

It is an algebraic version of a semi-norm, which is semi in the same sense as pseudometric space is pseudo.

[Johan Commelin]

I pushed to mathlib-bump-25-jul-22.

[Johan Commelin]

Modulo

src/for_mathlib/pullbacks.lean:117:6: error: rewrite tactic failed, did not find instance of the pattern in the target expression
  pullback_cone.fst S
state:
C : Type u_1,
D : Type u_2,
_inst_1 : category C,
_inst_2 : category D,
e : C ≌ D,
X Y B : D,
f : X ⟶ B,
g : Y ⟶ B,
_inst_3 : has_pullback (e.inverse.map f) (e.inverse.map g),
S : cone (cospan f g),
m : S.X ⟶ (e.pullback_cone f g).X,
h : m ≫ e.functor.map pullback.fst ≫ e.counit.app X = pullback_cone.fst S
⊢ e.inverse.map (S.π.app walking_cospan.left) =
    e.unit_iso.hom.app (e.inverse.obj S.X) ≫
      e.inverse.map (e.counit_iso.hom.app S.X) ≫
        e.inverse.map m ≫ e.unit_iso.inv.app (pullback (e.inverse.map f) (e.inverse.map g)) ≫ pullback.fst

I think that for_mathlib is error-free.

[Johan Commelin]

I'm working on making thm95 error-free.

[Johan Commelin]

That seems to be done. Looking at condensed/ next.

[Johan Commelin]

I've been pushing a bunch of fixes. Unfortunately I find it hard to say how much of the project compiles, and how much still needs to be fixed. Does Lean have a way of reporting this?

[Johan Commelin]

condensed/ seems to be error-free

[Andrew Yang]

Is the error in for_mathlib fixed yet? I could try if it is not.

[Johan Commelin]

I just did

[Johan Commelin]

Things are tentatively looking good. I'm compiling ext_aux1.lean locally.

[Johan Commelin]

Locally, it builds. But CI might complain at the linting step.

[Johan Commelin]

One linting error. I pushed a fix.

[Johan Commelin]

It's merged! The elephant is no longer in the room!

[Adam Topaz]

I'll believe it when the table at the bottom of
https://leanprover-community.github.io/lean_projects.html
is updated ;)

[Yaël Dillies]

Amazing! That means I can more easily work on nnrat and Gordan.

[Eric Wieser]

That table is apparently broken and possibly at the end of it's life due to a low ROI on maintaining it

[Riccardo Brasca]

I wanted to do a bump, but I very quickly got stuck with #15690. The definition of docs#homological_complex.hom.prev changed, and the docstring is now false, right? If there is no i such that r i j, then c.prev j = j and I think f.prev j is f.f j.

[Adam Topaz]

yeah that docstring is wrong

[Riccardo Brasca]

(also, the name of docs#X_prev_iso_zero and friends is now wrong)

[Riccardo Brasca]

So

lemma homological_complex.prev_eq_zero' [has_zero_morphisms C]
  {X Y : homological_complex C c} (f : X ⟶ Y) (i : M) (h : c.prev i = none) : f.prev i = 0

in for_mathlib/homological_complex_map_d_to_d_from is now false, and should be stated using the isomorphism above. Do you think it is going to affect a lot of stuff in other files?

[Adam Topaz]

no I think the correct thing to do now is to use the fact that X.d j j = 0

[Adam Topaz]

I guess the hope is that lemmas such as this will no longer be necessary. @Johan Commelin thoughts?

[Adam Topaz]

where is this prev_eq_zero' used?

[Adam Topaz]

For example, https://github.com/leanprover-community/lean-liquid/blob/9701fc4a29514852b599e9732c2409f34153ce2a/src/for_mathlib/homological_complex_map_d_to_d_from.lean#L31 should now be true just by definition!

[Johan Commelin]

I just returned from a week of holidays. I should probably do this bump, because I also made that mathlib PR.

[Riccardo Brasca]

#15940 for the modifications not done in the previous PR

[Johan Commelin]

I just started working on the bump. 1 file done:

 leanpkg.toml                                             |   2 +-
 src/for_mathlib/homological_complex_map_d_to_d_from.lean | 147 +++++++++++++++++++++------------------------------------------------------------------------------------------------------------------------------
 2 files changed, 22 insertions(+), 127 deletions(-)

[Johan Commelin]

I pushed what I have so far to mathlib-bump-aug-09

[Johan Commelin]

The proof strategy for

def homology_embed_nat_iso (𝓐 : Type*) [category 𝓐] [abelian 𝓐]
{c₁ : complex_shape ι₁} {c₂ : complex_shape ι₂} (e : c₁.embedding c₂) (he : e.c_iff)
  (i₁ : ι₁) (i₂ : ι₂) (h₁₂ : e.f i₁ = i₂) :
  embed e ⋙ homology_functor 𝓐 c₂ i₂ ≅ homology_functor 𝓐 c₁ i₁ :=

is now broken...

[Johan Commelin]

But that isom is still true. We just need a new way to fill it in.

[Kevin Buzzard]

I don't know if this compiles for you; my version of the branch is all broken.

def homology_embed_nat_iso (𝓐 : Type*) [category 𝓐] [abelian 𝓐]
{c₁ : complex_shape ι₁} {c₂ : complex_shape ι₂} (e : c₁.embedding c₂) (he : e.c_iff)
  (i₁ : ι₁) (i₂ : ι₂) (h₁₂ : e.f i₁ = i₂) :
  embed e ⋙ homology_functor 𝓐 c₂ i₂ ≅ homology_functor 𝓐 c₁ i₁ :=
begin
  calc embed e ⋙ homology_functor 𝓐 c₂ i₂ ≅
    embed e ⋙ (short_complex.functor_homological_complex 𝓐 c₂ i₂ ⋙
      short_complex.homology_functor) : _
  ... ≅ (embed e ⋙ short_complex.functor_homological_complex 𝓐 c₂ i₂) ⋙
      short_complex.homology_functor : _
  ... ≅ short_complex.functor_homological_complex 𝓐 c₁ i₁ ⋙
    short_complex.homology_functor : _
  ... ≅ homology_functor 𝓐 c₁ i₁ : _,
  { exact iso_whisker_left _ (short_complex.homology_functor_iso 𝓐 c₂ i₂), },
  { exact (functor.associator _ _ _).symm, },
  { subst h₁₂,
    congr', },
  { exact (short_complex.homology_functor_iso 𝓐 c₁ i₁).symm, },
end

[Kevin Buzzard]

I just took the line which didn't work, tried subst and then apparently congr' works, but honestly I have errors before this in the file, I have errors in imports, this might be nonsense.

[Kevin Buzzard]

{ subst h₁₂, refl, }, works for me too.

[Johan Commelin]

Ooh, maybe oleans did something weird. Let me try to compile.

[Kevin Buzzard]

Does the proof not work at your end?

[Johan Commelin]

Sorry, I'm a bit flooded by bureaucracy. Back at this problem. I don't see errors in imports at the moment.

[Johan Commelin]

subst h₁₂, congr' doesn't work for me.

[Johan Commelin]

It would also be very surprising. Because afaict that line is just false, with current mathlib.

[Johan Commelin]

Ooh, that's not actually true. The line is still fine. But the proof can not start with refine iso_whisker_right _. After that you would end up with something that isn't true.

[Joël Riou]

I do not have time now to fix this immediately, but I think one may remove the e.c_iff assumption which I introduced only as a convenience.

[Johan Commelin]

I think you need e.c_iff. What happens if you have a discrete complex_shape that doesn't have any rel i j and you embed it into a "normal" complex shape?

[Kevin Buzzard]

Oh, I had the correct lean-liquid oleans but probably incorrect mathlib oleans. Sorry for the noise!

[Johan Commelin]

Johan Commelin said:

I think you need e.c_iff. What happens if you have a discrete complex_shape that doesn't have any rel i j and you embed it into a "normal" complex shape?

Ooh never mind, I guess it actually still works out.

[Joël Riou]

Johan Commelin said:

Johan Commelin said:

I think you need e.c_iff. What happens if you have a discrete complex_shape that doesn't have any rel i j and you embed it into a "normal" complex shape?

Ah, I do not remember the details, but in your example, the d_to and d_from are all zeros, so that homologies are trivially the same.
Instead of constructing an isomorphism between two functors to short_complex as I initially did, a possible approach would be to define a natural transformation between two functors with values in short_complex, and then show it is an isomorphism object by object, which may require dealing with many cases...

[Adam Topaz]

I have some time now to play with this... what branch is this on?

[Adam Topaz]

and what file?

[Johan Commelin]

Johan Commelin said:

I pushed what I have so far to mathlib-bump-aug-09

It's in the file for_mathlib/complex_extend

[Adam Topaz]

Bah, we have embed_iso, but not embed_prev_iso or embed_next_iso.

[Adam Topaz]

$ leanproject get-mathlib-cache
SHA b'ec818836889c031d4035c928bcbc638af5fbd736' could not be resolved, git returned: b'ec818836889c031d4035c928bcbc638af5fbd736 missing'

[Adam Topaz]

on this branch....

[Adam Topaz]

The file for_mathlib/homological_complex_map_d_from_d seems broken on my end as well... can someone reproduce?

[Adam Topaz]

Is there a way to tell leanproject to pull the correct commit based on the hash in the toml file of a non-mathlib project?

[Adam Topaz]

I had to do things manually with git in the _target folder.

[Adam Topaz]

Unforunately...

def embed_prev_iso (i : ι) : ((embed e).obj X).X_prev (e.f i) ≅ X.X_prev i :=

isn't just embed_iso, so all the nice stuff we gained by redefining prev and next no longer applies when we have to deal with embedings :(

[Adam Topaz]

here embed_iso is

def embed_iso (i : ι) : ((embed e).obj X).X (e.f i) ≅ X.X i :=

[Adam Topaz]

Can we redefine the stuff around embeddings so that we get better defeqs? Is it worth it?

[Joël Riou]

Adam Topaz said:

Can we redefine the stuff around embeddings so that we get better defeqs? Is it worth it?

I do not think so. When we embed ℕ in ℤ (with the chain_complex convention) and start with a complex K indexed by ℕ, the homology comparison in degree 0 will be between the homology of the short complex K.X 1 ⟶ K.X 0 ⟶ K.X 0 (the right map is zero) and the homology of K.X 1 ⟶ K.X 0 ⟶ 0. With the homology refactor, embed_next_iso no longer exists.
What I suggested above is that one may still define a (natural) map of short_complex (take the identities when there are available, and 0 in the "irrelevant" cases), and it should be an isomorphism on homology.

[Johan Commelin]

And I guess that checking that it is an isom involves 4 cases?

[Johan Commelin]

Depending on whether prev/next exists or not.

[Joël Riou]

Yes, that is the idea. Actually, in order to have better definitional properties for the homology iso, instead of a natural transformation which turns out to be an iso, it should be possible to define natural transformations with values in short_complex in both directions, and then in homology, they would induce inverse isomorphisms.

[Adam Topaz]

So can someone explain again why we shouldn't just change the definition of complexes to be a bunch of short complexes glued with isomorphisms?

[Johan Commelin]

Maybe we should do that refactor of mathlib before bothering with this bump?

[Adam Topaz]

Well I though we're not all in agreement that this was the way to go.

[Johan Commelin]

I'll mull over it again in my sleep tonight (-;

[Joël Riou]

Adam Topaz said:

So can someone explain again why we shouldn't just change the definition of complexes to be a bunch of short complexes glued with isomorphisms?

The "bunch of short complexes" approach has several problems. One was the definition of morphisms of complexes, which was not straightforward. (I have some concerns also about the definition of homotopies.) Another problem I see with the draft definition you outlined is that I am not sure that the map which sends a complex K to the short complex "around a certain degree n" would be a functor, because if n has no prev, you only required that the left map of the short complex be zero, not that the left object is zero (which we cannot do if we want to allow complexes in categories with no zero object). Then, with this definition, there is no reason that two isomorphic complexes have isomorphic associated short complexes.

I think that the strategy I suggested above should work to get back embed_homology_nat_iso. Once the natural transformations are defined in both direction, the verification we have inverse isomorphims should follow mostly from statements like of_g_are_zeros, etc. at the end of homology_map_datum.lean.

[Adam Topaz]

The functoriality issue is easy to solve: ensure is_zero instead of just the morphism being zero. Yes, keeping track of the various isomorphisms would be tedious at first, but I think we just have to do this once then forget about all the coherences because they would be part of the data! With the current approach, it seems that we have to chase these isomorphisms whenever we pass to short complexes and/or homology. I would rather have slightly more pain at the start instead of constant mild pain every time we deal with homology.

[Johan Commelin]

Ensuring is_zero doesn't address Joël's point that we would rule out complexes in categories without a zero object. Note that we use those in LTE: stuff like breen_deligne.data.

Also, I don't think this approach would make it easier to define embed. (Also not much harder, to be fair.)
You will have to construct the short complex in degree -1 will be. And this involves two zero-objects, and the non-trivial X_next coming from the object in degree 0.

So for the issue at hand, I don't think this refactor will save us any work.

[Joël Riou]

I have implemented part of ideas I suggested for homology_embed_nat_iso in the following commit https://github.com/leanprover-community/lean-liquid/commit/88a880feb20226290b5d2f153fb4aa2c01494e10

[Joël Riou]

I have fixed one sorry about the commutativity of some square (the proof is not very elegant, but at least it works). The others sorries should be similar.

[Adam Topaz]

If we have a category with zero morphisms, then I think you can formally adjoin a zero object in a "free" way. In an ideal world it would be seamless to go back and forth between the original category and such a gadget. Unfortunately, I don't think we live in such an ideal world :(

Anyway, I was already convinced before that we need to allow complexes for categories with no zero object (even though you had to remind me!) and now I'm convinced that just assuming a morphism is zero on the extremes is not good because of funcotriality issues, as Joel pointed out. So I think the idea of gluing short complexes might be dead in the water.

But that doesn't change the fact that I think the current approach to complexes and homology isn't great. We want Lean to be a tool that regular mathematicians can use, so we should build out theories to match mathematicians' intuition as closely as possible, and I think the current definitions here are very far from doing that.

So what else can we do? I have another (completely different) idea that I'll try to sketch.

[Johan Commelin]

Adam Topaz said:

But that doesn't change the fact that I think the current approach to complexes and homology isn't great. We want Lean to be a tool that regular mathematicians can use, so we should build out theories to match methematicians' intuition as closely as possible, and I think the current definitions here are very far from doing that.

Completely agreed.

[Joël Riou]

homology_embed_nat_iso is almost done now. There are only three sorries (which are essentially isomorphic to the first ugly proof in embed_short_complex_ιin complex_extend.lean. If anyone wants to tidy this proof and duplicate it (changing prev/next, etc), feel free to do so, as I will not have time to do it today (India/Chennai time). (As I suggested above, I have removed the unnecessary iff assumption, so that a little fix should be necessary in the files which refer to homology_embed_nat_iso.)

[Johan Commelin]

Thanks!

[Kevin Buzzard]

Are the problems with cohomology really because of the definitions, or are we actually just missing good API? Why should the definitions matter? In Isabelle they don't!

[Adam Topaz]

Kevin when is the last time you considered the differential from $C^{37}(G,A)$ to $C^2(G,A)$ where $C^*(G,A)$ is the complex of inhomogeneous cochains of a group $G$?

[Kevin Buzzard]

You just don't like the fact that it makes sense? Yeah I didn't like that 1/0 made sense for a while. But do you think we can do spectral sequences with what we have?

[Adam Topaz]

I think it's an important point to keep spectral sequences in mind!

[Kevin Buzzard]

Or have they all been replaced with derived functors nowadays? Or even the derived infinity category?

[Adam Topaz]

Do we really want differentials going all over the place on the E_2 instead of just somehow restricting to E i j -> E (i+2) (j-1)? I don't know.

[Adam Topaz]

Sure, derived functors are the right level of generality, but things like the Serre spectral sequence are still important for explicit calculations which we should be able to do!

[Kevin Buzzard]

We have to have the differentials everywhere for the same reason we ended up having them everywhere on the E1 page

[Kevin Buzzard]

Actually we only had arbitrary horizontal ones I guess

[Adam Topaz]

Aside: should we make a separate homology stream to discuss this stuff?

[Johan Commelin]

Hmm, maybe 3 or 4 topics in #maths also works? But ey, streams are cheap. I don't care (-;

[Adam Topaz]

The maths stream is fine, but it's easy for things to get lost in there.

[Adam Topaz]

I can do it when I get back to my computer, if @Johan Commelin doesn't beat me to it :wink:

[Johan Commelin]

See #homological algebra

[Johan Commelin]

Joël Riou said:

homology_embed_nat_iso is almost done now. There are only three sorries (which are essentially isomorphic to the first ugly proof in embed_short_complex_ιin complex_extend.lean. If anyone wants to tidy this proof and duplicate it (changing prev/next, etc), feel free to do so, as I will not have time to do it today (India/Chennai time). (As I suggested above, I have removed the unnecessary iff assumption, so that a little fix should be necessary in the files which refer to homology_embed_nat_iso.)

Fixed the remaining sorries.

[Johan Commelin]

Bah, this bump is quite annoying.

[Johan Commelin]

I made it to 50% of mapping_cone.lean

[Johan Commelin]

I was hoping to continue today, after a bunch of travelling/holidays. But Deutsche Bahn has decided that I'll have to do it without the computational power of the beast in my office.

[Johan Commelin]

DB allowed me to travel to my office today. mapping_cone.lean has been fixed.

db_logo.jpg

[Johan Commelin]

Should compile now: https://github.com/leanprover-community/lean-liquid/pull/122

[Kevin Buzzard]

Nice work!

[Johan Commelin]

I particularly like https://github.com/leanprover-community/lean-liquid/pull/122/files#diff-ef25eff2213ff3cc983adabc2279c500d329f4eecf29f20ba80262ff44aa5a67R330

[Kevin Buzzard]

I will be absolutely honest and say that I was looking at the diff and it was precisely that line which motivated my previous post!

I also looked at the recent diff for the mathlib bump to new Lean. That's coming your way...(fortunately most of the changes seem trivial, it's just that there might be many many changes...)

[Yaël Dillies]

Oh does that mean we can now bump to nnrat?

[Johan Commelin]

Almost! Still need to have CI give the green flag on this PR.

[Johan Commelin]

It builds, but the linter complains: https://github.com/leanprover-community/lean-liquid/runs/8101380577?check_suite_focus=true

[Johan Commelin]

I'm done for the day though

[Riccardo Brasca]

I am fixing the linter.

[Riccardo Brasca]

It's merged!

[Johan Commelin]

@Riccardo Brasca thanks so much

[Yaël Dillies]

Let me start a new bump then!

[Johan Commelin]

I can join you in ~ 20 mins.

[Johan Commelin]

Somehow mapping_cone.lean is now in the deps of liquid.lean.

[Johan Commelin]

@Yaël Dillies fixed Gordan.lean.

[Johan Commelin]

Now liquid.lean compiles. I'll work on the rest of the bump.

[Johan Commelin]

It compiles locally. This bump was easy-peasy-lemon-squeezy. :smiley:

[Johan Commelin]

And it is merged!

[Kevin Buzzard]

That is awesome! You're on today's mathlib. I seriously thought that it would go like the perfectoid project -- beyond some point it would just prove too hard to bump. That's amazing that it's all compiling and also all up to date. Congratulations.

[Riccardo Brasca]

@Yaël Dillies can you have a look at branch bump-24-sep? There is an error in src/free_pfpng/epi.lean related to docs#exists_signed_sum univ, that you PRed to mathlib with a slightly different statement. I am catching a plane and I won't probably have time to fix it today, but it shouldn't be too hard. Thanks!

In any case if someone else wants to keep on doing the bump feel free to do so, it seems rather easy.

[Yaël Dillies]

It's not completely trivial to go from the version I PRed to the version we need, so it might take a week until I have time to fix this properly.

[Riccardo Brasca]

If it's complicated we can just change the name of the LTE version

[Johan Commelin]

I think that's maybe the easy fix that we should go for in this mathlib bump.

[Johan Commelin]

Then Yaël can refactor whenever they want/have time.

[Johan Commelin]

We're being bitten by

1c1
< has type
---
> but is expected to have type
22,24c22,23
<        (@category_theory.abelian.to_preadditive.{u+1 u+2} Ab.{u+1} AddCommGroup.large_category.{u+1}
<           AddCommGroup.category_theory.abelian.{u+1}))
<     (@category_theory.Sheaf.category_theory.preadditive.{u+2 u u+1} ExtrDisc.{u} ExtrDisc.category_theory.category.{u}
---
>        AddCommGroup.category_theory.preadditive.{u+1})
>     (@category_theory.Sheaf.preadditive.{u u+1 u+1 u+2} ExtrDisc.{u} ExtrDisc.category_theory.category.{u}
28,29c27
<        (@category_theory.abelian.to_preadditive.{u+1 u+2} Ab.{u+1} AddCommGroup.large_category.{u+1}
<           AddCommGroup.category_theory.abelian.{u+1}))
---
>        AddCommGroup.category_theory.preadditive.{u+1})

[Johan Commelin]

@Adam Topaz @Joël Riou @Andrew Yang do you recognize a change in category theory that might have caused this?

[Adam Topaz]

def free_Cech'_iso_ExtrDisc (F : arrow Profinite.{u}) :
  ((Condensed_ExtrSheaf_equiv _).inverse.map_homological_complex _).obj (free_Cech' F) ≅
  free_ExtrDisc_Cech' F :=
let e := ExtrDisc_sheafification_iso in
(whiskering_Cech_comp_iso F
  (Profinite_to_Condensed.{u} ⋙ CondensedSet_to_Condensed_Ab.{u})
  ((Condensed_ExtrSheaf_equiv.{u u+2} Ab.{u+1}).inverse)
  (Profinite_to_ExtrDisc_presheaf_Ab.{u} ⋙ presheaf_to_Sheaf.{u+2 u u+1} ExtrDisc.proetale_topology.{u} Ab.{u+1}) $
nat_iso.of_components
(λ S, e.symm.app _)
begin
  intros S T f,
  dsimp only [nat_iso.app_hom],
  erw e.symm.hom.naturality,
  refl,
end) ≪≫
begin
  dsimp [free_ExtrDisc_Cech'],
  convert iso.refl _,
  sorry
end

yields

F: arrow.{u u+1} Profinite.{u}
e: (whiskering_left.{u+1 u u+1 u u+2 u+1} ExtrDisc.{u}ᵒᵖ Profinite.{u}ᵒᵖ Ab.{u+1}).obj ExtrDisc_to_Profinite.{u}.op ⋙ presheaf_to_Sheaf.{u+2 u u+1} ExtrDisc.proetale_topology.{u} Ab.{u+1} ≅ presheaf_to_Sheaf.{u+2 u u+1} proetale_topology.{u} Ab.{u+1} ⋙ (Condensed_ExtrSheaf_equiv.{u u+2} Ab.{u+1}).inverse := ExtrDisc_sheafification_iso.{u}
⊢ Sheaf.preadditive.{u u+1 u+1 u+2} = abelian.to_preadditive.{u+1 u+2}

Did someone change anything about preadditive instances?

[Adam Topaz]

BTW, abelian C is a subsingleton. Does someone want to prove this?

[Riccardo Brasca]

#16403 just got merged, so it cannot be the guilty, but maybe it is worth to upgrade mathlib to it to avoid duplicating the work

[Adam Topaz]

it will take quite a lot of work to bump to #16403

[Adam Topaz]

but of course we should do it.

[Adam Topaz]

I'm SO confused:

def free_Cech'_iso_ExtrDisc (F : arrow Profinite.{u}) :
  ((Condensed_ExtrSheaf_equiv _).inverse.map_homological_complex _).obj (free_Cech' F) ≅
  free_ExtrDisc_Cech' F :=
let e := ExtrDisc_sheafification_iso in
(whiskering_Cech_comp_iso F
  (Profinite_to_Condensed.{u} ⋙ CondensedSet_to_Condensed_Ab.{u})
  ((Condensed_ExtrSheaf_equiv.{u u+2} Ab.{u+1}).inverse)
  (Profinite_to_ExtrDisc_presheaf_Ab.{u} ⋙ presheaf_to_Sheaf.{u+2 u u+1} ExtrDisc.proetale_topology.{u} Ab.{u+1}) $
nat_iso.of_components
(λ S, e.symm.app _)
begin
  intros S T f,
  dsimp only [nat_iso.app_hom],
  erw e.symm.hom.naturality,
  refl,
end) ≪≫
begin
  dsimp [free_ExtrDisc_Cech'],
  convert iso.refl _,
  apply preadditive.ext,
  apply funext, intros P, apply funext, intros Q,
  dsimp,
  apply add_comm_group.ext,
  apply funext, intros f, apply funext, intros g,
  refl,
end

Are these defeq? If so, why can't lean figure it out!?

[Adam Topaz]

Adam Topaz said:

BTW, abelian C is a subsingleton. Does someone want to prove this?

We have it (well, essentially)! docs#category_theory.subsingleton_preadditive_of_has_binary_biproducts

[Adam Topaz]

I fixed condensed/acyclic.lean in this branch.

[Adam Topaz]

The issue was the nsmul and zsmul from the preadditive instance on Sheaf _ was not defeq to what we had in LTE.
The source of the issue was that mathlib now knows that sheaves of abelian groups form a preadditive category, but the preadditive instance is obtained via docs#function.injective.add_comm_group which doesn't give the expected defeq behavior for nsmul and zsmul

[Adam Topaz]

Anyway, once we bump past #16403 then the abelian category instance on sheaves of abelian groups will come from mathlib and will end up having the mathlib preadditive instance, so all should be fine again.

[Adam Topaz]

The fix for now was to use the preadditive instance from mathlib in LTE.

[Adam Topaz]

(plus some minor error that was fixed with an explicit universe annotation)

[Johan Commelin]

Ooh wow, ugly nasty bug. Thanks for fixing it!

[Johan Commelin]

Thanks for finishing the bump!