The Coq mailing list

[Derek Dreyer <dreyer AT mpi-sws.org>]

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