The Coq mailing list

["Benjamin C. Pierce" <bcpierce AT cis.upenn.edu>]

Yeah, I know.  I really wish there were mailing list software that made 
sending back a posting policy the same number of keystrokes as “Accept” or 
“Reject.”  

Sadly, the upshot is that types-announce is now just epsilon better than 
useless, at least for me.

    - B




> On Jun 22, 2018, at 7:22 PM, Derek Dreyer 
> <dreyer AT mpi-sws.org>
>  wrote:
> 
> FWIW, I think that policy was loosened because there was such a deluge
> of "marginal" announcements, and it became quite annoying to respond
> to each one with a boilerplate request for an explicit preface.
> 
> Derek
> On Sat, Jun 23, 2018 at 1:21 AM Benjamin Pierce 
> <bcpierce AT cis.upenn.edu>
>  wrote:
>> 
>> Types-Announce used to have a policy of accepting ‘marginal’ announcements 
>> iff they included an explicit preface explaining their relevance to the 
>> types community. Recent moderators have loosened the policy, but I still 
>> think it was pretty good.
>> 
>>       - Benjamin
>> 
>>> On Jun 22, 2018, at 18:37, Derek Dreyer 
>>> <dreyer AT mpi-sws.org>
>>>  wrote:
>>> 
>>> Btw, Hugo, to answer your question about Types/announce: When I was
>>> moderator, we adopted a pretty lenient policy concerning
>>> announcements, but the announcements had to at least be something
>>> plausibly PL-related to be accepted.  The posts that raised some
>>> people's hackles earlier today seemed to be about random topics with
>>> no relation to PL.  We would have rejected those posts, but probably
>>> not the other posts that you mentioned in your mail.
>>> 
>>> Nevertheless, I would argue that independent of that point, it would
>>> be great to see announcements on a separate list because those posts
>>> are of a fundamentally different nature than the technical coq-club
>>> posts.
>>> 
>>> Thanks!
>>> Derek
>>> 
>>>> On Sat, Jun 23, 2018 at 12:24 AM Derek Dreyer 
>>>> <dreyer AT mpi-sws.org>
>>>>  wrote:
>>>> 
>>>> Hi, Hugo.
>>>> 
>>>> Given that the list is moderated, which I (and others) did not
>>>> realize, my suggestion would be to consider splitting the list into
>>>> two lists: one for actual substantial discussions concerning Coq, type
>>>> theory, etc., and one for announcements.  The TYPES list split into
>>>> two such lists a long time ago, and it was a useful distinction.
>>>> 
>>>> Personally, I can say for myself that I am not particularly interested
>>>> in any of the announcements posted on coq-club -- and I delete them
>>>> immediately -- because I expect that any sufficiently interesting
>>>> announcement will also be sent to Types-announce.  (That may or may
>>>> not be the case, but it is my attitude, and I imagine I'm not alone.)
>>>> 
>>>> So I would be quite happy if coq-club were split into two mailing
>>>> lists, the current one (reserved for actual Coq-related posts) and a
>>>> coq-club-announce list (for which you can apply whatever filter you
>>>> like because I wouldn't subscribe to it :-).
>>>> 
>>>> Best regards,
>>>> Derek
>>>>> On Sat, Jun 23, 2018 at 12:17 AM Hugo Herbelin 
>>>>> <Hugo.Herbelin AT inria.fr>
>>>>>  wrote:
>>>>> 
>>>>> Dear Benjamin, Derek, contributors to the discussion,
>>>>> 
>>>>> As indicated by Matthieu, the current discussion started from wrong
>>>>> assumptions. The ICPRAM/ICORES/ICAART mails which pushed Benjamin to
>>>>> initiate the discussion were sent by non-subscribed senders and
>>>>> arrived in the hands of the moderators.
>>>>> 
>>>>> Altogether, there are 5 people with moderation rights, but, out of
>>>>> habits, two are effectively moderating. One moderator is taking in
>>>>> charge to systematically forward Coq related messages from
>>>>> unsubscribed senders (unless this is a duplicate or similar reason)
>>>>> and I'm dealing with the rest of the messages.
>>>>> 
>>>>> In general, I'm forwarding the announcements related to our
>>>>> communities in a large sense (type theory, formal methods, ...),
>>>>> and/or with Program Committees including people from our communities,
>>>>> and/or which I feel may be of interest for some readers.
>>>>> 
>>>>> Evaluating whether it is worth to re-send an announcement is
>>>>> delicate. Sometimes, not knowing what decision to take, I'm even
>>>>> looking at what decisions other public lists such as U-Penn's TYPES,
>>>>> or the lists for Isabelle, or Agda, or OCaml are taking.
>>>>> 
>>>>> Maybe was I today in a favorable day. In any case, I shall accept the
>>>>> criticism that these 3 announcements are at the margin of the Coq
>>>>> topic and only loosely (potentially) connected to formal proofs. Are
>>>>> they spam? Are they fake? My quick evaluation was that there were not,
>>>>> but I may be wrong and I'd be ready to revise my judgment. After all,
>>>>> Coq is not exclusively used by people from our "usual" communities, so
>>>>> if some people from loosely connected communities evaluate (assuming
>>>>> good faith) that Coq is a potential valuable tool for their community,
>>>>> I don't see why they should be (at least systematically) excluded.
>>>>> 
>>>>> Then, how to reformulate Benjamin's question based on this new
>>>>> information?
>>>>> 
>>>>> - Is the non-moderation of the list to subscribers a problem?
>>>>> 
>>>>> Moderating each message would require more man power and would
>>>>> induce delays in the communication. My own feeling is that the
>>>>> current ratio signal/noise is rather good. Even if not everyone is
>>>>> interested in any "philosophical" question, or in any beginner
>>>>> question, or in any subscriber-sent announcement already sent on 3
>>>>> or 4 other mailing lists, it is relatively easy to select what is of
>>>>> interest for each of us.
>>>>> 
>>>>> - Should Coq-club stop to be about announcements not strictly related
>>>>> to Coq?
>>>>> 
>>>>> Then announcements for the Coq workshops would be ok, but no more
>>>>> announcement for general conferences or workshops of our
>>>>> communities, no more announcements for summer schools without a
>>>>> class on Coq, no more job offer not explicitly mentioning Coq...
>>>>> 
>>>>> After all, several of us receive such announcements in multiple
>>>>> copies and an extra announcement on Coq-club may not be needed to
>>>>> reach more people?
>>>>> 
>>>>> - If non-strictly-Coq announcements are still welcome, should the
>>>>> policy on announcements from non-subscribers be different?
>>>>> 
>>>>> For the record, in the recent weeks, announcements from
>>>>> non-subscribers were sent for CICM, SYNACS, MPC, iFM, ACL2, HOPE,
>>>>> VTSA, ... and I forwarded the mails. If we leave aside the 3
>>>>> contentious announcements sent today, is the moderation limit not
>>>>> put at the right place?
>>>>> 
>>>>> Incidentally, I would be curious at knowing what policy TYPES/announce
>>>>> or Haskell, or Isabelle, or Agda, ... are adopting for moderating
>>>>> conference announcements.
>>>>> 
>>>>> Best,
>>>>> 
>>>>> Hugo
>>>>> 
>>>>>> On Fri, Jun 22, 2018 at 10:03:50PM +0200, Matthieu Sozeau wrote:
>>>>>> Actually, posts are moderated! We just ought to be stricter on 
>>>>>> announcements.
>>>>>> Le ven. 22 juin 2018 à 20:28, Derek Dreyer 
>>>>>> <dreyer AT mpi-sws.org>
>>>>>>  a écrit :
>>>>>> 
>>>>>>   I thought of it, but didn't imagine the mailing list management would
>>>>>>   support such a feature easily.  If it does, then sure.
>>>>>> 
>>>>>>   Derek
>>>>>>   On Fri, Jun 22, 2018 at 8:26 PM Clément Pit-Claudel
>>>>>>   
>>>>>> <cpitclaudel AT gmail.com>
>>>>>>  wrote:
>>>>>>> 
>>>>>>>> On 2018-06-22 14:18, Derek Dreyer wrote:
>>>>>>>> Another idea would be to not moderate posts but have a stronger
>>>>>>>> vetting process for determining who has the right to post rather than
>>>>>>>> just allowing anyone.  However, this might have the effect of
>>>>>>>> discouraging newbies with real Coq questions.
>>>>>>> 
>>>>>>> Many online forums moderate the first few posts of each new user.  
>>>>>>> Could
>>>>>>   this work on coq-club?
>>>>>>> 
>>>>>>> Clément.
>>>>>> 
>>> 
>> 
>