Zulip Chat Archive

Stream: condensed mathematics

Topic: blueprint / dependency graph


view this post on Zulip 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.

https://math.commelin.net/web/
https://math.commelin.net/web/dep_graph.html

view this post on Zulip Johan Commelin (Jan 26 2021 at 18:53):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jan 26 2021 at 18:58):

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

view this post on Zulip Adam Topaz (Jan 26 2021 at 18:58):

Ah ok.

view this post on Zulip Adam Topaz (Jan 26 2021 at 18:59):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jan 26 2021 at 18:59):

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

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Jan 26 2021 at 19:00):

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

view this post on Zulip Adam Topaz (Jan 26 2021 at 19:00):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Yakov Pechersky (Jan 27 2021 at 19:48):

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

view this post on Zulip Yakov Pechersky (Jan 27 2021 at 19:49):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jan 27 2021 at 19:50):

Thank you so much for setting up the CI!

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Yakov Pechersky (Jan 27 2021 at 19:53):

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

view this post on Zulip Kevin Buzzard (Jan 27 2021 at 20:10):

This stuff is really sexy.

view this post on Zulip 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

view this post on Zulip 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....

view this post on Zulip David Michael Roberts (Jan 27 2021 at 23:01):

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

view this post on Zulip David Michael Roberts (Jan 27 2021 at 23:03):

And in the bibliography there is

to3em, Lectures on Analytic Geometry, 2020.

view this post on Zulip Johan Commelin (Jan 28 2021 at 06:20):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jan 29 2021 at 09:11):

I've changed the bib style to avoid the issue

view this post on Zulip Patrick Massot (Feb 05 2021 at 21:19):

@Yakov Pechersky it seems CI is no longer working.

view this post on Zulip 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.

view this post on Zulip Yakov Pechersky (Feb 05 2021 at 21:22):

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

view this post on Zulip 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?

view this post on Zulip Yakov Pechersky (Feb 05 2021 at 21:35):

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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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?

view this post on Zulip 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..?

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Feb 06 2021 at 07:35):

I've added links to both READMEs

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Feb 07 2021 at 14:47):

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

view this post on Zulip Yakov Pechersky (Feb 07 2021 at 14:47):

The crucial fix was https://github.com/leanprover-community/liquid/commit/063ed84ee1d21f0d330b285883b26558e9764aec

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

view this post on Zulip Yakov Pechersky (Feb 07 2021 at 14:48):

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

view this post on Zulip 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.

view this post on Zulip Bryan Gin-ge Chen (Feb 07 2021 at 15:19):

Thanks for working on this!

view this post on Zulip Kevin Buzzard (Feb 07 2021 at 15:21):

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

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Yakov Pechersky (Feb 07 2021 at 15:46):

image.png

view this post on Zulip 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.

view this post on Zulip Yakov Pechersky (Feb 07 2021 at 15:48):

Happy to participate in the project!

view this post on Zulip Johan Commelin (Feb 09 2021 at 06:03):

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

view this post on Zulip Yakov Pechersky (Feb 09 2021 at 06:04):

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

view this post on Zulip Johan Commelin (Feb 09 2021 at 06:15):

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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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).

view this post on Zulip Filippo A. E. Nuccio (Feb 09 2021 at 14:13):

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

view this post on Zulip Patrick Massot (Feb 09 2021 at 14:13):

Minimized version:

<!DOCTYPE html>
<html lang="en">
<head>
<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>
</head>

<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.

view this post on Zulip Patrick Massot (Feb 09 2021 at 14:15):

And Filippo gets credit for a successful psychoanalysis of mathjax!

view this post on Zulip Patrick Massot (Feb 09 2021 at 14:16):

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

view this post on Zulip 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...).

view this post on Zulip Filippo A. E. Nuccio (Feb 09 2021 at 14:18):

:wink:

view this post on Zulip Patrick Massot (Feb 09 2021 at 14:24):

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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Feb 09 2021 at 15:14):

there's \mid and \vert right?

view this post on Zulip Filippo A. E. Nuccio (Feb 09 2021 at 15:14):

Yes

view this post on Zulip 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 rr'-action of T1T^{-1}.

view this post on Zulip Johan Commelin (Feb 17 2021 at 11:00):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 15 2021 at 15:07):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 15 2021 at 16:02):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Mar 15 2021 at 16:04):

Sure, I'll do it.

view this post on Zulip 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...

view this post on Zulip 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:

view this post on Zulip Adam Topaz (Mar 16 2021 at 00:57):

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

view this post on Zulip 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

view this post on Zulip David Michael Roberts (Mar 16 2021 at 01:17):

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

view this post on Zulip Johan Commelin (Mar 16 2021 at 07:30):

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

view this post on Zulip David Michael Roberts (Mar 16 2021 at 22:52):

Ditto, it's very nice!


Last updated: May 09 2021 at 15:11 UTC