New verso website

.github/workflows/blueprint.yml

@@ -53,8 +53,7 @@ jobs:
 
       - name: Build Verso Documentation
         run: |
-          cd verso
-          ./build_manual.sh
+          ./build_all.sh
 
       - name: Compile blueprint and documentation
         uses: leanprover-community/docgen-action@deed0cdc44dd8e5de07a300773eb751d33e32fc8 # 2025-10-26

.gitignore

@@ -38,6 +38,9 @@ blueprint/src/web.pdf
 *.synctex.gz(busy)
 *.pdfsync
 ## Verso
-/verso/.lake/
-/verso/html/
-/home_page/verso
+/tutorial/.lake/
+/tutorial/html/
+/website/.lake/
+/website/_site/
+/website/html/
+/home_page/

CONTRIBUTING.md

@@ -8,7 +8,7 @@ Fork the repository and create a new branch for your contribution. Make your cha
 
 ## What to contribute
 
-See the [Roadmap](ROADMAP.md).
+See the [Roadmap](https://remydegenne.github.io/lean-bandits/roadmap).
 
 #### Finding tasks
 

LeanMachineLearning/SequentialLearning/Algorithm.lean

@@ -10,6 +10,19 @@ public import LeanMachineLearning.ForMathlib.Traj
 
 /-!
 # Algorithms
+
+## Main definitions
+
+* `Algorithm α R`: a stochastic, sequential algorithm.
+* `Environment α R`: a stochastic environment.
+* `IsAlgEnvSeq A R' alg env P`: an algorithm-environment sequence. TODO
+* `IsAlgEnvSeqUntil A R' alg env P N`: an algorithm-environment sequence until time `N`. TODO
+
+## Main statements
+
+* `isAlgEnvSeq_unique`: the law of the sequence of actions and observations generated by an
+  algorithm-environment pair is unique: it does not depend on the probability space used.
+
 -/
 
 @[expose] public section

LeanMachineLearning/SequentialLearning/Deterministic.lean

@@ -9,6 +9,16 @@ public import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace
 
 /-!
 # Deterministic algorithms
+
+A deterministic algorithm chooses its action in a deterministic way. That is, that action is given
+by a measurable function of the history and not by a Markov kernel.
+
+## Main definitions
+
+* `detAlgorithm nextAction h_next action0`: a deterministic algorithm that chooses its action
+  according to the measurable function `nextAction` (with proof of measurability `h_next`),
+  with initial action `action0`.
+
 -/
 
 @[expose] public section

README.md

@@ -24,6 +24,8 @@ 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.
+
 ## Current state of the library
 
 As a first proof of concept, the repository contains a formalization of regret bounds for several stochastic bandit algorithms.

build_all.sh

@@ -0,0 +1,25 @@
+set -x -e
+
+# Build tutorial
+cd tutorial
+lake build
+rm -rf html _out
+lake exe manual
+mkdir html
+mv _out/html-multi/* html/
+rm -rf _out
+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/