I am pleased to announce that
coqffi is almost ready for its first official release, and is already available in the
released repository of the Opam Coq Archive for users to try it.
If you do not already know,
coqffi generates the necessary Coq boilerplate to use OCaml functions in a Coq development, and configures the Coq extraction mechanism accordingly. In practice, it greatly reduces the hassle to use the Coq
opam update opam install coq-coqffi.1.0.0~beta2
coqffi has a hard dependency for Coq
8.12, but it will probably be relaxed to Coq
<= 8.10 before the
If you want to try it, we would love to have your feedback.
- You can read the manpage (
- I have released the first two articles of a series on
coqffion my website.
- If you still have any question left, feel free to say hi on Zulip!