Skip to Content.
Sympa Menu

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

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)


Chronological Thread 
  • From: Gabriel Scherer <gabriel.scherer AT gmail.com>
  • To: Coq Club <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 08:17:33 -0500
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gabriel.scherer AT gmail.com; spf=Pass smtp.mailfrom=gabriel.scherer AT gmail.com; spf=None smtp.helo=postmaster AT mail-ig0-f171.google.com
  • Ironport-phdr: 9a23:xOlosxRHnMtuhuuCaCXNrPU+/dpsv+yvbD5Q0YIujvd0So/mwa64YxON2/xhgRfzUJnB7Loc0qyN4/+mBjBLvcbJmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbvipNuMP04U1HKUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGY2zRakzTKRZATI6KCh1oZSz7ViQBTeIs1AbSy09lgdCS1zO6wi/VZPsuAP7sPB80W+UJ5ulY6ozXGGN5q1xSRLswBwMNzMj/Xuf3sN5hrharRbnvBd/zpTZeqmaMfN/euXWetZMFjkJZdpYSyEUWtD0VIAIFedUeL8A94Q=

Pierre-Marie, I think the worry is valid, and that sending an email to the author when there are licensing troubles is the right process to follow, independently of the author's sense of humor.

On Wed, Mar 2, 2016 at 5:47 PM, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:
On 02/03/2016 23:23, Soegtrop, Michael wrote:
> I guess so. I sent him an email explaining the situation. Let's see
> what happens.

You're seriously trying to make Sam Hocevar relicense a software he
wrote because of the name of the license? Do you know that apart from
being the designer of the WTFPL, he's also the developer of the famous
libcaca, one of the author of the famous http://cyclim.se/ site, as well
as a fan of that sort of stuff: http://sam.zoy.org/porn/ (do not worry,
that's SFW).

I would personally feel a bit ashamed to know that people ask him to do
this for the benefit of the Coq software...

« Gérard, reviens, ils sont devenus fous ! »

PMP





Archive powered by MHonArc 2.6.18.

Top of Page