coordination/github projects

Stream: graph theory

[Alena Gusakov]

Would it be cool if i made a project in the repository for graph theory? It might be easier to coordinate with each other if we sketch out the things we want to formalize

[Alena Gusakov]

I know that personally I'm kind of jumping around all over the place

[Alexandre Rademaker]

This is a nice idea. Mathlib at some point will need to be split into smaller parts, I think.

[Johan Commelin]

I don't think that splitting mathlib into pieces will be easy. There are tons of interdepencies. Even if a split is made, it will make later refactors and even PRs in general a lot harder.

[Alena Gusakov]

I more mean like one of these https://github.com/leanprover-community/mathlib/projects

[Johan Commelin]

Sure, you can do that. But not that a lot of those projects have trouble staying in sync with mathlib.

[Johan Commelin]

Mathlib moves very fast. As soon as you get stuff in mathlib, you make it the responsibility of the community to keep your stuff up to date. But if it's in a random project, then you have to do all the work yourself (-;

[Bhavik Mehta]

cough cough https://github.com/leanprover-community/lean-liquid :P

[Alena Gusakov]

Ah wait, from the url it looks like it's a link to this https://leanprover-community.github.io/lean_projects.html

[Alena Gusakov]

But I'm just referring to the kanban boards lol

[Johan Commelin]

Ooooh! Yes, such a project is a great idea

[Alena Gusakov]

Okay cool :)

[Kyle Miller]

:+1: to having something like a kanban board to keep track of what's being done and what's to be done

[Alena Gusakov]

https://github.com/leanprover-community/mathlib/projects/8

[Alena Gusakov]

i grabbed one of the automated templates