Chapter 09 — Embedding Hesper in Other Projects

Hesper is published as a Lake package. This chapter shows the three common ways to depend on it from your own code. The lakefile.lean snippets below are build-script DSL, not regular Lean — they're shown as text blocks because they can only be elaborated by the Lake driver.

Pattern 1: pure-Lean dependency

If you only need the DSL and the high-level API (no native customisation), add Hesper to your lakefile.lean:

import Lake
open Lake DSL

package «MyApp» where

require Hesper from git
  "https://github.com/Verilean/hesper.git" @ "main"

lean_lib «MyApp» where

@[default_target]
lean_exe «my-app» where
  root := `Main

Then lake update Hesper && lake build. The Hesper package's extraDepTargets := #[nativeDeps]` triggers the Dawn / Highway / CUDA bridge build automatically the first time you compile.

This is the right pattern for: applications, research scripts, training loops.

Pattern 2: pin a specific commit

For reproducibility, pin a tag or commit hash:

require Hesper from git
  "https://github.com/Verilean/hesper.git" @ "v0.7-gemma4"

The lake-manifest.json file at the root of your package records the resolved revision, so a fresh git clone of your project always pulls the same Hesper.

Pattern 3: local clone (for hacking on Hesper itself)

If you're developing both your app and Hesper, replace the git URL with a path:

require Hesper from "/path/to/local/hesper"

Saves you a push/pull cycle every time you tweak the library.

Linking your own native code

If your app has its own C++ FFI on top of Hesper's, you need to extend the link line. Hesper exposes stdLinkArgs and cudaExeArgs as defs in its lakefile.lean; mirror that pattern in your own:

def myExtraLinks : Array String := #[
  "-L/usr/local/lib", "-lmyhelper"
]

lean_exe «my-app» where
  root := `Main
  moreLinkArgs := Hesper.stdLinkArgs ++ Hesper.cudaExeArgs ++ myExtraLinks

Hesper.stdLinkArgs already pulls in Dawn, Highway, and (on Linux) the CUDA bridge static lib. You usually only add your own libs on top.

Choosing modules to import

The library is split so you can keep imports minimal:

Import What it brings in
Hesper.WGSL.DSL The type-safe Exp layer (no GPU device)
Hesper.WGSL.Monad The ShaderM monad
Hesper.Compute High-level device + buffer + dispatch API
Hesper.Layers.* Pre-built NN layers
Hesper.Core.Differentiable Reverse-mode autodiff core
Hesper.Models.BitNet The full BitNet engine
Hesper.Models.Gemma4 The full Gemma 4 engine (CUDA only)
Hesper.CUDA.* Direct CUDA driver bindings (advanced)

Lean is good at dead-code elimination across modules, so importing Hesper.Compute doesn't drag every model into your binary.

A complete runnable training loop lives in Examples/MachineLearning/.

Versioning and stability

Hesper is alpha (see the project README). API breakage policy:

  • Stable: Exp, ShaderM core, TensorDesc, Differentiable.
  • Stabilising: Circuit DSL, GPUBackend typeclass.
  • Unstable: model-specific internals (Hesper.Models.* private modules), CUDA-specific tuning knobs.

If you need stability today, pin to a tag and check docs/CHANGELOG.md before bumping.

What's next