The Coq mailing list

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

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