The Coq mailing list

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

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.
>>>> 
>