Delete website main page

.gitignore

@@ -40,7 +40,4 @@ blueprint/src/web.pdf
 ## Verso
 /tutorial/.lake/
 /tutorial/html/
-/website/.lake/
-/website/_site/
-/website/html/
 /home_page/

README.md

@@ -8,7 +8,7 @@
 </div>
 
 
-Website: [https://remydegenne.github.io/lean-bandits/](https://remydegenne.github.io/lean-bandits/)
+Website: [https://leanmachinelearning.github.io/](https://leanmachinelearning.github.io/)
 
 ## Goals
 
@@ -24,7 +24,7 @@ Please see our [contribution guide](CONTRIBUTING.md) and [code of conduct](CODE_
 
 For discussions, you can reach out to us on the [Lean prover Zulip chat](https://leanprover.zulipchat.com/).
 
-You can also see the [roadmap](https://remydegenne.github.io/lean-bandits/roadmap) for ideas on what to work on.
+You can also see the [roadmap](https://leanmachinelearning.github.io/roadmap) for ideas on what to work on.
 
 ## Current state of the library
 

build_all.sh

@@ -12,14 +12,6 @@ mkdir -p html/static
 cp static_files/* html/static
 cd ..
 
-# Build website
-cd website
-lake build
-rm -rf _site
-lake exe generate-site
-cd ..
-
 # Copy outputs to home_page
 mkdir -p home_page/tutorial
 cp -r tutorial/html/* home_page/tutorial
-cp -r website/_site/* home_page/

tutorial/Manual/Front.lean

@@ -16,7 +16,7 @@ authors := ["Rémy Degenne, Paulo Rauber"]
 shortTitle := "Lean Machine Learning"
 %%%
 
-These tutorial pages will guide you through using the Lean Machine Learning library.
+These tutorial pages will guide you through using the [Lean Machine Learning](https://leanmachinelearning.github.io) library.
 
 {include 0 Manual.Pages.Installation}