Rocqman

Rocqman is a Pacman-like game written in Rocq and extracted to C++ with Crane. The game uses the separate rocq-crane-sdl2 bindings submodule for SDL2 rendering, SDL2_image texture loading, SDL2_mixer audio playback, and itree-based effectful functions. This establishes, at least informally, that Rocq is Pacman-complete.

Features

• game logic written in Rocq
• extraction to C++ with Crane
• SDL2 rendering
• smooth sprite interpolation
• sound effects for dots, power pellets, ghost kills, losing a life, game over, and victory

Requirements

You need:

• Rocq with dune
• a C++23 compiler
• pkg-config
• SDL2
• SDL2_image
• SDL2_mixer
• Emscripten, if you want to build the WebAssembly page

Getting started

Clone the repo with everything it needs:

git clone --recurse-submodules https://github.com/joom/rocqman.git
cd rocqman

If you already cloned it without submodules, run:

git submodule update --init --recursive

Installing dependencies

macOS

Install the SDL packages with Homebrew:

brew install sdl2 sdl2_image sdl2_mixer

If you want to use Homebrew LLVM instead of the system toolchain:

brew install llvm

Linux

The exact package names vary by distribution, but you generally need:

sudo apt install clang pkg-config libsdl2-dev libsdl2-image-dev libsdl2-mixer-dev

Building

Build the game:

make

This does four things:

1. uses the local Crane checkout in ./crane
2. builds and installs the local rocq-crane-sdl2 submodule
3. extracts theories/Rocqman.v to C++
4. copies the generated C++ into src/generated/
5. compiles the final executable ./rocqman

Build with a different optimization level:

make OPT=-O2

Build the WebAssembly page:

make web

This writes the browser build to docs/index.html and the accompanying Emscripten outputs in docs/.

Running

Run the game:

make run

or:

./rocqman

Controls:

• arrow keys or WASD: move
• Space: pause or unpause
• Q or Esc: quit

Cleaning

Remove build outputs:

make clean

This removes:

• ./rocqman
• ./src/generated/
• ./rocqman.dSYM
• Dune build outputs

Repository structure

.
├── assets/
│   ├── *.mp3           sound effects
│   └── rocq.svg        player sprite
├── crane/              Crane submodule used for extraction
├── rocq-crane-sdl2/    SDL2 bindings submodule used by extraction
├── theories/
│   ├── Rocqman.v       game logic, rendering, extracted main
│   ├── RocqmanProofs.v proofs about gameplay transitions and control flow
│   └── dune            Rocq theory stanza
├── src/
│   ├── web_main.cpp    Emscripten frame-loop wrapper
│   └── web_shell.html  browser page shell used by make web
├── docs/               generated WebAssembly page
├── Makefile            extraction and native build entrypoint
├── dune-project        Dune project file
└── README.md

Generated files are written to:

src/generated/

These are build artifacts and should not be edited manually.

What Is Proved

The file theories/RocqmanProofs.v contains machine-checked proofs about the current game logic. At the moment, those proofs show that the pure gameplay transitions used by the frame loop preserve key monotonicity properties: score never decreases, lives never increase, and the number of collectibles left never increases. It also proves that terminal logical states are fixed points of tick, that paused gameplay stays paused until space is pressed, that pressing space while paused returns to Playing, and that WinScreen and GameOverScreen eventually request quit once enough time has elapsed.

Development notes

• The authoritative game logic lives in Rocq, not in the generated C++.
• The build expects Crane at crane/.
• The build expects the SDL bindings submodule at rocq-crane-sdl2/.
• Rocqman imports CraneSDL2 directly and runs its game loop as itree sdlE.
• The extracted program defines its own main, so there is no separate handwritten main.cpp.