feat(maintenance): clarifications on decision making and reviewer/maintainer teams

.github/CODEOWNERS

@@ -1,20 +1,5 @@
-# For an overview of the governance model of cslib, please refer to /GOVERNANCE.md
+# For an overview of the governance model of cslib, please refer to /GOVERNANCE.md and /DECISION_MAKING.md
 
-### Global access
-# This should be used sparingly.
-# - @fmontesi has global access as lead maintainer.
-# - @chenson2018 has global access to help with the release pipeline, which sometimes requires
-#   editing files in different areas of the codebase.
-
-* @fmontesi @chenson2018
+* @fmontesi @chenson2018 @kim-em @arademaker @sorrachai
 /.github/CODEOWNERS @fmontesi
-
-### Area access
-# Each area maintainer has access to parts that pertain them. They get automatically asked for
-# reviewing new PRs that touch those areas.
-/Cslib/Algorithms/ @fmontesi @sorrachai @chenson2018
-/Cslib/Foundations/Logic/ @arademaker @fmontesi @chenson2018
-/Cslib/Logics/ @arademaker @fmontesi @chenson2018
-/Cslib/Languages/LambdaCalculus/ @chenson2018 @fmontesi
-/.github/workflows @kim-em @fmontesi @chenson2018
-/scripts @kim-em @fmontesi @chenson2018
+/DECISION_MAKING.md @fmontesi

CONTRIBUTING.md

@@ -50,12 +50,16 @@ If you have any questions, a good place to ask them is the [Lean prover Zulip ch
 # Contribution model
 
 To get your code approved, you need to submit a [pull request (PR)](https://github.com/leanprover/cslib/pulls).
-Each PR needs to be approved by at least one relevant maintainer. You can read the [list of current maintainers](/GOVERNANCE.md#maintainers).
+Each PR needs to be approved by at least one maintainer.
+For more details on the decision making process about PRs, please see [pull request inclusion](/DECISION_MAKING.md#pull-request-inclusion).
+You can also read the [list of current maintainers](/GOVERNANCE.md#maintainers).
 
 If you are adding something new to CSLib and are in doubt about it, you are very welcome to contact us on the [Lean prover Zulip chat](https://leanprover.zulipchat.com/).
 
 If you are unfamiliar with CSLib as a whole and want to understand how to get started, please see [Getting started](#getting-started).
 
+For a more detailed explanation of CSLib's decision-making processes, see [decision making](/DECISION_MAKING.md).
+
 # The role of AI
 
 CSLib in general follows the Mathlib policy on [use of AI](https://leanprover-community.github.io/contribute/index.html#use-of-ai). In particular, take note of:

DECISION_MAKING.md

@@ -0,0 +1,107 @@
+# Decision making
+
+This document describes the framework for making decisions in CSLib.
+
+The processes described here are designed to support distributed, consensus-oriented decision making.
+They are expected to be followed. However, in general, CSLib is a collaborative project and no procedural framework can anticipate every situation.
+When distributed decision making cannot take place because of unavailable area-specific leadership or unresolved disagreement, the Lead Maintainer may intervene as the final decision-making authority (see [exceptional cases](#exceptional-cases)).
+
+## Pull request inclusion
+
+All code merged into CSLib must go through a pull request (PR).
+
+### Review
+
+Every PR must be reviewed before it is merged.
+
+Reviews are not restricted to members of the CSLib reviewer or maintainer teams. We welcome reviews from all contributors and consider reviewing work an important contribution in its own right. Regularly providing thoughtful and constructive reviews is also one of the ways in which contributors can establish the trust that may lead to an invitation to join the CSLib reviewer team.
+
+Members of the CSLib reviewer team are trusted contributors whose technical judgement is recognised by the maintainer team. Maintainers may rely on their reviews as substantive technical scrutiny of the parts of a pull request they have reviewed.
+
+We expect all review comments to be constructive, technically motivated, and aimed at improving the contribution. Whenever possible, comments should be grounded in concrete examples or plausible use cases. When suggesting an alternative, concrete examples are highly welcome.
+
+CSLib strongly encourages reuse of existing infrastructure whenever appropriate, from within CSLib and its dependencies. Reviewers and contributors should therefore consider whether a contribution can build on existing definitions, abstractions, APIs, or results rather than introducing parallel ones. Avoiding unnecessary duplication and fragmentation is an important consideration when evaluating a contribution.
+
+This principle is not absolute. Alternative abstractions or implementations can be valuable when they address limitations of existing infrastructure, support different use cases, or otherwise provide a clear technical benefit. In such cases, contributors should explain the motivation for introducing the alternative and, where relevant, its relationship to existing approaches.
+
+Adding or removing dependencies is managed carefully, taking into account the required CI/CD infrastructure, maintenance implications, and alignment with the broader Lean ecosystem.
+
+Review and acceptance are distinct: a review provides technical scrutiny of a contribution; acceptance authorises its inclusion in CSLib. A maintainer may both review and accept the same PR.
+
+### Acceptance
+
+To be accepted, a PR must:
+1. be approved by at least one maintainer; and
+2. have all of its substantive parts reviewed.
+
+Reviewers should use their best judgement in determining the scope of their review. A reviewer may consider themselves able to vouch for the PR as a whole, or only for particular parts of it. When the scope is limited, this should be made clear so that additional reviewers can cover the remaining parts. Collectively, the reviews should provide adequate scrutiny of the entire contribution.
+
+When these conditions are satisfied, they are sufficient for merging provided that there are no unresolved objections from members of the CSLib reviewer or maintainer teams.
+
+The decision to merge a pull request must be made by a maintainer. Maintainers act as responsible technical architects of CSLib and are expected to consider the broader coherence and long-term technical direction of the library when accepting contributions.
+A maintainer may, at their discretion, delegate the act of merging to a member of the reviewer team. This is commonly done when a pull request has been accepted subject only to minor revisions.
+
+The maintainers authorised to accept pull requests are codified in [CODEOWNERS](/.github/CODEOWNERS).
+
+If a maintainer is the author of a pull request, the required maintainer approval must come from another maintainer. Simple PRs for keeping CSLib up to date with the rest of the Lean ecosystem (e.g., dependency version bumps or fixes to deal with new Lean versions) are exempt from this rule.
+
+### Disagreement
+
+Technical disagreement is a normal and useful part of collaborative development. An objection should therefore be treated as a request to resolve a substantive concern, rather than as a vote against a contribution.
+
+If a member of the CSLib reviewer or maintainer teams raises an objection to a PR, the PR should not be merged while that objection remains unresolved. The participants should first attempt to reach consensus through technical discussion.
+
+Consensus does not require that every participant prefer the final outcome. It means that objections have been considered and resolved sufficiently for the project to move forwards.
+
+When disagreement cannot be resolved through the ordinary review process, the matter may be escalated to the Lead Maintainer. The Lead Maintainer has final authority to resolve such disagreements and determine how the project should proceed.
+In doing so, the Lead Maintainer will consider the arguments raised and may seek further feedback from the reviewer and maintainer teams.
+
+## Appointment of reviewers and maintainers
+
+Reviewers and maintainers are trusted members of the CSLib community who are expected to uphold a high standard of collaboration.
+
+New CSLib reviewers and maintainers may be proposed by any member of the CSLib reviewer team, maintainer team, or Steering Committee. Appointment requires affirmative support from at least half of the eligible CSLib voters, rounded up (eligibility is described in the next two sections). At least one affirmative vote must come from a maintainer.
+
+A candidacy remains under consideration for at least five calendar days. If the required support has been reached and there are no unresolved objections at the end of this period, the candidate is appointed.
+
+Members of the Steering Committee are not included when calculating the number of votes required for appointment, but may vote for both reviewers and maintainers. Their votes otherwise have the same effect as those of the eligible CSLib voters. The intention is to allow the Steering Committee members to contribute to appointment decisions without making their participation necessary for reaching the required threshold.
+
+Candidates should be considered on the basis of their contributions to CSLib and the qualities relevant to the role. These may include technical contributions, constructive reviewing activity, subject-matter expertise, reliability, collaboration with other contributors, and commitment to the long-term development of CSLib.
+
+### Reviewers
+
+Candidates for the CSLib reviewer team are discussed and voted on by the current CSLib reviewers and maintainers.
+
+During this process, reviewers and maintainers may privately seek input from other members of the CSLib community or from people who have worked with the candidate.
+
+Members of the Steering Committee are welcome to participate in the discussion of reviewer candidacies.
+
+### Maintainers
+
+Candidates for the CSLib maintainer team are discussed and voted on by the current CSLib maintainers.
+
+During this process, maintainers may privately seek input from reviewers, other members of the CSLib community, or from people who have worked with the candidate.
+
+Members of the Steering Committee are welcome to participate in the discussion of maintainer candidacies.
+
+### Re-nomination
+
+A candidate who is not appointed may be proposed again at a later time. There is no fixed waiting period, but a renewed candidacy should take into account any concerns or circumstances that prevented the previous appointment.
+
+### Resignation and removal
+
+A reviewer or maintainer may step down from their role at any time by informing the reviewer and maintainer teams (this is easiest done on Zulip) or, alternatively, the Lead Maintainer.
+
+Inactivity does not automatically result in removal. However, prolonged inactivity or other circumstances (e.g., inappropriate conduct) may lead to a review of a person's continued membership of the reviewer or maintainer team. When removal from a role is proposed, the matter should be considered by the same group that is responsible for appointments to that role. Whenever appropriate, the person concerned should be given an opportunity to provide their perspective before a decision is made.
+
+The Lead Maintainer is responsible for ensuring that the relevant governance documents and repository permissions are updated following an appointment, resignation, or removal.
+
+## Exceptional cases
+
+The ordinary processes described in this document may occasionally be inadequate to resolve a particular situation. Examples include prolonged disagreement, the unavailability of relevant area leadership, or ambiguous responsibility.
+
+In such cases, the Lead Maintainer may intervene to determine how a decision should be made to move the project forwards.
+
+## Maintenance of these policies
+
+The [CODEOWNERS](/.github/CODEOWNERS) file is maintained by the Lead Maintainer, who is also responsible for coordinating changes to this document and related CSLib governance policies.

GOVERNANCE.md

@@ -4,6 +4,8 @@ Cslib is governed by two main bodies:
 - A [steering committee](#steering-committee), responsible for securing financial support and guiding the overall vision of the project.
 - A [maintainer team](#maintainers), responsible for curating, expanding, and maintaining the code repository and its technical direction.
 
+The project also has a [reviewer team](#reviewers), consisting of trusted contributors who support the maintainer team by providing regular technical review and guidance.
+
 These groups work together to define the project's roadmap and foster a welcoming and productive environment.
 New members may be invited based on project needs and individual merit (e.g., contributions, review activity).
 
@@ -19,11 +21,13 @@ New members may be invited based on project needs and individual merit (e.g., co
 
 ## Maintainers
 
-The maintainer team is responsible for the quality of the codebase, establishing technical standards and ensuring coherence across contributions.
+The maintainer team is responsible for fostering the growth of the project, maintaining the quality of the codebase, establishing technical standards, and ensuring coherence across contributions. They form the technical decision-making authority for determining what code is included in CSLib.
+
+Maintainers also act as technical architects within their areas of responsibility. They are expected to guide the long-term development of those areas, promote reuse and coherence with the rest of CSLib, and help ensure that local design decisions contribute to a consistent overall architecture.
 
 ### Lead maintainer
 
-The lead maintainer coordinates the maintainer team's overall work and oversees the project's repositories.
+The Lead Maintainer is CSLib's chief architect, coordinates the maintainer team's overall work, oversees the project's repositories, ensures the overall architectural coherence of the library, and guides its long-term technical direction.
 
 - Fabrizio Montesi (@fmontesi), FORM, University of Southern Denmark and Danish Institute for Advanced Study.
 
@@ -40,10 +44,10 @@ Area maintainers are trusted contributors who take ownership of specific areas o
 
 - Chris Henson (@chenson2018), Drexel University. Areas: Lambda calculus, metaprogramming.
 - Kim Morrison (@kim-em), Lean FRO. Areas: Continuous Integration and Deployment (CI/CD) with upstream (Lean, mathlib).
-- Alexandre Rademaker (@arademaker), Atlas Computing and Getulio Vargas Foundation. Areas: logic.
+- Alexandre Rademaker (@arademaker), Renaissance Philanthropy and Getulio Vargas Foundation. Areas: logic.
 - Sorrachai Yingchareonthawornchai (@sorrachai), ETH Zurich. Areas: algorithms and data structures.
 
-### Reviewers
+## Reviewers
 
 Reviewers are trusted contributors who provide regular reviewing and technical guidance to PRs to CSLib.