Chapter 00 — Setup

This chapter gets you to a working Hesper environment. After it you can load any later chapter as a notebook and run its code cells.

Two ways to set up

  1. Docker (recommended). A pre-built image ships Lean 4, xeus-lean, Jupyter Lab, and all 12 tutorial chapters as runnable notebooks:

    docker run --rm -p 8888:8888 ghcr.io/verilean/hesper-tutorial:latest

    Open http://localhost:8888 in your browser. Pick ch00-setup.ipynb to verify everything works, then walk the chapter list in order.

  2. Local install. You'll need:

    • Lean 4 via elan
    • A C++17 toolchain (clang or g++)
    • cmake ≥ 3.16
    • For Gemma 4: NVIDIA driver + CUDA Toolkit ≥ 12.0

    Then:

    git clone https://github.com/Verilean/hesper.git
cd hesper
lake build Hesper

    First build takes 10–15 minutes (it builds Dawn and Highway from source). Subsequent builds are incremental.

A first sanity check

The smallest thing we can run is a Hesper smoke test that elaborates a WGSL expression and pretty-prints the generated shader code:

In [ ]:
import Hesper.WGSL.DSL

open Hesper.WGSL

-- Build a tiny shader expression — this fails at elaboration time if
-- the DSL doesn't load.
def smoke : Exp (.scalar .f32) :=
  let x : Exp (.scalar .f32) := var "x"
  sqrt (x * x + x)

-- And inspect the generated WGSL source:
#eval smoke.toWGSL

In a notebook this prints sqrt(((x * x) + x)). From the command line:

lake env lean --version
lake build Hesper          # rebuild if needed
lake exe dsl-basics        # print a few DSL example shaders

Switching between chapters

The Markdown sources live at docs/tutorial/md/Ch##_*.md. Each chapter is converted into both .lean and .ipynb by xlean-convert:

bash docs/tutorial/build-from-md.sh

The Docker image runs this at build time, so notebooks are already present when you start Jupyter Lab.

What's next