diff options
Diffstat (limited to 'site/posts/CoqffiEcho.org')
| -rw-r--r-- | site/posts/CoqffiEcho.org | 28 |
1 files changed, 16 insertions, 12 deletions
diff --git a/site/posts/CoqffiEcho.org b/site/posts/CoqffiEcho.org index 0c984dc..55ab172 100644 --- a/site/posts/CoqffiEcho.org +++ b/site/posts/CoqffiEcho.org @@ -17,12 +17,16 @@ need to install ~coq-simple-io~. The latter is available in the opam install coq-coqffi coq-simple-io #+END_SRC -Besides, this article is a literate programm, and you can download +Besides, this article is a literate program, and you can download [[/files/coqffi-tutorial.tar.gz][the resulting source tree]] if you want to try to read the source directly, or modify it to your taste. #+TOC: headlines 2 +#+BEGIN_EXPORT html +<div id="history">site/posts/CoqffiEcho.org</div> +#+END_EXPORT + * Project Layout Before diving too much into the implementation of our echo server, we @@ -39,7 +43,7 @@ We have three directories at the root of the project. - ~ffi/~ contains the low-level OCaml code :: It provides an OCaml library (~ffi~), and a Coq theory (~FFI~) which - gathers the FFI modules generated by ~coqffi + gathers the FFI modules generated by ~coqffi. - ~src/~ contains the Coq implementation of our echo server :: It provides a Coq theory (~Echo~) which depends on the ~FFI~ theory the ~SimpleIO~ theory of ~coq-simple~io~. This theory provides the @@ -105,9 +109,9 @@ The rest of this tutorial proceeds by diving into each directory. Our objective is to implement an echo server, /i.e./, a server which (1) accepts incoming connections, and (2) sends back any incoming messages. We will consider two classes of effects. One is related to -creating an manipulating sockets. The other is dedicated to process -management, more precisely to be able to fork when receiving incoming -connections. +creating and manipulating TCP sockets. The other is dedicated to +process management, more precisely to be able to fork when receiving +incoming connections. Therefore, the ~ffi~ library will provide two modules. Likewise, the ~FFI~ theory will provide two analogous modules generated by ~coqffi~. @@ -158,7 +162,7 @@ val close_socket : socket_descr -> unit [@@impure] Our focus is how to write the interface modules for ~coqffi~. Since the object of this tutorial is not the implementation of an echo server in itself, the implementation details of the ~ffi~ library will -not be discuss. +not be discussed. #+BEGIN_details #+HTML: <summary>Implementation for <code>socket.mli</code></summary> @@ -234,7 +238,7 @@ Interested readers can have a look at the generated Coq module below. ** Process Management In order to avoid a client to block the server by connecting to it -without sending anything, we can fork a new process for each clients. +without sending anything, we can fork a new process for each client. #+BEGIN_SRC ocaml :tangle coqffi-tutorial/ffi/proc.mli type identity = Parent of int | Child @@ -293,7 +297,7 @@ with the following content. In the rest of this section, we will discuss the content of the unique module of this theory. Hopefully, readers familiar with programming -impurity by means of monad will not find anything particularly +impurity by means of monads will not find anything particularly surprising here. Let us start with the inevitable sequence of import commands. We use @@ -305,7 +309,7 @@ From ExtLib Require Import Monad MonadFix. From FFI Require Import Proc Socket. #+END_SRC -Letting Coq guessing the type of unintroduced variables using the ~`~ +Letting Coq guess the type of unintroduced variables using the ~`~ annotation (/e.g./, in presence of ~`{Monad m}~, Coq understands ~m~ is of type ~Type -> Type~) is always nice, so we enable it. @@ -387,7 +391,7 @@ program, we will generally prefer the =IO= monad of ~coq-simple-io~. But we could also imagine verifying the client handler with FreeSpec, or the generic TCP server with Interaction Trees (which support diverging computations). Overall, we can have different verification -strategies for different part of our program, by leveraging the most +strategies for different parts of our program, by leveraging the most relevant framework for each part, yet being able to extract it in an efficient form. @@ -403,7 +407,7 @@ expected to generate ~ml~ files. In our case, we will write ~bin/echo.v~ to extract the ~echo_server~ in a ~echo.ml~ module, and uses the =executable= stanza of ~dune~ to get an executable from this file. To achieve this, the ~bin/dune~ -file simply consists in +file simply requires these two stanzas. #+BEGIN_SRC lisp :tangle coqffi-tutorial/bin/dune (coq.extraction @@ -417,7 +421,7 @@ file simply consists in #+END_SRC We are almost done. We now need to write the ~echo.v~ module, which -mostly consists in (1) providing a =MonadFix= instance for the =IO= +mostly consists of (1) providing a =MonadFix= instance for the =IO= monad, (2) using the =IO.unsafe_run= function to escape the =IO= monad, (3) calling the src_coq[:exports code]{Extraction} command to wrap it up. |