Crane

Menu

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

Rationale

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 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.

Warning

Crane is under active development. While many features are functional, parts of the extraction pipeline are still experimental, and you may encounter incomplete features or unexpected behavior. Please report issues on the GitHub tracker.

Examples

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.

Installation

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

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.

To preview the project easily and quickly, you can run dune build to run the tests and see if the plugin is working properly on your machine, and find the generated files (such as list.cpp for List.v) 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).

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

Usage

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.

Maintainers

• Joomy Korkut — [email protected]
• Matthew Weaver — [email protected]

Contributions

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.

License

Please refer to the LICENSE file for detailed information.

Code of Conduct

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 [email protected].