Zulip Chat Archive

Stream: graph theory

Topic: coordination/github projects


view this post on Zulip Alena Gusakov (Feb 03 2021 at 14:12):

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

view this post on Zulip Alena Gusakov (Feb 03 2021 at 14:13):

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

view this post on Zulip Alexandre Rademaker (Feb 04 2021 at 18:28):

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

view this post on Zulip Johan Commelin (Feb 04 2021 at 18:36):

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.

view this post on Zulip Alena Gusakov (Feb 04 2021 at 18:37):

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

view this post on Zulip Johan Commelin (Feb 04 2021 at 18:39):

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

view this post on Zulip Johan Commelin (Feb 04 2021 at 18:40):

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 (-;

view this post on Zulip Bhavik Mehta (Feb 04 2021 at 18:41):

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

view this post on Zulip Alena Gusakov (Feb 04 2021 at 18:41):

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

view this post on Zulip Alena Gusakov (Feb 04 2021 at 18:42):

But I'm just referring to the kanban boards lol

view this post on Zulip Johan Commelin (Feb 04 2021 at 18:42):

Ooooh! Yes, such a project is a great idea

view this post on Zulip Alena Gusakov (Feb 04 2021 at 18:42):

Okay cool :)

view this post on Zulip Kyle Miller (Feb 04 2021 at 18:44):

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

view this post on Zulip Alena Gusakov (Feb 04 2021 at 18:44):

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

view this post on Zulip Alena Gusakov (Feb 04 2021 at 18:47):

i grabbed one of the automated templates


Last updated: May 08 2021 at 22:13 UTC