## Stream: condensed mathematics

### Topic: blueprint / dependency graph

#### Johan Commelin (Jan 26 2021 at 18:52):

@Patrick Massot wrote some fantastic tooling for the Sphere eversion project, and has improved it over the last couple of days.
I've used it to write some sort of blueprint. But the parts that lie before us are not yet fleshed out in a lot of detail. Work in progress. As a wonderful side effect, we get a really nice graph of what is done, and where we want to go (at least as first target).

I hope that this will move to a more stable URL in a couple of days, but I'm sharing this now because it might already be useful for some things.

#### Johan Commelin (Jan 26 2021 at 18:53):

I have not yet updated the text about the snake lemma to reflect the recent discussions.

#### Johan Commelin (Jan 26 2021 at 18:53):

If you want to contribute to the text, just ping and I'll give you access to the underlying repo.

#### Adam Topaz (Jan 26 2021 at 18:58):

@Johan Commelin It might be worthwhile to add these two links to the README.md file in leanprover-community/lean-liquid.

#### Johan Commelin (Jan 26 2021 at 18:58):

I was thinking to wait with that till we have a better URL

Ah ok.

#### Adam Topaz (Jan 26 2021 at 18:59):

I mostly don't want to dig through zulip every time I want to find it :)

#### Johan Commelin (Jan 26 2021 at 18:59):

I'm sharing this now with people actively working on the project. But it should become a resource for others as well that want to browse/study the code.

#### Johan Commelin (Jan 26 2021 at 18:59):

Yes, but currently it's a random subdirectory of my homepage...

#### Johan Commelin (Jan 26 2021 at 18:59):

It should just use github pages, and auto-build using CI. But I don't really know how to set that up.

#### Adam Topaz (Jan 26 2021 at 19:00):

I guess we can ask how @Patrick Massot set it up for sphere eversion...

#### Adam Topaz (Jan 26 2021 at 19:00):

It looks like https://github.com/leanprover-community/sphere-eversion has no CI.

#### Johan Commelin (Jan 26 2021 at 19:01):

Patrick is very busy with setting up his course. And indeed the sphere project doesn't use CI.

#### Johan Commelin (Jan 26 2021 at 19:01):

But CI should be easier now, with the changes that Patrick made to his tooling last week.

#### Yakov Pechersky (Jan 27 2021 at 19:48):

http://leanprover-community.github.io/liquid

#### Yakov Pechersky (Jan 27 2021 at 19:49):

That will auto update on pushes to the master branch of the blueprint, like latex changes

#### Yakov Pechersky (Jan 27 2021 at 19:49):

And will also automatically make sure that it links properly to the declarations in the actual lean repo

#### Johan Commelin (Jan 27 2021 at 19:50):

Thank you so much for setting up the CI!

#### Johan Commelin (Jan 27 2021 at 19:50):

http://leanprover-community.github.io/liquid/dep_graph.html is the graph. we should add a link to it from the main page...

#### Yakov Pechersky (Jan 27 2021 at 19:51):

It's very nice to work with Patrick's tools, they're very clear on what they do. The ci is just plumbing his great tools with the ridiculous requirements of getting graphviz and latex to work.

#### Yakov Pechersky (Jan 27 2021 at 19:53):

Also Ron's leanprover contrib actions were quite helpful. I think the ci here could be generalized to any mathlib project. And we could provide lean images and actions.

#### Yakov Pechersky (Jan 27 2021 at 19:53):

Although probably not worth the effort for lean 3 anymore...

#### Kevin Buzzard (Jan 27 2021 at 20:10):

This stuff is really sexy.

#### Kevin Buzzard (Jan 27 2021 at 20:10):

I also like how the graph clearly explains how we're about 3/4 the way through the proof :P

#### Johan Commelin (Jan 27 2021 at 20:11):

That only means that I should write a lot more stuff about how we break 9.5 into pieces....

#### David Michael Roberts (Jan 27 2021 at 23:01):

Def 7 and Lemma 8 in section 2 have missing \tos.

#### David Michael Roberts (Jan 27 2021 at 23:03):

And in the bibliography there is

to3em, Lectures on Analytic Geometry, 2020.

#### Johan Commelin (Jan 28 2021 at 06:20):

@David Michael Roberts thanks, I'll fix them asap

#### Johan Commelin (Jan 29 2021 at 06:03):

I fixed the \tos. I have no idea what's happening in the bibliography. The .bib file looks fine.

#### Johan Commelin (Jan 29 2021 at 06:05):

Oooh, in the PDF it looks fine. It should be a long underscore, indicating "same author as above".

@Patrick Massot this seems like a small bug in plastex. Can you confirm?

#### Johan Commelin (Jan 29 2021 at 09:11):

I've changed the bib style to avoid the issue

#### Patrick Massot (Feb 05 2021 at 21:19):

@Yakov Pechersky it seems CI is no longer working.

#### Yakov Pechersky (Feb 05 2021 at 21:20):

Hmm. Seems like a pygraphviz issue. Could this be a function of pip turning off py2 support? Weird, because we're using py3.

#### Yakov Pechersky (Feb 05 2021 at 21:22):

Ah I see new pygraphviz doesn't need that cli arg

#### Yakov Pechersky (Feb 05 2021 at 21:33):

/home/runner/work/liquid/liquid/lean-liquid/src/system_of_double_complexes.lean:165:4: error: invalid field notation, 'col'' is not a valid "field" because environment does not contain 'system_of_double_complexes.col''


Is this expected?

#### Yakov Pechersky (Feb 05 2021 at 21:35):

Ah, it caught a bad lean-liquid commit. Let's try again.

#### Yakov Pechersky (Feb 05 2021 at 21:44):

kpathsea:make_tex: Invalid filename Latin Modern Math/OT', contains ' '
)

! Package fontspec Error: The font "Latin Modern Math" cannot be found.

For immediate help type H <return>.
...

l.9 \setmathfont
[range=\varnothing]{Asana Math}
?
! Emergency stop.
...

l.9 \setmathfont
[range=\varnothing]{Asana Math}
No pages of output.
Transcript written on ../print/blueprint.log.


#### Yakov Pechersky (Feb 05 2021 at 21:44):

I have to log off, unfortunately. So I can't fix this particular error currently. Next time I'll be able to will be tomorrow evening. Apologies. But the pygraphviz should be fixed though!

#### Scott Morrison (Feb 05 2021 at 22:36):

By the way --- the blueprint and/or dependency graph don't seem to have many links to them! I couldn't find any, and had to construct the URL myself from knowing how github-pages works. Presumably the README.md at https://github.com/leanprover-community/lean-liquid and at https://github.com/leanprover-community/liquid should contain direct links to the rendered pages?

#### Bryan Gin-ge Chen (Feb 05 2021 at 22:38):

@Yakov Pechersky The missing font error seems unrelated. The "Latin Modern Math" font was added to blueprint.tex in this commit. I'm not sure why the font isn't being found though; as far as I can tell it should be included in the TexLive image..?

#### Johan Commelin (Feb 06 2021 at 03:45):

@Scott Morrison Sorry, this is an artifact of launching the blueprint, but not creating links because it wasn't really fleshed out and there was no CI yet. Then gradually fixing those issues, but forgetting to add links. We should add those links now.

#### Yakov Pechersky (Feb 07 2021 at 01:27):

I have an idea on how to fix it, but before that, can we try to revert the font commit that added the Latin Modern Math and Asana Math to the tex files? The new apt add texlive... line would also need to be removed.

#### Bryan Gin-ge Chen (Feb 07 2021 at 01:32):

I'm sure Patrick won't mind as long as you're able to figure out how to get it working later.

#### Patrick Massot (Feb 07 2021 at 09:11):

I'm deeply shocked that any kind of setup can have difficulties having Latin modern math font, but I don't mind switching to any other font that has decent unicode support.

#### Patrick Massot (Feb 07 2021 at 09:13):

In any kind of project mixing LaTeX and Lean we want to be able to copy paste between Lean and LaTeX without converting unicode to ascii or ascii to unicode so \usepackage{unicode-math} is crucial.

#### Yakov Pechersky (Feb 07 2021 at 14:01):

The issue was naming the font, it requires hyphens for the Unix setup. I'm finalizing some fixes to speed up CI too

#### Yakov Pechersky (Feb 07 2021 at 14:47):

The CI is back to being fixed. And it should be marginally faster now too.

#### Yakov Pechersky (Feb 07 2021 at 14:47):

\setmathfont{latinmodern-math.otf}
\setmathfont[range=\varnothing]{Asana Math} \setmathfont[range=\varnothing]{Asana-Math.otf}


#### Yakov Pechersky (Feb 07 2021 at 14:48):

Hmm, no, the blueprint is now just the bibliography.

#### Yakov Pechersky (Feb 07 2021 at 15:17):

OK, I've reverted the various CI changes. The only crucial fixes were working with the newer pygraphviz and the font paths. And the websites work now. Sorry this took a while.

#### Bryan Gin-ge Chen (Feb 07 2021 at 15:19):

Thanks for working on this!

#### Kevin Buzzard (Feb 07 2021 at 15:21):

Yes -- many thanks. I show this web page to mathematicians quite a bit.

#### Yakov Pechersky (Feb 07 2021 at 15:22):

I'm glad to help. This type of CI work is a lot of yak shaving. And unfortunately, the github actions aren't amenable to testing locally. The only tool I know that supports this (nektos/act) doesn't support the yaml that we need to pipe the run commands to the texlive image.

#### Patrick Massot (Feb 07 2021 at 15:43):

I'm extremely grateful for your work on this because I hate setting up CI (exactly because of the difficulties you met).

image.png

#### Yakov Pechersky (Feb 07 2021 at 15:47):

Back to working. My current attempts at making it less brittle have led to empty pages. So I'm going to leave as is for now. The rate limiting step is still building the lean-liquid library.

#### Yakov Pechersky (Feb 07 2021 at 15:48):

Happy to participate in the project!

#### Johan Commelin (Feb 09 2021 at 06:03):

@Yakov Pechersky Thanks a lot for making everything work again!

#### Yakov Pechersky (Feb 09 2021 at 06:04):

Do you prefer all the Proof sections expanded by default on page load?

#### Johan Commelin (Feb 09 2021 at 06:15):

I don't have a strong preference here. What do others think? @Patrick Massot

#### Patrick Massot (Feb 09 2021 at 08:49):

This is actually a bug in the current blueprint plugin for plasTeX. Around Christmas I updated the default plasTeX theme and when I set up the liquid blueprint I adapted the blueprint plugin only minimally. If you look at the sphere eversion blueprint you'll see proof are folded by default and the + sign next to the proof word actually works.

#### Riccardo Brasca (Feb 09 2021 at 12:29):

This is maybe my fault, but in the proof of lemmas 4.7 and 4.8 in https://leanprover-community.github.io/liquid/ there is an equation that is not well displayed (I see the LaTeX source instead of the actual formula)

#### Patrick Massot (Feb 09 2021 at 14:07):

This is purely a mathjax issue, but I have a hard time understanding what mathjax doesn't like here (given that it likes several things that seem to use the same LaTeX stuff).

#### Filippo A. E. Nuccio (Feb 09 2021 at 14:13):

Is it able to understand \left and \right with the unicode symbol for \Vert?

#### Patrick Massot (Feb 09 2021 at 14:13):

Minimized version:

<!DOCTYPE html>
<html lang="en">
<script type="text/x-mathjax-config">
MathJax.Hub.Config({tex2jax: {inlineMath: [['$','$'], ['\$$','\$$']]}});
</script>
<script type="text/javascript" src="https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.7/latest.js?config=TeX-AMS_CHTML">
</script>
<meta charset="utf-8" />
<title>Mathjax is sometimes strange</title>

<body>
<p>The following works:</p>
<span>\begin{align*}  ‖y‖ & ≤ K ‖dw‖ + τ \\ & ≤ K (‖x_{|kc}‖ + K‖dx‖ + η) + τ \\ & ≤ K(K + 1) ‖x‖ + Kη + τ \end{align*}</span>
<p>but the following doesn't work:</p>
<span>\begin{align*}  ‖x_{|c} - dy‖ & = \left‖∑_{j ≥ 0} x^j_{|c} - dy^j\right‖ \\ & ≤ ∑_{j ≥ 0} \left‖x^j_{|c} - dy^j\right‖ \\ & ≤ ∑_{j ≥ 0} K‖dx^j‖ + δ_j \\ & ≤ K‖dx‖ + Kε_0 + δ_0 + ∑_{j > 0} (Kε_j + δ_j) \end{align*}</span>

</body>
</html>


Anyone can paste that in a html file and open it in a browser.

#### Patrick Massot (Feb 09 2021 at 14:15):

And Filippo gets credit for a successful psychoanalysis of mathjax!

#### Patrick Massot (Feb 09 2021 at 14:16):

So we should replace \left‖ by \left\| everywhere in the blueprint.

#### Patrick Massot (Feb 09 2021 at 14:17):

Maybe it's a good place to point out that || and \| do not produce the same result in LaTeX (the notes are full of ||`, this is minor point but since we are discussing it anyway...).

:wink:

#### Patrick Massot (Feb 09 2021 at 14:24):

I tried a search/replace, let's see whether CI builds something nicer.

#### Filippo A. E. Nuccio (Feb 09 2021 at 14:30):

Also, do you want to distinguish between delimiters and binary operations? They get mixed up, using |, no?

#### Kevin Buzzard (Feb 09 2021 at 15:14):

there's \mid and \vert right?

Yes

#### Johan Commelin (Feb 17 2021 at 10:59):

I have refactored the blueprint to the generalisation of the construction system of complexes to work for profinitely filtered pseudo-normed groups with $r'$-action of $T^{-1}$.

#### Johan Commelin (Feb 17 2021 at 11:00):

So now it should match the Lean code again, if I didn't mess up.

#### David Michael Roberts (Mar 15 2021 at 06:34):

Johan Commelin said:

http://leanprover-community.github.io/liquid/dep_graph.html is the graph. we should add a link to it from the main page...

I can't see such a link at https://leanprover-community.github.io/liquid/ or on the community homepage.

#### Johan Commelin (Mar 15 2021 at 15:07):

@Patrick Massot Can we easily add a link to the graph from the blueprint page?

#### Johan Commelin (Mar 15 2021 at 15:09):

I've started moving bits and pieces of the proof of 9.5 into separate definitions and sublemmas. I will continue doing that in the next few days. Hopefully that will give more people an idea of the global picture of the proof.

#### Patrick Massot (Mar 15 2021 at 16:01):

Maybe it's time to split the blueprint into several HTML pages anyway. In that case we can easily add a link to the graph page from the menu, as in https://leanprover-community.github.io/sphere-eversion/blueprint/index.html

#### Johan Commelin (Mar 15 2021 at 16:02):

I already split the tex into several files this morning...

#### Johan Commelin (Mar 15 2021 at 16:03):

@Patrick Massot If you could help with splitting the blueprint into several html pages, that would be great

#### Patrick Massot (Mar 15 2021 at 16:04):

Sure, I'll do it.

#### Patrick Massot (Mar 15 2021 at 23:04):

I managed to waste almost two hours on this because I forgot I set myself a trap in the leanblueprint plasTeX plugin. The liquid blueprint modification is two characters long (actually one would be enough) but it didn't work before I fixed the plugin. I forgot that the page layout is overidden in the blueprint plugin (precisely to add this dependency graph link!). And I forgot to propagate a plasTeX change there, so things were inconsistent...

#### David Michael Roberts (Mar 16 2021 at 00:42):

There's a funny empty lemma in the blueprint now: https://leanprover-community.github.io/liquid/sect0003.html#a0000000085. The proof is given as:

This is a standard result. We have not formalised it yet, but it is work in progress.

:rolling_on_the_floor_laughing:

#### Adam Topaz (Mar 16 2021 at 00:57):

This is referring to Gordan's lemma. It's a rendering issue.

#### Adam Topaz (Mar 16 2021 at 00:58):

You can take a look at the source here...
https://github.com/leanprover-community/liquid/blob/a905f671aa440b92ec44bb58e95ff0068579e78f/src/polyhedral_lattice.tex#L46

#### David Michael Roberts (Mar 16 2021 at 01:17):

I thought as much. Was just worth flagging, methinks.

#### Johan Commelin (Mar 16 2021 at 07:30):

@Patrick Massot Thanks a lot! The new version looks fantastic!

#### David Michael Roberts (Mar 16 2021 at 22:52):

Ditto, it's very nice!

Last updated: May 09 2021 at 15:11 UTC