Quivers: #17618 #17617 and #17665

Stream: PR reviews

[Rémi Bottinelli]

Hey, those PRs are rather small but I'd love for them to get merged to be able to do some more heavy work around quivers. Would welcome reviews! Thanks

[Scott Morrison]

If these could be modified to put to the new content for combinatorics.quiver.basic into a new file (e.g. .push) that would be good. I don't want these in the import path/porting path for all of category theory.

[Rémi Bottinelli]

Does that also hold for the cast part for arrows, that is #17617 ?

[Scott Morrison]

@Rémi Bottinelli, yes please.

[Rémi Bottinelli]

@Scott Morrison The first two PRs have been refactored

[Scott Morrison]

Merged one, left a note on the other; it needs a matching mathlib4 PR.

[Rémi Bottinelli]

Thanks! Is there any kind of guide on how to do this? I'm only vaguely aware of this port/synchronization effort so I'm not sure what doing such a PR involves.

[Scott Morrison]

Hopping on a plane now, but you can try #port-guide

[Scott Morrison]

Or look at other open PRs that are updating already ported files.

[Kevin Buzzard]

@Rémi Bottinelli I was about to do some porting work but for technical reasons I can't work on the file I wanted to work on. Do you want me to make this matching mathlib4 PR for you (or even livestream doing it whilst you watch?) Ping me if you're interested.

[Rémi Bottinelli]

@Kevin Buzzard gladly, yeah! I can arrange some time essentially any afternoon if you'd livestream it.

[Rémi Bottinelli]

@Scott Morrison … and I've updated the third PR too now: https://github.com/leanprover-community/mathlib/pull/17665

[Antoine Labelle]

@Scott Morrison For Cayley graphs and covering maps, we also need a version of docs#category_theory.single_obj for quivers, i.e. that doesn't assume you have a multiplication on the edge type. Do you think this should be independant of the category theory version or should we refactor docs#category_theory.single_obj to be based on the new quiver version?

[Rémi Bottinelli]

@Yaël Dillies re splitting this last PR: Is such PR hygiene really worth it? Isn't git bisect good enough that atomizing the PRs to this extent become more work than could even be theoretically beneficial?

[Rémi Bottinelli]

I'm always too eager to put a lot in a single PR, so I should definitely learn to play the other way around, but I also kind of feel bad about restarting the PR/CI process each time.

[Yaël Dillies]

I can't easily tell from the diff what was added and what was moved. If I want to figure it out, I need to check declarations one by one in both files.

[Yaël Dillies]

So either make a list of the new declarations, or split the PR.

[Rémi Bottinelli]

I'll make the list, then :) Thanks

[Rémi Bottinelli]

@Scott Morrison For the porting to mathlib4, should the PR be first merged in mathlib3 and only then ported? I'm not sure I understand from the guide.

[Ruben Van de Velde]

The mathlib 4 pr should be opened in parallel

[Rémi Bottinelli]

Ah, like this: https://github.com/leanprover-community/mathlib4/pull/799

[Rémi Bottinelli]

Do I need PR rights for mathlib4? Can I get them?

[Johan Commelin]

@Rémi Bottinelli Voila: https://github.com/leanprover-community/mathlib4/invitations

[Rémi Bottinelli]

That's fast, thanks!

[Rémi Bottinelli]

OK, here is the mathlib4 PR: https://github.com/leanprover-community/mathlib4/pull/858

[Johan Commelin]

@Rémi Bottinelli I haven't followed the quiver discussion. But I've kicked the ml4 PR on the queue already.

[Johan Commelin]

@Kyle Miller Could you please take a look at the ml3 PR #17617 ?

[Rémi Bottinelli]

Ah, actually in lean4, these are just rfl lemmas (I assume because of definitional eta for structs)… oh, well!

[Rémi Bottinelli]

I see we're also touching combinatorics/quiver/path.lean which is also synchronized with mathlib4.

[Rémi Bottinelli]

https://github.com/leanprover-community/mathlib4/pull/861
Here is a PR to synchronize the path.lean part. I'm waiting for a green light there to merge #17617 (which has Kyle's approval already).

[Rémi Bottinelli]

OK, I've now created https://github.com/leanprover-community/mathlib4/pull/971 to synchronize PR #17665

[Rémi Bottinelli]

I'm not sure exactly what the error on "Check that all files are imported" is, but I venture it's just because I added a new file?

[Yaël Dillies]

You need to add the import of your new file to Mathlib.lean

[Mario Carneiro]

yes, you want to run

find Mathlib -name "*.lean" | env LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean

to update Mathlib.lean

[Rémi Bottinelli]

Iirc, in mathlib3, the mathlib.lean file was generated automatically. Why is it changed here?

[Yaël Dillies]

Is there even a mathlib.lean in mathlib?

[Mario Carneiro]

there is an all.lean file made by a script

[Rémi Bottinelli]

(anyway, done and pushed, thanks for the help!)

[Yaël Dillies]

... which one has to run locally, right? I don't ever remember the script running automatically.

[Mario Carneiro]

but lean3 (in its role as package manager) doesn't use it when you lean --make src

[Mario Carneiro]

whereas lake build is lake build Mathlib which does need a top level file

[Rémi Bottinelli]

(Yael, thanks you're always so quick!!)

[Mario Carneiro]

anything not in that file is not built

[Mario Carneiro]

which means that if you have errors in unimported files then they might not be caught by CI without that extra step

[Yaël Dillies]

(I :eyes: )

[Rémi Bottinelli]

I need to stop hacking code together and learn lean4 properly in order to get this porting process faster

[Kevin Buzzard]

You can learn lean 4 by porting (this is how I learnt it). Just keep asking questions.

[Rémi Bottinelli]

Hey, could I ping again for #17665 ? Once it's approved I'll update the corresponding mathlib4 PR, but I'd like to get it merged. Thanks!