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: Enrico Tassi <enrico.tassi AT inria.fr>
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: Thu, 3 Mar 2016 15:34:58 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=enrico.tassi AT inria.fr; spf=None smtp.mailfrom=gares AT fettunta.org; spf=None smtp.helo=postmaster AT fettunta.org
Ironport-phdr: 9a23:JK7kexK3QbJp13Y3ntmcpTZWNBhigK39O0sv0rFitYgUKfvxwZ3uMQTl6Ol3ixeRBMOAu60C1Lad7v+ocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TWM5DIfUi/yKRBybrysXNWC0ILoi6vvpNX6WEZhunmUWftKNhK4rAHc5IE9oLBJDeIP8CbPuWZCYO9MxGlldhq5lhf44dqsrtY4q3wD86Fpy8kVWqLjOq88ULZwDTI8Mmlz6te4mwPESF6i4GEdWWJerhNTGAmNuBz8RJb6tW3mv/Fm2QGbO9f3RPY6Q2LxvO9QVBb0hXJfZHYC+2bNh5kogQ==

On Wed, Mar 02, 2016 at 11:47:39PM +0100, Pierre-Marie Pédrot wrote:
> I would personally feel a bit ashamed to know that people ask him to do
> this for the benefit of the Coq software...

I know and esteem Sam, as any Debian developer of my generation does,
and believe me, he is far from being a fool, despite his peculiar sense
of humor.

This is why I asked if a relicensing coming from him would help.
I think I could have some grip on this topic, given we share a common
background on free software. Also, his (to my taste) hilarious license
was designed as a pun to GPL-vs-BSD zealots, not to annoy companies.

Ciao
--
Enrico Tassi

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