meta.yml

---
fullname: '`coqffi`'
shortname: coqffi
organization: coq-community
community: true
branch: main
action: true
dune: true

synopsis: Tool for generating Coq FFI bindings to OCaml libraries

description: |-
  `coqffi` generates the necessary Coq boilerplate to use OCaml functions in a
  Coq development, and configures the Coq extraction mechanism accordingly.

authors:
- name: Thomas Letan
- name: Li-yao Xia
- name: Yann Régis-Gianas
- name: Yannick Zakowski

maintainers:
- name: Thomas Letan
  nickname: lthms

opam-file-maintainer: lthms@soap.coffee

opam-file-version: dev

license:
  fullname: MIT License
  identifier: MIT

supported_coq_versions:
  text: 8.12 or later
  opam: '{(>= "8.12" & < "8.13~") | (= "dev")}'

supported_ocaml_versions:
    text: 4.08 or later
    opam: '{>= "4.08" & < "4.12~" }'

tested_coq_opam_versions:
- version: 'dev-ocaml-4.11.1-flambda'
- version: '8.12-ocaml-4.11-flambda'
- version: '8.12-ocaml-4.10-flambda'

dependencies:
- opam:
    name: cmdliner
    version: '{>= "1.0.4"}'
  description: |-
    [Cmdliner](http://erratique.ch/software/cmdliner) 1.0.4 or later
- opam:
    name: sexplib
    version: '{>= "0.14"}'
  description: |-
    [Sexplib](https://github.com/janestreet/sexplib) 0.14 or later

namespace: CoqFFI

build: |-
 ## Building and installation instructions

 Make sure your OPAM installation points to the official Coq repository
 as documented [here](https://github.com/coq/opam-coq-archive), and
 then, the following should work:

 ``` shell
 git clone https://github.com/coq-community/coqffi.git
 cd coqffi
 opam install .
 ```

 Alternatively, you can install `coqffi`’s dependencies (as listed in
 the **Meta** section of the README), then build it.

 ```shell
 git clone https://github.com/coq-community/coqffi.git
 cd coqffi
 ./src-prepare.sh
 dune build -p coq-coqffi
 ```

keywords:
- name: foreign function interface
- name: extraction
- name: OCaml

categories:
- name: Miscellaneous/Coq Extensions

documentation: |-
  ## Example

  Suppose the following OCaml header file (`file.mli`) is given:

  ```ocaml
  type fd

  val std_out : fd
  val fd_equal : fd -> fd -> bool [@@pure]

  val openfile : string -> fd
  val closefile : fd -> unit
  val read_all : fd -> string
  val write : fd -> string -> unit
  ```

  `coqffi` then generates the necessary Coq boilerplate to use these
  functions in a Coq development:

  ```coq
  (* This file has been generated by coqffi. *)

  Set Implicit Arguments.
  Unset Strict Implicit.
  Set Contextual Implicit.
  Generalizable All Variables.

  From CoqFFI Require Export Extraction.
  From SimpleIO Require Import IO_Monad.
  From CoqFFI Require Import Interface.

  (** * Types *)

  Axiom fd : Type.

  Extract Constant fd => "Examples.File.fd".

  (** * Pure functions *)

  Axiom std_out : fd.
  Axiom fd_equal : fd -> fd -> bool.

  Extract Constant std_out => "Examples.File.std_out".
  Extract Constant fd_equal => "Examples.File.fd_equal".

  (** * Impure Primitives *)

  (** ** Monad Definition *)

  Class MonadFile (m : Type -> Type) : Type :=
    { openfile : string -> m fd
    ; closefile : fd -> m unit
    ; read_all : fd -> m string
    ; write : fd -> string -> m unit
    }.

  (** ** [IO] Instance *)

  Axiom io_openfile : string -> IO fd.
  Axiom io_closefile : fd -> IO unit.
  Axiom io_read_all : fd -> IO string.
  Axiom io_write : fd -> string -> IO unit.

  Extract Constant io_openfile
    => "(fun x0 k__ -> k__ (Examples.File.openfile x0))".
  Extract Constant io_closefile
    => "(fun x0 k__ -> k__ (Examples.File.closefile x0))".
  Extract Constant io_read_all
    => "(fun x0 k__ -> k__ (Examples.File.read_all x0))".
  Extract Constant io_write
    => "(fun x0 x1 k__ -> k__ (Examples.File.write x0 x1))".

  Instance IO_MonadFile : MonadFile IO :=
    { openfile := io_openfile
    ; closefile := io_closefile
    ; read_all := io_read_all
    ; write := io_write
    }.

  (* The generated file ends here. *)
  ```

  The generated module may introduce additional dependency to your
  project. For instance, the `simple-io` feature (enabled by default)
  generates the necessary boilerplate to use the impure primitives of
  the input module within the `IO` monad introduced by the
  `coq-simple-io` package.

  See the `coqffi` man pages for more information on how to use it.
---