Fix the mk_all check: executables out of the libraries

`lake exe mk_all --check` wants the root files of `MetropolisHastings` and
`Bandits` to be the import lists it generates. They carried a docstring, and
the executables `MetropolisHastings/Main.lean` and `Bandits/Main.lean`, being
in the library directories, were picked up as modules of the libraries.

The executables move to the top level, as `RunMetropolisHastings.lean` and
`RunBandits.lean`, like the other executables of the repository; the root
files are regenerated by `mk_all`, and their overview moves to the docstrings
of `MetropolisHastings.Defs` and `Bandits.Defs`.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Author: RemyDegenne

Bandits.lean

@@ -1,28 +1,5 @@
-/-
-Copyright (c) 2026 Rémy Degenne. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Rémy Degenne
--/
 module  -- shake: keep-all --deprecated_module: ignore
 
 public import Bandits.Defs
 public import Bandits.EpsGreedy
 public import Bandits.Theory
-
-/-!
-# A Gaussian bandit, written in `rdo`, proved and run
-
-* `Bandits.Defs`: one round of interaction, and `n` rounds, as `rdo` programs polymorphic in the
-  monad and the scalars; explore-then-commit and UCB as the algorithms choosing the arm.
-* `Bandits.Theory`: read at `Measure`, the programs have the law of LeanMachineLearning's
-  interaction, so its regret bounds hold for them.
-* `Bandits.EpsGreedy`: ε-greedy, a randomized algorithm whose policy is an `rdo` program; with
-  `alg_env_trace`, its internal draws give an exploration bound and a linear regret lower bound.
-
-To run them and draw the regret against the bounds, from the root of the repository:
-
-```
-lake exe bandits                  # 300 seeds × 5000 rounds; writes bandit_output/
-python3 scripts/bandit_plot.py    # checks them against numpy, draws bandit_output/*.png
-```
--/

Bandits/Defs.lean

@@ -20,7 +20,13 @@ arm pulled. One round of interaction is `banditStep`, and `banditRun n` plays `n
 
 The programs are polymorphic in the monad and in the scalars, as those of
 `RandomDo.Tactic.Computable.Polymorphic`: read at `Measure` and `ℝ`, they are what
-`Bandits.Theory` proves things about; run at `RandM` and `Float`, they sample.
+`Bandits.Theory` and `Bandits.EpsGreedy` prove things about; run at `RandM` and `Float`, they
+sample. To run them and draw the regret against the bounds, from the root of the repository:
+
+```
+lake exe bandits                  # 300 seeds × 5000 rounds; writes bandit_output/
+python3 scripts/bandit_plot.py    # checks them against numpy, draws bandit_output/*.png
+```
 
 The two algorithms, `etcArm` (explore-then-commit) and `ucbArm` (upper confidence bound), mirror
 the definitions of `Bandits.ETC.nextArm` and `Bandits.UCB.nextArm` in LeanMachineLearning, with the

MetropolisHastings.lean

@@ -1,31 +1,7 @@
-/-
-Copyright (c) 2026 Rémy Degenne. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Rémy Degenne
--/
 module  -- shake: keep-all --deprecated_module: ignore
 
 public import MetropolisHastings.Computable
 public import MetropolisHastings.Defs
 public import MetropolisHastings.Polymorphic
 public import MetropolisHastings.Targets
 public import MetropolisHastings.Theory
-
-/-!
-# Random-walk Metropolis–Hastings, written in `rdo`, proved and run
-
-* `MetropolisHastings.Defs`: the algorithm, as `rdo` programs over the Giry monad.
-* `MetropolisHastings.Theory`: they are Markov kernels, satisfy detailed balance with respect to the
-  target, and leave it invariant after any number of steps.
-* `MetropolisHastings.Computable`: the samplers `@[computable]` writes from them.
-* `MetropolisHastings.Polymorphic`: the same algorithm, polymorphic in the monad; at `Measure` it
-  is the one of `Defs`, so the theorems carry over, and at `RandM` it samples.
-* `MetropolisHastings.Targets`: two targets to run the chain on, for both routes.
-
-To run it and draw the plots, from the root of the repository:
-
-```
-lake exe mh                     # runs both samplers, checks they agree, writes mh_output/
-python3 scripts/mh_plot.py      # checks them against numpy, draws mh_output/*.png
-```
--/

MetropolisHastings/Defs.lean

@@ -17,7 +17,13 @@ chain stays at `x`. The chain runs `n` such steps from `x₀`.
 
 Both programs denote Markov kernels, written over the Giry monad. `MetropolisHastings.Theory`
 proves what they satisfy, `MetropolisHastings.Computable` and `MetropolisHastings.Polymorphic` turn
-them into programs that run.
+them into programs that run, and `MetropolisHastings.Targets` gives two targets to run them on.
+To run them and draw the plots, from the root of the repository:
+
+```
+lake exe mh                     # runs both samplers, checks they agree, writes mh_output/
+python3 scripts/mh_plot.py      # checks them against numpy, draws mh_output/*.png
+```
 
 ## Main definitions
 

Bandits/Main.lean RunBandits.leanBandits/Main.lean renamed to RunBandits.lean

@@ -46,8 +46,8 @@ root = "Polymorphic"
 
 [[lean_exe]]
 name = "mh"
-root = "MetropolisHastings.Main"
+root = "RunMetropolisHastings"
 
 [[lean_exe]]
 name = "bandits"
-root = "Bandits.Main"
+root = "RunBandits"