• Rationale
• Installation
• Usage
• Maintainers
• Contributions
• License

This project provides extraction of Rocq (formerly known as Coq) code to (optionally BDE-flavored) C++ code, implemented as a Rocq plugin. It extracts Rocq into valid, performant, and memory-safe, modern C++ code. The generated code avoids tracing garbage collection and does not need a separate runtime system, relying instead on std::shared_ptr or bsl::shared_ptr for reference counting.

The project is a fork of the Rocq-to-OCaml extraction that comes built-in with Rocq.

A curated selection of C++ files generated by Crane (accompanied with their source Rocq programs) is available to view in the tests directory. The tests are organized thematically, with tests/basics containing traditional, functional Rocq progams, and tests/monadic containing effectful examples.

Once you clone the repo, if you have opam and dune, you can run

opam install . --deps-only

To install OCaml (at least 4.14.0) and Rocq (at least 9.0.0). You can then build and install the project by running

make build && make install

Or using dune directly:

dune build -p rocq-crane && dune install

You will also need Clang 19 or higher to run the tests, and clang-format for standard formatting.

The Makefile provides convenient build commands:

• make build - Build only the plugin and theories (recommended for development, fast)
• make extract - Build the plugin and extract all of the tests (without compiling the generated code)
• make test - Build and run all tests with clean summary output
• make test-verbose - Run tests with detailed output
• make test-one TEST=name - Run a single test (e.g., make test-one TEST=list)
• make test-list - List all available tests
• make all - Build everything including tests
• make clean - Clean all build and test artifacts
• make help - Show all available commands

To preview the project, you can run make test to run the tests and see if the plugin is working properly on your machine. The test command will show a summary of passed/failed tests with a progress indicator. To run a single test during development, use make test-one TEST=list (or tree, nat, etc.). Use make test-list to see all available test names. Generated files (such as list.cpp for List.v) will be in the tests directory. Currently not all tests in the directory are expected to pass (and thus some failing does not mean the plugin is installed incorrectly).

For typical development, use make build to quickly rebuild after changes to src/ or theories/, then make test to verify your changes work correctly.

If you prefer to use dune directly:

# Build plugin and theories only
dune build src && dune build theories

# Build everything including tests
dune build

# Run tests (builds them first if needed)
dune runtest

Tests are organized by category in tests/basics/ (basic functionality) and tests/monadic/ (monadic code). Tests are not built by make build to keep development builds fast—use make test or dune runtest to build and run them.

Some tests use Bloomberg's BDE library. These are optional.

If you have BDE installed: The build will auto-detect BDE in common locations (~/Library/bde_install, ~/bde_install, /opt/bb). If installed elsewhere, set BDE_PREFIX:

export BDE_PREFIX=/path/to/bde_install
make test-one TEST=nat_bde

If you don't have BDE: BDE tests will fail with "file not found" errors—this is expected and can be ignored. All non-BDE tests will still run normally.

To run the Crane Benchmark command, you will need to have hyperfine installed.

Once you write your Rocq program, you can extract to C++:

Module Foo.

Fixpoint fac n :=
  match n with
  | 0 | 1 => 1
  | S n' => n * fac n'
  end.

End Foo.

Require Crane.Extraction.
Require Crane.Mapping.Std.
Crane Extraction "Foo" Foo.

(You can also extract a single function if you do not want to extract an entire module, which will just extract the function with all of its dependencies as opposed to this which extracts all the definitions in the module [and their dependencies].)

Now run:

rocq compile Foo.v && clang++ -c -std=c++23 Foo.cpp -o Foo.o

This command creates Foo.h and Foo.cpp files from the Rocq file, and the compiles the C++ to the object file Foo.o with Clang, ready to be linked to your own C++ file containing a main function for execution.

• Joomy Korkut — jkorkut@bloomberg.net
• Matthew Weaver — mweaver89@bloomberg.net

We ❤️ contributions.

If you've had a good experience with this project or wish to contribute improvements, we'd love to hear from you. Feel free to submit issue reports or suggestions, making sure to select an appropriate issue template.

Before opening a pull request, please review our contribution guidelines.

Please refer to the LICENSE file for detailed information.

This project has adopted a Code of Conduct. If you have any concerns about the code or behavior which you have experienced in the project, please contact us at opensource@bloomberg.net.