[Coq-Club] Is it time...

[Benjamin Pierce]

...to moderate coq-club? It is starting to become a dumping ground for random announcements.

- Benjamin

SUBMISSION DEADLINE
8th International Conference on Pattern Recognition Applications and Methods
Submission Deadline: October 1, 2018
http://www.icpram.org/
February 19 - 21, 2019
Prague, Czech Republic.
- Theory and Methods
- Applications
In Cooperation with: EUROGRAPHICS and AFIG. <br/>
Proceedings will be submitted for indexation by: DBLP, DBLP, Thomson Reuters, EI, SCOPUS, Semantic Scholar and Semantic Scholar. <br/>
Linda G. Shapiro, University of Washington, United States
Bram van Ginneken, Radboud University Medical Center, Netherlands
Michal Irani, Weizmann Institute of Science, Israel
Davide Maltoni, University of Bologna, Italy
A short list of presented papers will be selected so that revised and extended versions of these papers will be published by Springer.
All papers presented at the congress venue will also be available at the SCITEPRESS Digital Library (http://www.scitepress.org/DigitalLibrary/).
Should you have any question please don’t hesitate contacting me.
Kind regards,
ICPRAM Secretariat
Address: Av. D. Manuel I, 27A, 2º esq.
2910-595 Setubal, Portugal
Tel: [phone]
Fax: [phone]
Web: http://www.icpram.org/

[Derek Dreyer]

Yes, please. I was thinking the same thing.

Perhaps there could be a separate coq-club-announce list (like types-announce)?

Thanks,
Derek

Post by Benjamin Pierce
...to moderate coq-club? It is starting to become a dumping ground for random announcements.
- Benjamin

SUBMISSION DEADLINE
8th International Conference on Pattern Recognition Applications and Methods
Submission Deadline: October 1, 2018
http://www.icpram.org/
February 19 - 21, 2019
Prague, Czech Republic.
- Theory and Methods
- Applications
In Cooperation with: EUROGRAPHICS and AFIG. <br/>
Proceedings will be submitted for indexation by: DBLP, DBLP, Thomson Reuters, EI, SCOPUS, Semantic Scholar and Semantic Scholar. <br/>
Linda G. Shapiro, University of Washington, United States
Bram van Ginneken, Radboud University Medical Center, Netherlands
Michal Irani, Weizmann Institute of Science, Israel
Davide Maltoni, University of Bologna, Italy
A short list of presented papers will be selected so that revised and extended versions of these papers will be published by Springer.
All papers presented at the congress venue will also be available at the SCITEPRESS Digital Library (http://www.scitepress.org/DigitalLibrary/).
Should you have any question please don’t hesitate contacting me.
Kind regards,
ICPRAM Secretariat
Address: Av. D. Manuel I, 27A, 2º esq.
2910-595 Setubal, Portugal
Tel: [phone]
Fax: [phone]
Web: http://www.icpram.org/

[Dominique Unruh]

As a first step, we should probably clarify what belongs on Coq-club and
what doesn't. I see the following categories on the mailing list.

- Discussions about Coq
- Discussions about type theory in general
- Job offers (phd / postdoc) related to verification or type theory
- Conference announcements related to verification or type theory
- Conference announcements that are unrelated

Benjamin's mail came in reaction to a mail in the last category. Those we
obviously don't want. What about the others?

Best wishes,
Dominique.

Post by Benjamin Pierce
...to moderate coq-club? It is starting to become a dumping ground for
random announcements.
- Benjamin

SUBMISSION DEADLINE
8th International Conference on Pattern Recognition Applications and

Methods

Submission Deadline: October 1, 2018
http://www.icpram.org/
February 19 - 21, 2019
Prague, Czech Republic.
- Theory and Methods
- Applications
In Cooperation with: EUROGRAPHICS and AFIG. <br/>
Proceedings will be submitted for indexation by: DBLP, DBLP, Thomson

Reuters, EI, SCOPUS, Semantic Scholar and Semantic Scholar. <br/>

Linda G. Shapiro, University of Washington, United States
Bram van Ginneken, Radboud University Medical Center, Netherlands
Michal Irani, Weizmann Institute of Science, Israel
Davide Maltoni, University of Bologna, Italy
A short list of presented papers will be selected so that revised and

extended versions of these papers will be published by Springer.

All papers presented at the congress venue will also be available at the

SCITEPRESS Digital Library (http://www.scitepress.org/DigitalLibrary/).

Should you have any question please don’t hesitate contacting me.
Kind regards,
ICPRAM Secretariat
Address: Av. D. Manuel I, 27A, 2º esq.
2910-595 Setubal, Portugal
Tel: [phone]
Fax: [phone]
Web: http://www.icpram.org/

[Harrison, William L.]

And, as long as we’re on the subject, it would be nice to have a digest option for the coq-club mailing list, which I don’t believe is available now.


On Jun 22, 2018, at 7:11 AM, Dominique Unruh <***@ut.ee<mailto:***@ut.ee>> wrote:

As a first step, we should probably clarify what belongs on Coq-club and what doesn't. I see the following categories on the mailing list.

* Discussions about Coq
* Discussions about type theory in general
* Job offers (phd / postdoc) related to verification or type theory
* Conference announcements related to verification or type theory
* Conference announcements that are unrelated

Benjamin's mail came in reaction to a mail in the last category. Those we obviously don't want. What about the others?

Best wishes,
Dominique.





On 22 June 2018 at 14:19, Benjamin Pierce <***@cis.upenn.edu<mailto:***@cis.upenn.edu>> wrote:
...to moderate coq-club? It is starting to become a dumping ground for random announcements.

- Benjamin

SUBMISSION DEADLINE
8th International Conference on Pattern Recognition Applications and Methods
Submission Deadline: October 1, 2018
http://www.icpram.org/
February 19 - 21, 2019
Prague, Czech Republic.
- Theory and Methods
- Applications
In Cooperation with: EUROGRAPHICS and AFIG. <br/>
Proceedings will be submitted for indexation by: DBLP, DBLP, Thomson Reuters, EI, SCOPUS, Semantic Scholar and Semantic Scholar. <br/>
Linda G. Shapiro, University of Washington, United States
Bram van Ginneken, Radboud University Medical Center, Netherlands
Michal Irani, Weizmann Institute of Science, Israel
Davide Maltoni, University of Bologna, Italy
A short list of presented papers will be selected so that revised and extended versions of these papers will be published by Springer.
All papers presented at the congress venue will also be available at the SCITEPRESS Digital Library (http://www.scitepress.org/DigitalLibrary/).
Should you have any question please don’t hesitate contacting me.
Kind regards,
ICPRAM Secretariat
Address: Av. D. Manuel I, 27A, 2º esq.
2910-595 Setubal, Portugal
Tel: [phone]
Fax: [phone]
Web: http://www.icpram.org/

[karsar]

- Conference announcements that are unrelated

In my opinion, only that is off topic... General philosophical discussion
about type theory, where nothing is asked about Coq itself,
seems to be a bit off topic as well. Sometimes it happens here.

Best,
Karen

Post by Dominique Unruh
As a first step, we should probably clarify what belongs on Coq-club and
what doesn't. I see the following categories on the mailing list.
- Discussions about Coq
- Discussions about type theory in general
- Job offers (phd / postdoc) related to verification or type theory
- Conference announcements related to verification or type theory
- Conference announcements that are unrelated
Benjamin's mail came in reaction to a mail in the last category. Those we
obviously don't want. What about the others?
Best wishes,
Dominique.

Post by Benjamin Pierce
...to moderate coq-club? It is starting to become a dumping ground for
random announcements.
- Benjamin

SUBMISSION DEADLINE
8th International Conference on Pattern Recognition Applications and

Methods

Submission Deadline: October 1, 2018
http://www.icpram.org/
February 19 - 21, 2019
Prague, Czech Republic.
- Theory and Methods
- Applications
In Cooperation with: EUROGRAPHICS and AFIG. <br/>
Proceedings will be submitted for indexation by: DBLP, DBLP, Thomson

Reuters, EI, SCOPUS, Semantic Scholar and Semantic Scholar. <br/>

Linda G. Shapiro, University of Washington, United States
Bram van Ginneken, Radboud University Medical Center, Netherlands
Michal Irani, Weizmann Institute of Science, Israel
Davide Maltoni, University of Bologna, Italy
A short list of presented papers will be selected so that revised and

extended versions of these papers will be published by Springer.

All papers presented at the congress venue will also be available at

the SCITEPRESS Digital Library (http://www.scitepress.org/DigitalLibrary/
).

Should you have any question please don’t hesitate contacting me.
Kind regards,
ICPRAM Secretariat
Address: Av. D. Manuel I, 27A, 2º esq.
2910-595 Setubal, Portugal
Tel: [phone]
Fax: [phone]
Web: http://www.icpram.org/

[Derek Dreyer]

Yes, but there seem to be a lot of these conference announcements
recently, and there will continue to be so long as the list is
unmoderated.

Derek

Post by Dominique Unruh
Conference announcements that are unrelated
In my opinion, only that is off topic... General philosophical discussion about type theory, where nothing is asked about Coq itself,
seems to be a bit off topic as well. Sometimes it happens here.
Best,
Karen

Post by Harrison, William L.
As a first step, we should probably clarify what belongs on Coq-club and what doesn't. I see the following categories on the mailing list.
Discussions about Coq
Discussions about type theory in general
Job offers (phd / postdoc) related to verification or type theory
Conference announcements related to verification or type theory
Conference announcements that are unrelated
Benjamin's mail came in reaction to a mail in the last category. Those we obviously don't want. What about the others?
Best wishes,
Dominique.

Post by Benjamin Pierce
...to moderate coq-club? It is starting to become a dumping ground for random announcements.
- Benjamin

SUBMISSION DEADLINE
8th International Conference on Pattern Recognition Applications and Methods
Submission Deadline: October 1, 2018
http://www.icpram.org/
February 19 - 21, 2019
Prague, Czech Republic.
- Theory and Methods
- Applications
In Cooperation with: EUROGRAPHICS and AFIG. <br/>
Proceedings will be submitted for indexation by: DBLP, DBLP, Thomson Reuters, EI, SCOPUS, Semantic Scholar and Semantic Scholar. <br/>
Linda G. Shapiro, University of Washington, United States
Bram van Ginneken, Radboud University Medical Center, Netherlands
Michal Irani, Weizmann Institute of Science, Israel
Davide Maltoni, University of Bologna, Italy
A short list of presented papers will be selected so that revised and extended versions of these papers will be published by Springer.
All papers presented at the congress venue will also be available at the SCITEPRESS Digital Library (http://www.scitepress.org/DigitalLibrary/).
Should you have any question please don’t hesitate contacting me.
Kind regards,
ICPRAM Secretariat
Address: Av. D. Manuel I, 27A, 2º esq.
2910-595 Setubal, Portugal
Tel: [phone]
Fax: [phone]
Web: http://www.icpram.org/

[Soegtrop, Michael]

Dear Coq Users,

I guess it also needs to be discussed what is meant by "moderation".

For the time being I think it would be sufficient to have a way to report spammers, to have someone review these reports and in case to delete the account or otherwise ban them. As far as I can remember, there are only a handful, so this would be a fairly lightweight task.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: [phone], www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgeri

[Gabriel Scherer]

The spam here comes from 3 announces sent by *different* addresses
@insticc.info addresses, so banning senders wouldn't work. In my (and
I guess Benjamin's and Derek's) experience with the types-announces
moderation, irrelevant Call for Papers (CFPs) come from all sources.

The problem with mailing-lists is that any *relevance* moderation has
to be a-priori, because you cannot remove an email once it is sent.
(In contrast, tone moderation from specific individuals can be
after-the-fact, banning repeat offenders.) But any a-priori moderation
requires checking all moderated emails, which slows the posting flow
and generates work for humans.

If custom filters were available, it might be interesting to try to
automatically detect conference announcements (eg. "CFP" in the header
or "Call for" in general), and have a human moderate those. But unless
mailman gives this flexibility, you probably have to get a moderator
to check all messages before they are sent.

On Fri, Jun 22, 2018 at 2:58 PM, Soegtrop, Michael

Post by Soegtrop, Michael
Dear Coq Users,
I guess it also needs to be discussed what is meant by "moderation".
For the time being I think it would be sufficient to have a way to report spammers, to have someone review these reports and in case to delete the account or otherwise ban them. As far as I can remember, there are only a handful, so this would be a fairly lightweight task.
Best regards,
Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: [phone], www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

[Théo Zimmermann]

For the record, Coq-Club relies on Sympa, not Mailman, and Sympa does
include digest options (someone was asking about this earlier). Have a look
at https://sympa.inria.fr/sympa/suboptions/coq-club (you'll need to
register using your e-mail address first).

Best,
Théo

Post by Gabriel Scherer
The spam here comes from 3 announces sent by *different* addresses
@insticc.info addresses, so banning senders wouldn't work. In my (and
I guess Benjamin's and Derek's) experience with the types-announces
moderation, irrelevant Call for Papers (CFPs) come from all sources.
The problem with mailing-lists is that any *relevance* moderation has
to be a-priori, because you cannot remove an email once it is sent.
(In contrast, tone moderation from specific individuals can be
after-the-fact, banning repeat offenders.) But any a-priori moderation
requires checking all moderated emails, which slows the posting flow
and generates work for humans.
If custom filters were available, it might be interesting to try to
automatically detect conference announcements (eg. "CFP" in the header
or "Call for" in general), and have a human moderate those. But unless
mailman gives this flexibility, you probably have to get a moderator
to check all messages before they are sent.
On Fri, Jun 22, 2018 at 2:58 PM, Soegtrop, Michael

Post by Soegtrop, Michael
Dear Coq Users,
I guess it also needs to be discussed what is meant by "moderation".
For the time being I think it would be sufficient to have a way to

report spammers, to have someone review these reports and in case to delete
the account or otherwise ban them. As far as I can remember, there are only
a handful, so this would be a fairly lightweight task.

Post by Soegtrop, Michael
Best regards,
Michael
Intel Deutschland GmbH

<https://maps.google.com/?q=ered+Address:&entry=gmail&source=g> Am
Campeon 10-12, 85579 Neubiberg, Germany

Post by Soegtrop, Michael
Tel: [phone], www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

[Jim Fehrle]

insticc.info is not a registered domain but perhaps they are associated with http://www.insticc.org/Portal/It's worth asking them politely to stop sending announcements to the list.  Of course, this works betterif the requester can legitimately claim to represent the list users.
Jim

From: Gabriel Scherer <***@gmail.com>
To: Coq Club <coq-***@inria.fr>
Sent: Friday, June 22, 2018 9:09 AM
Subject: Re: [Coq-Club] Is it time...

The spam here comes from 3 announces sent by *different* addresses
@insticc.info addresses, so banning senders wouldn't work. In my (and
I guess Benjamin's and Derek's) experience with the types-announces
moderation, irrelevant Call for Papers (CFPs) come from all sources.

The problem with mailing-lists is that any *relevance* moderation has
to be a-priori, because you cannot remove an email once it is sent.
(In contrast, tone moderation from specific individuals can be
after-the-fact, banning repeat offenders.) But any a-priori moderation
requires checking all moderated emails, which slows the posting flow
and generates work for humans.

If custom filters were available, it might be interesting to try to
automatically detect conference announcements (eg. "CFP" in the header
or "Call for" in general), and have a human moderate those. But unless
mailman gives this flexibility, you probably have to get a moderator
to check all messages before they are sent.

On Fri, Jun 22, 2018 at 2:58 PM, Soegtrop, Michael

Post by Soegtrop, Michael
Dear Coq Users,
I guess it also needs to be discussed what is meant by "moderation".
For the time being I think it would be sufficient to have a way to report spammers, to have someone review these reports and in case to delete the account or otherwise ban them. As far as I can remember, there are only a handful, so this would be a fairly lightweight task.
Best regards,
Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: [phone], www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

[Derek Dreyer]

It's not just this one sender. I have been noticing a high volume of
irrelevant announcements on coq-club.

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.

I'm not sure of the right solution, but currently I find myself
clicking delete on so many coq-club posts that it feels like
types-announce.

Derek

insticc.info is not a registered domain but perhaps they are associated with http://www.insticc.org/Portal/
It's worth asking them politely to stop sending announcements to the list. Of course, this works better
if the requester can legitimately claim to represent the list users.
Jim
________________________________
Sent: Friday, June 22, 2018 9:09 AM
Subject: Re: [Coq-Club] Is it time...
The spam here comes from 3 announces sent by *different* addresses
@insticc.info addresses, so banning senders wouldn't work. In my (and
I guess Benjamin's and Derek's) experience with the types-announces
moderation, irrelevant Call for Papers (CFPs) come from all sources.
The problem with mailing-lists is that any *relevance* moderation has
to be a-priori, because you cannot remove an email once it is sent.
(In contrast, tone moderation from specific individuals can be
after-the-fact, banning repeat offenders.) But any a-priori moderation
requires checking all moderated emails, which slows the posting flow
and generates work for humans.
If custom filters were available, it might be interesting to try to
automatically detect conference announcements (eg. "CFP" in the header
or "Call for" in general), and have a human moderate those. But unless
mailman gives this flexibility, you probably have to get a moderator
to check all messages before they are sent.
On Fri, Jun 22, 2018 at 2:58 PM, Soegtrop, Michael

Post by Soegtrop, Michael
Dear Coq Users,
I guess it also needs to be discussed what is meant by "moderation".
For the time being I think it would be sufficient to have a way to report spammers, to have someone review these reports and in case to delete the account or otherwise ban them. As far as I can remember, there are only a handful, so this would be a fairly lightweight task.
Best regards,
Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: [phone], www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

[Pierre Vial]

Why not starting with moderating users only on their first message, hoping
that it will be enough to avoid irrelevant mails ? Coq newbies (like me)
won't probably start with offering a PhD positions or a cfp...

Pierre

Post by Derek Dreyer
It's not just this one sender. I have been noticing a high volume of
irrelevant announcements on coq-club.
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.
I'm not sure of the right solution, but currently I find myself
clicking delete on so many coq-club posts that it feels like
types-announce.
Derek

Post by Jim Fehrle
insticc.info is not a registered domain but perhaps they are associated

with http://www.insticc.org/Portal/

Post by Jim Fehrle
It's worth asking them politely to stop sending announcements to the

list. Of course, this works better

Post by Jim Fehrle
if the requester can legitimately claim to represent the list users.
Jim
________________________________
Sent: Friday, June 22, 2018 9:09 AM
Subject: Re: [Coq-Club] Is it time...
The spam here comes from 3 announces sent by *different* addresses
@insticc.info addresses, so banning senders wouldn't work. In my (and
I guess Benjamin's and Derek's) experience with the types-announces
moderation, irrelevant Call for Papers (CFPs) come from all sources.
The problem with mailing-lists is that any *relevance* moderation has
to be a-priori, because you cannot remove an email once it is sent.
(In contrast, tone moderation from specific individuals can be
after-the-fact, banning repeat offenders.) But any a-priori moderation
requires checking all moderated emails, which slows the posting flow
and generates work for humans.
If custom filters were available, it might be interesting to try to
automatically detect conference announcements (eg. "CFP" in the header
or "Call for" in general), and have a human moderate those. But unless
mailman gives this flexibility, you probably have to get a moderator
to check all messages before they are sent.
On Fri, Jun 22, 2018 at 2:58 PM, Soegtrop, Michael

Post by Soegtrop, Michael
Dear Coq Users,
I guess it also needs to be discussed what is meant by "moderation".
For the time being I think it would be sufficient to have a way to

report spammers, to have someone review these reports and in case to delete
the account or otherwise ban them. As far as I can remember, there are only
a handful, so this would be a fairly lightweight task.

Post by Jim Fehrle

Post by Soegtrop, Michael
Best regards,
Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: [phone], www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

[Clément Pit-Claudel]

Post by Derek Dreyer
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.

[Derek Dreyer]

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

Post by Clément Pit-Claudel

Post by Derek Dreyer
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.

[Matthieu Sozeau]

Actually, posts are moderated! We just ought to be stricter on
announcements.

Post by Derek Dreyer
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

Post by Clément Pit-Claudel

Post by Derek Dreyer
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?

Post by Clément Pit-Claudel
Clément.

[Hugo Herbelin]

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

Actually, posts are moderated! We just ought to be stricter on announcements.
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

Post by Derek Dreyer
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.

[Derek Dreyer]

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

Post by Hugo Herbelin
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

Actually, posts are moderated! We just ought to be stricter on announcements.
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

Post by Clément Pit-Claudel

Post by Derek Dreyer
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?

Post by Clément Pit-Claudel
Clément.

[Derek Dreyer]

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

Post by Derek Dreyer
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

Post by Hugo Herbelin
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

Actually, posts are moderated! We just ought to be stricter on announcements.
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

Post by Clément Pit-Claudel

Post by Derek Dreyer
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?

Post by Clément Pit-Claudel
Clément.

[Benjamin Pierce]

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

Post by Derek Dreyer
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

Post by Derek Dreyer
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

Post by Hugo Herbelin
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

Actually, posts are moderated! We just ought to be stricter on announcements.
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

Post by Clément Pit-Claudel

Post by Derek Dreyer
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?

Post by Clément Pit-Claudel
Clément.

[Derek Dreyer]

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

Post by Benjamin Pierce
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

Post by Derek Dreyer
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

Post by Derek Dreyer
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

Post by Hugo Herbelin
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

Actually, posts are moderated! We just ought to be stricter on announcements.
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

Post by Clément Pit-Claudel

Post by Derek Dreyer
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?

Post by Clément Pit-Claudel
Clément.

[Benjamin C. Pierce]

Yeah, I know. I really wish there were mailing list software that made sending back a posting policy the same number of keystrokes as “Accept” or “Reject.”

Sadly, the upshot is that types-announce is now just epsilon better than useless, at least for me.

- B

Post by Derek Dreyer
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

Post by Benjamin Pierce
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

Post by Derek Dreyer
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

Post by Derek Dreyer
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

Post by Hugo Herbelin
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

Actually, posts are moderated! We just ought to be stricter on announcements.
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

Post by Clément Pit-Claudel

Post by Derek Dreyer
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?

Post by Clément Pit-Claudel
Clément.

[Hugo Herbelin]

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

Post by 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?

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

Post by Derek Dreyer
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.

Post by Derek Dreyer
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

Post by Derek Dreyer
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

Post by Derek Dreyer
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

Post by Hugo Herbelin
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

Actually, posts are moderated! We just ought to be stricter on announcements.
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

Post by Clément Pit-Claudel

Post by Derek Dreyer
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?

Post by Clément Pit-Claudel
Clément.

[Gabriel Scherer]

You mention ACL2, SYNACS, CSL, and the EUTypes Summer School.
Those were advertised on types-announce, except for ACL2 (they don't seem
to communicate there).

That said, if I was an organizer of the EUTypes Summer School, I would have
sent to *both* coq-club and types-announces, because I think that this
particular announce (
http://lists.seas.upenn.edu/pipermail/types-announce/2018/007661.html ) is
particularly relevant to the coq-club audience where it may reach a
slightly different audience. In the same way, as the organizer of the OCaml
or the ML workshop, I write to caml-list as well as types-announces. On the
other hand, I don't think that CSL/SYNACS really benefit from specific
coq-club exposure.

One way to think about it is: the Coq community is like a town, and
coq-club is the local newpaper. Types-announce is more like a region-wide
newspaper. Some events are particularly relevant for the town *and* of
interest to the region at large, they get announced in both places. Events
about completely different downs, or about the whole region but with no
particular connection to the town, no need.

Post by Hugo Herbelin
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).

Post by 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?

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

Post by Derek Dreyer
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.

Post by Derek Dreyer
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
- 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

Post by Derek Dreyer
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

Post by Derek Dreyer
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

Post by Hugo Herbelin
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,

Post by Derek Dreyer

Post by Derek Dreyer

Post by Hugo Herbelin
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

Post by Derek Dreyer

Post by Derek Dreyer

Post by Hugo Herbelin
if some people from loosely connected communities evaluate (assuming
good faith) that Coq is a potential valuable tool for their

community,

Post by Derek Dreyer

Post by Derek Dreyer

Post by Hugo Herbelin
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

Post by Derek Dreyer

Post by Derek Dreyer

Post by Hugo Herbelin
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

Post by Derek Dreyer

Post by Derek Dreyer

Post by Hugo Herbelin
or Haskell, or Isabelle, or Agda, ... are adopting for moderating
conference announcements.
Best,
Hugo

Post by Matthieu Sozeau
Actually, posts are moderated! We just ought to be stricter on

announcements.

Post by Derek Dreyer

Post by Derek Dreyer

Post by Hugo Herbelin

Post by Matthieu Sozeau
I thought of it, but didn't imagine the mailing list

management would

Post by Derek Dreyer

Post by Derek Dreyer

Post by Hugo Herbelin

Post by Matthieu Sozeau
support such a feature easily. If it does, then sure.
Derek
On Fri, Jun 22, 2018 at 8:26 PM Clément Pit-Claudel

Post by Clément Pit-Claudel

Post by Derek Dreyer
Another idea would be to not moderate posts but have a

stronger

Post by Derek Dreyer

Post by Derek Dreyer

Post by Hugo Herbelin

Post by Matthieu Sozeau

Post by Clément Pit-Claudel

Post by Derek Dreyer
vetting process for determining who has the right to post

rather than

Post by Derek Dreyer

Post by Derek Dreyer

Post by Hugo Herbelin

Post by Matthieu Sozeau

Post by Clément Pit-Claudel

Post by Derek Dreyer
just allowing anyone. However, this might have the effect

of

Post by Derek Dreyer

Post by Derek Dreyer

Post by Hugo Herbelin

Post by Matthieu Sozeau

Post by Clément Pit-Claudel

Post by Derek Dreyer
discouraging newbies with real Coq questions.

Many online forums moderate the first few posts of each new

user. Could

Post by Derek Dreyer

Post by Derek Dreyer

Post by Hugo Herbelin

Post by Matthieu Sozeau
this work on coq-club?

Post by Clément Pit-Claudel
Clément.

[Jim Fehrle]

Saving up the announcements and releasing them simultaneously once a week would make them less intrusive.
From: Hugo Herbelin <***@inria.fr>
To: Derek Dreyer <***@mpi-sws.org>; Perry E. Metzger <***@piermont.com>
Cc: coq-***@inria.fr
Sent: Saturday, June 30, 2018 5:51 AM
Subject: Re: [Coq-Club] Is it time...

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

Post by 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?

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

Post by Derek Dreyer
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.

Post by Derek Dreyer
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

[Benjamin C. Pierce]

Post by Jim Fehrle
Saving up the announcements and releasing them simultaneously once a week would make them less intrusive.

This seems like a pretty good stopgap measure.

As I said in the discussion on the types list (which probably most people here read, or at least ignored :-), I think the best way to handle this issue is simply to ask posters of announcements that are not obviously related to the list topic to include a little paragraph explaining the connection. The only downside is that this requires a step that most mailing list software doesn’t support automatically: rejecting a message with an explanation and an invitation to resubmit after revision.

- Benjamin

Post by Jim Fehrle
Sent: Saturday, June 30, 2018 5:51 AM
Subject: Re: [Coq-Club] Is it time...
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).

Post by 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?

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

Post by Derek Dreyer
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.

Post by Derek Dreyer
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
- 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

[Perry E. Metzger]

On Fri, 22 Jun 2018 07:19:23 -0400 Benjamin Pierce

Post by Benjamin Pierce
...to moderate coq-club? It is starting to become a dumping ground
for random announcements.

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.

I would suggest automatically rejecting postings from
non-subscribers.

Perry