diff options
Diffstat (limited to 'site')
| -rw-r--r-- | site/index.org | 4 | ||||
| -rw-r--r-- | site/posts/Coqffi.org | 4 | ||||
| -rw-r--r-- | site/posts/CoqffiEcho.org | 28 | ||||
| -rw-r--r-- | site/posts/CoqffiIntro.org | 53 |
4 files changed, 48 insertions, 41 deletions
diff --git a/site/index.org b/site/index.org index ea0d27b..e1b61bc 100644 --- a/site/index.org +++ b/site/index.org @@ -54,9 +54,9 @@ machine-checked proofs. - [[./posts/Coqffi.org][A Series on ~coqffi~]] :: ~coqffi~ generates Coq FFI modules from compiled OCaml interface - modules (~.cmi~). In practice, it greatly reduces the hassle to mix + modules (~.cmi~). In practice, it greatly reduces the hassle to together OCaml and Coq modules within the same codebase, especially - when used together with the ~build~ build system. + when used together with the ~dune~ build system. * About Haskell diff --git a/site/posts/Coqffi.org b/site/posts/Coqffi.org index 7937901..3d8b867 100644 --- a/site/posts/Coqffi.org +++ b/site/posts/Coqffi.org @@ -4,8 +4,8 @@ ~coqffi~ generates Coq FFI modules from compiled OCaml interface modules (~.cmi~). In practice, it greatly reduces the hassle to mix -together OCaml and Coq modules within the same codebase, especially -when used together with the ~build~ build system. +OCaml and Coq modules within the same codebase, especially when used +together with the ~dune~ build system. - [[./CoqffiIntro.org][~coqffi~ in a Nutshell]] :: For each entry of a ~cmi~ file, ~coqffi~ tries to generate an 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. diff --git a/site/posts/CoqffiIntro.org b/site/posts/CoqffiIntro.org index dc76940..d622e03 100644 --- a/site/posts/CoqffiIntro.org +++ b/site/posts/CoqffiIntro.org @@ -7,19 +7,23 @@ equivalent (from the extraction mechanism perspective) Coq definition. In this article, we walk through how ~coqffi~ works. Note that we do not dive into the vernacular commands ~coqffi~ -generates. They are of no concern for ~coqffi~’s users. +generates. They are of no concern for users of ~coqffi~. #+TOC: headlines 2 +#+BEGIN_EXPORT html +<div id="history">site/posts/CoqffiIntro.org</div> +#+END_EXPORT + * Getting Started ** Requirements -The latest versiof of ~coqffi~ (~coqffi.1.0.0~beta2~ at the time of -writing) is compatible with OCaml ~4.08~ up to ~4.11~, and Coq ~8.12~. -If you want to use ~coqffi~, but have incompatible requirements of -your own, feel free to -[[https://github.com/coq-community/coqffi/issues][submit an issue]]. +The latest version of ~coqffi~ (~1.0.0~beta2~ at the time of writing) +is compatible with OCaml ~4.08~ up to ~4.11~, and Coq ~8.12~. If you +want to use ~coqffi~, but have incompatible requirements of your own, +feel free to [[https://github.com/coq-community/coqffi/issues][submit +an issue]]. ** Installing ~coqffi~ @@ -46,7 +50,7 @@ information to build it from source. ** Additional Dependencies One major difference between Coq and OCaml is that the former is pure, -while the latter is not. Impurity can be modelled in pure languages, +while the latter is not. Impurity can be modeled in pure languages, and Coq does not lack of frameworks in this respect. ~coqffi~ currently supports two of them: [[https://github.com/Lysxia/coq-simple-io][~coq-simple-io~]] and @@ -56,15 +60,15 @@ possible to use it with albeit in a less direct manner. -* Primitives Types +* Primitive Types -~coqffi~ supports a set of primitives types, /i.e./, a set of OCaml +~coqffi~ supports a set of primitive types, /i.e./, a set of OCaml types for which it knows an equivalent type in Coq. The list is the following (the Coq types are fully qualified in the table, but not in -the generated Coq module as the necessry ~Import~ statement are +the generated Coq module as the necessary ~Import~ statement are generated too). -| Ocaml type | Coq type | +| OCaml type | Coq type | |-------------+-------------------------------| | =bool= | =Coq.Init.Datatypes.bool= | | =char= | =Coq.Strings.Ascii.ascii= | @@ -81,19 +85,18 @@ primitive integers to Coq users. They are implemented on top of the primitive integers find their way to Coq upstream]]. When processing the entries of a given interface model, ~coqffi~ will -checks that they only use these types, or types introduced by the +check that they only use these types, or types introduced by the interface module itself. * Code Generation -~coqffi~ distinguishes three types of entries: -types, pure functions, and impure primitives. We now discuss how each -one of them are handled. +~coqffi~ distinguishes three types of entries: types, pure functions, +and impure primitives. We now discuss how each one of them is handled. ** Types By default, ~coqffi~ generates axiomatized definitions for each type -defined in a ~cmi~ files. This means that src_ocaml[:exports +defined in a ~.cmi~ file. This means that src_ocaml[:exports code]{type t} becomes src_coq[:exports code]{Axiom t : Type}. Polymorphism is supported, /i.e./, src_ocaml[:exports code]{type 'a t} becomes src_coq[:exports code]{Axiom t : forall (a : Type), Type}. @@ -193,7 +196,7 @@ Axiom map : forall (a : Type) (b : Type), (a -> b) -> list a -> list b. ** Impure Primitives Finally, ~coqffi~ reserves a special treatment for OCaml value -explicitely marked as impure, using the =impure= annotation. Impurity +explicitly marked as impure, using the =impure= annotation. Impurity is usually handled in pure programming languages by means of monads, and ~coqffi~ is no exception to the rule. @@ -210,7 +213,7 @@ val echo : string -> unit [@@impure] val scan : unit -> string [@@impure] #+END_SRC -where =echo= allows to write something the standard output, and =scan= +where =echo= allows writing something the standard output, and =scan= to read the standard input. Assuming the processed module interface is named ~console.mli~, the @@ -240,8 +243,8 @@ several frameworks have been released to tackle this challenge. *** ~simple-io~ -This feature allows to generate an instance of the typeclass for the -=IO= monad introduced in the ~coq-simple-io~ package +When this feature is enabled, ~coqffi~ generates an instance of the +typeclass for the =IO= monad introduced in the ~coq-simple-io~ package #+BEGIN_SRC coq Axiom io_echo : string -> IO unit. @@ -257,9 +260,9 @@ It is enabled by default, but can be disabled using the *** ~interface~ -This feature allows to generate an inductive type which describes the -set of primitives available, to be used with frameworks like -[[https://github.com/ANSSI-FR/FreeSpec][FreeSpec]] or +When this feature is enabled, ~coqffi~ generates an inductive type +which describes the set of primitives available, to be used with +frameworks like [[https://github.com/ANSSI-FR/FreeSpec][FreeSpec]] or [[https://github.com/DeepSpec/InteractionTrees][Interactions Trees]] #+BEGIN_SRC coq @@ -287,8 +290,8 @@ FreeSpec implements it]]). *** ~freespec~ -It allows to generate a semantics for the inductive type generated by -the ~interface~ feature. +When this feature in enabled, ~coqffi~ generates a semantics for the +inductive type generated by the ~interface~ feature. #+BEGIN_SRC coq Axiom unsafe_echo : string -> unit. |