Zulip Chat Archive

Stream: condensed mathematics

Topic: The elephant in the room


view this post on Zulip Adam Topaz (Jul 16 2022 at 12:28):

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

view this post on Zulip Riccardo Brasca (Jul 16 2022 at 12:32):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Jul 16 2022 at 12:34):

Right that was my position with perfectoid

view this post on Zulip Kevin Buzzard (Jul 16 2022 at 12:34):

I didn't want it to become an albatross.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Filippo A. E. Nuccio (Jul 16 2022 at 12:35):

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

view this post on Zulip 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.

view this post on Zulip Riccardo Brasca (Jul 16 2022 at 12:36):

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

view this post on Zulip Adam Topaz (Jul 16 2022 at 12:36):

Pretty old

view this post on Zulip Adam Topaz (Jul 16 2022 at 12:37):

In mathlib terms at least

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Riccardo Brasca (Jul 16 2022 at 12:38):

May 12th, not that old

view this post on Zulip Riccardo Brasca (Jul 16 2022 at 12:54):

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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Jul 16 2022 at 12:59):

in case it helps!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Yaël Dillies (Jul 16 2022 at 16:02):

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

view this post on Zulip Riccardo Brasca (Jul 16 2022 at 16:02):

Yes, in the minibump branch

view this post on Zulip Riccardo Brasca (Jul 16 2022 at 16:03):

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

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Jul 16 2022 at 18:26):

how big is LTE?

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jul 16 2022 at 18:26):

that is quite a number of lines

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Jul 16 2022 at 18:27):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Yaël Dillies (Jul 16 2022 at 18:28):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Adam Topaz (Jul 16 2022 at 18:30):

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

view this post on Zulip 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.

view this post on Zulip Thomas Browning (Jul 16 2022 at 18:31):

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?

view this post on Zulip Filippo A. E. Nuccio (Jul 16 2022 at 18:31):

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

view this post on Zulip 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.

view this post on Zulip 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 ;)

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Filippo A. E. Nuccio (Jul 16 2022 at 18:34):

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

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Jul 16 2022 at 18:37):

yeah probably 20 PR's would be good

view this post on Zulip Damiano Testa (Jul 16 2022 at 18:39):

There could be periodic mathlib spriltze...

view this post on Zulip Filippo A. E. Nuccio (Jul 16 2022 at 18:39):

I would imagine 200, rather...

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Riccardo Brasca (Jul 16 2022 at 18:42):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.).

view this post on Zulip Peter Scholze (Jul 16 2022 at 19:22):

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

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Jul 16 2022 at 20:36):

I fixed one file

view this post on Zulip Adam Topaz (Jul 16 2022 at 20:37):

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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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 MR(S)\mathcal{M}_{\mathbb{R}}(S)).

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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 ) :=
discrete_equiv.add_group

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

view this post on Zulip 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...)

view this post on Zulip 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!

view this post on Zulip Yaël Dillies (Jul 17 2022 at 10:19):

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

view this post on Zulip Yaël Dillies (Jul 17 2022 at 10:19):

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

view this post on Zulip 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.

view this post on Zulip Violeta Hernández (Jul 17 2022 at 18:52):

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

view this post on Zulip Riccardo Brasca (Jul 17 2022 at 19:32):

If pid.lean compiles it is enough

view this post on Zulip Violeta Hernández (Jul 17 2022 at 22:25):

I think I see an issue

view this post on Zulip Violeta Hernández (Jul 17 2022 at 22:27):

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

view this post on Zulip Violeta Hernández (Jul 17 2022 at 22:29):

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

view this post on Zulip 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)

view this post on Zulip Riccardo Brasca (Jul 17 2022 at 22:38):

At least CI will be happy

view this post on Zulip Violeta Hernández (Jul 17 2022 at 22:44):

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

view this post on Zulip Violeta Hernández (Jul 17 2022 at 22:44):

I just added the new enum_iso to the file

view this post on Zulip Violeta Hernández (Jul 17 2022 at 22:45):

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

view this post on Zulip Violeta Hernández (Jul 17 2022 at 22:46):

I hope my ordinal code doesn't cause further trouble

view this post on Zulip 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!

view this post on Zulip Johan Commelin (Jul 18 2022 at 06:43):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Jul 18 2022 at 09:07):

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

view this post on Zulip 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

view this post on Zulip 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".

view this post on Zulip Johan Commelin (Jul 18 2022 at 10:22):

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

view this post on Zulip Johan Commelin (Jul 18 2022 at 10:22):

I lost track...

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jul 18 2022 at 10:23):

Aah, gotcha

view this post on Zulip Riccardo Brasca (Jul 18 2022 at 10:24):

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

view this post on Zulip 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?

view this post on Zulip Andrew Yang (Jul 18 2022 at 10:26):

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

view this post on Zulip Riccardo Brasca (Jul 18 2022 at 10:27):

I am not working on it.

view this post on Zulip Johan Commelin (Jul 18 2022 at 11:19):

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

view this post on Zulip 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.

view this post on Zulip 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.

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

(This comment was wrong.)

view this post on Zulip Andrew Yang (Jul 18 2022 at 13:58):

bump_may_19 should now compile.

view this post on Zulip Johan Commelin (Jul 18 2022 at 13:58):

Wow! That's really helpful!

view this post on Zulip Johan Commelin (Jul 18 2022 at 13:58):

I was really scared of the shift-bump.

view this post on Zulip Johan Commelin (Jul 18 2022 at 13:59):

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

view this post on Zulip Adam Topaz (Jul 18 2022 at 14:01):

This is great!

view this post on Zulip Ben Toner (Jul 18 2022 at 14:01):

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

view this post on Zulip 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.

view this post on Zulip Riccardo Brasca (Jul 18 2022 at 14:21):

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

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jul 18 2022 at 15:11):

Yes please!

view this post on Zulip Riccardo Brasca (Jul 18 2022 at 15:12):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Riccardo Brasca (Jul 18 2022 at 15:18):

Ah sorry, then yes!

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jul 18 2022 at 18:26):

Thanks for all your help

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Jul 18 2022 at 20:26):

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

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Kevin Buzzard (Jul 19 2022 at 01:48):

My understanding is that this build has succeeded?

view this post on Zulip Johan Commelin (Jul 19 2022 at 07:20):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jul 19 2022 at 10:21):

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

view this post on Zulip Ben Toner (Jul 19 2022 at 10:37):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jul 19 2022 at 10:51):

I'm building this branch now

view this post on Zulip Riccardo Brasca (Jul 19 2022 at 11:19):

Yep

view this post on Zulip Johan Commelin (Jul 19 2022 at 11:20):

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

view this post on Zulip Johan Commelin (Jul 19 2022 at 11:36):

ext_coproducts builds again

view this post on Zulip Johan Commelin (Jul 19 2022 at 11:42):

single_coproducts done

view this post on Zulip Johan Commelin (Jul 19 2022 at 12:20):

Fixed a whole bunch of other files. Still going.

view this post on Zulip Johan Commelin (Jul 19 2022 at 13:42):

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

view this post on Zulip Adam Topaz (Jul 19 2022 at 13:44):

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

view this post on Zulip Johan Commelin (Jul 19 2022 at 14:08):

I have to do something else for ~ 1hr

view this post on Zulip Adam Topaz (Jul 19 2022 at 14:08):

What's the next file that needs fixing?

view this post on Zulip Riccardo Brasca (Jul 19 2022 at 14:09):

QprimeFP is done

view this post on Zulip Riccardo Brasca (Jul 19 2022 at 14:09):

Let me see what happens next

view this post on Zulip Johan Commelin (Jul 19 2022 at 14:34):

I'm back

view this post on Zulip Johan Commelin (Jul 19 2022 at 14:42):

@Riccardo Brasca How's it looking?

view this post on Zulip Riccardo Brasca (Jul 19 2022 at 14:46):

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

view this post on Zulip Johan Commelin (Jul 19 2022 at 14:46):

Heat wave?

view this post on Zulip Filippo A. E. Nuccio (Jul 19 2022 at 14:46):

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

view this post on Zulip Filippo A. E. Nuccio (Jul 19 2022 at 14:47):

On which branch are you working, @Riccardo Brasca ?

view this post on Zulip Riccardo Brasca (Jul 19 2022 at 14:53):

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

view this post on Zulip Riccardo Brasca (Jul 19 2022 at 14:53):

The branch is bump_may_19

view this post on Zulip Adam Topaz (Jul 19 2022 at 14:54):

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

view this post on Zulip Riccardo Brasca (Jul 19 2022 at 14:58):

Its projective_resolution.lean: is_zero_iff_forall_zero that it is super slow

view this post on Zulip Johan Commelin (Jul 19 2022 at 15:02):

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

view this post on Zulip Riccardo Brasca (Jul 19 2022 at 15:07):

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

view this post on Zulip Johan Commelin (Jul 19 2022 at 15:12):

Are there { tidy } proofs in there?

view this post on Zulip Johan Commelin (Jul 19 2022 at 15:13):

I had to replace those in projective_resolution_module.lean

view this post on Zulip Riccardo Brasca (Jul 19 2022 at 15:14):

yes, it's their fault

view this post on Zulip Johan Commelin (Jul 19 2022 at 15:14):

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

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Jul 19 2022 at 15:15):

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

view this post on Zulip Johan Commelin (Jul 19 2022 at 15:15):

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

view this post on Zulip Adam Topaz (Jul 19 2022 at 15:16):

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

view this post on Zulip 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?

view this post on Zulip Riccardo Brasca (Jul 19 2022 at 15:16):

it's done

view this post on Zulip Riccardo Brasca (Jul 19 2022 at 15:17):

Note that minibump is completely superseded by the other branch

view this post on Zulip Filippo A. E. Nuccio (Jul 19 2022 at 15:18):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jul 19 2022 at 15:19):

And your LTE oleans will also change

view this post on Zulip Johan Commelin (Jul 19 2022 at 15:19):

So I'm not surprised that this causes headaches

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jul 19 2022 at 15:21):

Riccardo Brasca said:

it's done

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

view this post on Zulip Riccardo Brasca (Jul 19 2022 at 15:21):

The file

view this post on Zulip Riccardo Brasca (Jul 19 2022 at 15:21):

Looking for the next error

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Riccardo Brasca (Jul 19 2022 at 15:30):

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

view this post on Zulip Riccardo Brasca (Jul 19 2022 at 15:30):

at least not yet

view this post on Zulip Filippo A. E. Nuccio (Jul 19 2022 at 15:30):

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

view this post on Zulip Riccardo Brasca (Jul 19 2022 at 15:31):

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

view this post on Zulip 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:

view this post on Zulip Riccardo Brasca (Jul 19 2022 at 15:36):

The bump compiles for me.

view this post on Zulip Johan Commelin (Jul 19 2022 at 16:50):

Nice!

view this post on Zulip Johan Commelin (Jul 19 2022 at 16:51):

Let's hope it passes CI!

view this post on Zulip Riccardo Brasca (Jul 19 2022 at 18:49):

Mmm, CI failed

view this post on Zulip Riccardo Brasca (Jul 19 2022 at 18:49):

With a mysterious error

view this post on Zulip Riccardo Brasca (Jul 19 2022 at 18:49):

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

view this post on Zulip Riccardo Brasca (Jul 19 2022 at 18:50):

I've relaunched it

view this post on Zulip Johan Commelin (Jul 19 2022 at 19:30):

Hmm, it got an error again

view this post on Zulip Adam Topaz (Jul 19 2022 at 19:30):

It looks like it's still building?

view this post on Zulip Johan Commelin (Jul 19 2022 at 19:31):

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

view this post on Zulip Adam Topaz (Jul 19 2022 at 19:31):

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

view this post on Zulip Johan Commelin (Jul 19 2022 at 19:31):

Ooh, that's a different run

view this post on Zulip Johan Commelin (Jul 19 2022 at 19:31):

Ooh wait... lol

view this post on Zulip Johan Commelin (Jul 19 2022 at 19:32):

I should learn to read messages in order.

view this post on Zulip Ben Toner (Jul 19 2022 at 20:34):

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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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/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
...

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Jul 19 2022 at 21:27):

Where does that python script come from?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 :)

view this post on Zulip 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.

view this post on Zulip Ben Toner (Jul 19 2022 at 21:34):

Adam Topaz said:

Where does that python script come from?

Which Python script? This one?

view this post on Zulip Adam Topaz (Jul 19 2022 at 21:35):

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

view this post on Zulip 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).

view this post on Zulip Mauricio Collares (Jul 19 2022 at 21:44):

(deleted)

view this post on Zulip 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 !)

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Jul 19 2022 at 21:48):

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

view this post on Zulip 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!

view this post on Zulip 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!

view this post on Zulip Ben Toner (Jul 19 2022 at 23:38):

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

view this post on Zulip Adam Topaz (Jul 20 2022 at 01:27):

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

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip Johan Commelin (Jul 20 2022 at 07:32):

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

view this post on Zulip Johan Commelin (Jul 20 2022 at 07:33):

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

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jul 20 2022 at 08:53):

It seems to be hanging on that step?

view this post on Zulip Johan Commelin (Jul 20 2022 at 08:54):

I'm too impatient. It worked

view this post on Zulip Riccardo Brasca (Jul 20 2022 at 09:59):

Do we know why it is so slower?

view this post on Zulip Riccardo Brasca (Jul 20 2022 at 10:08):

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

view this post on Zulip Eric Wieser (Jul 20 2022 at 10:41):

Quick, merge it!

view this post on Zulip Riccardo Brasca (Jul 20 2022 at 12:51):

It's merged.

view this post on Zulip Riccardo Brasca (Jul 20 2022 at 12:54):

Let's try one week later.

view this post on Zulip Johan Commelin (Jul 20 2022 at 13:14):

Maybe we should take slightly bigger steps now?

view this post on Zulip Johan Commelin (Jul 20 2022 at 13:14):

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

view this post on Zulip Johan Commelin (Jul 20 2022 at 14:46):

@Riccardo Brasca Did you already start a new branch?

view this post on Zulip Riccardo Brasca (Jul 20 2022 at 14:47):

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

view this post on Zulip Johan Commelin (Jul 20 2022 at 14:47):

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

view this post on Zulip Riccardo Brasca (Jul 20 2022 at 14:49):

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

view this post on Zulip Riccardo Brasca (Jul 20 2022 at 16:05):

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

view this post on Zulip Johan Commelin (Jul 20 2022 at 17:30):

Oww, that one seems pretty nasty.

view this post on Zulip Adam Topaz (Jul 20 2022 at 17:31):

What's the mathlib change that makes this bad?

view this post on Zulip Johan Commelin (Jul 20 2022 at 17:32):

Je ne sais pas

view this post on Zulip 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

view this post on Zulip Riccardo Brasca (Jul 20 2022 at 17:39):

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?

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jul 20 2022 at 17:43):

I think fetch_olean_cache should now work!

view this post on Zulip Adam Topaz (Jul 20 2022 at 17:44):

it's doing something!

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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 :)

view this post on Zulip Johan Commelin (Jul 20 2022 at 18:18):

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

view this post on Zulip Johan Commelin (Jul 20 2022 at 18:18):

And thanks for debugging!

view this post on Zulip 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,

view this post on Zulip Adam Topaz (Jul 20 2022 at 18:21):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Riccardo Brasca (Jul 20 2022 at 19:17):

It should compile now

view this post on Zulip Johan Commelin (Jul 20 2022 at 19:23):

Ooh, that went fast! Cool!

view this post on Zulip Johan Commelin (Jul 21 2022 at 06:33):

I'm starting on bump_jul_03

view this post on Zulip Riccardo Brasca (Jul 21 2022 at 10:09):

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

view this post on Zulip Johan Commelin (Jul 21 2022 at 11:24):

Sorry, I was gone for lunch

view this post on Zulip Johan Commelin (Jul 21 2022 at 11:25):

Now I'm back. How about you?

view this post on Zulip Riccardo Brasca (Jul 21 2022 at 11:25):

Let me push what I've done.

view this post on Zulip 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.

view this post on Zulip Riccardo Brasca (Jul 21 2022 at 11:42):

OK, it should be done and pushed.

view this post on Zulip Riccardo Brasca (Jul 21 2022 at 11:42):

I am stopping for at least half an hour

view this post on Zulip Johan Commelin (Jul 21 2022 at 11:47):

Okido, I'll take over

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jul 21 2022 at 12:56):

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

view this post on Zulip Johan Commelin (Jul 21 2022 at 13:11):

Qprime_isoms.lean is done

view this post on Zulip Johan Commelin (Jul 21 2022 at 13:39):

It's done!

view this post on Zulip Johan Commelin (Jul 21 2022 at 13:41):

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

view this post on Zulip Johan Commelin (Jul 21 2022 at 13:44):

I'm starting on bump-universes

view this post on Zulip 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.

view this post on Zulip Eric Rodriguez (Jul 21 2022 at 15:19):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jul 21 2022 at 17:12):

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

view this post on Zulip Johan Commelin (Jul 21 2022 at 17:13):

I understand your frustration.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Jul 21 2022 at 17:16):

yeah I found preserves_finite_limits_of_preserves_finite_limits_of_size

view this post on Zulip Adam Topaz (Jul 21 2022 at 17:16):

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

view this post on Zulip Johan Commelin (Jul 21 2022 at 17:31):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jul 21 2022 at 17:41):

Ouch! That's annoying.

view this post on Zulip 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

view this post on Zulip Adam Topaz (Jul 21 2022 at 17:58):

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

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jul 22 2022 at 06:58):

I fixed one more file

view this post on Zulip 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 (-;

view this post on Zulip Johan Commelin (Jul 22 2022 at 07:13):

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

view this post on Zulip Johan Commelin (Jul 22 2022 at 08:10):

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

view this post on Zulip Riccardo Brasca (Jul 22 2022 at 08:30):

I am having a look

view this post on Zulip Riccardo Brasca (Jul 22 2022 at 09:03):

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

view this post on Zulip Andrew Yang (Jul 22 2022 at 09:05):

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

view this post on Zulip Johan Commelin (Jul 22 2022 at 12:20):

@Andrew Yang did you already fix ab4.lean?

view this post on Zulip Andrew Yang (Jul 22 2022 at 12:20):

Yes. I can push what I have now.

view this post on Zulip Johan Commelin (Jul 22 2022 at 12:21):

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

view this post on Zulip Johan Commelin (Jul 22 2022 at 12:21):

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

view this post on Zulip Andrew Yang (Jul 22 2022 at 12:22):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jul 22 2022 at 12:54):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jul 22 2022 at 13:13):

Thanks, I'll try.

view this post on Zulip Johan Commelin (Jul 22 2022 at 13:34):

That worked. I fixed 3 files and pushed.

view this post on Zulip Johan Commelin (Jul 22 2022 at 13:55):

condensed/filtered_colimits seems to be quite a nightmare.

view this post on Zulip Johan Commelin (Jul 22 2022 at 13:55):

@Andrew Yang how is the tensor file going?

view this post on Zulip 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.

view this post on Zulip Andrew Yang (Jul 22 2022 at 15:10):

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

view this post on Zulip Johan Commelin (Jul 22 2022 at 15:41):

I'm working on condensed/acyclic

view this post on Zulip Johan Commelin (Jul 22 2022 at 16:05):

done, and now I need to go

view this post on Zulip Adam Topaz (Jul 22 2022 at 20:20):

I fixed condesed/filtered_colimits.

view this post on Zulip Adam Topaz (Jul 22 2022 at 20:21):

What a mess!

view this post on Zulip Johan Commelin (Jul 22 2022 at 20:27):

Wow! I had 3 attempts that all failed

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Jul 23 2022 at 00:30):

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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jul 25 2022 at 10:52):

I'm starting the mathlib bump to mathlib master.

view this post on Zulip 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.

view this post on Zulip Yaël Dillies (Jul 25 2022 at 11:22):

Is pseudo_normed_group pseudo in the same sense as pseudo_metric_space?

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jul 25 2022 at 14:19):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jul 25 2022 at 14:30):

I'm working on making thm95 error-free.

view this post on Zulip Johan Commelin (Jul 25 2022 at 14:55):

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

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jul 25 2022 at 16:59):

condensed/ seems to be error-free

view this post on Zulip Andrew Yang (Jul 25 2022 at 17:33):

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

view this post on Zulip Johan Commelin (Jul 25 2022 at 17:33):

I just did

view this post on Zulip Johan Commelin (Jul 25 2022 at 17:41):

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

view this post on Zulip Johan Commelin (Jul 25 2022 at 17:54):

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

view this post on Zulip Johan Commelin (Jul 25 2022 at 18:19):

One linting error. I pushed a fix.

view this post on Zulip Johan Commelin (Jul 25 2022 at 18:36):

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

view this post on Zulip 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 ;)

view this post on Zulip Yaël Dillies (Jul 25 2022 at 18:38):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Aug 08 2022 at 19:12):

yeah that docstring is wrong

view this post on Zulip Riccardo Brasca (Aug 08 2022 at 19:13):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Adam Topaz (Aug 08 2022 at 19:17):

where is this prev_eq_zero' used?

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Riccardo Brasca (Aug 08 2022 at 19:22):

#15940 for the modifications not done in the previous PR

view this post on Zulip 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(-)

view this post on Zulip Johan Commelin (Aug 09 2022 at 15:22):

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

view this post on Zulip 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...

view this post on Zulip Johan Commelin (Aug 09 2022 at 15:23):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Aug 09 2022 at 15:57):

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

view this post on Zulip Johan Commelin (Aug 09 2022 at 16:01):

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

view this post on Zulip Kevin Buzzard (Aug 09 2022 at 16:09):

Does the proof not work at your end?

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Aug 09 2022 at 16:27):

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

view this post on Zulip Johan Commelin (Aug 09 2022 at 16:27):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip Adam Topaz (Aug 09 2022 at 16:59):

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

view this post on Zulip Adam Topaz (Aug 09 2022 at 16:59):

and what file?

view this post on Zulip 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

view this post on Zulip Adam Topaz (Aug 09 2022 at 17:23):

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

view this post on Zulip Adam Topaz (Aug 09 2022 at 17:48):

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

view this post on Zulip Adam Topaz (Aug 09 2022 at 17:48):

on this branch....

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Adam Topaz (Aug 09 2022 at 18:17):

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

view this post on Zulip 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 :(

view this post on Zulip 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 :=

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Aug 09 2022 at 19:40):

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

view this post on Zulip Johan Commelin (Aug 09 2022 at 19:41):

Depending on whether prev/next exists or not.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Aug 09 2022 at 20:05):

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

view this post on Zulip Adam Topaz (Aug 09 2022 at 20:06):

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

view this post on Zulip Johan Commelin (Aug 09 2022 at 20:07):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip Johan Commelin (Aug 10 2022 at 13:30):

Thanks!

view this post on Zulip 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!

view this post on Zulip Adam Topaz (Aug 10 2022 at 14:43):

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

view this post on Zulip 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?

view this post on Zulip Adam Topaz (Aug 10 2022 at 16:57):

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

view this post on Zulip Kevin Buzzard (Aug 10 2022 at 16:58):

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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Aug 10 2022 at 17:01):

Actually we only had arbitrary horizontal ones I guess

view this post on Zulip Adam Topaz (Aug 10 2022 at 17:01):

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

view this post on Zulip 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 (-;

view this post on Zulip Adam Topaz (Aug 10 2022 at 17:02):

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

view this post on Zulip 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:

view this post on Zulip Johan Commelin (Aug 10 2022 at 17:05):

See #homological algebra

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Aug 13 2022 at 20:08):

Bah, this bump is quite annoying.


Last updated: Aug 16 2022 at 18:20 UTC