[Merged by Bors] - chore: forward port mathlib#17611, 18742, 18198, 18520#3389
[Merged by Bors] - chore: forward port mathlib#17611, 18742, 18198, 18520#3389Parcly-Taxel wants to merge 4 commits intomasterfrom
Conversation
|
Can you explain in the description why each of the SHA-only changes needs no forward-port? |
Ah, done. |
|
@Parcly-Taxel, please don't use numeric branch names: in some circumstances git is uncertain whether to interpret these as SHAs. |
|
bors merge |
SHA-only updates: * leanprover-community/mathlib3#17611 – `CategoryTheory.Sites.Sheaf` already uses `aesop_cat` at this location, nothing to port. * leanprover-community/mathlib3#18742 – fiber spelling, which is all of the changes to `Topology.FiberBundle.Trivialization`, is already in mathlib4. * leanprover-community/mathlib3#18198 – `FunLike` change to `Data.PEquiv` is already in mathlib4. Substantative forward port: * leanprover-community/mathlib3#18520 Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
SHA-only updates: * leanprover-community/mathlib3#17611 – `CategoryTheory.Sites.Sheaf` already uses `aesop_cat` at this location, nothing to port. * leanprover-community/mathlib3#18742 – fiber spelling, which is all of the changes to `Topology.FiberBundle.Trivialization`, is already in mathlib4. * leanprover-community/mathlib3#18198 – `FunLike` change to `Data.PEquiv` is already in mathlib4. Substantative forward port: * leanprover-community/mathlib3#18520 Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
|
https://leanprover-community.github.io/mathlib-port-status/out-of-sync On the dashboard, the forward port for mathlib#18520 does not seem to have come through. |
|
What do you mean by that? Also note that you have to write leanprover-community/mathlib3#18520 |
|
I realise now I got confused - I thought this fully forward-ported the connected components section, but this only does little bits of it. I'll work on the rest of that. Edit: I see now also that that's not possible yet as noted in the PR description. Sorry! |
SHA-only updates:
CategoryTheory.Sites.Sheafalready usesaesop_catat this location, nothing to port.Topology.FiberBundle.Trivialization, is already in mathlib4.fun_like,embedding_likemathlib3#18198 –FunLikechange toData.PEquivis already in mathlib4.Substantative forward port:
connected_componentmathlib3#18520category_theory.sites.sheaf@a67ec23dd8dc08195d77b6df2cd21f9c64989131..2efd2423f8d25fa57cf7a179f5d8652ab4d0df44topology.fiber_bundle.trivialization@f2ce6086713c78a7f880485f7917ea547a215982..be2c24f56783935652cefffb4bfca7e4b25d167edata.pequiv@ee0c179cd3c8a45aa5bffbf1b41d8dbede452865..7c3269ca3fa4c0c19e4d127cd7151edbdbf99ed4combinatorics.simple_graph.connectivity@13cd3e89b30352d5b1b7349f5537ea18ba878e40..e876965f7ee86f683b44e2f462ab5bfb47f993b3I have the diff that will forward port leanprover-community/mathlib3#18442 as well but it apparently depends on #3082 for a replacement for
rel_embedding.coe_coe_fn.