Proposal to publish project coqffi to coq-community

[lthms]

Project name: coqffi

Initial author(s): Thomas Letan (@lthms), with contributions from Li-yao Xia (@lysxia), Yann Régis-Gianas (@yurug), and Yannick Zakowski (@YaZko)

Current URL: None, it would be an initial publication

Kind: extractable program, Coq tooling

License: MIT

Description: coqffi automatically generates FFI binding to OCaml libraries for Coq. For instance, given the following .mli file

type fd

val fd_equal : fd -> fd -> bool

val openfile : string -> fd [@@impure]
val read_all : fd -> string [@@impure]
val write : fd -> string -> unit [@@impure]
val closefile : fd -> unit [@@impure]

coqffi generates the necessary Coq boilerplate to use these functions in a Coq development, and to configure the extraction mechanism accordingly, delegating impurity to coq-simple-io.

(* 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.

(** * Types *)

Axiom (fd : Type).

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

(** * Pure Functions *)

Axiom (std_out : fd).

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

(** * Impure Primitives *)

(** ** Monad *)

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 MonadFile_IO : MonadFile IO :=
  { openfile := io_openfile
  ; closefile := io_closefile
  ; read_all := io_read_all
  ; write := io_write
  }.

Status: Maintained, not yet publlished.

New maintainer: @lthms

[spitters]

I understand nothing is publically available yet, and that the name conflicts with this project by @maximedenes . I don't know of the status of that project. https://github.com/maximedenes/coqFFI

[lthms]

I can provide a public remote if that is necessary, prior to the initial publication in coq-community. As far the name, I have to admit I assumed the project was no longer underway due to the age of the latest commits, and I was already use to coqffi. Don’t hesitate to let me know if this is an important issue!

[spitters]

I'm generally supportive, but the description is a bit brief for me to understand what coqffi does. Others may know more. In any case, it seems interesting.

[lthms]

You are right, I should have taken a bit more time to write the issue. I have edited it to add the beginning of the README, and will probably set-up a temporary public repo so interested folks may have a look.

[spitters]

Cool!

There seem to be some overlap in goals with http://coq.io/.

[maximedenes]

I understand nothing is publically available yet, and that the name conflicts with this project by @maximedenes . I don't know of the status of that project. https://github.com/maximedenes/coqFFI

That project is indeed not very active, feel free to use the same name.

[lthms]

@maximedenes thanks for the feedback!

@spitters coq-io could be made compatible with coqffi quite easily (i.e., uses the file generated by coqffi); the tool has been conceived to that end, and provides the necessary abstractions.

[spitters]

@lthms sounds good. @clarus, the author of coq-io might be interested.

[clarus]

@spitters Thanks for the notification! I did not know about the project coqffi, looking forward for the publication!

[palmskog]

@lthms please consider the license for this project carefully. With GPLv3, the applicability and audience of the library/tool will be limited due to the reciprocal nature of the license. If I understand the intended usage correctly, anyone who relies on coqffi for extraction will be unable to distribute their extracted code under anything but GPLv3. And anyone who uses coqffi Coq code in a project will be forced to change the license of the project to be GPLv3.

While we accept any open source license in the end, our FAQ includes some recommendations about licensing of coq-community projects.

[lthms]

Thanks for the remark, @palmskog. I don’t think what you are saying is true. AFAICT, the license of coqffi applies to coqffi only, not the code generated by coqffi, so I don’t think there is a problem here (similarly to gcc being GPL does not implies your binary code is GPL).

[palmskog]

@lthms GCC has a special exception for generated code to not fall under GPL when it gets linked with GCC's runtime libraries. As far as I can tell, if you don't have a similar exception for linking with coqffi libraries in extracted code, the whole thing (extracted code + coqffi OCaml side) will automatically have to be licensed under the GPL.

[palmskog]

See also the GCC special exception FAQ which states:

These [runtime libraries] are automatically used by the object code that GCC produces. Because of that, if these libraries were simply distributed only under the terms of the GPL, all the object code that GCC produces would have to be distributed under the same terms.

[lthms]

I think about this this night, and:

• coqffi is a standalone OCaml tool which happens to produce a text output that is (most of the time I hope :D) a valid Coq program. I really don’t think the GPL applies to this text output. The exception of GCC you link refers to a code licensed under GPL injected into programs generated by GCC (a “runtime”) as far as I understand it.
• When we chose the license, there were no “runtime” necessary, but you made me realize that now, there is a small Coq theory necessary; this library, licensed as it is now, poses the same problem as GCC runtime I guess, so thank you for pointing that out.

I will have to rethink this. I would like to keep coqffi (the tool) GPL, but I guess I can either use a similar exception for the CoqFFI library or use a different license… or see if we should go for a different license for the entire bundle, I guess.

Again, thank you for pointing that out. I hadn’t think this as much as I thought!

[spitters]

@MSoegtropIMC may be interested in this licensing discussion.

[palmskog]

@lthms just because a GPL program is generating code, this doesn't necessarily mean the generated code is exempt from the GPL. For example, the GNU Bison parser generator copies large pieces of GPL code into its output, and thus has a special license exception for generated code. Before Bison version 1.24, any use of Bison in a software project forced the project to be GPL-licensed.

Absent any explicit statement that output is owned by the user, I would argue that only experts well-versed in both a program's implementation and the legal framework around software licensing can determine with any certainty whether a given GPL-licensed program which generates code will make everything it touches GPL or not.

[lthms]

Since I really wish coqffi will eventually be accepted by the community, and in order to let things remain as simple as possible, we will publish coqffi under the MIT license. Thanks for pointing this potential issue really quickly!

Is there any additional things we want to discuss? Do I need to make a first remote publicly available prior to the creation (or refusal of creation) of a coq-community/coqffi repo?

[palmskog]

@lthms our community is small and we are generally trusting, so it would be fine with me to do either of:

1. creating a new repo in the organization and pushing directly to it
2. creating a repo in your own GitHub account that is then transferred to coq-community

However, it may save some time if you let me take a look at your repo before transferring it, so that adding our usual metadata and automation is going to be straightforward.

Let me know what you prefer.

[lthms]

I can definitely set-up a repo, configure the CI, then give you enough time (and maybe push rights?) to it prior to transferring it!

[palmskog]

Then please go ahead and set up the repo in your account, but no need to add CI or give me push rights.

[lthms]

It took me some time, but I am now ready to transfer ownership of https://github.com/lthms/coqffi to the coq-community organization!

[palmskog]

@lthms I invited you to join the coq-community organization, so you can transfer the repo. Either check your email or go to https://github.com/coq-community

[lthms]

Neat! I have transferred the repo accordingly.

[palmskog]

Since the repo is now transferred (https://github.com/coq-community/coqffi), I'm closing this issue. Let's continue any discussion as repo issues.