|author||Thomas Letan <firstname.lastname@example.org>||2021-02-24 13:50:57 +0100|
|committer||Thomas Letan <email@example.com>||2021-02-24 13:50:57 +0100|
|parent||Add some news about January, 2021 (diff)|
Release of coqffi 1.0.0~beta4
Diffstat (limited to 'site/posts/CoqffiIntro.org')
1 files changed, 106 insertions, 32 deletions
diff --git a/site/posts/CoqffiIntro.org b/site/posts/CoqffiIntro.org
index d7d9482..053826b 100644
@@ -2,9 +2,10 @@
<h1><code>coqffi</code> in a Nutshell</h1>
-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.
+For each entry of a ~cmi~ file (a /compiled/ ~mli~ file), ~coqffi~
+tries to generate an equivalent (from the extraction mechanism
+perspective) Coq definition. In this article, we walk through how
Note that we do not dive into the vernacular commands ~coqffi~
generates. They are of no concern for users of ~coqffi~.
@@ -19,7 +20,7 @@ generates. They are of no concern for users of ~coqffi~.
-The latest version of ~coqffi~ (~1.0.0~beta3~ at the time of writing)
+The latest version of ~coqffi~ (~1.0.0~beta4~ 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
@@ -52,13 +53,9 @@ information to build it from source.
One major difference between Coq and OCaml is that the former is pure,
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/ANSSI-FR/FreeSpec][FreeSpec]]. It is also
-possible to use it with
-albeit in a less direct manner.
+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
* Primitive Types
@@ -68,15 +65,18 @@ following (the Coq types are fully qualified in the table, but not in
the generated Coq module as the necessary ~Import~ statement are
-| 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= |
+| 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 Seq.t= | =CoqFFI.Data.Seq.t= |
+| ='a option= | =Coq.Init.Datatypes.option a= |
+| =('a, 'e) result= | =Coq.Init.Datatypes.sum= |
+| =string= | =Coq.Strings.String.string= |
+| =unit= | =Coq.Init.Datatypes.unit= |
+| =exn= | =CoqFFI.Exn= |
The =i63= type is introduced by the =CoqFFI= theory to provide signed
primitive integers to Coq users. They are implemented on top of the
@@ -88,11 +88,60 @@ When processing the entries of a given interface model, ~coqffi~ will
check that they only use these types, or types introduced by the
interface module itself.
+Sometimes, you may encounter a situation where you have two interface
+modules ~b.mli~ and ~b.mli~, such that ~b.mli~ uses a type introduced
+in ~a.mli~. To deal with this scenario, you can use the ~--witness~
+flag to generate ~A.v~. This will tell ~coqffi~ to also generate
+~A.ffi~; this file can then be used when generating ~B.v~ thanks to
+the ~-I~ option. Furthermore, for ~B.v~ to compile the ~--require~
+option needs to be used to ensure the ~A~ Coq library (~A.v~) is
+To give a more concrete example, given ~a.mli~
+type a = A.t
+To generate ~A.v~, we can use the following commands:
+coqffi --witness -o A.v a.cmi
+Which would generate the following axiom for =t=.
+Axiom t : Type.
+Then, generating ~B.v~ can be achieved as follows:
+coqffi -I A.ffi -ftransparent-types -r A -o B.v b.cmi
+which results in the following output for =v=:
+Definition u : Type := A.t.
* Code Generation
~coqffi~ distinguishes five types of entries: types, pure values,
-impure primitives, exceptions, and exceptions. We now discuss how each
-one of them is handled.
+impure primitives, asynchronous primitives, exceptions, and
+modules. We now discuss how each one of them is handled.
@@ -172,12 +221,14 @@ with even : Type :=
| ESucc (x0 : odd) : even.
+Besides, ~coqffi~ supports alias types, as suggested in this write-up
+when we discuss witness files.
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. Similarly, it has *not* been tested with OCaml GADT yet,
-and will most certainly produced ill-formed code.
** Pure values
@@ -188,6 +239,9 @@ with the following heuristics:
- Functions are impure by default
- Functions with a =coq_model= annotation are pure
- Functions marked with the =pure= annotation are pure
+- If the ~pure-module~ feature is enabled (~-fpure-module~),
+ then synchronous functions (which do not live inside the [[https://ocsigen.org/lwt/5.3.0/manual/manual][~Lwt~]]
+ monad) are pure
Similarly to types, ~coqffi~ generates axioms (or definitions, if the
~coq_model~ annotation is used) for pure values. Then,
@@ -228,9 +282,9 @@ Axiom ast_to_string : forall (a : Type), string.
** Impure Primitives
-Finally, ~coqffi~ reserves a special treatment for _impure_ OCaml
-functions. Impurity is usually handled in pure programming languages
-by means of monads, and ~coqffi~ is no exception to the rule.
+~coqffi~ reserves a special treatment for /impure/ OCaml functions.
+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) generate a typeclass which gathers these primitives,
@@ -336,9 +390,29 @@ Definition console_unsafe_semantics : semantics CONSOLE :=
+** Asynchronous Primitives
+~coqffi~ also reserves a special treatment for /asynchronous/
+primitives —/i.e./, functions which live inside the ~Lwt~ monad— when
+the ~lwt~ feature is enabled.
+The treatment is very analoguous to the one for impure primitives: (1)
+a typeclass is generated (with the ~_Async~ suffix), and (2) an
+instance for the ~Lwt~ monad is generated. Besides, an instance for
+the “synchronous” primitives is also generated for ~Lwt~. If the
+~interface~ feature is enabled, an interface datatype is generated,
+which means you can potentially use Coq to reason about your
+asynchronous programs (using FreeSpec and alike, although the
+interleaving of asynchronous programs in not yet supported in
+By default, the type of the ~Lwt~ monad is ~Lwt.t~. You can override
+this setting using the ~--lwt-alias~ option. This can be useful when
+you are using an alias type in place of ~Lwt.t~.
-OCaml features an exception mechanisms. Developers can define their
+OCaml features an exception mechanism. Developers can define their
own exceptions using the ~exception~ keyword, whose syntax is similar
to constructors definition. For instance,
@@ -377,8 +451,8 @@ Instance FooExn_Exn : Exn FooExn :=
-Under the hood, =exn= is an open datatype, and how ~coqffi~ supports
-it will probably be generalized in future releases.
+Under the hood, =exn= is an [[https://caml.inria.fr/pub/docs/manual-ocaml/extensiblevariants.html][extensible datatype]], and how ~coqffi~
+supports it will probably be generalized in future releases.
Finally, ~coqffi~ has a minimal support for functions which may raise
exceptions. Since OCaml type system does not allow to identify such
@@ -438,5 +512,5 @@ module T : S
~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]].
+which explains how [[./CoqffiEcho.org][~coqffi~ can be used to easily implement an echo
+server in Coq]].