Zulip Chat Archive
Stream: condensed mathematics
Topic: mathlib bump
Johan Commelin (Jun 18 2021 at 20:00):
@Adam Topaz Could you please take a look at the branch mathlib-bump-21-06-18?
Adam Topaz (Jun 18 2021 at 20:00):
Sure, I'll take a look in a few hours
Johan Commelin (Jun 18 2021 at 20:00):
There is one error in for_mathlib/Profinite/clopen_limit.lean (line 404) that I don't immediately see how to fix.
Johan Commelin (Jun 18 2021 at 20:00):
The rest seems to be fine.
Adam Topaz (Jun 18 2021 at 20:01):
I'm on mobile now, but I can take a quick look now without writing any code
Johan Commelin (Jun 18 2021 at 20:02):
theorem exists_locally_constant_factors {α : Type*} [nonempty α] [inhabited J]
(hC : is_limit C) (ff : locally_constant C.X α) : ∃ (i : J)
(gg : locally_constant (F.obj i) α), gg ∘ (C.π.app i) = ff :=
begin
let S : discrete_quotient C.X := ff.to_discrete_quotient,
let fff : S → α := ff.desc, -- error is here
have hfff : fff ∘ S.proj = _ := ff.factors,
obtain ⟨i,T,hT⟩ := exists_discrete_quotient F C hC S,
Johan Commelin (Jun 18 2021 at 20:02):
invalid type ascription, term has type
Π (h : locally_constant ?m_1 ?m_2),
?m_5 ∘ ⇑ff = ⇑h → function.injective ?m_5 → locally_constant ?m_1 ?m_4 : Type (max (max ? ?) ? ?)
but is expected to have type
↥S → α : Type (max u u_1)
state:
J : Type u,
_inst_1 : semilattice_inf J,
F : J ⥤ Profinite,
C : cone F,
α : Type u_1,
_inst_2 : nonempty α,
_inst_3 : inhabited J,
hC : is_limit C,
ff : locally_constant ↥(C.X) α,
S : discrete_quotient ↥(C.X) := ff.to_discrete_quotient
⊢ ∃ (i : J) (gg : locally_constant ↥(F.obj i) α), ⇑gg ∘ ⇑(C.π.app i) = ⇑ff
Adam Topaz (Jun 18 2021 at 20:04):
Oh, that's because the desc that you removed is not the same desc that's now in mathlib
Johan Commelin (Jun 18 2021 at 20:04):
Right, but I don't see immediately how to fix it.
Johan Commelin (Jun 18 2021 at 20:05):
It's not just the order of arguments that changed, or something trivial like that.
Johan Commelin (Jun 18 2021 at 20:05):
So is there now a different decl that I need to use?
Adam Topaz (Jun 18 2021 at 20:05):
No, I still haven't added the necessary construction to mathlib.
Johan Commelin (Jun 18 2021 at 20:06):
So I should unremove desc and call it desc'?
Adam Topaz (Jun 18 2021 at 20:06):
Yeah, that should work for now.
Adam Topaz (Jun 18 2021 at 20:06):
I'm going to open a PR with a generalization of this theorem soon, so it won't stick around in for_mathlib for long :wink:
Johan Commelin (Jun 18 2021 at 20:32):
mathlib bump now pushed to master
Adam Topaz (Jun 18 2021 at 20:38):
I'm working on that followup PR now... N.B. it will depend on #7982
Adam Topaz (Jun 18 2021 at 21:29):
Adam Topaz (Jun 18 2021 at 21:30):
This should allow us to essentially completely remove the second half of for_mathlib/Profinite/clopen_limit.
Filippo A. E. Nuccio (Jun 20 2021 at 14:09):
Thanks to @Anne Baanen , I have realised that the lemma introduced in for_mathlib/finsupp called sum_eq_sum_fintype was already in mathlib, as finsupp.sum_fintype. I have modified all the occurrences, and commented the whole for_mathlib/finsupp, so we can actually throw it away.
Johan Commelin (Jun 21 2021 at 07:05):
Thanks!
Johan Commelin (Jun 21 2021 at 07:06):
@Filippo A. E. Nuccio In the future, feel free to just remove the file.
Johan Commelin (Jun 21 2021 at 08:44):
mathlib bumped again
Kevin Buzzard (Jun 21 2021 at 09:28):
What is the plan going forwards here? Right now the emphasis is on emptying for_mathlib before we go any further? [says the person whose term is finishing this Friday]
Johan Commelin (Jun 21 2021 at 09:28):
Yes, I've had very little Lean time in the past two weeks... but people are working on PRing parts of for_mathlib, which is great!
Filippo A. E. Nuccio (Jun 21 2021 at 09:28):
I'm working on getting rid of the linear_algebra file (see #7963) and of kronecker
Johan Commelin (Jun 21 2021 at 09:29):
Besides such PRs, I want to work on documenting the files outside of for_mathlib.
Riccardo Brasca (Jun 21 2021 at 09:34):
There is normed_group_hom_equalizer.lean that is more or less ready for PR. My only hesitation is that I don't see any monoid_hom.equalizer in mathlib (but there is alg_hom.equalizer). It would be a little strange to have the equalizer for morphisms of normed groups but not for groups...
Riccardo Brasca (Jun 21 2021 at 15:18):
I've bumped mathlib again to include #7875.
Adam Topaz (Jun 21 2021 at 19:19):
#7992 is ready for review, in case anyone wants to take a look. Once this is merged, it will help clean up a big chunk of for_mathlib/Profinite/*
Adam Topaz (Jun 22 2021 at 01:51):
I just did a bit of cleanup:
git diff 0253ede091338f3f3f84a1c52ac5c5a99f256e4b --stat
src/for_mathlib/Cech/adjunction.lean | 7 -------
src/for_mathlib/Profinite/arrow_limit.lean | 17 ++++++++++++++++-
src/for_mathlib/Profinite/fibprod.lean | 37 -------------------------------------
src/for_mathlib/arrow.lean | 53 -----------------------------------------------------
src/for_mathlib/topology.lean | 44 --------------------------------------------
src/for_mathlib/unused/Profinite/functorial_limit.lean | 16 ++++++++++++++--
src/prop819.lean | 36 ++++++++++++++----------------------
src/prop819/locally_constant.lean | 47 -----------------------------------------------
8 files changed, 44 insertions(+), 213 deletions(-)
Adam Topaz (Jun 22 2021 at 01:51):
We have a whole folder called for_mathlib/unused. Do we want to keep it around?
Johan Commelin (Jun 22 2021 at 04:48):
I'm not particularly attached to it :grinning:
Johan Commelin (Jun 22 2021 at 04:49):
We could add a branch unused-stuff just before dropping that directory, so that people can easily find it if they want to look at it again
Johan Commelin (Jun 22 2021 at 14:11):
The branch for-mathlib-unused now contains this directory.
Johan Commelin (Jun 22 2021 at 14:13):
87 src/for_mathlib/Cech/adjunction.lean
229 src/for_mathlib/Cech/split.lean
637 src/for_mathlib/Gordan.lean
329 src/for_mathlib/Profinite/arrow_limit.lean
425 src/for_mathlib/Profinite/clopen_limit.lean
151 src/for_mathlib/Profinite/compat_discrete_quotient.lean
36 src/for_mathlib/Profinite/locally_constant.lean
283 src/for_mathlib/SemiNormedGroup.lean
160 src/for_mathlib/SemiNormedGroup_Completion.lean
22 src/for_mathlib/arrow.lean
16 src/for_mathlib/arrow/iso_mk.lean
19 src/for_mathlib/arrow/split.lean
126 src/for_mathlib/data_setoid_partition.lean
74 src/for_mathlib/discrete_quotient.lean
47 src/for_mathlib/fin.lean
89 src/for_mathlib/finite_free.lean
385 src/for_mathlib/free_abelian_group.lean
87 src/for_mathlib/is_locally_constant.lean
90 src/for_mathlib/kronecker.lean
65 src/for_mathlib/linear_algebra.lean
593 src/for_mathlib/nnrat.lean
20 src/for_mathlib/nnreal.lean
60 src/for_mathlib/normed_group.lean
90 src/for_mathlib/normed_group_hom.lean
210 src/for_mathlib/normed_group_hom_completion.lean
92 src/for_mathlib/normed_group_hom_equalizer.lean
89 src/for_mathlib/order.lean
21 src/for_mathlib/quotient.lean
565 src/for_mathlib/rational_cones.lean
43 src/for_mathlib/simplicial/augmented.lean
161 src/for_mathlib/simplicial/complex.lean
64 src/for_mathlib/simplicial/iso.lean
16 src/for_mathlib/topology.lean
34 src/for_mathlib/tsum.lean
54 src/for_mathlib/wide_pullback.lean
5469 total
Johan Commelin (Jun 22 2021 at 14:13):
A little while there was over 7000 lines in for_mathlib. So we've made quite a dent already.
Adam Topaz (Jun 22 2021 at 14:16):
:ping_pong: for #7992 if you want to get that number even smaller :wink:
Johan Commelin (Jun 22 2021 at 14:25):
@Adam Topaz does that become easier if you use bool instead of fin 2?
Johan Commelin (Jun 22 2021 at 14:25):
Otherwise, lgtm
Eric Rodriguez (Jun 22 2021 at 14:26):
as an outsider, would there be any issues with me just diving in to some part of that code that I can understand, and try port it over to mathlib? or should I leave that to you all
Adam Topaz (Jun 22 2021 at 14:28):
I don't think using bool is much easier, especially given docs#locally_constant.of_clopen
Adam Topaz (Jun 22 2021 at 14:29):
And I tried making this of_clopen thing use bool. It turned out to be more or less the same as using fin 2
Johan Commelin (Jun 22 2021 at 14:30):
@Eric Rodriguez Feel free to browse through for_mathlib and PR whatever you think looks ready to PR.
Johan Commelin (Jun 22 2021 at 14:30):
(Some parts of it might need polishing... and you are free to do that as well, if you want to help!)
Johan Commelin (Jun 22 2021 at 14:31):
Also, please leave a note here when you "claim" a file. So that we don't duplicate efforts.
Johan Commelin (Jun 22 2021 at 14:32):
Adam Topaz said:
I don't think using
boolis much easier, especially given docs#locally_constant.of_clopen
Okido
Johan Commelin (Jun 22 2021 at 17:47):
src/for_mathlib/Profinite/compat_discrete_quotient.lean
src/for_mathlib/arrow.lean
src/for_mathlib/arrow/iso_mk.lean
src/for_mathlib/arrow/split.lean
src/for_mathlib/discrete_quotient.lean
src/for_mathlib/fin.lean
src/for_mathlib/finite_free.lean
src/for_mathlib/free_abelian_group.lean
src/for_mathlib/kronecker.lean
src/for_mathlib/linear_algebra.lean
src/for_mathlib/nnrat.lean
src/for_mathlib/nnreal.lean
src/for_mathlib/normed_group.lean
src/for_mathlib/order.lean
src/for_mathlib/quotient.lean
src/for_mathlib/simplicial/augmented.lean
src/for_mathlib/simplicial/complex.lean
src/for_mathlib/simplicial/iso.lean
src/for_mathlib/topology.lean
src/for_mathlib/tsum.lean
src/for_mathlib/wide_pullback.lean
:this: seem to be the files that do not import other files from LTE
Filippo A. E. Nuccio (Jun 22 2021 at 17:48):
Actually linear_algebra should have disappeared, I have just merged from bump-mathlib-220621 :thinking:
Johan Commelin (Jun 22 2021 at 17:51):
Ooh, I forgot to git pull :face_palm:
Johan Commelin (Jun 22 2021 at 17:52):
I'll take care of free_abelian_group.lean
Filippo A. E. Nuccio (Jun 22 2021 at 17:52):
I am not far from getting rid ofkroneckerbut I need another PR to go through.
Filippo A. E. Nuccio (Jun 22 2021 at 17:53):
(btw: can you confirm that my mathlib-bump was OK, meaning that linear_algebra has disappeared?)
Johan Commelin (Jun 22 2021 at 17:57):
@Filippo A. E. Nuccio I don't see a new commit on master
Filippo A. E. Nuccio (Jun 22 2021 at 17:58):
:thinking:
Filippo A. E. Nuccio (Jun 22 2021 at 17:59):
Should I git merge - while being in the master or in the bump-mathlib-*** branch? I would have said the latter, but I thought you suggested the former.
Adam Topaz (Jun 22 2021 at 18:05):
@Filippo A. E. Nuccio maybe you forgot to push?
Johan Commelin (Jun 22 2021 at 18:06):
git merge - means "merge the branch I was on previously into the branch I am on now"
Filippo A. E. Nuccio (Jun 22 2021 at 18:06):
OK, strange. The bump-mathlib-220621 branch online contains all my modifications, so I guess the push went through correctly.
Johan Commelin (Jun 22 2021 at 18:07):
#8046 contains most of for_mathlib/free_abelian_group.lean, namely the isomorphism with finsupp
Filippo A. E. Nuccio (Jun 22 2021 at 18:09):
I can try to do it again (or, for that matter, I believe anyone can do git merge - after git checkout bump-mathlib-220621 and git checkout master, right?) :speechless:
Adam Topaz (Jun 22 2021 at 18:17):
@Filippo A. E. Nuccio @Johan Commelin would you like me to merge bump-mathlib-220621 to master?
Filippo A. E. Nuccio (Jun 22 2021 at 18:17):
Yes please!
Adam Topaz (Jun 22 2021 at 18:17):
ok give me a sec
Adam Topaz (Jun 22 2021 at 18:20):
done
Filippo A. E. Nuccio (Jun 22 2021 at 18:20):
Thanks!
Adam Topaz (Jun 22 2021 at 18:36):
I'm working on another mathlib bump right now
Adam Topaz (Jun 22 2021 at 18:48):
git diff d6b8d023a38d11c57ba7460840276f4cbaeeb7a3 --stat
leanpkg.toml | 2 +-
src/for_mathlib/Profinite/clopen_limit.lean | 279 ------------------------------------------------------------
src/for_mathlib/Profinite/locally_constant.lean | 36 --------
src/for_mathlib/is_locally_constant.lean | 14 ---
src/prop819.lean | 13 +--
5 files changed, 5 insertions(+), 339 deletions(-)
Adam Topaz (Jun 22 2021 at 19:41):
I noticed some overlap with for_mathlib/locally_constant and some stuff from the recent mathlib PR that was merged. I deduplicated in the branch locally_constant_cleanup.
https://github.com/leanprover-community/lean-liquid/compare/locally_constant_cleanup
@Patrick Massot since this was your code, could you please take a look and see if you're okay with the changes?
Johan Commelin (Jun 22 2021 at 19:43):
I guess that will move us below the 5000 lines threshold :octopus:
Patrick Massot (Jun 22 2021 at 20:22):
If it still compiles then it's ok for me
Adam Topaz (Jun 22 2021 at 21:25):
Okay, it's merged to master now.
Adam Topaz (Jun 22 2021 at 21:30):
Not quite under 5000 just yet :sad:
87 Cech/adjunction.lean
229 Cech/split.lean
637 Gordan.lean
329 Profinite/arrow_limit.lean
146 Profinite/clopen_limit.lean
151 Profinite/compat_discrete_quotient.lean
283 SemiNormedGroup.lean
160 SemiNormedGroup_Completion.lean
22 arrow.lean
16 arrow/iso_mk.lean
19 arrow/split.lean
126 data_setoid_partition.lean
74 discrete_quotient.lean
47 fin.lean
89 finite_free.lean
382 free_abelian_group.lean
48 is_locally_constant.lean
90 kronecker.lean
593 nnrat.lean
20 nnreal.lean
60 normed_group.lean
90 normed_group_hom.lean
210 normed_group_hom_completion.lean
92 normed_group_hom_equalizer.lean
89 order.lean
21 quotient.lean
565 rational_cones.lean
43 simplicial/augmented.lean
161 simplicial/complex.lean
64 simplicial/iso.lean
16 topology.lean
34 tsum.lean
54 wide_pullback.lean
5047 total
Adam Topaz (Jun 22 2021 at 22:04):
#8048 is a very easy PR which will let us kill for_mathlib/topology.lean
Eric Rodriguez (Jun 22 2021 at 22:56):
#8049 knocks out for_mathlib/fin.lean. (and would be under 5000!)
Johan Commelin (Jun 23 2021 at 05:02):
It looks like we have ~1700 lines coming from nnrat, rational_cones and Gordan. This should definitely move to mathlib at some point. But I think nnrat can be generalized to "ordered semiring of non-negative elements of ordered ring". But that should probably wait till Damiano's order-refactor is done. Otherwise we need to do it twice.
Kevin Buzzard (Jun 23 2021 at 08:09):
Damiano"s refactor has been one of the unexpected benefits of the experiment. I remember Damiano and I discussing how to set up the very foundations of the theory for Gordan so they would apply to more than N v Z and nnreal v real, and I suspect this was one of the things which got him started experimenting with orders in general. The half of the project which we have pushed through has had knock-on benefits for mathlib beyond the obvious ones
Adam Topaz (Jun 23 2021 at 12:48):
(note: I just had to get the number under 5000, so I golfed a few proofs last night... I think it's around 4950ish now.)
Johan Commelin (Jun 23 2021 at 14:35):
#7457 takes care of arrow.lean (6 lines)
Johan Commelin (Jun 23 2021 at 14:59):
#8057 takes care of arrow/iso_mk.lean (again ~6 lines)
Damiano Testa (Jun 23 2021 at 19:31):
Kevin, I confirm that my decision to take over the order refactor stemmed from LTE! Besides, yours and Eric's gradings and part of Bhavik's and Yaël's push to finish Krein-Millman/Hahn-Banach and generally working with convex sets was also a consequence of this!
Yaël Dillies (Jun 23 2021 at 20:17):
Definitely! We had defined extreme and exposed sets, but we wouldn't have proved Krein-Milman without you (momentarily) needing it.
Johan Commelin (Jun 25 2021 at 05:58):
Eric Rodriguez said:
#8049 knocks out
for_mathlib/fin.lean. (and would be under 5000!)
This has now landed in mathlib. Thanks for your help @Eric Rodriguez. I'm bumping mathlib right now
Johan Commelin (Jun 25 2021 at 06:04):
Ooh, I now see that you already made a PR for this! :surprise: :lol: :octopus:
Adam Topaz (Jun 25 2021 at 22:53):
#8085 is a quick PR which takes care of for_mathlib/simplicial/augmented.
Johan Commelin (Jul 20 2021 at 12:07):
Mathlib bumped.
Johan Commelin (Aug 07 2021 at 17:09):
Does anyone know what happened to real.Sup_le?
Johan Commelin (Aug 07 2021 at 17:12):
Aha chore(data/real/basic): drop some lemmas (#8523) seems relevant. I was on a wrong branch of mathlib when I did git pull. Hence the logs didn't show anything.
Adam Topaz (Aug 07 2021 at 17:28):
@Johan Commelin is it causing some error in LTE? I fixed some error related to real.Sup_le missing a few days ago...
Johan Commelin (Aug 07 2021 at 17:36):
Hmm, let me check that I'm not duplicating your work.
Johan Commelin (Aug 07 2021 at 17:36):
Ok, I'm up to date. The error is in locally_constant/analysis
Johan Commelin (Aug 07 2021 at 17:37):
wip is in mathlib-bump-wip
Adam Topaz (Aug 07 2021 at 17:39):
Oh, sorry, I misremembered. I fixed something related to real.exists_sup.
Johan Commelin (Aug 07 2021 at 18:39):
This actually solves a golfing issue that we had (-; https://github.com/leanprover-community/lean-liquid/compare/mathlib-bump-wip?expand=1#diff-eaaa24ad786e47b8b16bacbf6e5b2ddc517e8d60bd585ade06d159f75125ce6dL27
Johan Commelin (Aug 07 2021 at 18:58):
bump complete
Johan Commelin (Aug 09 2021 at 14:32):
another day, another bump
Johan Commelin (Aug 13 2021 at 13:47):
$ git show --stat
commit fd47ddc5a6f29069a1c666beb11be57893914889 (HEAD -> master)
Author: Johan Commelin <johan@commelin.net>
Date: Fri Aug 13 13:47:25 2021 +0000
mathlib bump
leanpkg.toml | 4 ++--
src/for_mathlib/SemiNormedGroup.lean | 2 --
src/for_mathlib/normed_group_hom.lean | 88 ----------------------------------------------------------------------------------------
src/for_mathlib/normed_group_hom_completion.lean | 2 --
src/locally_constant/analysis.lean | 2 --
src/normed_group/controlled_exactness.lean | 3 +--
src/prop_92/concrete.lean | 4 ++--
src/pseudo_normed_group/LC.lean | 1 -
8 files changed, 5 insertions(+), 101 deletions(-)
Adam Topaz (Aug 13 2021 at 14:36):
@Johan Commelin did you push to master?
Johan Commelin (Aug 13 2021 at 14:36):
:face_palm:
Johan Commelin (Aug 13 2021 at 14:36):
done
Patrick Massot (Aug 16 2021 at 16:26):
#8499 has been merged, this is the end of a long series of mathlib PRs. I think the for_mathlib folder should now be almost empty of contributions from me.
Johan Commelin (Aug 16 2021 at 16:27):
I'm bumping right now.
Johan Commelin (Aug 16 2021 at 16:27):
But I started before that merge. So I suggest we do two bumps in a row.
Johan Commelin (Aug 16 2021 at 16:40):
I just did git push --set-upstream origin mathlib-bump-16-aug-2021
Johan Commelin (Aug 16 2021 at 16:40):
So far, I fixed 1 thingy. But now I get a super-annoying timeout in col_exact.lean
Johan Commelin (Aug 16 2021 at 16:40):
Well, the build on the command line doesn't even timeout. It just hangs forever.
Johan Commelin (Aug 16 2021 at 16:41):
I need to run now... sorry
Johan Commelin (Aug 17 2021 at 06:18):
I won't have time for this today either, I'm afraid. So if someone wants to hack on this, please go ahead.
Johan Commelin (Aug 17 2021 at 15:20):
I managed to finish the bump. ext got into problems somehow...
Johan Commelin (Aug 17 2021 at 15:21):
So now we are ready for Patrick's bump. And then there is the Kronecker bump.
Filippo A. E. Nuccio (Aug 17 2021 at 15:21):
I have the feeling we're almost done with the Kronecker PR, just waiting for a final approval.
Johan Commelin (Aug 17 2021 at 16:20):
I just bumped mathlib again
Scott Morrison (Aug 17 2021 at 23:51):
I noticed that https://leanprover-community.github.io/lean_projects.html says that lean-liquid is always failing. I wonder if this display could better reflect that lean-liquid is actually keeping up.
Eric Wieser (Aug 18 2021 at 00:20):
The failure is
lean-liquid was not built on version [3, 32, 1] because some of its dependencies do not have a corresponding version: ['lean-gptf']
Mario Carneiro (Aug 18 2021 at 00:38):
Daniel noted that the gptf dependency is not actually used, and has been removing it in build tests. Perhaps you could remove it from the actual project and let users add it themselves if they want?
Johan Commelin (Aug 18 2021 at 04:57):
I'm doing this right now
Johan Commelin (Aug 18 2021 at 05:06):
I'm getting
/home/jmc/data/math/lean-liquid/src/Mbar/Mbar_le.lean: parsing at line 724/- The `check_univs` linter reports: -/
/- THE STATEMENTS OF THE FOLLOWING DECLARATIONS HAVE BAD UNIVERSE LEVELS. This usually means that there is a `max u v` in the declaration where neither `u` nor `v` occur by themselves. Solution: Find the type (or type bundled with data) that has this universe argument and provide the universe level explicitly. If this happens in an implicit argument of the declaration, a better solution is to move this argument to a `variables` command (where the universe level can be kept implicit).
Note: if the linter flags an automatically generated declaration `xyz._proof_i`, it means that
the universe problem is with `xyz` itself (even if the linter doesn't flag `xyz`) -/
#print Mbar_le.Fintype_add_functor._proof_3 /- universes [u_1, u_2] only occur together. -/
#print Mbar_le.Fintype_add_functor._proof_6 /- universes [u_1, u_2] only occur together. -/
#print Mbar_le.Fintype_add_functor._proof_4 /- universes [u_1, u_2] only occur together. -/
#print Mbar_le.Fintype_add_functor._proof_1 /- universes [u_1, u_2] only occur together. -/
#print Mbar_le.Fintype_add_functor._proof_7 /- universes [u_1, u_2] only occur together. -/
#print Mbar_le.Fintype_add_functor._proof_2 /- universes [u_1, u_2] only occur together. -/
#print Mbar_le.Fintype_neg_functor._proof_2 /- universes [u_1, u_2] only occur together. -/
#print Mbar_le.Fintype_neg_functor._proof_1 /- universes [u_1, u_2] only occur together. -/
#print Mbar_le.Fintype_bifunctor._proof_4 /- universes [u_1, u_2] only occur together. -/
#print Mbar_le.Fintype_bifunctor._proof_2 /- universes [u_1, u_2] only occur together. -/
#print Mbar_le.Fintype_bifunctor._proof_3 /- universes [u_1, u_2] only occur together. -/
#print Mbar_le.Fintype_bifunctor._proof_5 /- universes [u_1, u_2] only occur together. -/
#print Mbar_le.functor_prod._proof_2 /- universes [u_1, u_2] only occur together. -/
#print Mbar_le.functor_prod._proof_1 /- universes [u_1, u_2] only occur together. -/
#print Mbar_le.functor_prod._proof_3 /- universes [u_1, u_2] only occur together. -/
#print Mbar_le.functor_prod_cone._proof_2 /- universes [u_1, u_2] only occur together. -/
#print Mbar_le.add_functor._proof_3 /- universes [u_1, u_2] only occur together. -/
#print Mbar_le.add_functor._proof_2 /- universes [u_1, u_2] only occur together. -/
#print Mbar_le.add_functor._proof_1 /- universes [u_1, u_2] only occur together. -/
#print Mbar_le.neg_functor._proof_1 /- universes [u_1, u_2] only occur together. -/
#print Mbar_le.bifunctor._proof_1 /- universes [u_1, u_2] only occur together. -/
#print Mbar_le.bifunctor._proof_2 /- universes [u_1, u_2] only occur together. -/
#print Mbar.profinite._proof_1 /- universes [u_1, u_2] only occur together. -/
Johan Commelin (Aug 18 2021 at 05:07):
But those declarations don't mention universes at all. So the elaborator (or its friend) is doing something silly
Johan Commelin (Aug 18 2021 at 05:12):
This one is weird:
profinite.{u_1 u_2} : Π (r' : ℝ≥0) [_inst_2 : fact (0 < r')], Profinite.{(max u_1 u_2)} ⥤ Type (max u_1 u_2)
Johan Commelin (Aug 18 2021 at 05:14):
Here is the Lean code:
/-- The functor `Mbar : Profinite ⥤ Type*`. -/
def profinite [fact (0 < r')] : Profinite ⥤ Type* :=
(as_small.down ⋙ profinite_diagram r').flip ⋙ colim
If I explicitly ask it to use .{u}, then I get an error:
failed to synthesize type class instance for
r' : ℝ≥0,
_inst_2 : fact (0 < r')
⊢ has_colimits_of_shape (as_small ℝ≥0) (Type u)
Floris van Doorn (Aug 18 2021 at 05:17):
The solution is to write Profinite.{u} explicitly
Floris van Doorn (Aug 18 2021 at 05:18):
The error probably means that the instance also needs an explicit .{u} somewhere
Johan Commelin (Aug 18 2021 at 05:18):
aha, that makes sense
Floris van Doorn (Aug 18 2021 at 05:18):
Probably you want to replace Profinite by Profinite.{u} in most places (once per declaration that doesn't mention u yet)
Johan Commelin (Aug 18 2021 at 05:18):
well, I'm adding a nolint for now. I'll first try to get everything to build. We can hunt down the bad instance afterwards.
Johan Commelin (Aug 18 2021 at 05:19):
but if the linter can figure out that all the max u v's can be replaced by u, then lean should be able to do that without my handholding, right?
Floris van Doorn (Aug 18 2021 at 05:19):
in theory, yes
Johan Commelin (Aug 18 2021 at 05:20):
I pushed
Floris van Doorn (Aug 18 2021 at 05:22):
the easy hackish solution is to check (after elaboration) whether there are two universe levels u and v, both of which only occur as max u v, and if so, replace max u v by a new universe variable.
A hard solution is to fix the underlying problem that causes these max u v's.
Johan Commelin (Aug 20 2021 at 05:21):
mathlib bumped
Johan Commelin (Aug 26 2021 at 13:52):
back from a short trip, bumped mathlib
Johan Commelin (Sep 14 2021 at 14:31):
I bumped mathlib again
Riccardo Brasca (Sep 16 2021 at 08:31):
Bumped again
Johan Commelin (Sep 16 2021 at 09:05):
thanks!
Johan Commelin (Sep 25 2021 at 18:53):
high time for another bump: we're on a new version of Lean now, and we can use semilinear maps!
Johan Commelin (Sep 25 2021 at 18:54):
commit e8fc8f972722318b8918c0340e7ecde3e1c9abb8 (HEAD -> master, origin/master, origin/HEAD)
Author: Johan Commelin <johan@commelin.net>
Date: Sat Sep 25 18:52:11 2021 +0000
bump mathlib
leanpkg.toml | 2 +-
src/combinatorial_lemma/lem97.lean | 2 +-
src/condensed/ab.lean | 1 +
src/for_mathlib/finite_free.lean | 4 ++--
src/for_mathlib/nnrat.lean | 2 +-
src/for_mathlib/rational_cones.lean | 4 ++--
src/for_mathlib/snake_lemma.lean | 3 ---
src/system_of_complexes/basic.lean | 1 -
8 files changed, 8 insertions(+), 11 deletions(-)
Adam Topaz (Sep 25 2021 at 19:25):
:tada: !
Riccardo Brasca (Sep 26 2021 at 13:42):
for_mathlib/finite_free is gone.
Johan Commelin (Oct 01 2021 at 07:41):
I started working on a mathlib bump. This one might be a bit messy...
Johan Commelin (Oct 01 2021 at 08:29):
@Riccardo Brasca I think you created linear_algebra/free_module, right? Should linear_algebra.free_module_pid also move there?
Riccardo Brasca (Oct 01 2021 at 08:37):
Ah yes, that's a good idea. I will do it
Johan Commelin (Oct 01 2021 at 09:21):
Bump finished
leanpkg.toml | 2 +-
src/Mbar/basic.lean | 2 +-
src/breen_deligne/constants.lean | 2 +-
src/breen_deligne/homotopy.lean | 4 ++--
src/breen_deligne/suitable.lean | 2 +-
src/combinatorial_lemma/default.lean | 4 ++--
src/combinatorial_lemma/lem97.lean | 5 ++---
src/facts/nnreal.lean | 2 +-
src/for_mathlib/Gordan.lean | 7 +------
src/for_mathlib/nnrat.lean | 6 +++---
src/for_mathlib/rational_cones.lean | 5 +++--
src/for_mathlib/real.lean | 20 +++-----------------
src/laurent_measures/thm69_bad.lean | 10 +++++-----
src/normed_group/normed_with_aut.lean | 2 +-
src/normed_snake_dual.lean | 6 +++---
src/normed_spectral.lean | 4 ++--
src/polyhedral_lattice/basic.lean | 2 +-
src/polyhedral_lattice/finsupp.lean | 1 +
src/polyhedral_lattice/pseudo_normed_group.lean | 2 +-
src/polyhedral_lattice/quotient.lean | 1 +
src/pseudo_normed_group/with_Tinv.lean | 2 +-
src/rescale/normed_group.lean | 2 +-
src/rescale/pseudo_normed_group.lean | 2 +-
src/thm95/col_exact.lean | 6 +++---
src/thm95/col_exact_prep.lean | 2 +-
src/thm95/polyhedral_iso.lean | 4 ++--
26 files changed, 45 insertions(+), 62 deletions(-)
Riccardo Brasca (Oct 01 2021 at 10:14):
Johan Commelin (Oct 08 2021 at 07:10):
bumped mathlib again
Riccardo Brasca (Oct 11 2021 at 14:14):
Mathlib bumped
Johan Commelin (Oct 11 2021 at 14:14):
Merci! I was about to start a bump
Riccardo Brasca (Oct 14 2021 at 07:40):
Bumping mathlib
Riccardo Brasca (Oct 14 2021 at 08:09):
What happened to exact fact.out _? It doesn't work anymore, "failed to synthesize type class instance for" and the instance is looking for is the goal. Not a real problem, manually doing exact _inst_3.out works, but it's weird.
Johan Commelin (Oct 14 2021 at 08:14):
Hmm, but explicitly mentioning _inst_3 is fragile.
Johan Commelin (Oct 14 2021 at 08:14):
I'm not aware of any changes to the fact machinery.
Johan Commelin (Oct 14 2021 at 08:14):
Is this a general problem, or just in a few cases?
Johan Commelin (Oct 14 2021 at 08:15):
I count 66 lines with fact.out _ in LTE. Are they all broken :fear: ?
Riccardo Brasca (Oct 14 2021 at 08:15):
No, I don't think so.
Riccardo Brasca (Oct 14 2021 at 08:16):
See for example here
https://github.com/leanprover-community/lean-liquid/commit/d90a89fae8432d3d91293a77f0872b21783e8fdd
Riccardo Brasca (Oct 14 2021 at 08:16):
Both are for 0 < r, with r : ℝ≥0, so it should be something related to that
Johan Commelin (Oct 14 2021 at 08:19):
Aah, some instances for nnreal changed to more general nonneg instances for {x // 0 ≤ x}. That might cause the problem?
Johan Commelin (Oct 14 2021 at 08:20):
The more stable solution in this case might be to write exact ‹fact (0 < r)›.out instead of mentioning _inst_3.
Riccardo Brasca (Oct 14 2021 at 08:21):
Yes, that works! Taking care of that
Riccardo Brasca (Oct 14 2021 at 09:07):
The bump is done. I will throw away for_mathlib/SemiNormedGroup later today.
Johan Commelin (Oct 14 2021 at 09:12):
Merci!
Adam Topaz (Oct 14 2021 at 18:19):
I'm working on another bump right now.
Adam Topaz (Oct 14 2021 at 18:53):
Not too bad...
git diff --stat 509fcea815344d9eba240f9ca859a2255bc9e3f1
leanpkg.toml | 2 +-
src/Mbar/bounded.lean | 4 ++--
src/for_mathlib/Gordan.lean | 14 +++++++-------
src/for_mathlib/abelian_group_object.lean | 31 ++++++++++++++++---------------
src/laurent_measures/bounded.lean | 8 ++++----
src/laurent_measures/thm69.lean | 17 +++++++++--------
src/polyhedral_lattice/topology.lean | 2 +-
src/thm95/constants/default.lean | 14 +++++++-------
8 files changed, 47 insertions(+), 45 deletions(-)
Adam Topaz (Oct 14 2021 at 19:30):
I also got rid of as_small in condensed, and proved the following theorem:
theorem category_theory.functor.is_proetale_sheaf_iff (P : Profinite.{w}ᵒᵖ ⥤ C) :
P.is_proetale_sheaf ↔ presheaf.is_sheaf proetale_topology P :=
where
def category_theory.functor.is_proetale_sheaf (P : Profinite.{w}ᵒᵖ ⥤ C) : Prop := ∀
-- a finite family of morphisms with base B
(α : Type w) [fintype α] (B : Profinite.{w}) (X : α → Profinite.{w}) (f : Π a, X a ⟶ B)
-- jointly surjective
(surj : ∀ b : B, ∃ a (x : X a), f a x = b)
-- test object
(T : C)
-- family of moprhisms
(x : Π a, T ⟶ P.obj (op (X a)))
-- which is compatible
(compat : ∀ (a b : α) (Z : Profinite.{w}) (g₁ : Z ⟶ X a) (g₂ : Z ⟶ X b),
(g₁ ≫ f a = g₂ ≫ f b) → x a ≫ P.map g₁.op = x b ≫ P.map g₂.op),
-- the actual condition
∃! t : T ⟶ P.obj (op B), ∀ a : α, t ≫ P.map (f a).op = x a
Adam Topaz (Oct 14 2021 at 19:30):
That's a version of the sheaf condition that I hope is a bit more familiar...
Adam Topaz (Oct 14 2021 at 19:31):
We still need to rethink the universe levels in condensed/Ab.lean.
Adam Topaz (Oct 14 2021 at 19:33):
Another piece of good news:
@[derive category]
def Condensed (C : Type u) [category.{v} C] := Sheaf proetale_topology.{w} C
example : category.{u+1} (Condensed.{u} Ab.{u+1}) := infer_instance
example : category.{u+37} (Condensed.{u} Ring.{u+37}) := infer_instance
Johan Commelin (Oct 14 2021 at 19:34):
@Adam Topaz Wow, thanks a lot! That looks really good.
Johan Commelin (Oct 14 2021 at 19:34):
So I guess that in this strand, the next step would be the sheaf condition in terms of extr.disc.s?
Adam Topaz (Oct 14 2021 at 19:35):
Yeah, I'll work on that next...
Riccardo Brasca (Oct 17 2021 at 07:03):
Mathlib bumped, for_mathlib/SemiNormedGroup is gone.
Riccardo Brasca (Oct 18 2021 at 16:06):
After the next bump (I can to it later today), for_mathlib/SemiNormedGroup_Completion can be removed. I think that there will be nothing left in for_mathlib related to normed_group. It has been quite a journey, if I remember correctly we didn't had even normed_group_hom in mathlib before LTE (we had the operator norm for normed spaces). We added exotic stuff like pseudo_emetric_space, but also quotients and completions of normed groups. Do you think the story is worth a small blog post? To show how projects like LTE can be useful to mathlib.
Johan Commelin (Oct 18 2021 at 16:16):
Thanks for all your work on this. A blogpost definitely seems appropriate.
Riccardo Brasca (Oct 19 2021 at 08:48):
The bump is done.
Riccardo Brasca (Oct 23 2021 at 16:40):
I tried another bump, but has_coe_to_fun changed and I don't really understand it, so I leave it to someone more experienced :)
Yaël Dillies (Oct 23 2021 at 16:43):
Also beware of floor/ceil/nat_floor/nat_ceil now being int.floor/int.ceil/nat.floor/nat.ceil.
Yaël Dillies (Oct 23 2021 at 16:43):
And @Filippo A. E. Nuccio, enjoy!
Riccardo Brasca (Oct 23 2021 at 16:44):
Also, did the behavior of namespace changed? I had to move it after a variables declaration to make everything working.
Johan Commelin (Oct 23 2021 at 16:56):
Hmm weird, I'm not aware of changes to namespace
Johan Commelin (Oct 23 2021 at 16:57):
I don't have time for a bump this weekend. I'll look at it Monday if it's still an issue then.
Riccardo Brasca (Oct 23 2021 at 17:06):
ah, everything is here
Ben Toner (Oct 23 2021 at 22:53):
I'm attempting to do the bump now.
Ben Toner (Oct 23 2021 at 23:55):
Bump done, but probably someone should review as I am a beginner!
To deal with the lean upgrade in the commit linked by @Riccardo Brasca above, and the issue with namespace, I changed
namespace homological_complex
open category_theory category_theory.limits
to
namespace homological_complex
open _root_.category_theory _root_.category_theory.limits
and similarly in a couple of other places. But I don't understand why that is necessary. Is there a way to trace what's going on?
Scott Morrison (Oct 23 2021 at 23:57):
The behaviour of open was changed recently, to match the behaviour in Lean4.
Scott Morrison (Oct 23 2021 at 23:58):
If A is open, and both B and A.B exist, now open B means open A.B, whereas it used to mean open _root_.B.
Scott Morrison (Oct 23 2021 at 23:59):
Often you can move your open statements outside of namespaces, or just change the order of the opens, to avoid having to write the ugly _root_ so much.
Ben Toner (Oct 24 2021 at 00:10):
@Scott Morrison thanks - I'll change the order. I'm still confused though: there is no homological_complex.category_theory so what's it finding?
Ben Toner (Oct 24 2021 at 01:04):
Never mind - I figured it out, I think: because the namespace homological_complex already has an instance homological_complex.category_theory.category from an import, homological_complex.category_theory does exist, and so it's necessary to disambiguate.
Johan Commelin (Oct 24 2021 at 07:01):
@Ben Toner Thanks a lot for thise fixes!
Filippo A. E. Nuccio (Oct 25 2021 at 13:35):
Thanks!
Johan Commelin (Oct 28 2021 at 06:23):
I'm attempting to bump LTE to zpow/zsmul and co.
Sebastien Gouezel (Oct 28 2021 at 07:38):
Here is a recipe for this: global search and replace of gpow and fpow with zpow. Then, where compilation fails, add a subscript 0 at the end of the offending lemma. That's it!
Johan Commelin (Oct 28 2021 at 07:52):
Yeah, and luckily we aren't using gpowers :smiley:
Johan Commelin (Oct 28 2021 at 07:52):
Indeed, I just checked, and the build finished. So bump is done.
Johan Commelin (Nov 16 2021 at 17:36):
I got distracted for a moment, but the bump is now done
Johan Commelin (Nov 29 2021 at 10:14):
I'm starting a bump
Johan Commelin (Nov 29 2021 at 10:29):
When this bump is done, we'll have much more flexible categorical limits in LTE. Will be interesting to see if we can get rid of some ulifts.
Johan Commelin (Nov 29 2021 at 10:29):
@Adam Topaz Do you think we should remove the universe polymorphism from simplex_category now?
Johan Commelin (Nov 29 2021 at 11:43):
Bump finished
commit 85213c7b7155a8947e24987bcdc0636407eb8c74 (HEAD -> master, origin/master, origin/HEAD)
Author: Johan Commelin <johan@commelin.net>
Date: Mon Nov 29 11:42:59 2021 +0000
bump mathlib
leanpkg.toml | 2 +-
src/banach.lean | 2 +-
src/breen_deligne/eval.lean | 2 +-
src/breen_deligne/suitable.lean | 2 +-
src/breen_deligne/universal_map.lean | 1 +
src/for_mathlib/Profinite/disjoint_union.lean | 47 -----------------------------------------------
src/for_mathlib/abelian_sheaves/main.lean | 10 +++++-----
src/for_mathlib/concrete_filtered_colimit_commutes.lean | 8 ++++----
src/for_mathlib/nnrat.lean | 4 ++--
src/real_measures.lean | 2 +-
src/thm95/col_exact.lean | 3 ++-
src/thm95/constants/default.lean | 2 +-
12 files changed, 20 insertions(+), 65 deletions(-)
Yaël Dillies (Nov 29 2021 at 12:59):
You missed is_preconnected.preimage and is_connected.preimage! But I'll take care of it myself once #10511 hits mathlib.
Johan Commelin (Nov 29 2021 at 13:01):
What do you mean with "missed"?
Johan Commelin (Nov 29 2021 at 13:01):
Lean didn't complain about them. So I didn't touch them.
Yaël Dillies (Nov 29 2021 at 13:02):
docs#is_preconnected.preimage_of_open_map
Johan Commelin (Nov 29 2021 at 13:02):
I see. Well, that's your job :stuck_out_tongue_wink:
Yaël Dillies (Nov 29 2021 at 13:02):
I guess :grinning_face_with_smiling_eyes:
Johan Commelin (Nov 29 2021 at 13:02):
I think mathlib bumps should do the minimal thing to get the build working again.
Adam Topaz (Nov 29 2021 at 14:05):
Johan Commelin said:
Adam Topaz Do you think we should remove the universe polymorphism from
simplex_categorynow?
It's certainly worth trying!
Adam Topaz (Dec 03 2021 at 22:12):
Mathlib bumped -- please refresh your oleans.
There is a bunch of cleanup to do for unneeded code now, especially in condensed/adjunctions.lean, but I'm not sure I'll have time for it today.
Johan Commelin (Dec 04 2021 at 05:53):
@Adam Topaz Thanks!
Johan Commelin (Dec 04 2021 at 05:54):
What's next on plan? To PR the stuff on abelian sheaves? Or do you want to first try out some use cases (i.e. more about Cond(Ab))?
Yaël Dillies (Dec 04 2021 at 09:23):
How does one refresh oleans?
Kevin Buzzard (Dec 04 2021 at 09:28):
leanproject get-mathlib-cache
Kevin Buzzard (Dec 04 2021 at 09:33):
In fact this is the thing where I don't actually know the correct workflow. Here's what I just did (all in the lean-liquid repo, on the command line):
1) Check you're on master branch and don't have any random stuff which needs to be committed or whatever with git status
2) git pull and note that leanpkg.toml just changed.
3) leanproject build and wait until lean --make src starts running and the computer starts recompiling mathlib from scratch (on Linux I see stuff in _target/deps/mathlib beginning to be compiled). Then Ctrl-C to exit this process (I don't want to compile mathlib)
4) leanproject get-m (=get-mathlib-cache) to get the correct mathlib oleans.
5) leanproject build again (and this time it starts building the lean-liquid repo rather than mathlib.
Kevin Buzzard (Dec 04 2021 at 09:34):
In fact instead of (5) I usually do lean -M6000 --make src with the -M flag so I can control how much memory the build uses. But I use leanproject build for (3) because it's helping to sort out _target.
Kevin Buzzard (Dec 04 2021 at 09:38):
What I think is going on is that after (2) git pull the toml says that we're supposed to be using one commit of mathlib (the new one), but the actual mathlib git repo in _target is pointing at another commit (the old one) and leanproject get-m directly after git pull might not do all of (a) pulling the master branch of mathlib in _target from github (b) switching to the correct commit according to the lean-liquid toml (c) pulling the correct oleans from Azure. I haven't tried this with leanproject 1.1.0 though (and I just missed my chance). I think (3) leanproject build gets the lean files in _target into the correct state and then (4) leanproject get-m gets the olean files into the correct state.
Johan Commelin (Dec 04 2021 at 10:02):
@Kevin Buzzard ./scripts/get-cache.sh will download LTE oleans for you.
Kevin Buzzard (Dec 04 2021 at 10:06):
OK so I just tried this on another machine with a clean master branch which hasn't been synced with github for a few days. The question is "the project I'm working on with someone else has mathlib as a dependency, and the other person bumped mathlib; what do I do?"
1) Note that leanproject up (=leanproject upgrade-mathlib) is not what we want to do if we're not the person who's actually doing the bumping. This command bumps mathlib to current master, rather than the commit specified in the project toml, and this is definitely not what we want.
2) After git pull, the toml now points to the new mathlib commit, but _target leans and oleans are on the old mathlib commit.
3) Directly running leanproject get-mathlib-cache now looks in the new toml and downloads the oleans corresponding to the new commit, but it does not seem to change the lean files at all, so now we have new oleans but old lean files. Your project is now in a dangerous state! but it's Ok because...
4) Running leanproject build now switches the commit in _target to the correct one, and doesn't touch the oleans (which is good because they were already correct).
So on this occasion, git pull, leanproject get-mathlib-cache, leanproject build works.
I am a bit nervous about whether this always works though; I think I've run into trouble before when people make structural changes to mathlib, e.g. renaming the file data/foo.lean to data/foo/basic.lean and doing other stuff like this; because in step (3) above when the lean files are on one commit and the olean files are on the other commit, in the past you have been able to find yourself in a situation where leanproject wants to put olean files in directories which do not actually exist yet. So whilst the incantation in this message works on this occasion, I am a bit nervous about whether it works 100% of the time.
Another proof I've used with 100% success rate is git pull, rm -rf _target, leanproject build.
Kevin Buzzard (Dec 04 2021 at 10:22):
PS just to confirm that ./scripts/get-cache.sh works for me -- however on both the machines I tried it on, it reported (on line 3 of the output) "Found local lean-liquid oleans" which cannot possibly be true (unless it means "I found some oleans in src on your computer, which now are not at all relevant")
Kevin Buzzard (Dec 04 2021 at 10:26):
Aah! So does git pull, rm -rf _target, ./scripts/get-cache.sh always work?? This script also gets mathlib leans and oleans, it seems! If this is the case then for this particular project that might be the easiest workflow. It just worked for me now.
Kevin Buzzard (Dec 04 2021 at 10:28):
It would be interesting to know whether git pull, ./scripts/get-cache.sh works or whether this leaves _target pointing at the wrong mathlib commit. If anyone who didn't bump yet wants to continue this experiment further they could try it and see if lean --make src returns after a few seconds with no output or starts compiling mathlib. My fear is that it will leave the system with all the right olean files but with mathlib in _target still on the old commit.
Kevin Buzzard (Dec 04 2021 at 10:33):
Oh this is interesting -- I think that the workflow above does leave you with the wrong lean files but with the correct olean files, so lean --make src does work but jump to definition in VS Code is broken!
Kevin Buzzard (Dec 04 2021 at 10:35):
Conclusion: assuming you haven't been an evil person and have edited mathlib files in _target ("I'll PR it later, promise"), thengit pull, rm -rf _target, ./scripts/get-cache.sh is the golfiest way to happiness, but that's only for this specific project. For other projects with mathlib as dependency, git pull, rm -rf _target, leanproject get-mathlib-cache, leanproject build looks like a failsafe approach.
Eric Rodriguez (Dec 04 2021 at 11:30):
leanproject pull does what git pull, rm -rf _target does
Eric Wieser (Dec 06 2021 at 13:45):
It sounds like we're missing a leanproject command that updates the oleans and leans from the toml version
Eric Wieser (Dec 06 2021 at 13:46):
I assumed get-mathlib-cache was the command, but evidently it's not.
Ben Toner (Dec 06 2021 at 14:46):
The scripts/get-cache.sh script was meant to be a temporary workaround. The plan was that leanproject get-cache would retrieve the cached oleans for a project and its dependencies. At one point I said I'd do this but I haven't and I'm unlikely to this year. Design is in this thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/CI.20for.20liquid.20tensor.20experiment
Johan Commelin (Dec 29 2021 at 10:38):
It's been a long time since the last mathlib bump. I'm trying one now, and it's quite messy :see_no_evil: :rofl:
The biggest pain is in src/for_mathlib/abelian_sheaves/main.lean. I think I've fixed almost all the other trouble.
I've pushed my progress to branch bump-29-Dec-21.
Johan Commelin (Dec 29 2021 at 10:38):
Now I need to prepare some lunch
Johan Commelin (Dec 29 2021 at 10:40):
Concerning fixing sheafy stuff: since the last mathlib bump, sheaves and sheaf homs now have dedicated structures as their defs.
So a sheaf must be defined as { val := ..., cond := ... } and a hom as ⟨...⟩ or more precisely { val := ... }.
Adam Topaz (Dec 29 2021 at 11:47):
I'll try to fix up main.lean now...
Adam Topaz (Dec 29 2021 at 11:48):
(before my laptop battery dies ;))
Johan Commelin (Dec 29 2021 at 12:26):
Great! Thanks a lot
Adam Topaz (Dec 29 2021 at 12:32):
main.lean is fixed and my laptop still has 44% battery. I'll try to build locally to see what else breaks.
Johan Commelin (Dec 29 2021 at 12:34):
There's an error in condensed/ab.lean
Johan Commelin (Dec 29 2021 at 12:34):
That seems to be the only thing remaining.
Adam Topaz (Dec 29 2021 at 12:35):
Still building the necessary oleans for me...
Adam Topaz (Dec 29 2021 at 12:40):
ok, ab.lean was very easy to fix.
Adam Topaz (Dec 29 2021 at 12:42):
@Andrew Yang I'm working on getting the left exactness of sheafification into mathlib as well... I have a branch called branch#left_exact_sheafification with the proof more-or-less done, just very slow.
Andrew Yang (Dec 29 2021 at 12:43):
Thats great! looking forward to the result.
Johan Commelin (Dec 29 2021 at 12:43):
So we can merge the bump into master now?
Adam Topaz (Dec 29 2021 at 12:44):
If it builds, sure!
Adam Topaz (Dec 29 2021 at 12:44):
I'm still building on my end...
Adam Topaz (Dec 29 2021 at 12:44):
If you're done building, feel free to merge Johan
Johan Commelin (Dec 29 2021 at 12:45):
Yep, done (and pushed)
Johan Commelin (Jan 04 2022 at 09:12):
I did another mathlib bump.
Johan Commelin (Jan 04 2022 at 09:12):
This is the current sorry count:
1 src/challenge.lean
6 src/condensed/basic.lean
21 src/condensed/ab.lean
2 src/condensed/adjunctions.lean
3 src/condensed/proj_cond.lean
2 src/condensed/is_proetale_sheaf.lean
1 src/Mbar/functor.lean
32 src/laurent_measures/thm69.lean
2 src/laurent_measures/basic.lean
5 src/for_mathlib/concrete_multiequalizer.lean
4 src/for_mathlib/homological_complex_abelian.lean
1 src/for_mathlib/split_exact.lean
2 src/for_mathlib/derived_functor.lean
2 src/for_mathlib/abelian_group_object.lean
1 src/for_mathlib/homological_complex.lean
3 src/for_mathlib/mapping_cone.lean
2 src/for_mathlib/homological_complex_shift_jmc.lean
1 src/for_mathlib/short_exact_sequence.lean
1 src/for_mathlib/Profinite/extend.lean
1 src/for_mathlib/Profinite/disjoint_union.lean
9 src/for_mathlib/abelian_sheaves/left_exact-backup.lean
5 src/for_mathlib/abelian_sheaves/main.lean
Total: 107
Adam Topaz (Jan 04 2022 at 15:36):
for_mathlib/abelian_sheaves/left_exact-backup.lean can be removed to reduce the count by 9.
Johan Commelin (Jan 04 2022 at 15:37):
Which would instantly bring us below 100 :rofl:
Adam Topaz (Jan 04 2022 at 15:38):
But wait, there's more! I think the strategy in for_mathlib/abelian_group_object.lean has been abandoned. We can at least comment out the code in that file.
Adam Topaz (Jan 04 2022 at 15:39):
That reminds me... I should finish off the PR on left exactness. Would you mind looking at #11154 which will be used in the left-exactness work?
Johan Commelin (Jan 04 2022 at 15:48):
Looking at it now
Filippo A. E. Nuccio (Jan 04 2022 at 16:36):
In thm69.lean there are things which are now abandoned, so I guess the count will also drop as soon as I comment them (later tonight)
Johan Commelin (Jan 05 2022 at 17:33):
Adam Topaz said:
for_mathlib/abelian_sheaves/left_exact-backup.leancan be removed to reduce the count by 9.
Since this is now in mathlib, I can just completely trash the file, right?
Adam Topaz (Jan 05 2022 at 17:33):
yes, and also the for_mathlib/src/abelian_sheaves/left_exact.lean file once mathlib is bumped.
Johan Commelin (Jan 05 2022 at 17:36):
I will start a bump now
Filippo A. E. Nuccio (Jan 05 2022 at 17:37):
OK, I won't push things until you are done, then.
Johan Commelin (Jan 05 2022 at 19:09):
I've pushed to 05-Jan-22-bump-mathlib. Somehow the new left_exact.lean doesn't slot in perfectly with the old one.
Johan Commelin (Jan 05 2022 at 19:09):
So now some instance about preserving limits can't be found.
Adam Topaz (Jan 05 2022 at 19:13):
I'll take a look soon
Adam Topaz (Jan 05 2022 at 19:27):
Which file has the error?
Johan Commelin (Jan 05 2022 at 19:29):
main.lean
Adam Topaz (Jan 05 2022 at 19:35):
annoying... the missing thing was the fact that abelian categories have finite limits. I just added [has_finite_limits A], and it's fixed.
Adam Topaz (Jan 05 2022 at 19:35):
At some point I'll do this properly and deduce the instance from [abelian A].
Johan Commelin (Jan 05 2022 at 19:36):
aah, thanks a lot for fixing!
Johan Commelin (Jan 05 2022 at 19:36):
This solved both errors in that file?
Adam Topaz (Jan 05 2022 at 19:36):
pushed to the branch.
Johan Commelin (Jan 05 2022 at 19:36):
Ok, I will compile
Johan Commelin (Jan 05 2022 at 19:48):
@Adam Topaz what is the purpose of for_mathlib/concrete_filtered_colimit_commutes.lean? It doesn't seem to be imported atm
Johan Commelin (Jan 05 2022 at 19:49):
Pushed mathlib bump to master.
Adam Topaz (Jan 05 2022 at 19:51):
Oh, that whole file can be removed.
Adam Topaz (Jan 05 2022 at 19:55):
Adam Topaz (Jan 05 2022 at 19:57):
Johan Commelin said:
Adam Topaz what is the purpose of
for_mathlib/concrete_filtered_colimit_commutes.lean? It doesn't seem to be imported atm
The content of that file was more-or-less done in #11154
Johan Commelin (Jan 05 2022 at 19:59):
I see, that's sort of what I was guessing.
Johan Commelin (Jan 05 2022 at 19:59):
Just wanted to double check.
Adam Topaz (Jan 05 2022 at 19:59):
Sorry, I've been bad about cleaning up after myself in for_mathlib/...
Johan Commelin (Jan 05 2022 at 19:59):
Adam Topaz said:
Oh, that whole file can be removed.
done
Johan Commelin (Jan 05 2022 at 21:00):
@Adam Topaz The comment above the sorrys in src/condensed/adjunctions.lean is now no longer accurate, right? Do you still want to keep those sorryd examples?
Adam Topaz (Jan 05 2022 at 21:14):
Yeah, those comments can be removed!
Adam Topaz (Jan 05 2022 at 21:25):
I removed the comments
Filippo A. E. Nuccio (Jan 06 2022 at 14:56):
The leanproject pull command seems to give an error after yesterday's bump; I get
$ leanproject pull
Pulling from origin
SHA b'9fd7a02d03ba2ea9786eea4bf547b2c51e56ed6a' could not be resolved, git returned: b'9fd7a02d03ba2ea9786eea4bf547b2c51e56ed6a missing'
Adam Topaz (Jan 06 2022 at 14:58):
Does git pull work?
Filippo A. E. Nuccio (Jan 06 2022 at 14:58):
Yes, it does
Kevin Buzzard (Jan 06 2022 at 14:58):
Try removing the _target directory
Adam Topaz (Jan 06 2022 at 14:58):
maybe a bug in leanproject?
Filippo A. E. Nuccio (Jan 06 2022 at 14:59):
Kevin Buzzard said:
Try removing _target
You mean by brute force? Just throw it away?
Riccardo Brasca (Jan 06 2022 at 14:59):
I usually try a leanproject build in this case
Riccardo Brasca (Jan 06 2022 at 14:59):
If it starts compiling everything try leanproject get-mathlib-cache
Filippo A. E. Nuccio (Jan 06 2022 at 14:59):
Well,
Riccardo Brasca said:
I usually try a
leanproject buildin this case
I did a leanproject up (which works)
Filippo A. E. Nuccio (Jan 06 2022 at 15:00):
Trying with build...
Johan Commelin (Jan 06 2022 at 15:09):
leanproject up starts a mathlib bump.
Johan Commelin (Jan 06 2022 at 15:09):
So now you have a mathlib in your _target that is newer than it was a few minutes ago. And so the build might be broken.
Filippo A. E. Nuccio (Jan 06 2022 at 15:10):
Ah, I see. OK.
Filippo A. E. Nuccio (Jan 06 2022 at 15:10):
Then I'd rather simply trash my current folder and clone a fresh new one.
Johan Commelin (Jan 06 2022 at 15:11):
Well, please make sure you don't throw away stuff that you haven't pushed to github
Filippo A. E. Nuccio (Jan 06 2022 at 15:11):
Yes, I am sure (I pulled yesterday and haven't done anything today yet).
Filippo A. E. Nuccio (Jan 06 2022 at 15:12):
Still, the problem with leanproject pull is strange, no?
Riccardo Brasca (Jan 06 2022 at 15:23):
I've got the same error in flt-regular, but not anymore. Maybe leanproject has been updated?
Filippo A. E. Nuccio (Jan 06 2022 at 15:24):
@Patrick Massot ?
Riccardo Brasca (Jan 06 2022 at 15:26):
leanproject --version says 1.1.0
Filippo A. E. Nuccio (Jan 06 2022 at 15:31):
BTW, shouldn't the flt appear also here?
Eric Rodriguez (Jan 06 2022 at 19:34):
You should remove _target (which just has mathlib and maybe gptf) and then leanproject pull/leanpkg configure
Eric Rodriguez (Jan 06 2022 at 19:34):
If you always leanproject pull this shouldn't happen but I agree, it's pretty wild that the tooling fails completely if it's done mildly incorrectly once
Filippo A. E. Nuccio (Jan 07 2022 at 12:11):
Just for the record; after I have deleted the local folder lean_liquid and cloned a new one, leanproject pull is working again like a charm.
Adam Topaz (Jan 07 2022 at 15:16):
Just cleaning up a bit:
$ git diff 17cbfe3c8e445ccba03833ee81fcbf8c1ae37283 --stat
src/for_mathlib/concrete.lean | 51 ---------
src/for_mathlib/concrete_filtered_colimit_commutes.lean | 304 ----------------------------------------------------
src/for_mathlib/concrete_multiequalizer.lean | 89 ---------------
src/for_mathlib/evaluation_adjunction.lean | 65 -----------
src/for_mathlib/is_sheaf.lean | 19 ----
src/for_mathlib/limit_obj.lean | 17 ---
6 files changed, 545 deletions(-)
Adam Topaz (Jan 07 2022 at 15:25):
Oops! I broke the build... but leanproject build succeeds on my machine with these files deleted.
Adam Topaz (Jan 07 2022 at 15:39):
Does leanproject build not ignore the zombie oleans before building?
Kevin Buzzard (Jan 07 2022 at 15:50):
Doesn't import foo just work in the presence of either foo.lean or foo.olean?
Adam Topaz (Jan 07 2022 at 15:51):
yeah, that's exactly the issue. I had oleans for files that I deleted, so my local leanproject build happily completed and I pushed to master on github only to get an angry email from CI.
Adam Topaz (Jan 07 2022 at 15:51):
anyway, I'm fixing it now...
Adam Topaz (Jan 07 2022 at 15:53):
BTW, is there some flag I can pass to leanproject build that will make it so that the warning: imported file ... uses sorry messages don't show up, but any build errors still show up?
Kevin Buzzard (Jan 07 2022 at 17:41):
Are the warnings going to STDOUT and the errors to STDERR?
Adam Topaz (Jan 07 2022 at 17:42):
I'm not sure. let me check.
Adam Topaz (Jan 07 2022 at 17:45):
ok, so the ... uses sorry messages are not sent to stderr.
Adam Topaz (Jan 07 2022 at 17:45):
at least they still appear with leanproject build 2>/dev/null
Adam Topaz (Jan 07 2022 at 17:46):
and it seems that actual build errors also are not sent to stderr.
Kevin Buzzard (Jan 07 2022 at 17:50):
open an issue? I'm not really a computer scientist but I'm a bit surprised about this. Or is it normal?
Adam Topaz (Jan 07 2022 at 17:57):
I suppose these messages come from lean itself?
Alex J. Best (Jan 07 2022 at 18:14):
Right these errors do come from Lean, and all go to stdout, I couldn't see any built in way using lean or leanproject to filter these out.
Probably some simple shell script can do this too but one fairly easy way to manually filter these out is using the json output mode and using https://stedolan.github.io/jq/ like so:
$ lean --json src/s.lean | jq 'select(.severity == "error")'
{
"caption": "",
"file_name": "/home/alex/test/src/s.lean",
"pos_col": 19,
"pos_line": 3,
"severity": "error",
"text": "type mismatch, term\n trivial\nhas type\n true\nbut is expected to have type\n false"
}
doing the inverse filter gets you the opposite
$ lean --json src/s.lean | jq 'select(.severity == "warning")'
{
"caption": "",
"file_name": "/home/alex/test/src/t.lean",
"pos_col": 0,
"pos_line": 1,
"severity": "warning",
"text": "declaration 't' uses sorry"
}
{
"caption": "",
"file_name": "/home/alex/test/src/s.lean",
"pos_col": 0,
"pos_line": 1,
"severity": "warning",
"text": "imported file '/home/alex/test/src/t.lean' uses sorry"
}
you can pretty easily configure this to only print out the actual file name and text of the errors or put it in whatever format you want, or even only filter warnings containing the string sorry and leave the rest.
Adam Topaz (Jan 07 2022 at 18:14):
Nice.
Adam Topaz (Jan 07 2022 at 18:14):
I was going to hack something together with sed, but I like jq ;)
Alex J. Best (Jan 07 2022 at 18:19):
Yeah it even nicely formats and colorizes. This seems a decent setup: lean --json src/s.lean | jq 'select(.severity == "error") | [{"name":.file_name,"error":.text, "line":.pos_line}]'
Johan Commelin (Jan 08 2022 at 06:32):
'nother day, 'nother mathlib bump
Johan Commelin (Jan 08 2022 at 06:32):
We're now down to 90 sorrys:
1 src/challenge.lean
6 src/condensed/basic.lean
21 src/condensed/ab.lean
3 src/condensed/proj_cond.lean
2 src/condensed/is_proetale_sheaf.lean
1 src/Mbar/functor.lean
34 src/laurent_measures/thm69.lean
2 src/laurent_measures/basic.lean
4 src/for_mathlib/homological_complex_abelian.lean
1 src/for_mathlib/homological_complex.lean
3 src/for_mathlib/mapping_cone.lean
2 src/for_mathlib/homological_complex_shift_jmc.lean
1 src/for_mathlib/short_exact_sequence.lean
1 src/for_mathlib/Profinite/extend.lean
2 src/for_mathlib/derived_functor.lean
5 src/for_mathlib/abelian_sheaves/main.lean
1 src/for_mathlib/split_exact.lean
Total: 90
Johan Commelin (Jan 10 2022 at 05:15):
And down to 75!
1 src/challenge.lean
6 src/condensed/basic.lean
21 src/condensed/ab.lean
3 src/condensed/proj_cond.lean
2 src/condensed/is_proetale_sheaf.lean
1 src/Mbar/functor.lean
23 src/laurent_measures/thm69.lean
2 src/laurent_measures/basic.lean
2 src/for_mathlib/derived_functor.lean
1 src/for_mathlib/split_exact.lean
1 src/for_mathlib/homological_complex.lean
3 src/for_mathlib/mapping_cone.lean
2 src/for_mathlib/homological_complex_shift_jmc.lean
1 src/for_mathlib/Profinite/extend.lean
1 src/for_mathlib/short_exact_sequence.lean
5 src/for_mathlib/abelian_sheaves/main.lean
Total: 75
Adam Topaz (Jan 10 2022 at 12:24):
The 5 sorry's in abelian_sheaves/main are in a comment ;)
Adam Topaz (Jan 10 2022 at 12:24):
ditto for the one in Profinite/extend
Adam Topaz (Jan 10 2022 at 12:27):
and the two in laurent_measures/basic
Johan Commelin (Jan 10 2022 at 12:30):
Ok, I will replace them with (by) admit to make the sorry count a bit more accurate
Adam Topaz (Jan 10 2022 at 12:30):
Unfortunately, I think the sorry in Mbar/functor is wrong, but it should be okay (and even sorry-free) if we replace ProFiltPseuNormGrpWithTinv with ProFiltPseuNormGrpWithTinv₁
Adam Topaz (Jan 10 2022 at 12:31):
Andrew Yang (Jan 10 2022 at 12:33):
The two in mapping_cone.lean are commented out as well.
Johan Commelin (Jan 10 2022 at 12:34):
Ok, I will update those as well
Johan Commelin (Jan 10 2022 at 12:34):
1 src/challenge.lean
6 src/condensed/basic.lean
21 src/condensed/ab.lean
3 src/condensed/proj_cond.lean
2 src/condensed/is_proetale_sheaf.lean
1 src/Mbar/functor.lean
23 src/laurent_measures/thm69.lean
2 src/for_mathlib/derived_functor.lean
1 src/for_mathlib/homological_complex.lean
1 src/for_mathlib/mapping_cone.lean
1 src/for_mathlib/short_exact_sequence.lean
1 src/for_mathlib/split_exact.lean
Total: 63
Andrew Yang (Jan 10 2022 at 12:35):
btw what's homological_complex_shift_jmc.lean?
Johan Commelin (Jan 10 2022 at 12:35):
Old cruft. I think it should be removed.
Johan Commelin (Jan 10 2022 at 12:36):
Aah, it's not even checked into git. It's just a random file I had locally.
Johan Commelin (Jan 10 2022 at 12:37):
Bamm, down to 63 (-;
Johan Commelin (Jan 10 2022 at 12:37):
Cheap way of getting rid of sorrys :octopus:
Adam Topaz (Jan 10 2022 at 12:38):
leanproject sorrycount should be a thing.
Mario Carneiro (Jan 10 2022 at 12:38):
the easiest way to get rid of a sorry is to delete the theorem :grinning:
Johan Commelin (Jan 10 2022 at 12:41):
This is my sorrycount:
rg -l sorry | rg -v scripts | xargs -I % sh -c 'nsorry=`rg sorry % | wc -l`; echo -n "$nsorry\t%\n"'; echo -en "Total:\t"; rg sorry | rg -v scripts | wc -l
Johan Commelin (Jan 10 2022 at 12:42):
@Adam Topaz Do you think the sorry in Mbar/functor is now tractable, after we add the ₁s?
Adam Topaz (Jan 10 2022 at 12:43):
yeah, it should just be taken care of by tc resolution in fact
Johan Commelin (Jan 10 2022 at 12:44):
I'm building :fencing: right now, but I'll try it afterwards.
Adam Topaz (Jan 10 2022 at 12:44):
If you need the functor to land in the category without the , we have the canonical functors from foo_1 to foo.
Johan Commelin (Jan 10 2022 at 12:44):
It should also be possible to fix ≥ 10 of the sorrys in condensed/ab.lean, I think.
Adam Topaz (Jan 10 2022 at 12:45):
yeah, it should be. I'll try to fix some of those a little later (if they're still there)
Johan Commelin (Jan 10 2022 at 12:56):
The sorry in Mbar/functor is fixed.
Kevin Buzzard (Jan 10 2022 at 21:10):
Filippo A. E. Nuccio said:
The
leanproject pullcommand seems to give an error after yesterday'sbump; I get$ leanproject pull Pulling from origin SHA b'9fd7a02d03ba2ea9786eea4bf547b2c51e56ed6a' could not be resolved, git returned: b'9fd7a02d03ba2ea9786eea4bf547b2c51e56ed6a missing'
I just ran into this issue on another repo, after a git pull changed leanpkg.toml. I accidentally typed leanproject get-c instead of leanproject get-m (I don't know if this had anything to do with it). After leanproject get-m I got the dreaded "SHA could not be resolved" error. I fixed it by leanproject build and then breaking out of the build (it was compiling mathlib) and then leanproject get-m again, and then leanproject build worked fine.
Eric Wieser (Jan 11 2022 at 00:20):
Can you open an issue on the mathlibtools git repository?
Kevin Buzzard (Jan 11 2022 at 06:47):
I've told Patrick many times that I don't understand the workflow when someone else bumps mathlib and hence changes leanpkg.toml in a joint project with mathlib as a dependency. All that's happened is that the error message has changed recently
Riccardo Brasca (Jan 11 2022 at 06:50):
I used to have the same problem. I now only use leanproject pull and everything works.
Kevin Buzzard (Jan 11 2022 at 06:51):
Ah that's right, I think this is the command he wrote when I complained the last time. My problem is that I don't remember this command, nothing more
Kevin Buzzard (Jan 11 2022 at 06:51):
I remember the workarounds
Johan Commelin (Jan 11 2022 at 14:31):
bumped mathlib. We're now on lean 3.37.0c and default no longer takes an explicit argument. Otherwise, uneventful bump.
Johan Commelin (Jan 12 2022 at 10:06):
Another mathlib bump. We're now on lean 3.38.0c. This means that simp is more powerful, and a bunch of congrs could be removed.
@Filippo A. E. Nuccio I made a couple of changes to thm69.lean. So be aware :wink:
Filippo A. E. Nuccio (Jan 13 2022 at 17:37):
I have just killed 15 sorries.
Johan Commelin (Jan 13 2022 at 17:58):
That's the definition of progress :rofl:
Johan Commelin (Jan 13 2022 at 17:58):
1 src/challenge.lean
6 src/condensed/basic.lean
4 src/condensed/ab.lean
2 src/condensed/top_comparison.lean
2 src/condensed/is_proetale_sheaf.lean
1 src/combinatorial_lemma/profinite.lean
11 src/laurent_measures/thm69.lean
2 src/for_mathlib/derived_functor.lean
1 src/for_mathlib/split_exact.lean
1 src/for_mathlib/homological_complex.lean
1 src/for_mathlib/mapping_cone.lean
1 src/for_mathlib/short_exact_sequence.lean
Total: 33
Johan Commelin (Jan 13 2022 at 17:58):
Big congrats, @Filippo A. E. Nuccio !!
Adam Topaz (Jan 13 2022 at 19:32):
... And I just increased the sorry count (in condensed/extr)
Adam Topaz (Jan 13 2022 at 20:42):
The file condensed/extr now has 15 sorrys, so I counteracted all of the progress that Filippo has made.
On the other hand, all of these sorry's are props, some are more doable than others, and they should give the equivalence between Condensed C and ExtrSheaf C (which is some version of sheaves on ExtrDisc, the category of projective objects in Profinite).
Filippo A. E. Nuccio (Jan 13 2022 at 20:43):
Ok, I'll try my best to insert at least 6 sorries ASAP! :stuck_out_tongue_wink:
Johan Commelin (Jan 18 2022 at 07:00):
@Ben Toner Thanks so much for fix the build!
Adam Topaz (Jan 22 2022 at 02:54):
I just bumped mathlib. Just a reminder to refresh your oleans!
Andrew Yang (Jan 23 2022 at 09:27):
mathlib bumped again. Please refresh your oleans.
Damiano Testa (Jan 25 2022 at 09:01):
I believe that I just did a bump: as this was my (almost) first time, I hope that I did not mess anything up!
The most important change was the addition of open_locale pointwise for the category stuff.
Riccardo Brasca (Jan 25 2022 at 09:05):
Looking at your last commit, you didn't change leanpkg.toml, so you didn't actually bumped mathlib. Have you done leanproject up?
Johan Commelin (Jan 25 2022 at 09:05):
Looks good. Thanks!
Johan Commelin (Jan 25 2022 at 09:05):
Hmm, when I did a git pull just now, leanpkg.toml was changed.
Johan Commelin (Jan 25 2022 at 09:05):
Was that from an earlier commit?
Riccardo Brasca (Jan 25 2022 at 09:05):
I am talking about 7b3e09e
Riccardo Brasca (Jan 25 2022 at 09:07):
But the bot updated mathlib in 2adc6eb, so probably no manual intervention was needed.
Johan Commelin (Jan 25 2022 at 09:07):
The toml now points to
commit 32cd27879f81e108b4537c4f2ca64701f765dc83
Author: Yury G. Kudryashov <urkud@urkud.name>
Date: Mon Jan 24 03:52:26 2022 +0000
which seems good to me.
Damiano Testa (Jan 25 2022 at 09:59):
Ok, I am glad that it worked! I did not touch the toml file, since it scares me. My flow was
leanproject up
leanproject get-m #probably unnecessary
leanproject build
repeat {fix, build}
Riccardo Brasca (Jan 25 2022 at 10:17):
leanproject up modifies the file for you. It didn't in this case because it was already up-to-date
Adam Topaz (Jan 25 2022 at 14:52):
I'm curious about this fix bash script you have Damiano...
Johan Commelin (Jan 31 2022 at 08:18):
I just pushed a trivial bump. But this does mean that we have access to some of the goodies that @Arthur Paulino pushed to mathlib recently.
Johan Commelin (Feb 04 2022 at 07:47):
bumped
Johan Commelin (Feb 04 2022 at 07:47):
Sorry count:
1 src/challenge.lean
3 src/condensed/basic.lean
2 src/condensed/ab.lean
2 src/condensed/is_proetale_sheaf.lean
8 src/laurent_measures/aux_lemmas.lean
2 src/for_mathlib/derived_functor.lean
1 src/for_mathlib/homological_complex.lean
1 src/for_mathlib/short_exact_sequence.lean
Total: 20
Riccardo Brasca (Feb 17 2022 at 09:32):
Bumbed again.
Riccardo Brasca (Feb 17 2022 at 11:33):
I don't know why but leanproject didn't pick the last mathlib, so I bumped again.
Alex J. Best (Feb 17 2022 at 13:04):
The reason is https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/lean-3.2E39.2E1.20branch.20not.20updating/near/272249334, so probably using leanproject up will bump down until that process does its business and tags mathlib branches again
Riccardo Brasca (Mar 01 2022 at 14:16):
Bumped.
Johan Commelin (Mar 10 2022 at 16:00):
commit 0d4e3e7ca25671add2f585ec44baccd43fa454ac (HEAD -> master)
Author: Johan Commelin <johan@commelin.net>
Date: Thu Mar 10 15:59:52 2022 +0000
bump mathlib
leanpkg.toml | 2 +-
src/Lbar/ses.lean | 3 ++-
src/for_mathlib/derived_functor_zero.lean | 36 +++++++++++++++++-------------------
src/for_mathlib/homology.lean | 48 ------------------------------------------------
src/for_mathlib/homotopy_category.lean | 33 ++++++++++++++++++++++++++++++---
src/for_mathlib/mapping_cone.lean | 2 +-
src/for_mathlib/short_exact_sequence.lean | 18 +++++++++++++++++-
src/laurent_measures/simpler_laurent_measures.lean | 4 +---
src/laurent_measures/theta.lean | 5 ++++-
src/pseudo_normed_group/profinitely_filtered.lean | 66 +++++++++++++++++++++++++++++++++++++++++++-----------------------
10 files changed, 116 insertions(+), 101 deletions(-)
Johan Commelin (Mar 10 2022 at 16:00):
Mathlib changed quite a bit in the last two weeks.
Riccardo Brasca (Mar 20 2022 at 11:34):
Bumped.
leanpkg.toml | 4 +-
src/Lbar/basic.lean | 4 +-
src/challenge.lean | 1 +
src/for_mathlib/derived_functor_zero.lean | 286 +++++++-------------------------------------------------------------------------------------------------------------
src/for_mathlib/is_biprod.lean | 2 +-
src/for_mathlib/pid.lean | 9 ++--
src/for_mathlib/projective_replacement.lean | 2 +
src/laurent_measures/aux_lemmas.lean | 2 +-
src/laurent_measures/basic.lean | 2 +-
src/laurent_measures/bounded.lean | 2 +-
src/laurent_measures/int_nat_shifts.lean | 2 +-
src/laurent_measures/no_longer_needed_maybe.lean | 2 +-
src/real_measures/basic.lean | 2 +-
src/system_of_complexes/completion.lean | 2 +-
14 files changed, 35 insertions(+), 287 deletions(-)
Riccardo Brasca (Mar 20 2022 at 13:53):
The linter gives now an error I don't understand
/home/runner/work/lean-liquid/lean-liquid/scripts/lint_project.lean:9:0: error: invalid import: category_theory.abelian.homology
invalid object declaration, environment already has an object named 'category_theory.abelian.homology_c._proof_1'
Unfortunately I don't have time today to investigate this.
Adam Topaz (Mar 20 2022 at 14:30):
It happens when there are two automatically generated lemmas that are named the same. It looks like for_mathlib/homology needs to be cleaned up after the bump.
Riccardo Brasca (Mar 21 2022 at 11:27):
Bumped again, and fixed the problem with homology.
Johan Commelin (Apr 07 2022 at 14:58):
I've pushed a start to mathlib-bump-07-apr-22
Johan Commelin (Apr 07 2022 at 14:58):
need to run to my train now
Johan Commelin (Apr 07 2022 at 15:09):
todo: rename pseudo_exact_of_exact to use dot-notation
Johan Commelin (Apr 07 2022 at 15:13):
Afaict the proof of thm9.5 should work without problems again. Of course the tricky part is bumping all the homological stuff, because exact is no longer a typeclass. But it seems to be pretty straightforward.
Johan Commelin (Apr 07 2022 at 17:39):
TODO: abelian.category_theory.limits.cokernel.desc.category_theory.mono is a real name
Yaël Dillies (Apr 07 2022 at 17:58):
How hard would it be to make autogenerated instance names not add the same namespace several times?
Johan Commelin (Apr 07 2022 at 19:24):
mathlib bump is done
Johan Commelin (Apr 07 2022 at 19:24):
hopefully oleans will be ready in a couple of minutes
Johan Commelin (Apr 22 2022 at 09:40):
I'm starting another mathlib bump
Johan Commelin (Apr 22 2022 at 18:43):
That was a most awful bump
leanpkg.toml | 2 +-
src/breen_deligne/functorial_map.lean | 4 ++--
src/challenge.lean | 4 ++--
src/condensed/acyclic.lean | 2 +-
src/condensed/exact.lean | 2 +-
src/condensed/projective_resolution.lean | 6 ++----
src/for_mathlib/AddCommGroup/kernels.lean | 8 ++++----
src/for_mathlib/abelian_category.lean | 74 ++++++++++++++++++++++++++++----------------------------------------------
src/for_mathlib/abelian_sheaves/functor_category.lean | 12 ++++++++----
src/for_mathlib/acyclic.lean | 4 +++-
src/for_mathlib/delta_functor.lean | 4 ++--
src/for_mathlib/derived/bounded_homotopy_category.lean | 55 +++++++++++++++++++++++++++++++++++++++----------------
src/for_mathlib/derived/derived_cat.lean | 42 ++++++++++++++++++++++++++----------------
src/for_mathlib/derived/example.lean | 19 +++++++++++--------
src/for_mathlib/derived/lemmas.lean | 3 +--
src/for_mathlib/derived/les_facts.lean | 2 +-
src/for_mathlib/exact_seq2.lean | 4 ++--
src/for_mathlib/free_abelian_group.lean | 4 ++--
src/for_mathlib/homological_complex_abelian.lean | 10 ++++++----
src/for_mathlib/homological_complex_equiv_functor_category.lean | 8 ++++----
src/for_mathlib/homology_exact.lean | 31 +++++++++++++++++++++----------
src/for_mathlib/homotopy_category.lean | 20 +++++++++++++++-----
src/for_mathlib/homotopy_category_pretriangulated.lean | 10 ++++++++--
src/for_mathlib/les_homology.lean | 14 ++++----------
src/for_mathlib/mapping_cone.lean | 43 +++++++++++++++++++++++++++++++++++++++----
src/for_mathlib/pid.lean | 3 +--
src/for_mathlib/projective_replacement.lean | 30 +++++++-----------------------
src/for_mathlib/sheafification_mono.lean | 45 +++++++++------------------------------------
src/for_mathlib/simplicial/complex.lean | 2 +-
src/for_mathlib/split_exact.lean | 18 +++++++++++++-----
src/free_pfpng/acyclic.lean | 10 +++-------
src/invpoly/basic.lean | 2 +-
src/laurent_measures/basic.lean | 2 +-
src/laurent_measures/ses.lean | 2 +-
src/laurent_measures/thm69.lean | 2 +-
src/polyhedral_lattice/cech.lean | 2 +-
src/prop819.lean | 2 ++
src/pseudo_normed_group/LC.lean | 2 +-
src/rescale/LC.lean | 2 +-
src/thm95/constants/default.lean | 1 -
src/thm95/homotopy.lean | 2 +-
41 files changed, 277 insertions(+), 237 deletions(-)
Johan Commelin (Apr 22 2022 at 18:43):
But it solved a very annoying sorry.
Johan Commelin (Apr 22 2022 at 18:44):
At the same time for_mathlib/derived/derived_cat.lean is timing out like crazy. So I've had to introduce a few sorrys there.
Johan Commelin (Apr 22 2022 at 18:44):
On my hardware at home, there is no way I can fix that file.
Peter Scholze (Apr 22 2022 at 19:07):
If and when the time comes that we'll all be asked to write computer-checked proofs, will access to insane computer clusters become critical to pure math research? (With the bonus question: Is the required electricity/energy worth it in times of climate change?)
Johan Commelin (Apr 22 2022 at 19:16):
It's a question that we can still ignore for a little time, but not for too long, I guess. It's not clear to me what the cause of these speed issues is. At least they don't seem to be exponential, otherwise we would have been forced to a grinding halt quite a while ago.
Once LTE is over, I think there's some interesting CS / engineering questions to be answered about the repo.
Eric Rodriguez (Apr 22 2022 at 20:00):
I was messing around with this and got rid of the first 4 sorries, but this managed to make shift_functor_localization_functor time out. How could this even be? The first four sorries are not data...
Eric Rodriguez (Apr 22 2022 at 20:00):
or does LTE use a bigger timeout value than mathlib?
Adam Topaz (Apr 23 2022 at 01:20):
I'm going to attempt to look at derived_cat.lean on my dinky laptop. Wish me luck!
Adam Topaz (Apr 23 2022 at 01:57):
Okay, I finished off all the remaining sorries in derived_cat.lean.
Johan Commelin (Apr 23 2022 at 06:19):
Wow, I'm impressed! How did you avoid all the timeouts? I really couldn't work with the file.
Adam Topaz (Apr 23 2022 at 10:57):
I didn't really have any issues... I just got the necessary oleans from the imports using lean --make foobar.lean, which did take a little while, but once that was done I didn't hit any timeouts.
My vscode settings are
- Memory: 16000
- Time limit: 200000
Are these unusually high?
Eric Rodriguez (Apr 23 2022 at 11:16):
Ahh, I had 100000 time limit, I think that's why. It's higher than the mathlib one, not that high, though. I similarly found editing the file to be okay!
Johan Commelin (Apr 23 2022 at 11:24):
I also had 100000, just increased it to 200000. And I had 12GB memory, which I've increased to 16GB.
Scott Morrison (Apr 25 2022 at 12:32):
I would like for_mathlib/abelian_sheaves/functor_category.lean over in mathlib (setting up representation theory). I think this is yours, @Adam Topaz. I haven't looked at it beyond checking it has the results I need, but I can have a go at getting it PR ready.
Scott Morrison (Apr 25 2022 at 12:36):
I guess it mostly looks good, just a matter of finding homes for everything. The proof of nat_trans.coimage_image_comparison_app has suspiciously many dsimps, so perhaps some lemmas are still missing.
Scott Morrison (Apr 25 2022 at 12:43):
On the other hand, maybe I'll just do it from scratch. I think there's no point doing these special constructions with kernels and cokernels in the functor category. At the end of the day we're assuming D is abelian, so the functor category already has all finite limits and colimits by existing abstract nonsense, which you can compute pointwise.
Adam Topaz (Apr 25 2022 at 13:22):
Sounds good to me @Scott Morrison !
Scott Morrison (Apr 25 2022 at 14:23):
Scott Morrison (Apr 25 2022 at 14:24):
Seems to work as hoped.
Johan Commelin (Apr 25 2022 at 15:35):
FYI: I'm doing a mathlib bump now. Shouldn't be hard this time. After your PR is merged we can do another bump.
Johan Commelin (Apr 25 2022 at 16:33):
My b0xen completed the bump while I had dinner.
Johan Commelin (May 12 2022 at 11:34):
I just bumped mathlib again. We now have limits in Ab for arbitrary small universes. Thanks @Scott Morrison
Johan Commelin (May 12 2022 at 11:35):
I didn't generalize limits all over the place, so I've just added .{u u} in many places.
Last updated: Dec 20 2023 at 11:08 UTC