OPAM package about compcert HOT 7 CLOSED

You might want to post this to the CompCert github page somewhere just to
be thorough.

On Thu, Sep 17, 2015 at 9:17 AM, Pierre Chambart [email protected]
wrote:

I wanted to package CompCert, but I'd like to know before if the license
prevent it or if there is any objections.

—
Reply to this email directly or view it on GitHub
#53.

from compcert.

As far as I can see, nothing in the "no commercial use" license for the public CompCert distribution prevents packaging. However, users of the package are still bound by the license. How do they know about the restrictions of this license? Say that one user of the package violates the license, then blames it on you (the packager) saying "oh, but I thought in good faith that all OPAM packages are free software". Do you want to take this responsibility? More generally, what is the policy regarding non-free software for the OPAM package collection at opam.ocaml.org?

from compcert.

I don't think that there is any non-free software packaged currently in OPAM. @avsm is there any precedent and is there a way to show a notification sufficiently explicitely (like an OPAM post-install hook that must be validated ?)

from compcert.

You can issue a prominent messages entry, but this doesnt get the user to agree. Another option is to replace the binaries with a shell wrapper that forces the user to agree to the license on the first invocation, and then replaces them (in the ~/.opam space which is user-writable) with the proper binaries.

from compcert.

More generally, what is the policy regarding non-free software for the OPAM package collection at opam.ocaml.org

We don't have a strict policy on this at the moment, aside from that it has to be open source. As long as it's marked clearly, I don't see why non-commercial licenses wouldn't be acceptable.

from compcert.

Apparently the Coq-OPAM people went ahead and made a CompCert package: http://coq.io/opam/coq:compcert.2.5.0.html . So be it. Closing this report.

from compcert.

They also appear to have a prettier HTML output page than the main OCaml OPAM repo :-)

On 1 Nov 2015, at 15:10, Xavier Leroy [email protected] wrote:

Apparently the Coq-OPAM people went ahead and made a CompCert package: http://coq.io/opam/coq:compcert.2.5.0.html http://coq.io/opam/coq:compcert.2.5.0.html . So be it. Closing this report.

—
Reply to this email directly or view it on GitHub #53 (comment).

from compcert.