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
- RE: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), (continued)
- RE: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Soegtrop, Michael, 03/01/2016
- RE: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Soegtrop, Michael, 03/02/2016
- RE: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Soegtrop, Michael, 03/02/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Pierre-Marie Pédrot, 03/02/2016
- RE: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Soegtrop, Michael, 03/02/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Ralf Jung, 03/02/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Clément Pit--Claudel, 03/02/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Enrico Tassi, 03/02/2016
- RE: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Soegtrop, Michael, 03/02/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Pierre-Marie Pédrot, 03/02/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Gabriel Scherer, 03/03/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Enrico Tassi, 03/03/2016
- RE: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Soegtrop, Michael, 03/03/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Clément Pit--Claudel, 03/03/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Jonathan Leivent, 03/03/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Lucian M. Patcas, 03/04/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Clément Pit--Claudel, 03/04/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Clément Pit--Claudel, 03/06/2016
- RE: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Soegtrop, Michael, 03/04/2016
- RE: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Soegtrop, Michael, 03/09/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Pierre Courtieu, 03/11/2016
Archive powered by MHonArc 2.6.18.