How to make a Blueprint

Stream: Is there code for X?

[Andre Hernandez-Espiet (Rutgers)]

Is there a tutorial in how to make something like https://leanprover-community.github.io/sphere-eversion/blueprint/index.html ?

[Floris van Doorn]

@Patrick Massot will be able to give you a more detailed answer, but you can always copy the source from https://github.com/leanprover-community/sphere-eversion and adapt to your needs. The Readme of the linked repo has detailed instructions to build the blueprint from the source.

[Andre Hernandez-Espiet (Rutgers)]

I'm trying to install it in a windows computer. I can't seem to figure out how to run sudo apt install graphviz libgraphviz-dev, and while I searched around for other ways to do this I didn't find anything that worked. Any ideas?

[Alex J. Best]

That command installs graphviz and development headers, if you download the installer from https://graphviz.org/download/ for windows you can try and just install graphviz with that, but I have no experience using lean-blueprint on windows.
You might be better off just trying to do everything in WSL instead

[Filippo A. E. Nuccio]

FWIW, I have just installed WSL on my Win11 machine (thank you @Alex J. Best , I did not know it existed!) and was able to make a blueprint following the instructions in the sphere eversion project.

[Filippo A. E. Nuccio]

What is strange is that all inv commands (like pdf, qpdf, web, qweb) are quite fast, while inv serve takes forever. @Patrick Massot is it normal, in your opinion?

[Patrick Massot]

inv serve is meant to takes forever, as long as you wish to browse the blueprint.

[Patrick Massot]

It's launching a webserver and that server waits for you

[Filippo A. E. Nuccio]

Ah ok, good. Another problem is that I am missing all lean declarations: I have the buttons, but when I click on them they do not point anywhere (I am testing this locally with the flt-regular project, which works online, so it is not a problem of wrong links or something like this)

[Patrick Massot]

What if you run inv all?

[Filippo A. E. Nuccio]

No idea what 'all' is!

[Filippo A. E. Nuccio]

(this is the console speaking, not me :smile: )

[Floris van Doorn]

You might need to copy the sphere-eversion tasks.py to flt-regular for inv all to work.
Also, you have to run leanproject build before any of the inv commands.

[Filippo A. E. Nuccio]

Ok, let me try (I think they copied it from LTE rather than sphere-eversion)

[Floris van Doorn]

(note: there's 2 directories with a tasks.py, you might need to copy both)

[Filippo A. E. Nuccio]

Well, the trees are quite different, so I am getting errors all over the places. As I am mainly testing whether the program runs locally on my PC, I am now cloning sphere-eversion and trying with that instead of flt-regular.

[Filippo A. E. Nuccio]

I was unable to run the blueprint for sphere-eversion but managed to have the one for flt-regular work (and for my project as well, as it is copied from that one). I still cannot get the lean links and moreover I have a problem if calling \usepackage{fontspec} probably because its calls l3kernel and xparse in turn and somewhere this creates problem. This is not very important, so I can live without, but the lean links missing is a bit annoying.

[Filippo A. E. Nuccio]

I was able to make some advances. I still have three questions for people compiling the blueprint locally:

1. Although leanproject build completes in 20/30 secs on my project, and inv qweb builds very quickly, when I call inv web it takes forever (or at least > 10 minutes). Is it normal?
2. I now have a nice graph, the bibliography is OK and when I click on the Lean icon at the right of a def/lemma, a window opens with the right declarations. Yet, if I click on the hyperlink, I get an error 404: File not found message. Is it related to 1.?
3. By default, all proofs are visible like in LTE rather than like in the sphere eversion project. How can I switch from one to the other?

[Floris van Doorn]

2: Given that the description of qweb is

def qweb(ctx):
    """Quick web (don't try to rebuild references or links to Lean code)"""

I don't think that is very surprising.
https://github.com/leanprover-community/flt-regular/blob/master/tasks.py#L48

[Filippo A. E. Nuccio]

I agree, that's why I thought it was related to 1. But the fact that I can never complete the inv web is annoying.

[Filippo A. E. Nuccio]

After all, the difference seems to simply lie in decls and this does not much more than building the project, no?

[Floris van Doorn]

The longest part of inv web is inv decl. This requires to

• build the whole project
• compile a file that imports the whole project
• create a list of all declarations and positions of all imported files, including mathlib (or at least, something like that).

If you just build all files in the source, does inv decl run in a reasonable time? For me in sphere-eversion, building the whole project takes quite a bit longer than invoke (though inv decl still takes a while).

[Filippo A. E. Nuccio]

You mean to try leanproject build followed by inv decl?

[Floris van Doorn]

yeah

[Filippo A. E. Nuccio]

Let me try

[Filippo A. E. Nuccio]

built in less than 1 min. Now I try decl

[Filippo A. E. Nuccio]

Started... in the meantime, can I ask how big is your decls.yaml file for the spere eversion?

[Filippo A. E. Nuccio]

(6 minutes...) :sleeping:

[Floris van Doorn]

last time I made it, 316k lines...

[Filippo A. E. Nuccio]

Ah ok, it is huge. I was afraid of my 5k...

[Filippo A. E. Nuccio]

Done!

[Filippo A. E. Nuccio]

12 mins

[Filippo A. E. Nuccio]

decls.yaml is 256k lines

[Floris van Doorn]

Ok, now everything else should be quick!

[Filippo A. E. Nuccio]

But should I call inv web now? Or will it start again?

[Floris van Doorn]

probably you want to run inv qweb now, to avoid doing the same again...

[Filippo A. E. Nuccio]

...nahhh, unfortunately I still have an error when I click on the hyperlink

[Floris van Doorn]

Does inv qweb raise any errors? Any occurrences of "declaration not found" or something?

[Floris van Doorn]

to where do the URLs link?

[Floris van Doorn]

did you make a local server with inv serve?

[Filippo A. E. Nuccio]

1. No, no error. Only a unrecognized command/environmnent definitionname (that I am going to investigate)
2. What do you mean by "to where the URLs link"?
3. Yes

[Floris van Doorn]

1: I think that might be the issue. Make sure you provide the full Lean name in all lemmas/definitions.

[Filippo A. E. Nuccio]

You mean with the namespace? What if it is in _root_?

[Floris van Doorn]

yes, with full namespaces. If it's in the root namespace, no need to add anything.

[Floris van Doorn]

2: it is a hyperlink. What is the URL of the hyperlink (what's in the URL bar after you click the hyperlink)?

[Filippo A. E. Nuccio]

http://localhost:8000/blob/9ed20455dca90d17d8ddea47f4267f0e776efe38/src/mixed_characteristic.lean#L12

[Floris van Doorn]

I just tested it in sphere-eversion. My links refer to something like
https://github.com/leanprover-community/sphere-eversion//blob/707b0d1de8f5634f0d47627d68b1c9765b452ef2/src/loops/basic.lean#L203
So it seems that something goes wrong with adding the github prefix.

[Filippo A. E. Nuccio]

But is this the hyperlink you get locally?

[Floris van Doorn]

Also, the commit 9ed20455dca90d17d8ddea47f4267f0e776efe38 does not seem to exist on flt-regular. Maybe it helps if you push your current commit to the remote repo (can be on a branch).

[Filippo A. E. Nuccio]

No, I am not on flt-regular, I am on another project.

[Floris van Doorn]

Yeah, it seems to link to Github. This also makes sense: even the blueprint will have to link to Github, not to a separate page on the same website.

[Floris van Doorn]

oh

[Filippo A. E. Nuccio]

I moved the lemma to another file blueprint_tests.lean and now the hyperlink points to
http://localhost:8000/blob/18f71bddd41d98a80ee2b5f14a94df714a064421/src/blueprint_tests.lean#L5
To me, this seems to mean that the blueprint is doing its job pretty well, since it understood that the lemma has moved (and it is indeed on the fifth line), but the problem is more with the browser that does not know what to do with that link.

[Filippo A. E. Nuccio]

Perhaps, once the project will become public and land on github things will improve, for the time being this is not really a problem.

[Filippo A. E. Nuccio]

And do you have any idea about proofs being hidden/shown by default?

[Floris van Doorn]

Probably it's related to some option in plastex.cfg.

[Floris van Doorn]

Note that the sphere eversion web.tex contains:

\home{https://leanprover-community.github.io/sphere-eversion/}
\github{https://github.com/leanprover-community/sphere-eversion/}

This probably tells the web page where to link to.
It's really hard to help you without knowing your configuration.

[Filippo A. E. Nuccio]

I know, thank you. You have already done a lot and the situation is much much better. I will try to go on myself from here, I think what remains are small details that can be fixed in the future.

[Filippo A. E. Nuccio]

Floris van Doorn said:

Note that the sphere eversion web.tex contains:

\home{https://leanprover-community.github.io/sphere-eversion/}
\github{https://github.com/leanprover-community/sphere-eversion/}

This probably tells the web page where to link to.
It's really hard to help you without knowing your configuration.

Yes, that was exactly the point, and now it works! Thank you so much once more. :octopus: