WebGPU bindings for Lean 4 — write GPU-accelerated graphics and compute programs in Lean, powered by wgpu-native and GLFW.

lean-wgpu provides Lean 4 FFI bindings to the WebGPU API via wgpu-native, along with GLFW bindings for window management and input handling. The bindings are built using Alloy, which allows writing inline C inside Lean source files.

The project ships with 27 example programs covering a wide range of GPU programming topics:

• Lean 4 (v4.28.0) — see lean-toolchain
• clang — used to compile the glfw3webgpu bridge
• wgpu-native — prebuilt static library (see below)
• GLFW 3 — system-installed shared library

macOS:

brew install glfw

Linux (Debian/Ubuntu):

sudo apt install libglfw3-dev

Linux (Arch):

sudo pacman -S glfw

Download the appropriate debug build from the wgpu-native GitHub releases and extract it into the libs/ directory so the structure looks like:

libs/
  wgpu-linux-x86_64-debug/
    libwgpu_native.a
    webgpu.h
    wgpu.h
  # or for macOS:
  wgpu-macos-aarch64-debug/
    libwgpu_native.a
    webgpu.h
    wgpu.h

The lakefile automatically selects the right directory based on your OS and architecture.

lake build

This builds the default target (helloworld— a basic triangle).

Run any example by name:

lake exe helloworld
lake exe coloredtriangle
lake exe computedouble
lake exe raytracer
# ...etc

Or using the -R flag for a release-profile build:

lake -R exe raytracer

├── Wgpu.lean              # Core WebGPU bindings
├── Wgpu/
│   └── Async.lean         # Async callback utilities
├── Glfw.lean              # GLFW window/input bindings
├── Examples/              # 27 example programs
│   ├── Main.lean          # Default triangle example
│   ├── ColoredTriangle.lean
│   ├── RayTracer.lean
│   └── ...
├── glfw3webgpu/           # C bridge: GLFW ↔ WebGPU surface creation
├── libs/                  # wgpu-native prebuilt libraries (user-provided)
├── lakefile.lean          # Build configuration
└── lean-toolchain         # Lean version pin

The bindings use Alloy to embed C code directly in Lean source files. Alloy's alloy c extern and alloy c opaque_extern_type declarations create Lean-accessible wrappers around the C WebGPU API. Opaque extern types are reference-counted by Lean's runtime, with custom finalizers that call the appropriate wgpu*Release functions.

The glfw3webgpu bridge handles the platform-specific logic for creating a WebGPU surface from a GLFW window.

Contributions are welcome! If you'd like to help, some areas that could use attention:

• Expanding binding coverage (not all WebGPU functions are wrapped yet)
• Windows support
• Automatic downloading of wgpu-native in the build
• Higher-level Lean abstractions over the raw C API
• More examples and documentation

• WebGPU specification
• wgpu-native
• LearnWebGPU guide — C++ focused, but explains WebGPU concepts well
• Lean 4 FFI documentation
• Alloy (Lean 4 C FFI)