The Coq mailing list

[Lionel Elie Mamane <lionel AT mamane.lu>]

Beste Rene,

On Mon, Oct 11, 2004 at 01:13:14AM +0200, Rene Ladan wrote:

> Is it ok if I port Coq 8.0 to FreeBSD, i.e. write a Makefile and
> optionally some patches so that Coq can be installed from the ports
> tree?

I'm not in any way the "legal department" of the Coq team, but note
that (as the webpage puts it) "Coq is distributed under the GNU Lesser
General Public Licence Version 2.1 (LGPL)". A copy of the LGPL comes
with Coq and is there http://www.fsf.org/licenses/lgpl.html . From my
understanding of these documents, it is OK if you port Coq to FreeBSD,
as long as you give the Coq source code, with your eventual changes,
to the people you give the binaries to and if you license your
changes, and the resulting binary, under the terms of the LGPL 2.1 or
the GPL 2 (or a compatible license like the two-clause, no-ad, BSD
license FreeBSD itself uses
http://www.freebsd.org/copyright/freebsd-license.html ;(for your
changes, the binary will have to be LGPL 2.1 or GPL 2)).

Last time I checked, some parts of Coq were actually GPL 2; unless you
strip them off, you will probably have to treat Coq as GPL from
FreeBSD policies point of view.



Groeten,

-- 
Lionel Elie Mamane