Create a blueprint

Stream: Is there code for X?

[Tianchen Zhao]

I saw the latest project on Liquid Tensor Experiment https://github.com/leanprover-community/lean-liquid and I wonder how to make a blueprint like that https://leanprover-community.github.io/liquid/. I am familiar with writing latex but I am a web page noob. Thank you :smile:

[Adam Topaz]

The repo for the blueprint is here: https://github.com/leanprover-community/liquid
The readme has some more info about the setup

[Johan Commelin]

It uses https://github.com/PatrickMassot/leanblueprint. The LaTeX source is in https://github.com/leanprover-community/liquid, and Github auto-generates the corresponding webpage using a so-called Github action: https://github.com/leanprover-community/liquid/blob/master/.github/workflows/gh-pages.yml

[Tianchen Zhao]

Johan Commelin said:

It uses https://github.com/PatrickMassot/leanblueprint. The LaTeX source is in https://github.com/leanprover-community/liquid, and Github auto-generates the corresponding webpage using a so-called Github action: https://github.com/leanprover-community/liquid/blob/master/.github/workflows/gh-pages.yml

I am not completely sure. So I need to create another repo like https://github.com/leanprover-community/liquid (eg replace .tex files in src with my own latex files), set up the workflow and then github can generate github pages displaying the latex files.

Also, for gh-pages.yml, my gh-pages.yml should be mostly the same from the one in liquid project and I just need to change the following to my own repo. Is that right?

leanproject get leanprover-community/lean-liquid
ln -s lean-liquid project

[Marc Masdeu]

I have tried to use @Patrick Massot's blueprint implementation but I'd like to have both the lean source and the blueprint on the same repo (it is confusing to me to have two repos about a single project). I have tried many ways and it mostly works, but I can't make to get the links to the actual lean code on the website. Has someone successfully done it? You can see my effort at https://github.com/mmasdeu/brouwerfixedpoint. If you go to https://mmasdeu.github.io/brouwerfixedpoint/sect0001.html and hover next to Definition 1.1, you will see that nothing appears when one clicks on "LEAN"... Thanks!

[Yaël Dillies]

Btw are you planning on proving Sperner's lemma? We have a close to complete proof on the branch sperner-again.

[Patrick Massot]

The sphere eversion project has only one repo with Lean code and the blueprint so it's certainly possible.

[Patrick Massot]

If you can't figure it out from this example then I'll try to give more instructions (and hopefully put them in some documentation).

[Eric Wieser]

Your blueprint job seems to have been failing for a while: https://github.com/mmasdeu/brouwerfixedpoint/actions/workflows/gh-pages.yml

[Marc Masdeu]

Yaël Dillies said:

Btw are you planning on proving Sperner's lemma? We have a close to complete proof on the branch sperner-again.

We are aware of your project, we just want to prove Brouwer from your version of Sperner :smile:

[Marc Masdeu]

Eric Wieser said:

Your blueprint job seems to have been failing for a while: https://github.com/mmasdeu/brouwerfixedpoint/actions/workflows/gh-pages.yml

Yes, a month ago I tried hard to make this work, and then gave up until yesterday. I decided to give up and ask the Zulip masters. My guess is that I am forgetting to change a path in some file to point to the right place, but I don't know how to debug it and have got tired of trying random combinations of possible solutions...

The blueprint appears on a website and it all seems to work, except for the link to the actual lean code (where the website shows a blank space).

@Patrick Massot I looked at the Sphere Eversion Project, but the code there is much older (I assume?) than what I am using now, what I wanted is not a custom setup, but a "template" that I can use in other projects. I took it from the LTE and made it work with two repos, but then wanted to join it all into one. In particular, this "template" should all run through a Github action, put the website on gh-pages, and use the least amount of code in the repo as possible.

[Yaël Dillies]

Marc Masdeu said:

Yaël Dillies said:

Btw are you planning on proving Sperner's lemma? We have a close to complete proof on the branch sperner-again.

We are aware of your project, we just want to prove Brouwer from your version of Sperner :smile:

Ohohoh! Very much approving.

[Patrick Massot]

I'll have a look but not very soon. Please ask again next week if nothing happen.

[Eric Wieser]

Marc Masdeu said:

Eric Wieser said:

Your blueprint job seems to have been failing for a while: https://github.com/mmasdeu/brouwerfixedpoint/actions/workflows/gh-pages.yml

Yes, a month ago I tried hard to make this work, and then gave up until yesterday. I decided to give up and ask the Zulip masters. My guess is that I am forgetting to change a path in some file to point to the right place, but I don't know how to debug it and have got tired of trying random combinations of possible solutions...

The failure is here: https://github.com/mmasdeu/brouwerfixedpoint/runs/3218608683?check_suite_focus=true#step:7:77

[Marc Masdeu]

I managed to make it work. The problem (a bug which I haven't fixed yet) was in the repo there happens to be a file (krein-milman.lean) which has a hyphen. This doesn't work well, apparently, and after constructing inv_decls.lean then the code gets confused (it looks for krein.lean, in fact). By changing the hyphen to an underscore all is well. Thanks for all the help!

[Kevin Buzzard]

Good catch!

[Patrick Massot]

Ouch, it looks bad. Did you manage to understand where is this bug? I would understand that something evil like a file name containing a space could trigger bugs, but a hyphen looks reasonnable.

[Alex J. Best]

@Patrick Massot lean itself doesn't like hyphens in import filenames, they can be used if they are wrapped in double french quotes. Would you welcome a PR to mathlibtools that takes more care around such filenames (i.e. wraps them properly in make_all) I think this will work then

[Patrick Massot]

Thanks Alex! I'm relieved because I really couldn't imagine having messed up so badly that hyphens in file names become problematic in python.

[Yaël Dillies]

Oh is this krein-milman.lean coming from me? #8112 doesn't have it.

[Marc Masdeu]

Yaël Dillies said:

Oh is this krein-milman.lean coming from me? #8112 doesn't have it.

Yes, that is the misbehaving one. It's okay if it has served to catch a bug!

[Yaël Dillies]

@Bhavik Mehta, maybe it's time for you to actually PR Hahn-Banach once and for all!

[Ruben Van de Velde]

Like #7288?

[Patrick Massot]

That PR is tagged as work in progress.

[Yaël Dillies]

Ruben Van de Velde said:

Like #7288?

Yes, exactly. I meant that Bhavik should spend a few more hours tidying up that PR (which is essentially ready already) and get it to hit master.