Visualising local growth of the project

Stream: FLT

[Kevin Buzzard]

I'm unhappy with the current state of the blueprint graph, for the following reason. On 1st October the funding starts and I'll release some material and there will be things for people to work on, including formalising some quite basic stuff, and there will be parts of the blueprint graph which will be \emph{active} and fast-changing, unlike the majority of the blueprint graph which will remain static for the near future. The hive of activity will be some random small connected component in the graph, and furthermore it will jump about randomly on the whim of the graph visualisation software.

I noticed that in LTE they have two blueprint graphs. Does anyone know how this was done? I would rather have small components being viewable separately than everything being in one big chaotic mess.

[Adam Topaz]

I think splitting it up into sections should be straightforward? See https://github.com/leanprover-community/liquid/blob/master/src/content.tex

[Patrick Massot]

I looked it up because I couldn’t remember the name of the option. It is documented in the README of https://github.com/PatrickMassot/plastexdepgraph. The option name is dep_by.

[Patrick Massot]

Which is indeed used at https://github.com/leanprover-community/liquid/blob/master/src/web.tex#L3

[Patrick Massot]

which creates one graph per section.

[Kevin Buzzard]

The LTE line also had a coverage option which I don't seem to have.

[Kevin Buzzard]

chapter1.png

Looking good. How do I get it to not say "Chapter 1 graph" and instead say a more interesting string?

[Patrick Massot]

Kevin Buzzard said:

The LTE line also had a coverage option which I don't seem to have.

This is vestigial and no longer does anything useful.

[Patrick Massot]

Kevin Buzzard said:

Looking good. How do I get it to not say "Chapter 1 graph" and instead say a more interesting string?

I don’t think I prepared anything for that. What would you like to see there? The chapter title followed by the word graph?

[Kevin Buzzard]

That would be perfect thanks!

[Kevin Buzzard]

Maybe ": graph" is better?

[Kevin Buzzard]

wait

[Kevin Buzzard]

maybe you should just put the links up with the chapters? Or isn't it as easy as that :-) I think <chapter title>: graph is fine.

[Patrick Massot]

Do you mean you would like each chapter to end with its graph?

[Patrick Massot]

This is definitely possible, but graphs would be somewhat hidden compared to the current convention.

[Utensil Song]

Previously, I imagined having a section "Dependency graphs", and then just the origin section names one level below it. Just like an appendix.

[Utensil Song]

One caveat of using dep_by is that the dependency graphs don't penetrate across sections, you can't even see that e.g. section 5 depends on section 3 and 1 but not others.

[Kevin Buzzard]

Patrick Massot said:

This is definitely possible, but graphs would be somewhat hidden compared to the current convention.

This would currently be the best model for me, because we will be having a lot of "chapters" which will only relate to each other much later. Right now we just need to make a ton of distinct definitions and state/prove what are right now unrelated theorems.

[Mario Carneiro]

You could also put a graph icon in the sidebar next to each chapter