summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorThomas Letan <lthms@soap.coffee>2020-12-10 14:15:24 +0100
committerThomas Letan <lthms@soap.coffee>2020-12-10 14:15:24 +0100
commit2706544cf000a6f9875e81f86d885d4dc68dfb23 (patch)
tree5c1cf8ce1f5704dabef5e55353a3f9196894eb1a
parenta611c4e22b5425a0e79604a601ef93f4db51d679 (diff)
Add a Series on coqffi, and the first literate program of this blog
-rw-r--r--.gitignore81
-rw-r--r--site/cleopatra.org2
-rw-r--r--site/cleopatra/coq.org7
-rw-r--r--site/cleopatra/literate-programming.org42
-rw-r--r--site/cleopatra/org.org40
-rw-r--r--site/cleopatra/soupault.org2
-rw-r--r--site/index.org6
-rw-r--r--site/posts/CleopatraV1.org18
-rw-r--r--site/posts/Coqffi.org17
-rw-r--r--site/posts/CoqffiEcho.org468
-rw-r--r--site/posts/CoqffiIntro.org310
11 files changed, 932 insertions, 61 deletions
diff --git a/.gitignore b/.gitignore
index 4fadbbb..3dff654 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,8 +1,11 @@
+*~
# begin generated files
.cleopatra
site/style/coq.sass
coq.mk
+export-lp.el
+literate-programming.mk
.emacs
site/style/org.sass
org.mk
@@ -25,36 +28,78 @@ theme.mk
site/style/main.sass
templates/main.html
build.log
-*.vo
-*.vok
-*.vos
-.*.aux
-*.glob
+site/posts/RewritingInCoq.vo
+site/posts/StronglySpecifiedFunctionsRefine.vo
+site/posts/AlgebraicDatatypes.vo
+site/posts/MixingLtacAndGallina.vo
+site/posts/LtacPatternMatching.vo
+site/posts/ClightIntroduction.vo
+site/posts/StronglySpecifiedFunctionsProgram.vo
+site/posts/LtacMetaprogramming.vo
+site/posts/RewritingInCoq.vok
+site/posts/StronglySpecifiedFunctionsRefine.vok
+site/posts/AlgebraicDatatypes.vok
+site/posts/MixingLtacAndGallina.vok
+site/posts/LtacPatternMatching.vok
+site/posts/ClightIntroduction.vok
+site/posts/StronglySpecifiedFunctionsProgram.vok
+site/posts/LtacMetaprogramming.vok
+site/posts/RewritingInCoq.vos
+site/posts/StronglySpecifiedFunctionsRefine.vos
+site/posts/AlgebraicDatatypes.vos
+site/posts/MixingLtacAndGallina.vos
+site/posts/LtacPatternMatching.vos
+site/posts/ClightIntroduction.vos
+site/posts/StronglySpecifiedFunctionsProgram.vos
+site/posts/LtacMetaprogramming.vos
+site/posts/RewritingInCoq.glob
+site/posts/StronglySpecifiedFunctionsRefine.glob
+site/posts/AlgebraicDatatypes.glob
+site/posts/MixingLtacAndGallina.glob
+site/posts/LtacPatternMatching.glob
+site/posts/ClightIntroduction.glob
+site/posts/StronglySpecifiedFunctionsProgram.glob
+site/posts/LtacMetaprogramming.glob
+site/posts/.RewritingInCoq.aux
+site/posts/.StronglySpecifiedFunctionsRefine.aux
+site/posts/.AlgebraicDatatypes.aux
+site/posts/.MixingLtacAndGallina.aux
+site/posts/.LtacPatternMatching.aux
+site/posts/.ClightIntroduction.aux
+site/posts/.StronglySpecifiedFunctionsProgram.aux
+site/posts/.LtacMetaprogramming.aux
.lia.cache
-site/posts/AlgebraicDatatypes.html
site/posts/RewritingInCoq.html
-site/posts/LtacPatternMatching.html
+site/posts/StronglySpecifiedFunctionsRefine.html
+site/posts/AlgebraicDatatypes.html
site/posts/MixingLtacAndGallina.html
-site/posts/LtacMetaprogramming.html
-site/posts/StronglySpecifiedFunctionsProgram.html
+site/posts/LtacPatternMatching.html
site/posts/ClightIntroduction.html
-site/posts/StronglySpecifiedFunctionsRefine.html
-site/cleopatra.html
+site/posts/StronglySpecifiedFunctionsProgram.html
+site/posts/LtacMetaprogramming.html
+lp/
+site/files/coqffi-tutorial.tar.gz
+site/posts/deps.svg
site/opinions/MonadTransformers.html
site/opinions/index.html
+site/news/ColorlessThemes-0.2.html
+site/projects/index.html
site/cleopatra/soupault.html
-site/cleopatra/coq.html
site/cleopatra/org.html
+site/cleopatra/literate-programming.html
+site/cleopatra/coq.html
site/cleopatra/theme.html
-site/index.html
-site/news/ColorlessThemes-0.2.html
-site/projects/index.html
-site/posts/Thanks.html
+site/posts/ExtensibleTypeSafeErrorHandling.html
+site/posts/CoqffiEcho.html
site/posts/DiscoveringCommonLisp.html
-site/posts/StronglySpecifiedFunctions.html
+site/posts/CoqffiIntro.html
site/posts/CleopatraV1.html
-site/posts/ExtensibleTypeSafeErrorHandling.html
+site/posts/StronglySpecifiedFunctions.html
+site/posts/Thanks.html
site/posts/Ltac.html
+site/posts/Coqffi.html
+site/cleopatra.html
+site/index.html
build/
site/style/main.css
# end generated files
diff --git a/site/cleopatra.org b/site/cleopatra.org
index 67fd917..313007f 100644
--- a/site/cleopatra.org
+++ b/site/cleopatra.org
@@ -40,6 +40,8 @@ written as literate programs.
- [[file:cleopatra/coq.org][Authoring Contents As Coq Documents ~(TODO)~]] ::
+- [[./cleopatra/literate-programming.org][Authoring Literate Programs ~(TODO)~]] ::
+
- [[./cleopatra/org.org][Authoring Contents As Org Documents ~(TODO)~]] ::
- [[./cleopatra/soupault.org][Processing HTML with ~soupault~]] ::
diff --git a/site/cleopatra/coq.org b/site/cleopatra/coq.org
index 7bd5d48..fcbee03 100644
--- a/site/cleopatra/coq.org
+++ b/site/cleopatra/coq.org
@@ -5,13 +5,18 @@
#+BEGIN_SRC makefile :tangle coq.mk
COQ_POSTS := $(shell find site/ -name "*.v")
COQ_HTML := $(COQ_POSTS:.v=.html)
+COQ_ARTIFACTS := $(COQ_POSTS:.v=.vo) \
+ $(COQ_POSTS:.v=.vok) \
+ $(COQ_POSTS:.v=.vos) \
+ $(COQ_POSTS:.v=.glob) \
+ $(join $(dir ${COQ_POSTS}),$(addprefix ".",$(notdir $(COQ_POSTS:.v=.aux))))
coq-build : ${COQ_HTML}
theme-build : site/style/coq.sass
soupault-build : coq-build
-ARTIFACTS += *.vo *.vok *.vos .*.aux *.glob .lia.cache
+ARTIFACTS += ${COQ_ARTIFACTS} .lia.cache
ARTIFACTS += ${COQ_HTML}
COQLIB := "https://coq.inria.fr/distrib/current/stdlib/"
diff --git a/site/cleopatra/literate-programming.org b/site/cleopatra/literate-programming.org
new file mode 100644
index 0000000..7310864
--- /dev/null
+++ b/site/cleopatra/literate-programming.org
@@ -0,0 +1,42 @@
+#+BEGIN_EXPORT html
+<h1>Literate Programming Projects</h1>
+#+END_EXPORT
+
+#+BEGIN_SRC makefile :tangle literate-programming.mk
+literate-programming-prebuild :
+ @cleopatra echo "Tangling" "literate programming project"
+ @cleopatra exec -- cleopatra-run-elisp export-lp.el >> build.log
+
+org-build : literate-programming-build
+
+COQFFI_ARCHIVE := site/files/coqffi-tutorial.tar.gz
+
+coqffi-tutorial-build : literate-programming-prebuild
+ @cleopatra echo "Building" "coqffi tutorial"
+ @cd lp/coqffi-tutorial; dune build --display quiet
+ @cleopatra echo "Archiving" "coqffi tutorial"
+ @rm -f ${COQFFI_ARCHIVE}
+ @tar --exclude="_build" -czvf ${COQFFI_ARCHIVE} lp/coqffi-tutorial >> build.log
+
+literate-programming-build : coqffi-tutorial-build
+
+ARTIFACTS += lp/ ${COQFFI_ARCHIVE} site/posts/deps.svg
+
+#+END_SRC
+
+#+BEGIN_SRC emacs-lisp :tangle export-lp.el
+(cleopatra:configure)
+
+(org-babel-do-load-languages
+ 'org-babel-load-languages
+ '((shell . t)))
+
+(setq org-publish-project-alist
+ '(("lp"
+ :base-directory "site/posts"
+ :publishing-directory "lp"
+ :recursive t
+ :publishing-function cleopatra:tangle-publish)))
+
+(org-publish-all)
+#+END_SRC
diff --git a/site/cleopatra/org.org b/site/cleopatra/org.org
index e6f7a9a..9c2728b 100644
--- a/site/cleopatra/org.org
+++ b/site/cleopatra/org.org
@@ -9,6 +9,8 @@
(use-package haskell-mode :ensure t :defer t)
(use-package toml-mode :ensure t :defer t)
(use-package json-mode :ensure t :defer t)
+(use-package proof-general :ensure t :defer t)
+(use-package tuareg :ensure t :defer t)
(use-package github-modern-theme :ensure t :defer t
:init
(load-theme 'github-modern t))
@@ -17,9 +19,13 @@
#+BEGIN_SRC emacs-lisp :tangle scripts/export-org.el
(cleopatra:configure)
+(setq org-html-doctype "html5")
+(setq org-html-html5-fancy t)
+
(org-babel-do-load-languages
'org-babel-load-languages
- '((shell . t)))
+ '((shell . t)
+ (dot . t)))
(setq org-export-with-toc nil)
@@ -28,37 +34,6 @@
(add-to-list 'org-entities-user
'("mi" "\\)" nil "</span>" "" "" ""))
-(setq org-babel-exp-code-template
- (concat "#+BEGIN_SRC %lang%switches%flags "
- ":tangle %tangle :name %name\n"
- "%body\n"
- "#+END_SRC"))
-
-(defun cleopatra-html-src-block (oldfun src-block contents info)
- (let*
- ((old-ret (funcall oldfun src-block contents info))
- (pars (org-babel-parse-header-arguments
- (org-element-property :parameters src-block)))
- (tangle (cdr (assoc :tangle pars)))
- (name (cdr (assoc :name pars))))
- (cond
- (name
- (concat
- "<div class=\"org-literate-programming\">"
- (format "<div class=\"org-src-name\">&lt;&lt%s&gt;&gt :=</div>" name)
- old-ret
- "</div>"))
- ((not (string= tangle "no"))
- (concat
- "<div class=\"org-literate-programming\">"
- old-ret
- (format "<div class=\"org-src-tangled-to\">%s</div>" tangle)
- "</div>"))
- (t old-ret))))
-
-(advice-add 'org-html-src-block
- :around #'cleopatra-html-src-block)
-
(org-html-export-to-html nil nil nil t)
#+END_SRC
@@ -73,6 +48,7 @@ org-build : ${ORG_HTML}
theme-build : site/style/org.sass
soupault-build : org-build
+org-build : literate-programming-build
ARTIFACTS += ${ORG_HTML}
CONFIGURE += .emacs
diff --git a/site/cleopatra/soupault.org b/site/cleopatra/soupault.org
index 02fe7f4..e7de9bf 100644
--- a/site/cleopatra/soupault.org
+++ b/site/cleopatra/soupault.org
@@ -648,7 +648,7 @@ consequence, we systematically ~touch~ ~packase-lock.json~ to satisfy ~make~.
#+BEGIN_SRC makefile :tangle katex.mk
package-lock.json : package.json
- @echo " init npm packages"
+ @cleopatra echo "Fetching" "npm packages"
@npm install &>> build.log
@touch $@
diff --git a/site/index.org b/site/index.org
index 263395e..ea0d27b 100644
--- a/site/index.org
+++ b/site/index.org
@@ -52,6 +52,12 @@ machine-checked proofs.
means the definitions of ~+~ and ~*~ have to satisfy properties such as
commutativity or the existence of neutral elements.
+- [[./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
+ together OCaml and Coq modules within the same codebase, especially
+ when used together with the ~build~ build system.
+
* About Haskell
Haskell is a pure, lazy, functional programming language with a very expressive
diff --git a/site/posts/CleopatraV1.org b/site/posts/CleopatraV1.org
index 11d796b..ee5789d 100644
--- a/site/posts/CleopatraV1.org
+++ b/site/posts/CleopatraV1.org
@@ -78,7 +78,7 @@ In a nutshell,
For this website, these constants are defined as follows.
-#+BEGIN_SRC makefile :tangle Makefile :noweb no-export
+#+BEGIN_SRC makefile :noweb no-export
ROOT := $(shell pwd)
CLEODIR := site/cleopatra
#+END_SRC
@@ -94,7 +94,7 @@ and providing rules to remove them.
Long-term artifacts whose generation can be time consuming. They will only be
removed by ~make cleanall~.
-#+BEGIN_SRC makefile :tangle Makefile
+#+BEGIN_SRC makefile
ARTIFACTS := build.log
CONFIGURE :=
#+END_SRC
@@ -114,7 +114,7 @@ deleted with ~make clean~ for instance). However, it is overwritten. If you try
to modify it and find that *~cleopatra~* does not work properly, you should
restore it using ~git~.
-#+BEGIN_SRC emacs-lisp :tangle scripts/tangle-org.el
+#+BEGIN_SRC emacs-lisp
(require 'org)
(cd (getenv "ROOT"))
(setq org-confirm-babel-evaluate nil)
@@ -130,7 +130,7 @@ restore it using ~git~.
We define variables that ensure that the ~ROOT~ environment variable is set and
~tangle-org.el~ is loaded when using Emacs.
-#+BEGIN_SRC makefile :tangle Makefile
+#+BEGIN_SRC makefile
EMACSBIN := emacs
EMACS := ROOT="${ROOT}" ${EMACSBIN}
TANGLE := --batch \
@@ -142,7 +142,7 @@ Finally, we introduce a
[[https://www.gnu.org/software/make/manual/html_node/Canned-Recipes.html#Canned-Recipes][canned
recipe]] to seamlessly tangle a given file.
-#+BEGIN_SRC makefile :tangle Makefile
+#+BEGIN_SRC makefile
define emacs-tangle =
echo " tangle $<"
${EMACS} $< ${TANGLE}
@@ -157,7 +157,7 @@ processes. This chain is divided into three stages: ~prebuild~, ~build~, and
This translates as follows in ~Makefile~.
-#+BEGIN_SRC makefile :tangle Makefile
+#+BEGIN_SRC makefile
default : postbuild ignore
init :
@@ -261,7 +261,7 @@ source block when the latter is tangled.
We derive the rule to tangle ~bootstrap.mk~ using =extends=, which gives us the
following Makefile snippet.
-#+BEGIN_SRC makefile :tangle Makefile :noweb yes
+#+BEGIN_SRC makefile :noweb yes
<<extends(IN="Bootstrap.org", PROC="bootstrap", AUX="scripts/update-gitignore.sh")>>
#+END_SRC
@@ -287,7 +287,7 @@ Each generation process shall
* Wrapping-up
-#+BEGIN_SRC bash :tangle scripts/update-gitignore.sh :shebang "#+/bin/bash"
+#+BEGIN_SRC bash :shebang "#+/bin/bash"
BEGIN_MARKER="# begin generated files"
END_MARKER="# begin generated files"
@@ -305,7 +305,7 @@ done
echo ${END_MARKER} >> .gitignore
#+END_SRC
-#+BEGIN_SRC makefile :tangle bootstrap.mk
+#+BEGIN_SRC makefile
ignore :
@echo " update gitignore"
@scripts/update-gitignore.sh \
diff --git a/site/posts/Coqffi.org b/site/posts/Coqffi.org
new file mode 100644
index 0000000..7937901
--- /dev/null
+++ b/site/posts/Coqffi.org
@@ -0,0 +1,17 @@
+#+BEGIN_EXPORT html
+<h1>A Series on <code>coqffi</code></h1>
+#+END_EXPORT
+
+~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.
+
+- [[./CoqffiIntro.org][~coqffi~ in a Nutshell]] ::
+ For each entry of a ~cmi~ file, ~coqffi~ tries to generate an
+ equivalent (from the extraction mechanism perspective) Coq
+ definition. In this article, we walk through how ~coqffi~ works.
+- [[./CoqffiEcho.org][Implementing an Echo Server in Coq with ~coqffi~]] ::
+ In this tutorial, we will demonstrate how ~coqffi~ can be used to
+ implement an echo server, /i.e./, a TCP server which sends back
+ any input it receives from its clients.
diff --git a/site/posts/CoqffiEcho.org b/site/posts/CoqffiEcho.org
new file mode 100644
index 0000000..0c984dc
--- /dev/null
+++ b/site/posts/CoqffiEcho.org
@@ -0,0 +1,468 @@
+#+BEGIN_EXPORT html
+<h1>Implementing an Echo Server in Coq with <code>coqffi</code></h1>
+#+END_EXPORT
+
+#+NAME: coqffi_output
+#+BEGIN_SRC sh :results output :exports none :var mod=""
+cat ${ROOT}/lp/coqffi-tutorial/_build/default/ffi/${mod}
+#+END_SRC
+
+In this article, we will demonstrate how ~coqffi~ can be used to
+implement an echo server, /i.e./, a TCP server which sends back any
+input it receives from its clients. In addition to ~coqffi~, you will
+need to install ~coq-simple-io~. The latter is available in the
+~released~ repository of the Opam Coq Archive.
+
+#+BEGIN_SRC sh
+opam install coq-coqffi coq-simple-io
+#+END_SRC
+
+Besides, this article is a literate programm, 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
+
+* Project Layout
+
+Before diving too much into the implementation of our echo server, we
+first give an overview of the resulting project’s layout. Since we aim
+at implementing a program, we draw our inspiration from the idiomatic
+way of organizing a OCaml project.
+
+#+BEGIN_SRC sh :results output :exports results
+cd ${ROOT}/lp/coqffi-tutorial/
+tree --noreport -I "_build"
+#+END_SRC
+
+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
+- ~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
+ implementation of our echo server in Coq.
+- ~bin/~ contains the pieces of code to get an executable program ::
+ It contains a Coq module (~echo.v~) which configures and uses the
+ extraction mechanism to generate an OCaml module (~echo.ml~). This
+ OCaml module can be compiled to get an executable program.
+
+Note that we could have decided to only have one Coq theory. We could
+also have added a fourth directory (~theories/~) for formal
+verification specific code, but this is out of the scope of this
+tutorial.
+
+Overall, we use ~dune~ to compile and compose the different parts of
+the echo server. ~dune~ has a native —yet unstable at the time of
+writing— support for building Coq projects, with very convenient
+stanzas like =coq.theory= and =coq.extraction=.
+
+The following graph summarizes the dependencies between each component
+(plain arrows symbolize software dependencies).
+
+#+BEGIN_SRC dot :file deps.svg :exports results
+digraph dependencies {
+ graph [nodesep="0.4"];
+ rankdir="LR";
+ node [shape=box];
+ subgraph {
+ rank=same;
+ FFI [label="(coq.theory FFI)"];
+ ffi [label="(library ffi)"];
+ }
+ subgraph {
+ Echo [label="(coq.theory Echo)"];
+ }
+
+ subgraph {
+ rank=same;
+ echo_v [label="(coq.extraction echo)"];
+ echo_ml [label="(executable echo)"];
+ }
+
+ ffi -> FFI [style="dotted" label="generated by coqffi"];
+ echo_ml -> echo_v [dir=back style="dotted" label="generated by Coq"];
+ echo_v -> Echo -> FFI;
+ echo_ml -> ffi;
+}
+#+END_SRC
+
+We enable Coq-related stanza with ~(using coq 0.2)~ in the
+~dune-project~.
+file.
+
+#+BEGIN_SRC lisp :tangle coqffi-tutorial/dune-project
+(lang dune 2.7)
+(using coq 0.2)
+#+END_SRC
+
+The rest of this tutorial proceeds by diving into each directory.
+
+* FFI Bindings
+
+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.
+
+Therefore, the ~ffi~ library will provide two modules. Likewise, the
+~FFI~ theory will provide two analogous modules generated by ~coqffi~.
+
+In the ~ffi/~ directory, we add the following stanza to the ~dune~
+file.
+
+#+BEGIN_SRC lisp :tangle coqffi-tutorial/ffi/dune
+(library
+ (name ffi)
+ (libraries unix))
+#+END_SRC
+
+~dune~ will look for any ~.ml~ and ~.mli~ files within the directory
+and will consider they belong to the ~ffi~ library. We use the
+[[https://caml.inria.fr/pub/docs/manual-ocaml/libref/Unix.html][~unix~]]
+library to implement the features we are looking for.
+
+Then, we add the following stanza to the ~dune~ file of the ~ffi/~
+directory.
+
+#+BEGIN_SRC lisp :tangle coqffi-tutorial/ffi/dune
+(coq.theory
+ (name FFI))
+#+END_SRC
+
+This tells ~dune~ to look for ~.v~ file within the ~ffi/~ directory,
+in order to build them with Coq. A nice feature of ~dune~ is that if
+we automatically generate Coq files, they will be automatically
+“attached” to this theory.
+
+** Sockets
+
+Sockets are boring. The following OCaml module interface provides the
+necessary type and functions to manipulate them.
+
+#+BEGIN_SRC ocaml :tangle coqffi-tutorial/ffi/socket.mli
+type socket_descr
+
+val open_socket : string -> int -> socket_descr [@@impure]
+val listen : socket_descr -> unit [@@impure]
+val recv : socket_descr -> string [@@impure]
+val send : socket_descr -> string -> int [@@impure]
+val accept_connection : socket_descr -> socket_descr [@@impure]
+val close_socket : socket_descr -> unit [@@impure]
+#+END_SRC
+
+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.
+
+#+BEGIN_details
+#+HTML: <summary>Implementation for <code>socket.mli</code></summary>
+
+There is not much to say, except that (as already stated) we use the
+~Unix~ module to manipulate sockets, and we attach to each socket a
+buffer to store incoming bytes.
+
+#+BEGIN_SRC ocaml :tangle coqffi-tutorial/ffi/socket.ml
+let buffer_size = 1024
+
+type socket_descr = {
+ fd : Unix.file_descr;
+ recv_buffer : bytes;
+}
+
+let from_fd fd =
+ let rbuff = Bytes.create buffer_size in
+ { fd = fd; recv_buffer = rbuff }
+
+let open_socket hostname port =
+ let open Unix in
+ let addr = inet_addr_of_string hostname in
+ let fd = socket PF_INET SOCK_STREAM 0 in
+ setsockopt fd SO_REUSEADDR true;
+ bind fd (ADDR_INET (addr, port));
+ from_fd fd
+
+let listen sock = Unix.listen sock.fd 1
+
+let recv sock =
+ let s = Unix.read sock.fd sock.recv_buffer 0 buffer_size in
+ Bytes.sub_string sock.recv_buffer 0 s
+
+let send sock msg =
+ Unix.write_substring sock.fd msg 0 (String.length msg)
+
+let accept_connection sock =
+ Unix.accept sock.fd |> fst |> from_fd
+
+let close_socket sock = Unix.close sock.fd
+#+END_SRC
+#+END_details
+
+~dune~ generates ~.cmi~ files for the ~.mli~ files of our library, and
+provides the necessary bits to easily locate them. Besides, the
+=action= stanza can be used here to tell to ~dune~ how to generate the
+module ~Socket.v~ from ~file.cmi~. We add the following entry to
+~ffi/dune~.
+
+#+BEGIN_SRC lisp :tangle coqffi-tutorial/ffi/dune
+(rule
+ (target Socket.v)
+ (action (run coqffi %{cmi:socket} -o %{target})))
+#+END_SRC
+
+We call ~coqffi~ without any feature-related command-line argument,
+which means only the ~simple-io~ feature is enabled. As a consequence,
+the ~socket_descr~ type is axiomatized in Coq, and in addition to a
+=MonadSocket= monad, ~coqffi~ will generate an instance for this monad
+for the =IO= monad of ~coq-simple-io~.
+
+Interested readers can have a look at the generated Coq module below.
+
+#+BEGIN_details
+#+HTML: <summary><code>Socket.v</code> as generated by <code>coqffi</code></summary>
+
+#+BEGIN_SRC coq :noweb yes
+<<coqffi_output(mod="Socket.v")>>
+#+END_SRC
+#+END_details
+
+** 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.
+
+#+BEGIN_SRC ocaml :tangle coqffi-tutorial/ffi/proc.mli
+type identity = Parent of int | Child
+
+val fork : unit -> identity [@@impure]
+#+END_SRC
+
+#+BEGIN_details
+#+HTML: <summary>Implementation for <code>proc.mli</code></summary>
+
+Again, thanks to the ~Unix~ module, the implementation is pretty
+straightforward.
+
+#+BEGIN_SRC ocaml :tangle coqffi-tutorial/ffi/proc.ml
+type identity = Parent of int | Child
+
+let fork x =
+ match Unix.fork x with
+ | 0 -> Child
+ | x -> Parent x
+#+END_SRC
+#+END_details
+
+This time, the ~proc.mli~ module interface introduces a transparent
+type, /i.e./, it also provides its definition. This is a good use case
+for the ~transparent-types~ feature of ~coqffi~. In the stanza for
+generating ~Proc.v~, we enable it with the ~-ftransparent-types~
+command-line argument, like this.
+
+#+BEGIN_SRC lisp :tangle coqffi-tutorial/ffi/dune
+(rule
+ (target Proc.v)
+ (action (run coqffi -ftransparent-types %{cmi:proc} -o %{target})))
+#+END_SRC
+
+#+BEGIN_details
+#+HTML: <summary><code>Proc.v</code> as generated by <code>coqffi</code></summary>
+#+BEGIN_SRC coq :noweb yes
+<<coqffi_output(mod="Proc.v")>>
+#+END_SRC
+#+END_details
+
+We now have everything we need to implement an echo server in Coq.
+
+* Implementing an Echo Server
+
+Our implementation will be part of a dedicated Coq theory, called
+~Echo~. This is done easily a ~dune~ file in the ~src/~ directory,
+with the following content.
+
+#+BEGIN_SRC lisp :tangle coqffi-tutorial/src/dune
+(coq.theory
+ (name Echo)
+ (theories FFI))
+#+END_SRC
+
+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
+surprising here.
+
+Let us start with the inevitable sequence of import commands. We use
+the =Monad= and =MonadFix= typeclasses of =ExtLib=, and our FFI
+modules from the =FFI= theory we have previously defined.
+
+#+BEGIN_SRC coq :tangle coqffi-tutorial/src/Server.v
+From ExtLib Require Import Monad MonadFix.
+From FFI Require Import Proc Socket.
+#+END_SRC
+
+Letting Coq guessing 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.
+
+#+BEGIN_SRC coq :tangle coqffi-tutorial/src/Server.v
+Generalizable All Variables.
+#+END_SRC
+
+We enable the monad notation provided by =ExtLib=. In this article, we
+prefer the ~let*~ notation (as recently introduced by OCaml) over the
+~<-~ notation of Haskell, but both are available.
+
+#+BEGIN_SRC coq :tangle coqffi-tutorial/src/Server.v
+Import MonadLetNotation.
+Open Scope monad_scope.
+#+END_SRC
+
+Then, we define a notation to be able to define local, monadic
+recursive functions using the =mfix= combinator of the =MonadFix=
+typeclass.
+
+#+BEGIN_SRC coq :tangle coqffi-tutorial/src/Server.v
+Notation "'let_rec*' f x ':=' p 'in' q" :=
+ (let f := mfix (fun f x => p) in q)
+ (at level 61, x pattern, f ident, q at next level, right associativity).
+#+END_SRC
+
+Note that ~mfix~ does /not/ check whether or not the defined function
+will terminate (contrary to the ~fix~ keyword of Coq). This is
+fortunate because in our case, we do not want our echo server to
+converge, but rather to accept an infinite number of connections.
+
+We can demonstrate how this notation can be leveraged by defining a
+generic TCP server, parameterized by a handler to deal with incoming
+connections.
+
+#+BEGIN_SRC coq :tangle coqffi-tutorial/src/Server.v
+Definition tcp_srv `{Monad m, MonadFix m, MonadProc m, MonadSocket m}
+ (handler : socket_descr -> m unit)
+ : m unit :=
+ let* srv := open_socket "127.0.0.1" 8888 in
+ listen srv;;
+
+ let_rec* tcp_aux _ :=
+ let* client := accept_connection srv in
+ let* res := fork tt in
+ match res with
+ | Parent _ => close_socket client >>= tcp_aux
+ | Child => handler client
+ end
+ in
+
+ tcp_aux tt.
+#+END_SRC
+
+The handler for the echo server is straightforward: it just reads
+incoming bytes from the socket, sends it back, and closes the socket.
+
+#+BEGIN_SRC coq :tangle coqffi-tutorial/src/Server.v
+Definition echo_handler `{Monad m, MonadSocket m} (sock : socket_descr)
+ : m unit :=
+ let* msg := recv sock in
+ send sock msg;;
+ close_socket sock.
+#+END_SRC
+
+Composing our generic TCP server with our echo handler gives us an
+echo server.
+
+#+BEGIN_SRC coq :tangle coqffi-tutorial/src/Server.v
+Definition echo_server `{Monad m, MonadFix m, MonadProc m, MonadSocket m}
+ : m unit :=
+ tcp_srv echo_handler.
+#+END_SRC
+
+Because ~coqffi~ has generated typeclasses for the impure primitives
+of ~proc.mli~ and ~socket.mli~, =echo_server= is polymorphic, and can
+be instantiated for different monads. When it comes to extracting our
+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
+relevant framework for each part, yet being able to extract it in an
+efficient form.
+
+The next section shows how this last part is achieved using, once
+again, a convenient stanza of dune.
+
+* Extracting and Building an Executable
+
+The ~0.2~ version of the Coq-related stanzas of ~dune~ provides the
+~coq.extraction~ stanza, which can be used to build a Coq module
+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
+
+#+BEGIN_SRC lisp :tangle coqffi-tutorial/bin/dune
+(coq.extraction
+ (prelude echo)
+ (theories Echo)
+ (extracted_modules echo))
+
+(executable
+ (name echo)
+ (libraries ffi))
+#+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=
+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.
+
+#+BEGIN_SRC coq :tangle coqffi-tutorial/bin/echo.v
+From Coq Require Extraction.
+From ExtLib Require Import MonadFix.
+From SimpleIO Require Import SimpleIO.
+From Echo Require Import Server.
+
+Instance MonadFix_IO : MonadFix IO :=
+ { mfix := @IO.fix_io }.
+
+Definition main : io_unit :=
+ IO.unsafe_run echo_server.
+
+Extraction "echo.ml" main.
+#+END_SRC
+
+Since we are using the =i63= type (signed 63bits integers) of the
+~CoqFFI~ theory, and since =i63= is implemented under the hood with
+Coq primitive integers, we /also/ need to provide a =Uint63= module
+with a =of_int= function. Fortunately, this module is straightforward
+to write.
+
+#+BEGIN_SRC ocaml :tangle coqffi-tutorial/bin/uint63.ml
+let of_int x = x
+#+END_SRC
+
+And /voilà/. A call to ~dune~ at the root of the repository will
+build everything (Coq and OCaml alike). Starting the echo server
+is as simple as
+
+#+BEGIN_SRC sh
+dune exec bin/echo.exe
+#+END_SRC
+
+And connecting to it can be achieved with a program like =telnet=.
+
+#+BEGIN_SRC console
+$ telnet 127.0.0.1 8888
+Trying 127.0.0.1...
+Connected to 127.0.0.1.
+Escape character is '^]'.
+hello, echo server!
+hello, echo server!
+Connection closed by foreign host.
+#+END_SRC
diff --git a/site/posts/CoqffiIntro.org b/site/posts/CoqffiIntro.org
new file mode 100644
index 0000000..dc76940
--- /dev/null
+++ b/site/posts/CoqffiIntro.org
@@ -0,0 +1,310 @@
+#+BEGIN_EXPORT html
+<h1><code>coqffi</code> in a Nutshell</h1>
+#+END_EXPORT
+
+For each entry of a ~cmi~ file, ~coqffi~ tries to generate an
+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.
+
+#+TOC: headlines 2
+
+* 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]].
+
+** Installing ~coqffi~
+
+The recommended way to install ~coqffi~ is through the
+[[https://coq.inria.fr/opam/www][Opam Coq Archive]], in the ~released~
+repository. If you haven’t activated this repository yet, you can use
+the following bash command.
+
+#+BEGIN_SRC sh
+opam repo add coq-released https://coq.inria.fr/opam/released
+#+END_SRC
+
+Then, installing ~coqffi~ is as simple as
+
+#+BEGIN_SRC sh
+opam install coq-coqffi
+#+END_SRC
+
+You can also get the source from
+[[https://github.com/coq-community/coqffi][the upstream ~git~
+repository]]. The ~README~ provides the necessary pieces of
+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,
+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
+[[https://github.com/ANSSI-FR/FreeSpec][FreeSpec]]. It is also
+possible to use it with
+[[https://github.com/DeepSpec/InteractionTrees][Interaction Trees]],
+albeit in a less direct manner.
+
+
+* Primitives Types
+
+~coqffi~ supports a set of primitives 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
+generated too).
+
+| Ocaml type | Coq type |
+|-------------+-------------------------------|
+| =bool= | =Coq.Init.Datatypes.bool= |
+| =char= | =Coq.Strings.Ascii.ascii= |
+| =int= | =CoqFFI.Data.Int.i63= |
+| ='a list= | =Coq.Init.Datatypes.list a= |
+| ='a option= | =Coq.Init.Datatypes.option a= |
+| =string= | =Coq.Strings.String.string= |
+| =unit= | =Coq.Init.Datatypes.unit= |
+
+The =i63= type is introduced by the =CoqFFI= theory to provide signed
+primitive integers to Coq users. They are implemented on top of the
+(sadly unsigned) Coq native integers introduced in Coq
+~8.10~. Hopefully, the =i63= type will be deprecated once [[https://github.com/coq/coq/pull/13559][signed
+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
+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.
+
+** Types
+
+By default, ~coqffi~ generates axiomatized definitions for each type
+defined in a ~cmi~ files. 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}.
+
+It is possible to provide a “model” for a type using the =coq_model=
+annotation, for instance for reasoning purposes. For instance,
+we can specify that a type is equivalent to a =list=.
+
+#+BEGIN_SRC ocaml
+type 'a t [@@coq_model "list"]
+#+END_SRC
+
+This generates the following Coq definition.
+
+#+BEGIN_SRC coq
+Definition t : forall (a : Type), Type := list.
+#+END_SRC
+
+It is important to be careful when using the =coq_model= annotation.
+More precisely, the fact that =t= is a =list= in the “Coq universe”
+shall not be used while the implementation phase, only the
+verification phase.
+
+Finally, ~coqffi~ has got an experimental feature called
+~transparent-types~ (enable by using the ~-ftransparent-types~
+command-line argument). If the type definition is given in the module
+interface, then ~coqffi~ tries to generates an equivalent definition
+in Coq. For instance,
+
+#+BEGIN_SRC ocaml
+type 'a llist =
+ | LCons of 'a * (unit -> 'a llist)
+ | LNil
+#+END_SRC
+
+becomes
+
+#+BEGIN_SRC coq
+Inductive llist (a : Type) : Type :=
+| LCons (x0 : a) (x1 : unit -> llist a) : llist a
+| LNil : llist a.
+#+END_SRC
+
+Mutually recursive types are supported, so
+
+#+BEGIN_SRC ocaml
+type even = Zero | ESucc of odd
+and odd = OSucc of even
+#+END_SRC
+
+becomes
+
+#+BEGIN_SRC coq
+Inductive odd : Type :=
+| OSucc (x0 : even) : odd
+with even : Type :=
+| Zero : even
+| ESucc (x0 : odd) : even.
+#+END_SRC
+
+The ~transparent-types~ feature is *experimental*, and is currently
+limited to variant types. It notably does not support
+records. Besides, it may generate incorrect Coq types, because it does
+not check whether or not the
+[[https://coq.inria.fr/refman/language/core/inductive.html#positivity-condition][positivity
+condition]] is satisfied.
+
+** Pure Functions
+
+~coqffi~ assumes OCaml values are pure by default, and will generate
+regular axiomatized Coq definitions for them. Similarly to type
+entries, it is possible to provide a Coq model using the =coq_module=
+annotation.
+
+#+BEGIN_SRC ocaml
+val unpack : string -> (char * string) option
+#+END_SRC
+
+becomes
+
+#+BEGIN_SRC coq
+Axiom unpack : string -> option (ascii * string).
+#+END_SRC
+
+Polymorphic functions are supported.
+
+#+BEGIN_SRC ocaml
+val map : ('a -> 'b) -> 'a list -> 'b list
+#+END_SRC
+
+becomes
+
+#+BEGIN_SRC coq
+Axiom map : forall (a : Type) (b : Type), (a -> b) -> list a -> list b.
+#+END_SRC
+
+** Impure Primitives
+
+Finally, ~coqffi~ reserves a special treatment for OCaml value
+explicitely 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.
+
+Given the set of impure primitives declared in an interface module,
+~coqffi~ will (1) generates a typeclass which gathers these
+primitives, and (2) generates instances of this typeclass for
+supported backends.
+
+We illustrate the rest of this section with the following impure
+primitives.
+
+#+BEGIN_SRC ocaml
+val echo : string -> unit [@@impure]
+val scan : unit -> string [@@impure]
+#+END_SRC
+
+where =echo= allows to write something the standard output, and =scan=
+to read the standard input.
+
+Assuming the processed module interface is named ~console.mli~, the
+following Coq typeclass is generated.
+
+#+BEGIN_SRC coq
+Class MonadConsole (m : Type -> Type) := { echo : string -> m unit
+ ; scan : unit -> m string
+ }.
+#+END_SRC
+
+Using this typeclass and with the additional support of an additional
+=Monad= typeclass, we can specify impure computations which interacts
+with the console. For instance, with the support of ~ExtLib~, one can
+write.
+
+#+BEGIN_SRC coq
+Definition pipe `{Monad m, MonadConsole m} : m unit :=
+ let* msg := scan () in
+ echo msg.
+#+END_SRC
+
+There is no canonical way to model impurity in Coq, but over the years
+several frameworks have been released to tackle this challenge.
+
+~coqffi~ provides three features related to impure primitives.
+
+*** ~simple-io~
+
+This feature allows to generate 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.
+Axiom io_scan : unit -> IO string.
+
+Instance IO_MonadConsole : MonadConsole IO := { echo := io_echo
+ ; scan := io_scan
+ }.
+#+END_SRC
+
+It is enabled by default, but can be disabled using the
+~-fno-simple-io~ command-line argument.
+
+*** ~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
+[[https://github.com/DeepSpec/InteractionTrees][Interactions Trees]]
+
+#+BEGIN_SRC coq
+Inductive CONSOLE : Type -> Type :=
+| Echo : string -> CONSOLE unit
+| Scan : unit -> CONSOLE string.
+
+Definition inj_echo `{Inject CONSOLE m} (x0 : string) : m unit :=
+ inject (Echo x0).
+
+Definition inj_scan `{Inject CONSOLE m} (x0 : unit) : m string :=
+ inject (Scan x0).
+
+Instance Inject_MonadConsole `{Inject CONSOLE m} : MonadConsole m :=
+ { echo := inj_echo
+ ; scan := inj_scan
+ }.
+#+END_SRC
+
+Providing an instance of the form src_coq[:exports code]{forall i,
+Inject i M} is enough for your monad =M= to be compatible with this
+feature (see for instance
+[[https://github.com/ANSSI-FR/FreeSpec/blob/master/theories/FFI/FFI.v][how
+FreeSpec implements it]]).
+
+*** ~freespec~
+
+It allows to generate a semantics for the inductive type generated by
+the ~interface~ feature.
+
+#+BEGIN_SRC coq
+Axiom unsafe_echo : string -> unit.
+Axiom unsafe_scan : uint -> string.
+
+Definition console_unsafe_semantics : semantics CONSOLE :=
+ bootstrap (fun a e =>
+ local match e in CONSOLE a return a with
+ | Echo x0 => unsafe_echo x0
+ | Scan x0 => unsafe_scan x0
+ end).
+#+END_SRC
+
+* Moving Forward
+
+~coqffi~ comes with a comprehensive man page. In addition, the
+interested reader can proceed to the next article of this series,
+which explains how [[./CoqffiEcho.org][~coqffi~ can be used to easily
+implement an echo server in Coq]].