blueprint update

Stream: condensed mathematics

[Johan Commelin]

I just pushed to the blueprint:

 src/CLC.tex                | 239 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 src/Mbar.tex               |  78 ----------------------
 src/Vhat.tex               | 128 -------------------------------------
 src/breen_deligne.tex      | 341 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++----------------------------
 src/content.tex            | 334 ++---------------------------------------------------------------------------------------------
 src/homotopies.tex         |  30 +++++++--
 src/macros.tex             |   5 +-
 src/normed_groups.tex      |  96 ++++++++++++++++++++++++++++
 src/normed_homological.tex |  68 ++++++++++++++------
 src/polyhedral_lattice.tex |  41 +++++++++++-
 src/proof.tex              | 387 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 11 files changed, 1093 insertions(+), 654 deletions(-)

[Johan Commelin]

The graph will probably look a bit different once CI has checked everything.

[Johan Commelin]

:sad: CI givens an error:

  Exception: ERROR: The 'make' utility is missing from PATH
  ----------------------------------------
  ERROR: Failed building wheel for pynacl
  Building wheel for cffi (setup.py): started
  Building wheel for cffi (setup.py): finished with status 'done'
  Created wheel for cffi: filename=cffi-1.14.5-cp38-cp38-linux_x86_64.whl size=417247 sha256=f77bc25266e23622e399dd0fb3a4c5a445ec32a40c0a4dbaa6b72f222db504c0
  Stored in directory: /tmp/pip-ephem-wheel-cache-h7zceb6g/wheels/04/f4/d8/7ce287ba472b28f118422005f3e885c8124dd5dd092889685b
  Building wheel for wrapt (setup.py): started
  Building wheel for wrapt (setup.py): finished with status 'done'
  Created wheel for wrapt: filename=wrapt-1.12.1-cp38-cp38-linux_x86_64.whl size=76365 sha256=bac2da20d99b3fd7c240e1896d8c70b9bc91680ae567ee93de833e2c175d9cd7
  Stored in directory: /tmp/pip-ephem-wheel-cache-h7zceb6g/wheels/5f/fd/9e/b6cf5890494cb8ef0b5eaff72e5d55a70fb56316007d6dfe73
ERROR: Could not build wheels for pynacl which use PEP 517 and cannot be installed directly
Successfully built leanblueprint plasTeX MarkupSafe Pillow PyYAML cffi wrapt
Failed to build pynacl

[Johan Commelin]

@Yakov Pechersky Do you by chance know what's going on?

[Johan Commelin]

https://github.com/leanprover-community/liquid/runs/2492653494

[Yakov Pechersky]

Taking a look now

[Yakov Pechersky]

It might be a couple hours before I can really focus on this

[Yakov Pechersky]

Apologies!

[Yakov Pechersky]

@Scott Morrison where did you hit the "missing make utility" issue on images, and how did you solve it?

[Scott Morrison]

Yeah, exact same issue for the (now abandoned) alpine based docker image.

[Yakov Pechersky]

let's see if apt add make is enough

[Johan Commelin]

https://stackoverflow.com/questions/67337408/pynacl-doesnt-want-to-install-during-pygithub-instalationwheel-building-doesn suggests apt install python-dev...

[Johan Commelin]

No idea whether that is reasonable

[Johan Commelin]

@Yakov Pechersky Great! You fixed it: https://github.com/leanprover-community/liquid/runs/2492832789 :tada:

[Johan Commelin]

And of course some of the input data for the graph wasn't updated correctly, so I've pushed another fix.

[Yakov Pechersky]

Great! The system works =)

[Yakov Pechersky]

https://github.com/leanprover-community/liquid/blob/905d04bb57946b4d71c3c8bf06f0cf73d36fe08a/src/proof.tex#L15 should have \kappa instead

[Johan Commelin]

Thanks, I'll fix it

[Johan Commelin]

I think that the blueprint is pretty much in sync again.

[Filippo A. E. Nuccio]

I have found a small typo in the blueprint (a missing s from the word such in the explanation of what functioriality means, right after Theorem 2.1 in the "Breen-Deligne" section), but I don't have permissions to push to the repository. What should I do?

[Johan Commelin]

You should wait a second (-;

[Johan Commelin]

@Filippo A. E. Nuccio https://github.com/leanprover-community/liquid/invitations

[Filippo A. E. Nuccio]

Thanks! Done and pushed.

[Johan Commelin]

@Filippo A. E. Nuccio Wrote a section on the surjectivity of $ℤ((T))_r → ℝ$. I've added the lean blueprint info, and pushed to master.

[Johan Commelin]

My plan is to thoroughly update the blueprint for the second half of the project. So the graph will be less green in the future.

[Johan Commelin]

@Patrick Massot It looks like there is a little \qedhere bug: https://leanprover-community.github.io/liquid/sect0006.html#theta.finite_sum
I guess we need to teach PlasTeX about \qedhere? Or is it something else?

[Johan Commelin]

And for some reason the new connected component(s) of the dependency graph aren't clickable (but the old one is)

[Johan Commelin]

I somehow messed up the blueprint directives. But I don't know how.