## Stream: condensed mathematics

### Topic: The elephant in the room

#### Adam Topaz (Jul 16 2022 at 12:28):

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

#### Riccardo Brasca (Jul 16 2022 at 12:32):

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

#### Kevin Buzzard (Jul 16 2022 at 12:32):

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 (Jul 16 2022 at 12:33):

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

#### Kevin Buzzard (Jul 16 2022 at 12:33):

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 (Jul 16 2022 at 12:34):

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 (Jul 16 2022 at 12:34):

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

#### Kevin Buzzard (Jul 16 2022 at 12:34):

Right that was my position with perfectoid

#### Kevin Buzzard (Jul 16 2022 at 12:34):

I didn't want it to become an albatross.

#### Filippo A. E. Nuccio (Jul 16 2022 at 12:34):

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 (Jul 16 2022 at 12:35):

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

#### Filippo A. E. Nuccio (Jul 16 2022 at 12:35):

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

#### Riccardo Brasca (Jul 16 2022 at 12:35):

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

#### Riccardo Brasca (Jul 16 2022 at 12:36):

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

Pretty old

#### Adam Topaz (Jul 16 2022 at 12:37):

In mathlib terms at least

#### Filippo A. E. Nuccio (Jul 16 2022 at 12:37):

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

#### Adam Topaz (Jul 16 2022 at 12:38):

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 (Jul 16 2022 at 12:38):

May 12th, not that old

#### Riccardo Brasca (Jul 16 2022 at 12:54):

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

#### Adam Topaz (Jul 16 2022 at 12:59):

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

#### Adam Topaz (Jul 16 2022 at 12:59):

in case it helps!

#### Riccardo Brasca (Jul 16 2022 at 13:17):

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 (Jul 16 2022 at 13:50):

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 (Jul 16 2022 at 15:55):

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 (Jul 16 2022 at 16:02):

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

#### Riccardo Brasca (Jul 16 2022 at 16:02):

Yes, in the minibump branch

#### Riccardo Brasca (Jul 16 2022 at 16:03):

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

#### Riccardo Brasca (Jul 16 2022 at 16:05):

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 (Jul 16 2022 at 16:16):

@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 (Jul 16 2022 at 16:25):

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 (Jul 16 2022 at 18:25):

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?

how big is LTE?

#### Adam Topaz (Jul 16 2022 at 18:26):

Ben Toner said:

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

#### Kenny Lau (Jul 16 2022 at 18:26):

that is quite a number of lines

#### Robert Brijder (Jul 16 2022 at 18:27):

Kenny Lau said:

that is quite a number of lines

So, mathlib is not supposed to grow so much?

#### Yaël Dillies (Jul 16 2022 at 18:27):

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 (Jul 16 2022 at 18:27):

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

#### Filippo A. E. Nuccio (Jul 16 2022 at 18:28):

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 (Jul 16 2022 at 18:28):

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 (Jul 16 2022 at 18:28):

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

#### Damiano Testa (Jul 16 2022 at 18:29):

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 (Jul 16 2022 at 18:29):

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 (Jul 16 2022 at 18:29):

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 (Jul 16 2022 at 18:30):

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 (Jul 16 2022 at 18:30):

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 (Jul 16 2022 at 18:30):

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

#### Filippo A. E. Nuccio (Jul 16 2022 at 18:31):

@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 (Jul 16 2022 at 18:31):

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 (Jul 16 2022 at 18:31):

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

#### Yaël Dillies (Jul 16 2022 at 18:32):

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

#### Adam Topaz (Jul 16 2022 at 18:33):

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 (Jul 16 2022 at 18:33):

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 (Jul 16 2022 at 18:34):

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

#### Filippo A. E. Nuccio (Jul 16 2022 at 18:34):

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

#### Yaël Dillies (Jul 16 2022 at 18:36):

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 (Jul 16 2022 at 18:37):

yeah probably 20 PR's would be good

#### Damiano Testa (Jul 16 2022 at 18:39):

There could be periodic mathlib spriltze...

#### Filippo A. E. Nuccio (Jul 16 2022 at 18:39):

I would imagine 200, rather...

#### Yaël Dillies (Jul 16 2022 at 18:39):

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

#### Filippo A. E. Nuccio (Jul 16 2022 at 18:41):

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 (Jul 16 2022 at 18:41):

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 (Jul 16 2022 at 18:42):

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 (Jul 16 2022 at 18:42):

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

#### Adam Topaz (Jul 16 2022 at 18:44):

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 (Jul 16 2022 at 18:44):

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 (Jul 16 2022 at 18:45):

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

#### Riccardo Brasca (Jul 16 2022 at 18:49):

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 (Jul 16 2022 at 18:53):

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 (Jul 16 2022 at 19:10):

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 (Jul 16 2022 at 19:22):

Thomas Browning 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 (Jul 16 2022 at 20:18):

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.

I fixed one file

#### Adam Topaz (Jul 16 2022 at 20:37):

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

#### Riccardo Brasca (Jul 16 2022 at 20:40):

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 (Jul 16 2022 at 21:14):

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 (Jul 16 2022 at 21:20):

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 (Jul 16 2022 at 21:53):

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 (Jul 16 2022 at 21:59):

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 (Jul 16 2022 at 22:22):

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

instance : add_group (discrete ℤ) :=


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

#### Peter Scholze (Jul 17 2022 at 05:51):

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 (Jul 17 2022 at 10:11):

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 (Jul 17 2022 at 10:19):

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

#### Yaël Dillies (Jul 17 2022 at 10:19):

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

#### Riccardo Brasca (Jul 17 2022 at 10:32):

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 (Jul 17 2022 at 18:52):

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

#### Riccardo Brasca (Jul 17 2022 at 19:32):

If pid.lean compiles it is enough

#### Violeta Hernández (Jul 17 2022 at 22:25):

I think I see an issue

#### Violeta Hernández (Jul 17 2022 at 22:27):

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

#### Violeta Hernández (Jul 17 2022 at 22:29):

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

#### Riccardo Brasca (Jul 17 2022 at 22:38):

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 (Jul 17 2022 at 22:38):

At least CI will be happy

#### Violeta Hernández (Jul 17 2022 at 22:44):

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

#### Violeta Hernández (Jul 17 2022 at 22:44):

I just added the new enum_iso to the file

#### Violeta Hernández (Jul 17 2022 at 22:45):

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

#### Violeta Hernández (Jul 17 2022 at 22:46):

I hope my ordinal code doesn't cause further trouble

#### Riccardo Brasca (Jul 17 2022 at 22:51):

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 (Jul 18 2022 at 06:43):

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

#### Riccardo Brasca (Jul 18 2022 at 08:36):

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 (Jul 18 2022 at 08:54):

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

#### Floris van Doorn (Jul 18 2022 at 09:02):

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

#### Eric Wieser (Jul 18 2022 at 09:07):

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

#### Riccardo Brasca (Jul 18 2022 at 09:23):

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 (Jul 18 2022 at 09:25):

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 (Jul 18 2022 at 10:22):

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

I lost track...

#### Riccardo Brasca (Jul 18 2022 at 10:23):

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.

Aah, gotcha

#### Riccardo Brasca (Jul 18 2022 at 10:24):

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

#### Andrew Yang (Jul 18 2022 at 10:25):

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 (Jul 18 2022 at 10:26):

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

#### Riccardo Brasca (Jul 18 2022 at 10:27):

I am not working on it.

#### Johan Commelin (Jul 18 2022 at 11:19):

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

#### Ben Toner (Jul 18 2022 at 13:29):

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 (Jul 18 2022 at 13:50):

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.

(This comment was wrong.)

#### Andrew Yang (Jul 18 2022 at 13:58):

bump_may_19 should now compile.

#### Johan Commelin (Jul 18 2022 at 13:58):

I was really scared of the shift-bump.

#### Johan Commelin (Jul 18 2022 at 13:59):

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

This is great!

#### Adam Topaz (Jul 18 2022 at 14:02):

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

#### Yaël Dillies (Jul 18 2022 at 15:10):

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?

#### Riccardo Brasca (Jul 18 2022 at 15:12):

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

#### Riccardo Brasca (Jul 18 2022 at 15:13):

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

#### Riccardo Brasca (Jul 18 2022 at 15:13):

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

#### Yaël Dillies (Jul 18 2022 at 15:17):

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

#### Riccardo Brasca (Jul 18 2022 at 15:18):

Ah sorry, then yes!

#### Riccardo Brasca (Jul 18 2022 at 16:34):

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.

#### Ben Toner (Jul 18 2022 at 20:25):

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 (Jul 18 2022 at 20:26):

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

#### Ben Toner (Jul 18 2022 at 20:28):

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 (Jul 18 2022 at 23:26):

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 (Jul 19 2022 at 01:48):

My understanding is that this build has succeeded?

#### Johan Commelin (Jul 19 2022 at 07:20):

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

#### Johan Commelin (Jul 19 2022 at 07:23):

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 (Jul 19 2022 at 10:21):

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

#### Ben Toner (Jul 19 2022 at 10:37):

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

#### Ben Toner (Jul 19 2022 at 10:41):

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 (Jul 19 2022 at 10:43):

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

#### Johan Commelin (Jul 19 2022 at 10:46):

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

#### Johan Commelin (Jul 19 2022 at 10:51):

I'm building this branch now

Yep

#### Johan Commelin (Jul 19 2022 at 11:20):

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

#### Johan Commelin (Jul 19 2022 at 11:36):

ext_coproducts builds again

#### Johan Commelin (Jul 19 2022 at 11:42):

single_coproducts done

#### Johan Commelin (Jul 19 2022 at 12:20):

Fixed a whole bunch of other files. Still going.

#### Johan Commelin (Jul 19 2022 at 13:42):

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

#### Adam Topaz (Jul 19 2022 at 13:44):

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

#### Johan Commelin (Jul 19 2022 at 14:08):

I have to do something else for ~ 1hr

#### Adam Topaz (Jul 19 2022 at 14:08):

What's the next file that needs fixing?

#### Riccardo Brasca (Jul 19 2022 at 14:09):

QprimeFP is done

#### Riccardo Brasca (Jul 19 2022 at 14:09):

Let me see what happens next

I'm back

#### Johan Commelin (Jul 19 2022 at 14:42):

@Riccardo Brasca How's it looking?

#### Riccardo Brasca (Jul 19 2022 at 14:46):

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

Heat wave?

#### Filippo A. E. Nuccio (Jul 19 2022 at 14:46):

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

#### Filippo A. E. Nuccio (Jul 19 2022 at 14:47):

On which branch are you working, @Riccardo Brasca ?

#### Riccardo Brasca (Jul 19 2022 at 14:53):

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

#### Riccardo Brasca (Jul 19 2022 at 14:53):

The branch is bump_may_19

#### Adam Topaz (Jul 19 2022 at 14:54):

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

#### Riccardo Brasca (Jul 19 2022 at 14:58):

Its projective_resolution.lean: is_zero_iff_forall_zero that it is super slow

#### Johan Commelin (Jul 19 2022 at 15:02):

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

#### Riccardo Brasca (Jul 19 2022 at 15:07):

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

#### Johan Commelin (Jul 19 2022 at 15:12):

Are there { tidy } proofs in there?

#### Johan Commelin (Jul 19 2022 at 15:13):

I had to replace those in projective_resolution_module.lean

#### Riccardo Brasca (Jul 19 2022 at 15:14):

yes, it's their fault

#### Johan Commelin (Jul 19 2022 at 15:14):

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

#### Adam Topaz (Jul 19 2022 at 15:15):

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 (Jul 19 2022 at 15:15):

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

#### Johan Commelin (Jul 19 2022 at 15:15):

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

#### Adam Topaz (Jul 19 2022 at 15:16):

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

#### Filippo A. E. Nuccio (Jul 19 2022 at 15:16):

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?

it's done

#### Riccardo Brasca (Jul 19 2022 at 15:17):

Note that minibump is completely superseded by the other branch

#### Filippo A. E. Nuccio (Jul 19 2022 at 15:18):

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

#### Johan Commelin (Jul 19 2022 at 15:19):

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

#### Johan Commelin (Jul 19 2022 at 15:19):

And your LTE oleans will also change

#### Johan Commelin (Jul 19 2022 at 15:19):

So I'm not surprised that this causes headaches

#### Filippo A. E. Nuccio (Jul 19 2022 at 15:20):

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

#### Johan Commelin (Jul 19 2022 at 15:21):

Riccardo Brasca said:

it's done

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

The file

#### Riccardo Brasca (Jul 19 2022 at 15:21):

Looking for the next error

#### Filippo A. E. Nuccio (Jul 19 2022 at 15:27):

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 (Jul 19 2022 at 15:29):

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

#### Riccardo Brasca (Jul 19 2022 at 15:30):

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

at least not yet

#### Filippo A. E. Nuccio (Jul 19 2022 at 15:30):

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

#### Riccardo Brasca (Jul 19 2022 at 15:31):

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

#### Filippo A. E. Nuccio (Jul 19 2022 at 15:33):

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

#### Riccardo Brasca (Jul 19 2022 at 15:36):

The bump compiles for me.

Nice!

#### Johan Commelin (Jul 19 2022 at 16:51):

Let's hope it passes CI!

Mmm, CI failed

#### Riccardo Brasca (Jul 19 2022 at 18:49):

With a mysterious error

#### Riccardo Brasca (Jul 19 2022 at 18:49):

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

#### Riccardo Brasca (Jul 19 2022 at 18:50):

I've relaunched it

#### Johan Commelin (Jul 19 2022 at 19:30):

Hmm, it got an error again

#### Adam Topaz (Jul 19 2022 at 19:30):

It looks like it's still building?

#### Johan Commelin (Jul 19 2022 at 19:31):

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

#### Adam Topaz (Jul 19 2022 at 19:31):

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

#### Johan Commelin (Jul 19 2022 at 19:31):

Ooh, that's a different run

Ooh wait... lol

#### Johan Commelin (Jul 19 2022 at 19:32):

I should learn to read messages in order.

#### Ben Toner (Jul 19 2022 at 20:34):

date: extra operand ‘%T’
Starting build at


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 (Jul 19 2022 at 20:39):

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 (Jul 19 2022 at 21:19):

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 (Jul 19 2022 at 21:21):

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

#### Mauricio Collares (Jul 19 2022 at 21:24):

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/pullbacks.lean:123:2: error: (deterministic) timeout
/home/collares/lean-liquid/src/for_mathlib/pullbacks.lean:62:41: error: (deterministic) timeout
...


#### Adam Topaz (Jul 19 2022 at 21:26):

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 (Jul 19 2022 at 21:27):

Where does that python script come from?

#### Filippo A. E. Nuccio (Jul 19 2022 at 21:27):

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 (Jul 19 2022 at 21:28):

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 (Jul 19 2022 at 21:29):

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

#### Filippo A. E. Nuccio (Jul 19 2022 at 21:30):

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

#### Adam Topaz (Jul 19 2022 at 21:30):

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 (Jul 19 2022 at 21:32):

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 (Jul 19 2022 at 21:34):

Where does that python script come from?

Which Python script? This one?

#### Adam Topaz (Jul 19 2022 at 21:35):

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

#### Mauricio Collares (Jul 19 2022 at 21:37):

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).

(deleted)

#### Adam Topaz (Jul 19 2022 at 21:45):

@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 (Jul 19 2022 at 21:47):

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 (Jul 19 2022 at 21:48):

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

#### Adam Topaz (Jul 19 2022 at 22:46):

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 (Jul 19 2022 at 22:50):

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 (Jul 19 2022 at 23:38):

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

#### Adam Topaz (Jul 20 2022 at 01:27):

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

#### Johan Commelin (Jul 20 2022 at 06:16):

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

#### Johan Commelin (Jul 20 2022 at 07:10):

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 (Jul 20 2022 at 07:32):

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

#### Johan Commelin (Jul 20 2022 at 08:48):

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

#### Johan Commelin (Jul 20 2022 at 08:52):

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

#### Johan Commelin (Jul 20 2022 at 08:53):

It seems to be hanging on that step?

#### Johan Commelin (Jul 20 2022 at 08:54):

I'm too impatient. It worked

#### Riccardo Brasca (Jul 20 2022 at 09:59):

Do we know why it is so slower?

Quick, merge it!

It's merged.

#### Riccardo Brasca (Jul 20 2022 at 12:54):

Let's try one week later.

#### Johan Commelin (Jul 20 2022 at 13:14):

Maybe we should take slightly bigger steps now?

#### Johan Commelin (Jul 20 2022 at 13:14):

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

#### Johan Commelin (Jul 20 2022 at 14:46):

@Riccardo Brasca Did you already start a new branch?

#### Riccardo Brasca (Jul 20 2022 at 14:47):

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

#### Johan Commelin (Jul 20 2022 at 14:47):

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

#### Riccardo Brasca (Jul 20 2022 at 14:49):

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

#### Riccardo Brasca (Jul 20 2022 at 16:05):

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

#### Johan Commelin (Jul 20 2022 at 17:30):

Oww, that one seems pretty nasty.

#### Adam Topaz (Jul 20 2022 at 17:31):

What's the mathlib change that makes this bad?

Je ne sais pas

#### Johan Commelin (Jul 20 2022 at 17:33):

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

#### Riccardo Brasca (Jul 20 2022 at 17:39):

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 (Jul 20 2022 at 17:41):

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

#### Johan Commelin (Jul 20 2022 at 17:43):

I think fetch_olean_cache should now work!

#### Adam Topaz (Jul 20 2022 at 17:44):

it's doing something!

#### Adam Topaz (Jul 20 2022 at 18:08):

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 (Jul 20 2022 at 18:09):

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 (Jul 20 2022 at 18:10):

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 (Jul 20 2022 at 18:14):

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 (Jul 20 2022 at 18:17):

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

#### Johan Commelin (Jul 20 2022 at 18:18):

And thanks for debugging!

#### Adam Topaz (Jul 20 2022 at 18:19):

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 (Jul 20 2022 at 18:21):

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

#### Johan Commelin (Jul 20 2022 at 18:22):

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

#### Riccardo Brasca (Jul 20 2022 at 18:41):

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

#### Riccardo Brasca (Jul 20 2022 at 19:17):

It should compile now

#### Johan Commelin (Jul 20 2022 at 19:23):

Ooh, that went fast! Cool!

#### Johan Commelin (Jul 21 2022 at 06:33):

I'm starting on bump_jul_03

#### Riccardo Brasca (Jul 21 2022 at 10:09):

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

#### Johan Commelin (Jul 21 2022 at 11:24):

Sorry, I was gone for lunch

#### Johan Commelin (Jul 21 2022 at 11:25):

Now I'm back. How about you?

#### Riccardo Brasca (Jul 21 2022 at 11:25):

Let me push what I've done.

#### Riccardo Brasca (Jul 21 2022 at 11:31):

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

#### Riccardo Brasca (Jul 21 2022 at 11:42):

OK, it should be done and pushed.

#### Riccardo Brasca (Jul 21 2022 at 11:42):

I am stopping for at least half an hour

#### Johan Commelin (Jul 21 2022 at 11:47):

Okido, I'll take over

#### Johan Commelin (Jul 21 2022 at 12:32):

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 (Jul 21 2022 at 12:56):

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

#### Johan Commelin (Jul 21 2022 at 13:11):

Qprime_isoms.lean is done

It's done!

#### Johan Commelin (Jul 21 2022 at 13:41):

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

#### Johan Commelin (Jul 21 2022 at 13:44):

I'm starting on bump-universes

#### Adam Topaz (Jul 21 2022 at 14:57):

Can someone reproduce the following?

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


And lean starts compiling mathlib.

#### Adam Topaz (Jul 21 2022 at 15:37):

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 (Jul 21 2022 at 16:25):

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 (Jul 21 2022 at 17:04):

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 (Jul 21 2022 at 17:05):

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 (Jul 21 2022 at 17:12):

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

#### Johan Commelin (Jul 21 2022 at 17:13):

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

#### Johan Commelin (Jul 21 2022 at 17:14):

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 (Jul 21 2022 at 17:16):

yeah I found preserves_finite_limits_of_preserves_finite_limits_of_size

#### Adam Topaz (Jul 21 2022 at 17:16):

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

#### Johan Commelin (Jul 21 2022 at 17:31):

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

#### Adam Topaz (Jul 21 2022 at 17:35):

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

#### Johan Commelin (Jul 21 2022 at 17:41):

Ouch! That's annoying.

#### Adam Topaz (Jul 21 2022 at 17:43):

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

#### Adam Topaz (Jul 21 2022 at 17:58):

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

#### Andrew Yang (Jul 21 2022 at 19:09):

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

#### Andrew Yang (Jul 21 2022 at 19:13):

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 (Jul 21 2022 at 19:27):

@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 (Jul 21 2022 at 20:13):

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 (Jul 22 2022 at 01:02):

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 (Jul 22 2022 at 06:58):

I fixed one more file

#### Johan Commelin (Jul 22 2022 at 06:59):

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

#### Johan Commelin (Jul 22 2022 at 07:13):

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

#### Johan Commelin (Jul 22 2022 at 08:10):

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

#### Riccardo Brasca (Jul 22 2022 at 08:30):

I am having a look

#### Riccardo Brasca (Jul 22 2022 at 09:03):

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

#### Andrew Yang (Jul 22 2022 at 09:05):

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

#### Johan Commelin (Jul 22 2022 at 12:20):

@Andrew Yang did you already fix ab4.lean?

#### Andrew Yang (Jul 22 2022 at 12:20):

Yes. I can push what I have now.

#### Johan Commelin (Jul 22 2022 at 12:21):

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

#### Johan Commelin (Jul 22 2022 at 12:21):

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

#### Andrew Yang (Jul 22 2022 at 12:22):

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

#### Johan Commelin (Jul 22 2022 at 12:54):

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 (Jul 22 2022 at 12:54):

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

#### Andrew Yang (Jul 22 2022 at 13:12):

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

#### Johan Commelin (Jul 22 2022 at 13:13):

Thanks, I'll try.

#### Johan Commelin (Jul 22 2022 at 13:34):

That worked. I fixed 3 files and pushed.

#### Johan Commelin (Jul 22 2022 at 13:55):

condensed/filtered_colimits seems to be quite a nightmare.

#### Johan Commelin (Jul 22 2022 at 13:55):

@Andrew Yang how is the tensor file going?

#### Andrew Yang (Jul 22 2022 at 13:57):

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 (Jul 22 2022 at 15:10):

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

#### Johan Commelin (Jul 22 2022 at 15:41):

I'm working on condensed/acyclic

#### Johan Commelin (Jul 22 2022 at 16:05):

done, and now I need to go

#### Adam Topaz (Jul 22 2022 at 20:20):

I fixed condesed/filtered_colimits.

What a mess!

#### Johan Commelin (Jul 22 2022 at 20:27):

Wow! I had 3 attempts that all failed

#### Adam Topaz (Jul 22 2022 at 23:12):

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 (Jul 23 2022 at 00:30):

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 (Jul 23 2022 at 01:55):

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

#### Adam Topaz (Jul 23 2022 at 02:01):

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 (Jul 25 2022 at 10:52):

I'm starting the mathlib bump to mathlib master.

#### Johan Commelin (Jul 25 2022 at 11:10):

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

#### Yaël Dillies (Jul 25 2022 at 11:22):

Is pseudo_normed_group pseudo in the same sense as pseudo_metric_space?

#### Andrew Yang (Jul 25 2022 at 11:27):

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

#### Johan Commelin (Jul 25 2022 at 14:19):

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

#### Johan Commelin (Jul 25 2022 at 14:20):

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 (Jul 25 2022 at 14:30):

I'm working on making thm95 error-free.

#### Johan Commelin (Jul 25 2022 at 14:55):

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

#### Johan Commelin (Jul 25 2022 at 16:44):

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 (Jul 25 2022 at 16:59):

condensed/ seems to be error-free

#### Andrew Yang (Jul 25 2022 at 17:33):

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

I just did

#### Johan Commelin (Jul 25 2022 at 17:41):

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

#### Johan Commelin (Jul 25 2022 at 17:54):

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

#### Johan Commelin (Jul 25 2022 at 18:19):

One linting error. I pushed a fix.

#### Johan Commelin (Jul 25 2022 at 18:36):

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

#### Adam Topaz (Jul 25 2022 at 18:38):

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

#### Yaël Dillies (Jul 25 2022 at 18:38):

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

#### Eric Wieser (Jul 26 2022 at 06:21):

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

#### Riccardo Brasca (Aug 08 2022 at 19:11):

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 (Aug 08 2022 at 19:12):

yeah that docstring is wrong

#### Riccardo Brasca (Aug 08 2022 at 19:13):

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

#### Riccardo Brasca (Aug 08 2022 at 19:14):

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 (Aug 08 2022 at 19:15):

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

#### Adam Topaz (Aug 08 2022 at 19:16):

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

#### Adam Topaz (Aug 08 2022 at 19:17):

where is this prev_eq_zero' used?

#### Adam Topaz (Aug 08 2022 at 19:20):

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 (Aug 08 2022 at 19:21):

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

#### Riccardo Brasca (Aug 08 2022 at 19:22):

#15940 for the modifications not done in the previous PR

#### Johan Commelin (Aug 09 2022 at 06:31):

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 (Aug 09 2022 at 15:22):

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

#### Johan Commelin (Aug 09 2022 at 15:23):

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 (Aug 09 2022 at 15:23):

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

#### Kevin Buzzard (Aug 09 2022 at 15:55):

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 (Aug 09 2022 at 15:56):

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 (Aug 09 2022 at 15:57):

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

#### Johan Commelin (Aug 09 2022 at 16:01):

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

#### Kevin Buzzard (Aug 09 2022 at 16:09):

Does the proof not work at your end?

#### Johan Commelin (Aug 09 2022 at 16:26):

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

#### Johan Commelin (Aug 09 2022 at 16:27):

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

#### Johan Commelin (Aug 09 2022 at 16:27):

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

#### Johan Commelin (Aug 09 2022 at 16:29):

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 (Aug 09 2022 at 16:30):

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 (Aug 09 2022 at 16:33):

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 (Aug 09 2022 at 16:34):

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

#### Johan Commelin (Aug 09 2022 at 16:34):

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 (Aug 09 2022 at 16:39):

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 (Aug 09 2022 at 16:59):

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

and what file?

#### Johan Commelin (Aug 09 2022 at 17:00):

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 (Aug 09 2022 at 17:23):

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

$leanproject get-mathlib-cache SHA b'ec818836889c031d4035c928bcbc638af5fbd736' could not be resolved, git returned: b'ec818836889c031d4035c928bcbc638af5fbd736 missing'  #### Adam Topaz (Aug 09 2022 at 17:48): on this branch.... #### Adam Topaz (Aug 09 2022 at 18:06): The file for_mathlib/homological_complex_map_d_from_d seems broken on my end as well... can someone reproduce? #### Adam Topaz (Aug 09 2022 at 18:17): 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 (Aug 09 2022 at 18:17): I had to do things manually with git in the _target folder. #### Adam Topaz (Aug 09 2022 at 18:56): 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 (Aug 09 2022 at 18:57): here embed_iso is def embed_iso (i : ι) : ((embed e).obj X).X (e.f i) ≅ X.X i :=  #### Adam Topaz (Aug 09 2022 at 19:01): Can we redefine the stuff around embeddings so that we get better defeqs? Is it worth it? #### Joël Riou (Aug 09 2022 at 19:36): 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 (Aug 09 2022 at 19:40): And I guess that checking that it is an isom involves 4 cases? #### Johan Commelin (Aug 09 2022 at 19:41): Depending on whether prev/next exists or not. #### Joël Riou (Aug 09 2022 at 19:56): 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 (Aug 09 2022 at 19:57): 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 (Aug 09 2022 at 20:05): Maybe we should do that refactor of mathlib before bothering with this bump? #### Adam Topaz (Aug 09 2022 at 20:06): Well I though we're not all in agreement that this was the way to go. #### Johan Commelin (Aug 09 2022 at 20:07): I'll mull over it again in my sleep tonight (-; #### Joël Riou (Aug 09 2022 at 20:44): 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 (Aug 09 2022 at 20:49): 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 (Aug 10 2022 at 04:52): 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 (Aug 10 2022 at 07:22): 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 (Aug 10 2022 at 08:39): 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 (Aug 10 2022 at 11:30): 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 (Aug 10 2022 at 11:55): 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 (Aug 10 2022 at 12:59): 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 (Aug 10 2022 at 13:30): Thanks! #### Kevin Buzzard (Aug 10 2022 at 14:36): 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 (Aug 10 2022 at 14:43): 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 (Aug 10 2022 at 16:46): 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 (Aug 10 2022 at 16:57): I think it's an important point to keep spectral sequences in mind! #### Kevin Buzzard (Aug 10 2022 at 16:58): Or have they all been replaced with derived functors nowadays? Or even the derived infinity category? #### Adam Topaz (Aug 10 2022 at 16:59): 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 (Aug 10 2022 at 17:00): 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 (Aug 10 2022 at 17:00): We have to have the differentials everywhere for the same reason we ended up having them everywhere on the E1 page #### Kevin Buzzard (Aug 10 2022 at 17:01): Actually we only had arbitrary horizontal ones I guess #### Adam Topaz (Aug 10 2022 at 17:01): Aside: should we make a separate homology stream to discuss this stuff? #### Johan Commelin (Aug 10 2022 at 17:02): Hmm, maybe 3 or 4 topics in #maths also works? But ey, streams are cheap. I don't care (-; #### Adam Topaz (Aug 10 2022 at 17:02): The maths stream is fine, but it's easy for things to get lost in there. #### Adam Topaz (Aug 10 2022 at 17:03): I can do it when I get back to my computer, if @Johan Commelin doesn't beat me to it :wink: #### Johan Commelin (Aug 10 2022 at 17:05): #### Johan Commelin (Aug 12 2022 at 07:41): 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 (Aug 13 2022 at 20:08): Bah, this bump is quite annoying. #### Johan Commelin (Aug 17 2022 at 18:47): I made it to 50% of mapping_cone.lean #### Johan Commelin (Aug 29 2022 at 08:47): 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 (Aug 30 2022 at 09:57): DB allowed me to travel to my office today. mapping_cone.lean has been fixed. db_logo.jpg #### Johan Commelin (Aug 30 2022 at 16:55): Should compile now: https://github.com/leanprover-community/lean-liquid/pull/122 #### Kevin Buzzard (Aug 30 2022 at 16:56): Nice work! #### Johan Commelin (Aug 30 2022 at 16:58): #### Kevin Buzzard (Aug 30 2022 at 17:00): 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 (Aug 30 2022 at 17:04): Oh does that mean we can now bump to nnrat? #### Johan Commelin (Aug 30 2022 at 17:07): Almost! Still need to have CI give the green flag on this PR. #### Johan Commelin (Aug 30 2022 at 21:07): It builds, but the linter complains: https://github.com/leanprover-community/lean-liquid/runs/8101380577?check_suite_focus=true #### Johan Commelin (Aug 30 2022 at 21:07): I'm done for the day though #### Riccardo Brasca (Aug 30 2022 at 22:12): I am fixing the linter. #### Riccardo Brasca (Aug 31 2022 at 03:14): It's merged! #### Johan Commelin (Aug 31 2022 at 05:13): @Riccardo Brasca thanks so much #### Yaël Dillies (Aug 31 2022 at 06:22): Let me start a new bump then! #### Johan Commelin (Aug 31 2022 at 06:26): I can join you in ~ 20 mins. #### Johan Commelin (Aug 31 2022 at 07:41): Somehow mapping_cone.lean is now in the deps of liquid.lean. #### Johan Commelin (Aug 31 2022 at 08:01): @Yaël Dillies fixed Gordan.lean. #### Johan Commelin (Aug 31 2022 at 08:01): Now liquid.lean compiles. I'll work on the rest of the bump. #### Johan Commelin (Aug 31 2022 at 08:57): It compiles locally. This bump was easy-peasy-lemon-squeezy. :smiley: #### Johan Commelin (Aug 31 2022 at 11:02): And it is merged! #### Kevin Buzzard (Aug 31 2022 at 15:38): 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 (Sep 25 2022 at 04:03): @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 (Sep 25 2022 at 20:16): 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 (Sep 25 2022 at 21:44): If it's complicated we can just change the name of the LTE version #### Johan Commelin (Sep 26 2022 at 05:18): I think that's maybe the easy fix that we should go for in this mathlib bump. #### Johan Commelin (Sep 26 2022 at 05:18): Then Yaël can refactor whenever they want/have time. #### Johan Commelin (Sep 26 2022 at 06:10): 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 (Sep 26 2022 at 06:25): @Adam Topaz @Joël Riou @Andrew Yang do you recognize a change in category theory that might have caused this? #### Adam Topaz (Sep 26 2022 at 17:00): 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}


#### Adam Topaz (Sep 26 2022 at 17:02):

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

#### Riccardo Brasca (Sep 26 2022 at 17:06):

#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 (Sep 26 2022 at 17:07):

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

#### Adam Topaz (Sep 26 2022 at 17:07):

but of course we should do it.

#### Adam Topaz (Sep 26 2022 at 17:08):

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 funext, intros P, apply funext, intros Q,
dsimp,
apply funext, intros f, apply funext, intros g,
refl,
end


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

#### Adam Topaz (Sep 26 2022 at 19:31):

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 (Sep 26 2022 at 22:02):

I fixed condensed/acyclic.lean in this branch.

#### Adam Topaz (Sep 26 2022 at 22:05):

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 (Sep 26 2022 at 22:06):

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 (Sep 26 2022 at 22:06):

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

#### Adam Topaz (Sep 26 2022 at 22:06):

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

#### Johan Commelin (Sep 27 2022 at 02:51):

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

#### Johan Commelin (Sep 27 2022 at 09:43):

Thanks for finishing the bump!

Last updated: Jan 31 2023 at 21:29 UTC