Update blueprint

docs/_layouts/default.html

@@ -45,7 +45,7 @@ <h2 class="project-tagline">{{ page.description | default: site.description | de
     <footer class="site-footer">
       {% if site.github.is_project_page %}
       <span class="site-footer-owner"><a href="{{ site.github.repository_url }}">{{ site.github.repository_name }}</a>
-        is maintained by Pietro Monticone. Visit the GitHub repository for more information.</span>
+        is maintained by Pietro Monticone from the University of Trento. Visit the GitHub repository for more information.</span>
       {% endif %}
     </footer>
   </main>

docs/index.md

@@ -1,3 +1,13 @@
+---
+# Feel free to add content and custom Front Matter to this file.
+# To modify the layout, see https://jekyllrb.com/docs/themes/#overriding-theme-defaults
+
+# layout: home
+usemathjax: true
+---
+
+{% include mathjax.html %}
+
 # Fermat's Last Theorem for Exponent 3
 
 ## Introduction
@@ -11,6 +21,38 @@
 $$a^3+b^3 = (a+b)(a^2 - ab + b^2)
           = (a+b)(a + e^{\frac{2\pi i}{3}} b )(a+ e^{\frac{4\pi i}{3}} b)$$
 
+## Build the Lean files
+
+To build the Lean files of this project, you need to have a working version of Lean.
+See [the installation instructions](https://leanprover-community.github.io/get_started.html) (under Regular install).
+
+To build the project, run `lake exe cache get` and then `lake build`.
+
+## Build the blueprint
+
+To build the web version of the blueprint, you need a working LaTeX installation.
+Furthermore, you need some packages:
+
+```
+sudo apt install graphviz libgraphviz-dev
+pip3 install invoke pandoc
+cd .. # go to folder where you are happy clone git repos
+git clone git@github.com:plastex/plastex
+pip3 install ./plastex
+git clone git@github.com:PatrickMassot/leanblueprint
+pip3 install ./leanblueprint
+cd sphere-eversion
+```
+
+To actually build the blueprint, run
+
+```
+lake exe cache get
+lake build
+inv all
+```
+
+
 ## References
 
 Hindry (2011) [Arithmetics](https://doi.org/10.1007/978-1-4471-2131-2). *Springer*.

tasks.py

@@ -0,0 +1,20 @@
+import os
+import shutil
+import subprocess
+from pathlib import Path
+from invoke import run, task
+
+from blueprint.tasks import web, bp, print_bp, serve
+
+ROOT = Path(__file__).parent
+
+@task(bp, web)
+def all(ctx):
+    shutil.rmtree(ROOT/'docs'/'blueprint', ignore_errors=True)
+    shutil.copytree(ROOT/'blueprint'/'web', ROOT/'docs'/'blueprint')
+    shutil.copy2(ROOT/'blueprint'/'print'/'print.pdf', ROOT/'docs'/'blueprint.pdf')
+
+@task(web)
+def html(ctx):
+    shutil.rmtree(ROOT/'docs'/'blueprint', ignore_errors=True)
+    shutil.copytree(ROOT/'blueprint'/'web', ROOT/'docs'/'blueprint')