Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Code of Conduct for the Coq community. #6477

Closed
ejgallego opened this issue Dec 20, 2017 · 39 comments · Fixed by #8071
Closed

Code of Conduct for the Coq community. #6477

ejgallego opened this issue Dec 20, 2017 · 39 comments · Fixed by #8071
Labels
kind: meta About the process of developing Coq.
Milestone

Comments

@ejgallego
Copy link
Member

We don't have a code of conduct for Coq yet; feel free to propose the model you'd like to see adopted by Coq. GitHub itself is governed by https://github.com/blog/2039-adopting-the-open-code-of-conduct , see also https://opensource.guide/code-of-conduct/

Personally, I'd like to see the project to adopt a strong zero-tolerance-to-bigotry policy.

@ejgallego ejgallego added the kind: meta About the process of developing Coq. label Dec 20, 2017
@ejgallego
Copy link
Member Author

Another example: https://www.contributor-covenant.org/version/1/4/code-of-conduct.md

[not saying that I'd endorse it]

@herbelin
Copy link
Member

herbelin commented Dec 21, 2017

These links look all interesting. Anyone wants to make a concrete proposition?

As far as I'm concerned, I'm in favor of dealing with "conflictual" situations through communication. whenever possible. I'm convinced that when someone has something to say, even if under the apparent cover of trolling, there is a message behind, and denying this message is most probably going to have this message to find other ways of expressing itself, on other channels, or by other means.

I also consider that whatever the code of conduct is, enforcing the code of conduct should follow a strict policy through a collective process (like the standard reprimand / temporary exclusion / permanent exclusion protocol).

In particular, it would be a welcoming attitude from us, to unblock @williammpratt and talk with him first.

EDIT by Théo: fixing the mention (the william part has two m).

@ejgallego
Copy link
Member Author

@herbelin precisely, trolling is the act of having no intention to communicate, but only to bother and create non-productive discussion.

IMHO the project shall have zero tolerance to fake accounts and trolls, we all have better things to do than to lose our time with a clear troll using a fake account.

And by the way, you got the nickname wrong.

@Zimmi48
Copy link
Member

Zimmi48 commented Dec 21, 2017

In particular, it would be a welcoming attitude from us, to unblock @williammpratt and talk with him first.

Although a lot of the corresponding messages have been deleted and I don't have the records, having stopped to receive e-mail notifications, I believe that the person was first warned that their attitude had to change before they were blocked (I don't know how long was the delay and how many message were posted by the user after this warning). Given the aggressive attitude of the person (commenting lots of PRs and making dismissing remarks, on a repository they had never contributed to), I can perfectly understand the quick blocking response. Not only the person pollutes a lot of issue / PR threads, but they could also spam the wiki if they decide to take their negative attitude further. While I am not opposed to this ban being a temporary one, I would be against a lengthy discussion with @williammpratt happening on this repository. Anyways let's first decide what the Code of Conduct shall be.

I'd also like to recommend this video about the way the Rust community is managed: https://www.youtube.com/watch?v=dIageYT0Vgg. An important point is that if we want a thriving and welcoming community, it is important not to be afraid to push people whose attitude conflicts with this goal away.

@ejgallego
Copy link
Member Author

it is important not to be afraid to push people whose attitude conflicts with this goal away.

+100000000

As @Zimmi48 said this was a clear case, I've got the archive with all their postings thou, so please ping me by mail if you are curious.

@herbelin
Copy link
Member

@ejgallego: from where do you infer that @williammpratt has no intention to communicate, but only to bother and create non-productive discussion. Did you ask him? And did you let other talk with him, starting with me? He was blocked even before I could talk with him.

To not start the "it is forbidden to forbid" debate, our only possible attitude with unwelcoming attitudes is to turn unwelcoming attitudes into welcoming ones, not to unwelcome them.

@SkySkimmer
Copy link
Contributor

from where do you infer that @williammpratt has no intention to communicate, but only to bother and create non-productive discussion.

Full quote:

This is so misguided in so many ways. I can't be bothered to explain the details.

Your quoting is also not correct. I have no interest in a conversation with the author. Please let a more experienced person go over the details if the author doesn't get the hint like this.

(on the fix parallel make PR)

@ejgallego
Copy link
Member Author

from where do you infer that @williammpratt has no intention to communicate, but only to bother and create non-productive discussion. Did you ask him?

He explicitly said so. @herbelin , have you read their messages? As I said, I would be happy to relay them to you if you couldn't access them.

@ejgallego
Copy link
Member Author

IMVHO opinion the goal of a code of conduct is to make sure everybody feels welcomed and safe in the project, specially newcomers and beginners. This includes encouraging them to do things and of course encouraging failure and learning too.

As you say, everybody should feel welcomed, but trolls and toxic persons, who should feel extremely unwelcomed.

@ejgallego
Copy link
Member Author

our only possible attitude with unwelcoming attitudes is to turn unwelcoming attitudes into welcoming ones, not to unwelcome them.

Sorry I don't share that view. Our attitude with asshats and trolls should be "fast and automated ban".

@herbelin
Copy link
Member

@ejgallego: I have the record of messages in my mailbox.

our only possible attitude with unwelcoming attitudes is to turn unwelcoming attitudes into welcoming ones, not to unwelcome them.

Sorry I don't share that view. Our attitude with asshats and trolls should be "fast and automated ban".

Let's turn the question differently. Assume that you arrive in a community, and this community estimates that you are a troll and block you. Would you feel this judgement ok or would you like to justify your truth which is that you are not a troll?

@SkySkimmer: Yes, I saw this quote, but again, the person was blocked without letting others, including me, have a discussion with him. Justice is not a personal but a collective matter.

@ejgallego
Copy link
Member Author

ejgallego commented Dec 21, 2017

I have the record of messages in my mailbox.

Then honestly, I find the defense of that particular person indefensibly.

Assume that you arrive in a community, and this community estimates that you are a troll and block you. Would you feel this judgement ok or would you like to justify your truth which is that you are not a troll?

Let me rewrite that to reflect a bit better what happened here:

Assume that you arrive in a community, insults developers, and show a general lack of respect to it and this community estimates that you are a troll and block you. Would you feel this judgement ok or would you like to justify your truth which is that you are not a troll?

Obviously as a troll I would hope for them to engage with me so my troll objective is achieved; wrt them banning me I would think "pity, they didn't bite the bait, I'll have to look for another victim".

Justice is not a personal but a collective matter.

This is not about justice, Coq's github shall not be a place where justice is built and administered.

Our rules should be simple "be nice to others, otherwise, go away".

@ejgallego
Copy link
Member Author

IMHO it should be also said that in cases of abuse [such as the one we are discussing here], reaction time is critical.

There is not space for a delay when some persons are being abused in your community. The moderators have to act immediately.

@herbelin
Copy link
Member

To me, there was a panic, and the panic led to block this user without any further notice, maybe by fear of being invaded and insulted again by him. This panic did not let place to discussion. I would have liked a discussion but the discussion was blocked.

I would have liked a proper message of the form: « you said: "I have no interest in a conversation with the author". But are you aware that you are on a platform which is precisely for discussion and that if you have no interest in a discussion with the author, we have no interest in welcoming your messages? ». Even to the risk of looking too much explicit, I would have liked a proper message of the form: « you are on a platform where it is expected to use a non insulting language (and we consider that accumulation of sentences such as "you are ignorant", or "ridiculous comments" are insulting). Would you be ok to use instead factual expressions such as "I disagree with you", "I think there would be advantages to do so", so that the technical contents of your message can find all their impact? Otherwise, our rules are that people with repeated insulting attitudes are blocked. Is that what you'd like? ».

@ejgallego: Let me tell an anecdote: you were at PAM's defense. You remember that someone asked a question in the audience. You remember that the chair of the committee was TC. Do you think that the person who asked a question was a troll? (I you think so, I'll tell you something.)

@ejgallego: Do you think that some people are "trolls" by definition or do you think that people are behaving as "trolls" and that they may behave differently in different contexts?

@ejgallego: I'm convinced that this person is precisely someone who has been in an environment where he regularly received comments of the form "you are ignorant", "you are making ridiculous comments", etc., to a point where he started to behave the way others were behaving with him. I'm convinced that telling this person that he is a troll can only make him trolling even more somewhere else. Maybe it is too late, and this person will continue behaving as a "troll" longer and longer, because this is how people defined him. But if ever we had the slighter hope that this person (which is not an ignorant obviously) eventually uses his mind for not trolling, it can only be by considering him as an ordinary person, and not as a "troll".

@ejgallego
Copy link
Member Author

To me, there was a panic, and the panic led to block this user without any further notice, maybe by fear of being invaded and insulted again by him. This panic did not let place to discussion. I would have liked a discussion but the discussion was blocked.

Sorry, this is not what happened. What happened is that there was aggression and abuse from said user to other members of the community. The correct reaction is to immediately stop that abuse. Abuse shall not have place here, IMO. That is the whole story.

With regards to PAM's defense, I'm afraid that your comparison seems to me like a huge "red herring", are you really comparing the discussion that happened there, with what happened here? Don't you see some differences between the two situations?

With regards to your last point, I'm afraid I cannot judge a person I have never met, much less on a few messages, and that would be disregarding the fact that I am not qualified to do so. But I disagree with both the form and substance of the analysis, the correct word for that person is "bully", and while indeed "perpetuation of the circle of abuse" is a well-explored cause in the field of people studying that kind of stuff, I retake @Zimmi48 's point that we are not here to provide help to bullies, but IMO our role as community moderators is to protect the community from them.

And that is what it was done.

@ejgallego
Copy link
Member Author

I'm convinced that this person is precisely someone who has been in an environment where he regularly received comments of the form "you are ignorant", "you are making ridiculous comments", etc.,

IMO we should be careful about finding narratives and justifications for abuse. It is easy to evade personal responsibility this way. For better or worse there is no justification for abuse, and even if I know you are not saying that, what you write could be read as "by being tolerant to abuse, we will actually help the abuser to stop doing so", which looks problematic in principle to me.

@herbelin
Copy link
Member

I agree with the purpose of protecting the community from aggressive attitudes. I'm unsure however that blocking the abuser is better than installing a discussion. Blocking the user will not repair the damage made by the insults. One will remain with the wound of the insults. While if a discussion happens, if the discussion shows that the insults of the person have absolutely no ground, and that the problem is the person him/herself, then the insults will more easily become void of their aggressive contents.

If I mentioned PAM's defense, it is that I would not be surprised that this person has somehow some link with Coq already. And this is one of the thing I'd like to understand.

IMO we should be careful about finding narratives and justifications for abuse. It is easy to evade personal responsibility this way. For better or worse there is no justification for abuse, and even if I know you are not saying that, what you write could be read as "by being tolerant to abuse, we will actually help the abuser to stop doing so", which looks problematic in principle to me.

I'm not talking about being tolerant. There are people who (even adults) are in a provocative attitude and with respect to such attitude, there is nothing else to do than putting a limit.

Here, I'm talking about understanding. Why are they courts and not only lynching? It is also because victims often needs a repairing, needs to understand the motivations of the abuser, needs to find peace with respect to the abuse, and peace is also found by understanding.

@ejgallego
Copy link
Member Author

I understand that zero-tolerance policies may do indeed seem very radical, indeed I do myself think they are and I personally don't have this policy but quite the contrary.

However, in the context of github projects, they are IMHO the best available policy. In fact, we can repurpose the discussion of the CoC as "do we want a zero-tolerance policy"

IMHO yes, but of course we ought to discuss it.

@ejgallego
Copy link
Member Author

Why do I support a "zero-tolerance" CoC?

My reasoning is as follows: we should send a strong message about what this project is about, and we should send a strong message to people joining the community.

It is not a secret that Coq and type theory are challenging endeavors, and the only way to make it look less intimidating is by absolutely frowning up attitudes like the one we recently saw.

@herbelin
Copy link
Member

herbelin commented Dec 21, 2017

I do think that showing that the abuser is wrong in his attitude is the strongest message that we could send (e.g. in systematically replying to abusing comments by enforcing instead our values - and our values are to be welcoming, respectful, open-minded, ...). A better message than blocking an abuser which would leave the situation without conclusion, and with the feeling that "something is wrong" in the discourse that pretends to be welcoming, respectful and open-minded.

@ejgallego
Copy link
Member Author

A better message than blocking an abuser which would leave the situation without conclusion, and with the feeling that "something is wrong" in the discourse that pretends to be welcoming, respectful and open-minded.

Unfortunately that strategy doesn't protect the potential victims from being abused again.

IMHO the situation was not "left without conclusion" but quite the opposite, it was fully resolved in a very satisfactory way. We are reasonably welcoming, respectful, and open-minded (well, we have some room to improve) but we are also strong-willed to not tolerate abuse. There is nothing wrong with expelling abusers from the community.

Being welcoming to your house doesn't mean that you won't kick out people who tries to destroy it.

@herbelin
Copy link
Member

I believe that what people from the community need is the feeling that the community is protecting. Expelling someone who is abusing can be perceived as protecting enough for people victims of the abuse. I believe however that showing that we are right in our way of doing would be an even more protective attitude, showing that the protection is not only physical but also moral (and in particular inclusive).

@ejgallego
Copy link
Member Author

ejgallego commented Dec 21, 2017

I am not sure I understand what you mean, as I am convinced the right thing was done.

So far, the only other option would have been not to ban that abuser from the project, and that is not the kind of inclusivity we should aim for IMHO.

@SkySkimmer
Copy link
Contributor

We could in principle have some appeal path, ie some gitter room or email address where people who feel they were unfairly blocked can argue their case. I don't think that it would be worth the effort, at least for our current possible user. Also I'm not the one who would have that shit job (it should be someone with a bit of seniority) so it's a bit easy to suggest for me.

@herbelin
Copy link
Member

@SkySkimmer: By the way and by curiosity, how did you feel the comments from this person? Did you perceive them as hurting, inappropriate, surrealistic, mad, provocative, painful, ..., or maybe simply ridiculous?

@herbelin
Copy link
Member

We could in principle have some appeal path, ie some gitter room or email address where people who feel they were unfairly blocked can argue their case. I don't think that it would be worth the effort, at least for our current possible user. Also I'm not the one who would have that shit job (it should be someone with a bit of seniority) so it's a bit easy to suggest for me.

I would suspect too that this user would not use such an appeal path but I would indeed have preferred if the blocking had been preceded by a message of the form "we are several people to find your attitude unacceptable and we are preventively going to block you. If you think this is unjustified, you may contact the following people: ...." (with typically my name and @mattam82's name).

@mattam82
Copy link
Member

@herbelin @ejgallego I'm fine with that policy, with a message and "recourse" link.

@Zimmi48
Copy link
Member

Zimmi48 commented Dec 21, 2017

I also think that the right thing was done but having a Code of Conduct with a clear policy on how we react to abuse would be better.
This Code of Conduct should contain the following:

  • If someone is being abusive (which would have to be defined first), we warn them that their attitude is not welcomed, that they risk a ban, with a link to the Code of Conduct.
  • If they post again abusive / aggressive comments (in this case the person replied to the warning with "I remember the time that competent people worked on Coq. Too bad that's not the case anymore."), we block them swiftly and post a new message saying "Following our procedure on abusive behavior, you have been blocked. This initial ban is temporary. You may request the ban to be lifted after one week by sending an e-mail to aaa@bbb.ccc. This e-mail shall contain a declaration that you are ready to abide by the Code of Conduct."
  • We do not delete all the messages of the blocked user, we leave at least part of the comments on the thread where the warning was given (including the warning message and the final notice) to document our response to negative behavior (so as not to give the impression to other people that we are censoring someone).

@ejgallego
Copy link
Member Author

Sounds good @Zimmi48 , but we should be sure we do not spend energy on defending and justifying harassers. Harassment is massive in online communities due (among other factors) to tolerance, so it is important to have a swift hand.

Engaging in discussions with them as @herbelin proposes is IMHO extremely counterproductive and it sends the message that we tolerate their behavior and that we are willing to spend energy trying to help the bully and not their victims.

@ppedrot
Copy link
Member

ppedrot commented Dec 21, 2017

C'est pas parce qu'on a rien à dire qu'il faut fermer sa gueule, so I'll gladly give my irrelevant opinion on the current matter.

As inconsistent as it may seem, I hate formal rules, which are the armed wing of the arch-demon known as Bureaucracy. I'm not really surprised that what I consider the Code-of-Conduct mass hysteria stems from the US mindset, a people quite well historically documented for their strong group pressure leading to properly irrational behaviours (remember the Salem trials?). Furthermore, this tendency to overspecify contracts is strongly rooted in the Common Law system where one has to give minutious details in order to ensure that a judge won't repel a case thanks to some ridiculous overlook in a text.

I'd rather favour a very broad rule crystalizing l'Esprit de la Loi, probably summarized by Thou shalt not bother thy neighbour. No need to give a 57-item list describing what constitutes harassment or insults, this can be solve on a by-case basis. So far it seems we only had this problem once, I fail to see the need to resort to heavy artillery. Also, like @herbelin I believe that discussion is of tantamount importance in social interactions, that the legitimacy of the law stems from consensus, and that flexibility is the necessary foundation of true democracy (cough Greek crisis cough).

Nonetheless, obvious trolling is obvious, so it doesn't take a PhD in international laws of war to discriminate trolls and swiftly signify them to either behave or shut the fuck up, banning them quickly if needed. We had the perfect example yesterday and it did not require any CoC whatsoever.

TL;DR: People are assumed to be socially capable.

@ejgallego
Copy link
Member Author

@ppedrot, indeed it seems to me that your commment is the perfect example on why we need a code of conduct for Coq.

The fact that you and me don't have the need for it doesn't imply that it is not extremely important to atract a different profile of collaborator. We both belong to an extremely privileged class in the sense that we are relatively sure of what we do, and we go eating trolls anyways when our postdoc salary means that we don't meet ends at the end of the month. At least for myself, every time a BOFH-wannabe reminds me of my admitedly large ignorance about make or bash-quoting I smile and think "Emilio, you have done the right choices in life!"

I'd warn about dismissing the voices asking for more civil (even if reglamented) discourse as "hysterical". Again, a word that is perfectly fine for us won't have the same effect for people not so integrated in the community.

Let me remind that last time I asked I got a total consensus on that our technology and our community were seen as "extremely intimidating", and IMVHO we absolutely ought to change that.

An intimidating community acts as a kind of death filter, Egyptian-style. Yes, only bold and proactive people will feel able to join, but in the end them alone wont suffice to keep it alive.

@psteckler
Copy link
Contributor

I agree with the proposal of @Zimmi48: have a Code of Conduct, with a limited ability for violators to re-gain access.

@herbelin
Copy link
Member

@psteckler: I had the opportunity of talking about CoCs with various people and my conclusion was that such CoCs are reassuring as they send a message that people can feel protected, at least from usual kinds of harassment (in a large sense: insulting, racism, victimization, non-respect of the inherent worth of a person or a group, negation of the seek for mutual understanding, negation of the diversity of cultures, diversity of feelings, diversity of opinions, ...).

The question remains: how to evaluate that some limit between violation and non violation has been crossed? The blocking here was made by a small group not taking into account the general position of developers and this is not good. So, do you intend e.g. having a group of 2 or 3 moderators with a clear mandate and taking decisions of a warning and of a possible exclusion consensually?

@ejgallego:

Let me remind that last time I asked I got a total consensus on that our technology and our community were seen as "extremely intimidating", and IMVHO we absolutely ought to change that.

This remark is very interesting, but I don't see the relation with the present case. Here, we had a fleeting someone with no particular status in the community. How can he have an impact on a community being "extremely intimidating". What matters for newcomers is our own attitude. So, if our community is "extremely intimidating", it can only be because of established members of the community themselves. Is it because of the use of a jargon? Is it because of the excessive care for precision of some people? Is it because some of us are a bit, say direct, in their way to comment, criticize, or request changes on PRs? Is it about too opiniated people? Is it about coq-club? Is it about gitter? Or maybe is it also because of the inherent mathematical complexity of the software?

Coming back to @williammpratt, it may be the case that I don't have as much experience as other developers with internet fora and with the troll phenomenon, but as a result, not having this experience makes me curious about understanding better.

Even if I acknowledge the protective role of a CoC, I continue to disagree with the view that swift censoring and deleting messages is productive. Even if @williammpratt is clearly insulting (and actually insulting us), his systematic trolling behavior is simply ridiculous as soon as we take it second degree. Moreover, I'd be ready to bet that this person is in some way or another connected to Coq and that it is not any person (as the sentence highlighted by @Zimmi48 actually suggests). I'd like to understand why he is behaving so and interacting in an open way with him is the only way to know.

@psteckler
Copy link
Contributor

psteckler commented Dec 21, 2017

@herbelin I have no trouble delegating the responsibility of making such decisions to a small group, chosen from the larger group. It would be good if they mentioned to the larger group "we plan to block M. Bad-Guy because he did such-and-such", and offer the chance for the group to object within a reasonable period.

@ejgallego
Copy link
Member Author

The blocking here was made by a small group not taking into account the general position of developers and this is not good.

The decision was taken by me alone, and I stand by it. Do you consider the behavior and comments acceptable? Do you consider the comments to be of any value? If so, which one?

Maybe I am not clear on what "zero-tolerance" means. IMO we should have a zero-tolerance policy to this kind of behavior. If you think that we should have some degree of tolerance to harassment then we'll have to disagree.

So, do you intend e.g. having a group of 2 or 3 moderators with a clear mandate and taking decisions of a warning and of a possible exclusion consensualy?

Hopefully we will have a few years troll-free and in harmony, so no group will be needed. In the case any random person comes here and start harassing contributors, I hope that whatever developer happens to be online swiftly sends them to the limbo, without even a warning.

@maximedenes
Copy link
Member

maximedenes commented Dec 22, 2017

As too much energy has been spent on this already (remember, it's exactly what trolls are trying to achieve), here is a summary of my opinion:

  • A code of conduct would be good to have, should summarize the general guidelines (accepted behaviors and sanctions), the default should be extremely strict (typically one warning then bann), with the development team reserving the right to lift sanctions.
  • Engaging communication with people having such behaviors is exactly what should not be done. I've been moderating an online chess website for more than 10 years. My conclusion is that minimal interaction with people with bad behaviors is what you want. You can't imagine how much people can threaten you and/or make you waste time, and we are clearly not qualified to bring psychological support.
  • I don't like the idea of exposing core developers by encouraging people having shown inappropriate behavior to contact them (the last part of @Zimmi48 's proposal), but as long as it is not my nickname, I won't oppose to it.
  • Reaction time is critical, when people start commenting inappropriately on many PRs, you want any core developer to be allowed to stop them. We can then discuss briefly what happened, and in some rare cases lift the sanction if the team thinks it is the right thing to do. I hope @herbelin is not suggesting we should lift it in the current case.
  • This has nothing to do with justice, it is about preserving a sound working environment.

@gares
Copy link
Member

gares commented Dec 22, 2017

FTR, the strategy proposed by @maximedenes is very close to the one adopted on Debian mailing lists.

@herbelin
Copy link
Member

@ejgallego:

The decision was taken by me alone, and I stand by it.

This was my point, @ejgallego. I can understand the motivations which led you to take this decision (e.g. that it is somehow the usage these days in internet communities) but by doing so you left no place to a discussion with the rest of the group as a whole. As a result, at wanting to be swift, this just leaves the impression that you wanted to avoid a discussion, which I know is not the case.

Do you consider the behavior and comments acceptable? Do you consider the comments to be of any value? If so, which one?

I don't consider the behavior and comments as valuable, but as for the decision taken, I indeed wish we have stronger expectations. There is a problem and the solution found is to hide the problem, as if hiding the problem would make the problem disappear. This person pronounced words which hurt us, but whatever we do, these words have still been pronounced. How do we answer to his accusations? How do we restore the truth? How do we show him that it is us who are right and not him if we ourselves gives him an evidence, behind the apparent authority, that we are hurt?

Sure, we don't "feed the troll" as @maximedenes says but we don't address the issue either.

To be honest, I don't have experiences with troll (except between ourselves, but the kind of trolling among us is generally not "pathological"...). And I'm frustrated not having had the opportunity to talk with him, because I would bet that he's someone who would behave perfectly normally whenever we talk at him as a person and not as a troll. (But maybe I'm wrong.)

Not disregarding the fact that it could perfectly be someone we know...

Wishing you otherwise happy holydays!

@Zimmi48
Copy link
Member

Zimmi48 commented Dec 23, 2017

How do we answer to his accusations? How do we restore the truth? How do we show him that it is us who are right and not him if we ourselves gives him an evidence, behind the apparent authority, that we are hurt?

We don't.

Someone is wrong on the internet

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: meta About the process of developing Coq.
Projects
None yet
Development

Successfully merging a pull request may close this issue.

9 participants