some webpage reorganization

docs/_config.yml

@@ -18,11 +18,11 @@
 # You can create any custom variable you would like, and they will be accessible
 # in the templates via {{ site.myvariable }}.
 
-title: Bonn Analysis Seminar
+title: Collaborative Formalization of Analysis
 #email: your-email@example.com
-description: A formalization in Lean 4
+description: Bonn Seminar on formalizing Fourier analysis in Lean 4
 baseurl: "" # the subpath of your site, e.g. /blog
-url: "https://fpvandoorn.github.io/BonnAnalysis/" # the base hostname & protocol for your site, e.g. http://example.com
+url: "https://florisvandoorn.com/BonnAnalysis/" # the base hostname & protocol for your site, e.g. http://example.com
 #twitter_username: jekyllrb
 github_username: fpvandoorn
 repository: fpvandoorn/BonnAnalysis

docs/_layouts/default.html

@@ -28,8 +28,8 @@ <h1 class="project-name">{{ page.title | default: site.title | default: site.git
     <h2 class="project-tagline">{{ page.description | default: site.description | default: site.github.project_tagline
       }}</h2>
     <a href="blueprint" class="btn">Blueprint</a>
+    <a href="blueprint.pdf" class="btn">Blueprint (pdf)</a>
     <a href="docs" class="btn">Documentation</a>
-    <a href="blueprint.pdf" class="btn">Paper</a>
     {% if site.github.is_project_page %}
     <a href="{{ site.github.repository_url }}" class="btn">View on GitHub</a>
     {% endif %}

docs/index.md

@@ -10,9 +10,7 @@ usemathjax: true
 
 # Bonn Analysis Seminar
 
-* [Blueprint of the proof](https://florisvandoorn.com/BonnAnalysis/blueprint/)
-* [Blueprint (pdf)](https://florisvandoorn.com/BonnAnalysis/blueprint.pdf)
-* [Documentation of the methods](https://florisvandoorn.com/BonnAnalysis/docs/)
+We will formalize results in Fourier analysis, such as Plancherel's theorem and the interpolation theorems.
 
 ## Build the Lean files
 
@@ -21,11 +19,7 @@ See [the installation instructions](https://leanprover-community.github.io/get_s
 
 To build the project, run `lake exe cache get` and then `lake build`.
 
-## Build the blueprint
-
-The blueprint is automatically built on each push to the project.
-You can test whether the build is working by building the pdf locally:
-`xelatex blueprint/src/print.tex`.
+For more detailed build and contribution instructions see the Github README.
 
 <!-- To build the web version of the blueprint locally, you need a working LaTeX installation.
 Furthermore, you need some packages: