Clone · compile · explore

Installation

The repository pins its Lean and Mathlib versions, so Elan and Lake can reproduce the same environment used by the formalization website and GitHub Actions.

Reproducible path

flowchart LR
    Clone["Clone canonical repository"] --> Elan["Install Elan<br/>use pinned lean-toolchain"]
    Elan --> Update["lake update"]
    Update --> Check["python tools/bandit.py check"]
    Check --> Query["Query BanditRLlib declarations"]
    Check --> Site["Build and check website"]
    Check --> IDE["Run loopback Live Formalization server"]

Reproducible setup path for BanditRLlib, its website, and the local formalization service · editable Mermaid source

1. Install the prerequisites

Git

Lake uses Git to fetch Mathlib, and contributors use Git branches and pull requests for review.

Lean through Elan

Follow the official Lean installation guide. Elan reads lean-toolchain and selects leanprover/lean4:v4.29.1 automatically.

Python 3

The ABRL proof gate, site generator, integrity checks, and local preview helpers use Python 3 and only the standard library.

2. Clone the project

git clone https://github.com/DakeBU/Auto-Bandit-RL-Proof-In-Sleep.git
cd Auto-Bandit-RL-Proof-In-Sleep
lake update

lake update fetches the pinned Mathlib dependency from lakefile.lean. The first run may take several minutes.

3. Run the mandatory Lean gate

python3 tools/bandit.py check

On Windows, py -3 tools/bandit.py check is equivalent when the Python launcher is installed. The gate runs lake build, builds Tests, and scans local Lean files for forbidden placeholders.

Successful result. The command exits with status 0 after both Lean build targets and repository integrity checks pass. A first build may be slow while Lake downloads and compiles pinned dependencies.

Do not skip this step. A theorem is marked compiled on the website only after the project gate passes for the source snapshot being published.

4. Build and preview the literate site

python3 website/scripts/build_site.py --lean-verified
python3 website/scripts/check_site.py
python3 -m http.server 8000 --directory website/_site

Open http://localhost:8000/. The static Research IDE is at /ide/; local Lean compilation requires the loopback-only companion server documented on that page.

If dependency downloads fail. A transient GitHub or Mathlib CDN error is external to the proof tree. Preserve the pinned toolchain, retry after connectivity recovers, and only edit repository configuration when the failure is reproducible.

5. Choose your first route

Open the book map Search Lean declarations How to contribute