Anyone using blueprint graphs for current miniprojects?

Stream: FLT

[Kevin Buzzard]

Right now we have ongoing miniprojects on adeles, Haar characters, Fujisaki's lemma, Quaternion algebras and Hecke operators. Each one of them is proceding nicely. But is anyone using at the blueprint graphs for these miniprojects? They are here: Adeles, Haar characters, Fujisaki's lemma, Quaternion algebras and Hecke Operators.

I am wondering whether we should ditch these graphs, and go back to "one graph for the entire project". I don't use the graphs, I look through the code for sorries to find out what needs doing because each project is relatively self-contained. But will other people be upset if I remove these graphs from the website?

The motivation is that I'm unhappy that currently it's really difficult to figure out how progress is going in the proof of FLT by looking at graphs.

[Django Peeters]

Can't we have both ways? Like some automatic graph stitching code that puts them all together?

[Kevin Buzzard]

I guess the answer to that is: in theory yes, in practice someone would have to write that code and get Patrick to merge it, and so for me by far the simplest option is what I suggested above. Code which glues graphs from different sections together would be a much better solution but is a much bigger problem.

[Ruben Van de Velde]

I haven't looked at them for

[Ruben Van de Velde]

a long time - would certainly be nice have more insight in where we're going :)

[Rado Kirov]

Asked Copilot to vibe code something quick - https://red-berget-83.tiiny.site/ Does that look like what you are envisioning? It is all sorts of hacky (parsing with regexp, etc) but also these days it is amazingly quick to get prototypes like this done - see https://github.com/rkirov/FLT/tree/vibe-viz (I just wrote a few comments and TS interfaces).

No idea why most edges seem to be missing? Is it a parsing issue with the script or they are not in the .tex files? I still feel there needs to be a system the seamlessly switches to the more reliable symbol dep graph from .lean files once they are exist and compile. But with namespaces symbol resolution is more complex there and probably will need actual compiler help.

Is the spring-repusle viz any good for deps visualization, or graphviz Dot layout is better?

[Kevin Buzzard]

So this is displaying (some form of) the entire blueprint graph, which is exactly what I don't want displayed.

What I think the FLT graph should look like right now is only this https://imperialcollegelondon.github.io/FLT/blueprint/dep_graph_chapter_2.html , however what I think it should look like in a week or two's time is the union of this and another similar-sized graph which I will have made in a different section. The four or 5 graphs I linked to above are also one other (paper-sized) project but they are a "bottom-up" contribution, so different to the "top-down" map which I linked to above, which has the FLT node.

[Ruben Van de Velde]

Oh, that sounds harder

[Kevin Buzzard]

When the next file is written I'll be able to better explain the visualisation I would like for FLT. Working on it!

[Mr Proof]

Would it be possible to add a percentage to the graphs. e.g. How much of the graph is complete? (Estimated)

Or maybe more useful, estimation of how many lines of code each node will take (roughly) and how much has been done.

It's hard to see from the graphs, how far the project is along and how much there is more to do.

(Or even a difficulty level for each section).

Good luck.