The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

In the absence of more comments about how to make the policy about
announcements evolve, let me tell that I will release four
announcements from non-subscribed senders (ACL2, SYNACS, CSL, EUTypes
summer school).

As for the discussion:

From Derek Dreyer:
> 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.)

I believe that I'm roughly in the same situation, so this view seems
reasonable to me. For instance, about the 4 announcements above, would
someone be missing one if there had been not forwarded?

From Derek Dreyer:
> 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.

Under the assumption that coq-club continues to redistribute general
conference / jobs / school announcements such as POPL, LICS, CSL, ...
that's a possibility. But then we need a clear policy for subscribers
too. Also, I feel that what matters is more the degree of connection
with Coq than the fact that it is an announcement or not. For
instance, I don't see why we should suscribe to a different list which
shall give a lot of general announcements which we can get elsewhere
only to get the few announcements for the workshops, courses or jobs
directly related to Coq. If, at the end, the second list is only for
general announcements, why to have it at all since the general
announcements are available also on more dedicated lists such as
TYPES-announce.

From Perry E. Metzger:
> I run several large (thousands of subscribers) mailing lists. I've
> found over time that simply restricting postings to people who are
> actually subscribed to the list has an amazingly salutary effect.

Yes, it seems so.

> I would suggest automatically rejecting postings from
> non-subscribers.

This is also a possibility which would give a good compromise. If ever
the situation becomes unmanageable for moderators (which is not the
case currently) that should probably be the solution.

* Summary *

I did not have the opportunity to discuss the question with Matthieu
and other developers, but, to summarize, wrt releasing announces from
non-subscribers, I feel that it should:
- either be the status quo (but avoiding forwarding too off-topic
  conferences like ICPRAM last time),
- or downright renouncing to forward any announcement which has not an
  explicit link with Coq (typically leaving the role of distributing
  general announcements to TYPES-announce).

In the latter case, the policy should extend to subscribers.

Does my summary make sense? In any case, unless the discussion evolves
with a different outcome, I believe that I shall continue in the
meantime as it is.

Best regards,

Hugo

On Sat, Jun 23, 2018 at 12:37:07AM +0200, Derek Dreyer 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.
> > > >