Towards coqffi.1.0.0 (Call for Testers)

Announcements
#1

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.
  • If you still have any question left, feel free to say hi on Zulip!
2 Likes
#2

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.

Sorry about that.

#3

I am pleased to announce that I have released coq-coqffi.1.0.0~beta3. which is way more significant than anticipated.

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!

#4

I am pleased to announce that I have released coq-coqffi.1.0.0~beta4, which is again more 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!