coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover)

From: Ralf Jung <jung AT mpi-sws.org>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover)
Date: Wed, 2 Mar 2016 18:49:50 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jung AT mpi-sws.org; spf=Pass smtp.mailfrom=jung AT mpi-sws.org; spf=None smtp.helo=postmaster AT hera.mpi-klsb.mpg.de
Ironport-phdr: 9a23:1+HTIhSnnxN9XPDrdPfOqGd/ldpsv+yvbD5Q0YIujvd0So/mwa64Zh2N2/xhgRfzUJnB7Loc0qyN4/+mBjZLsMjJmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbvipNuMOU4Z2nKUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGfayQ6NtRrtBST8iLmod5cvxtBCFQxHcyGEbVzAsmx5GSyrY6h6yCpXstCTSs/J8nTKFJovxV79iCmfq1LtiVBK90HRPDDU+6myC0sE=

Hi,

> Of cause the WTFPL would also allow to relicense it say under LGPL
> like Coq. So INRIA could do this and publish all under LGPL. But then
> some corporate users will likely find out (there are automated tools
> for this) and wonder why INRIA changes the license and maybe start
> bothering you with questions around this.

This is pretty normal practice, albeit it often happens implicitly --
whenever someone is distributing, e.g., a GPL-ed application with a
BSD-licensed library, they are effectively re-licensing the library
under GPL to make it compatible with the application.

Kind regards,
Ralf

Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), (continued)