Blueprints on windows

Stream: general

[Patrick Massot]

I have a question for people who struggled to run the blueprint infrastructure on Windows (for instance I think @Terence Tao and @Rémy Degenne mentioned this recently). Is the issue coming only from the dependency on GraphViz? If yes, it would be nice to try to install networkx on your computer. If this is much easier then I could try to switch to networkx.

[Patrick Massot]

To clarify the situation, graphviz is not used essentially in the python part of blueprints. It is used essentially in the javascript part to do the graph layout, but this is OS-independent. The pygraphviz library offers python bindings to graphviz and it sounds natural to use it to create graphviz graphs. But networkx can also output graphs in the graphviz format. The only place where the blueprint python tool actually calls a graphviz program is to perform transitive reduction of the graph, but networks also knows how to do that.

[Sébastien Gouëzel]

I struggled a little bit to get the blueprint on windows, purely because of graphviz (more precisely, pygraphviz). In the end, it worked fine, but I encountered two difficulties in the pygraphviz download instructions on windows:

• pygraphviz is not compatible with the last version of graphviz, contrary to what the sentence "For this reason, PyGraphviz 1.7 only supports Graphviz 2.46.0 or higher on Windows" says implicitly. Use version 2.46.
• the quotes in the windows installation instructions don't work (they ignore the fact that there is a space in "Program files").

Once one is aware of these two issues, installation is smooth.

[Patrick Massot]

Ok, that's good to know. I'll wait a bit for Rémy who complained about it very recently, but I'd be happy to simply keep the current solution with instructions in the README.

[Rémy Degenne]

The installation of (py)graphviz was a big headache indeed. As Sébastien wrote, the instructions on the website don't work and need to be tweaked.
The second point were I think that windows was an issue is when I tried to install doc-gen (which is needed for some blueprint functions I think?). However I did not take any notes there and I gave up rather quickly, so I am not sure of what the issue was exactly and not 100% sure Windows is the source of the problem.

[Henrik Böving]

Windows is a problem, doc-gen is not at all engineered to compile under windows right now.

[Henrik Böving]

Also to expand on this: The primary reason is that we compile and link in a C library for markdown and I do have neither the knowledge nor the motivation to port this to Windows for essentially barely any users since almost all of doc-gen runs in CI anyways. Furthermore: Even if I did port the compilation procedure to Windows people would have to install a C compiler on Windows which is more annoying than on Linux. That makes me believe the average Lean Windows user (i.e. a mathematician with average computer skills) would probably not go through the effort of doing that if they can wait a bit and see the docs in CI.

There is the alternative of writing a markdown parser + to HTML converter myself in Lean but:
Once David's documentation language does eventually get integrated properly with Lean and we can use it to render doc-strings we will be able to drop the C dependency completely and replace it with pure Lean code anyways. At this point the Windows issue would be resolved anyways so I would rather not spend cycles on this right now unless we really need it.

If you really want doc-gen on Windows right now and you do not want to wait for or do not have CI my suggestion would be to run it in WSL which is reasonably easy to set up nowadays.

[Patrick Massot]

Ok, this is one more reason to keep the current design. Windows users will suffer anyway, there is nothing I can do about doc-gen.

[Yury G. Kudryashov]

Henrik Böving said:

Once David's documentation language does eventually get integrated properly with Lean and we can use it to render doc-strings we will be able to drop the C dependency completely and replace it with pure Lean code anyways.

Where can I read more about David's documentation language?

[Johan Commelin]

You can watch his talk from Lean Together

[Henrik Böving]

https://www.youtube.com/watch?v=FZFOJBxzAo0

[Yaël Dillies]

The reason we need docgen in the blueprint is because we lost the Python script that fetched Lean declarations to link to the source code in the blueprint.

[Yaël Dillies]

I do think we should not depend on docgen but only on a "declaration finder" which is currently contained in docgen but should IMO be separate.

[Rémy Degenne]

I now remember that I gave up on doc-gen after trying to install a suitable C compiler, indeed.
I don't care much if Windows is not supported, personally. I also work on Linux. At the time I was preparing a practical session for a course (unrelated to lean) and I was making sure that it also worked on Windows, and I stayed on the same OS when I started installing blueprint.

[Henrik Böving]

I now remember that I gave up on doc-gen after trying to install a suitable C compiler, indeed.

QED :D I can try to throw some more docs at the README so people are not confused

[Patrick Massot]

Yaël Dillies said:

The reason we need docgen in the blueprint is because we lost the Python script that fetched Lean declarations to link to the source code in the blueprint.

It's more complicated than that. doc-gen provides more than a link to GitHub. You get to see the full statements (whereas in the source without language server support you need to find variables) and the link to source is also there if you want it.

[Yaël Dillies]

Patrick Massot said:

You get to see the full statements (whereas in the source without language server support you need to find variables) and the link to source is also there if you want it.

To me this still falls under "util which should be used by doc-gen, not be part of it", but yeah good point.

[Henrik Böving]

If good source links is your only reason to depend on doc-gen you can reproduce this functionality yourself without too much hassle.

[Henrik Böving]

First we use this functionality in the lakefile to obtain all of the base source links in a rather heuristic, github specific fashion: https://github.com/leanprover/doc-gen4/blob/main/lakefile.lean#L117

And then this information gets used over here: https://github.com/leanprover/doc-gen4/blob/main/DocGen4/Output/SourceLinker.lean to construct source URLs.

The declaration range in turn can be extracted from the environment using docs#Lean.findDeclarationRanges?

[Patrick Massot]

Henrik Böving said:

If good source links is your only reason to depend on doc-gen you can reproduce this functionality yourself without too much hassle.

This is not what I meant. I meant that doc-gen provides more than the source and since it also provides source links it is strictly superior to a source link.