A series on
coqffi generates Coq FFI modules from compiled OCaml interface
.cmi). In practice, it greatly reduces the hassle to mix
OCaml and Coq modules within the same codebase, especially when used
together with the
dune build system.
coqffiin a Nutshell
- For each entry of a
coqffitries to generate an equivalent (from the extraction mechanism perspective) Coq definition. In this article, we walk through how
- Implementing an Echo Server in Coq with
- In this tutorial, we will demonstrate how
coqffican be used to implement an echo server, i.e., a TCP server which sends back any input it receives from its clients.