The Coq mailing list

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

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