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 Extraction mechanism.
opam update
opam install coq-coqffi.1.0.0~beta2
Currently, coqffi has a hard dependency for Coq 8.12, but it will probably be relaxed to Coq <= 8.10 before the 1.0.0 release.
If you want to try it, we would love to have your feedback.
You can read the manpage (coqffi --help or man coqffi)
I have released the first two articles of a series on coqffi on my website.
I’ve just found that the link to the literate echo server is wrong in the opening post, and couldn’t find a way to edit it, so here is the correct one.
The coqffi in a Nutshell has been updated to reflect the changes (along with is companion article on how to use coqffi to implement an Echo server in Coq.
I am more than ever looking for courageous volunteer to try coqffi out, as there is probably many bugs yet to be found prior a 1.0.0 release. Therefore, if you have a good usecase for coqffi, but lack time, energy or motivation to do it alone, please, reach out to me. I would love to help!
I am pleased to announce that I have released coq-coqffi.1.0.0~beta4, which is againmore significant than anticipated. This time, I have focused on bug fixes, and quality life improvement. The big new feature of this release is the support of the Lwt framework, although this remains in a very early stage.
The articles have been updated accordingly, although I am strating to suspect I will need to rewrite them from the ground up soon, to give coqffi a proper reference manual.
Again, feel free to reach to me if you are interested in conducting experiments with coqffi!
This will probably be the last beta before a proper 1.0.0 version. To be honest, I feel like said release shoud have happened months agos .
So, one last time, if you happen to use the Coq extraction mechanism feature in a project of yours and want to give coqffi a try to reduce the headache, feel free to reach out to me. I would gladly help.
Out of curiosity, and even if it is unlikely, I will still ask: is there anyone interested in (co-)maintaining coqffi?
I don’t have as much time to improve it, but I still believe it is a very interested project for the Coq ecosystem. I’d be happy to pass the torch to someone else!
.