Rework governance

data/governance.yml

@@ -1,24 +1,21 @@
 teams:
-- id: governance
-  name: Governance
-  description: The governance is ensured by the Core team and its Project Leader.
-  subteams:
-  - id: core
-    name: Core
-    description: The Core team is composed of co-opted, long-term and significant 
-      contributors to the Rocq project and its scientific underpinnings.
-      It is responsible for the Rocq Prover and all official Rocq Projects.
-    default_role: Core developer
-    dev_meeting:
-      date: Every Tuesday
-      time: 4:00 PM CET (see wiki) Open to all
-      calendar: https://github.com/coq/coq/wiki/Coq-Calls
-      link: https://rendez-vous.renater.fr/coq-call
-      notes: https://github.com/coq/coq/wiki/Coq-Calls
-    members:
-    - name: Matthieu Sozeau
-      github: mattam82
-      role: Project Leader
+- id: core
+  name: Core Team
+  description: The Core team and its Project Leader govern the project.
+    The Core team is composed of co-opted, long-term and significant 
+    contributors to the Rocq project and its scientific underpinnings.
+    It is responsible for the Rocq Prover and all official Rocq Projects.
+  default_role: Core developer
+  dev_meeting:
+    date: Every Tuesday
+    time: 4:00 PM CET (see wiki) Open to all
+    calendar: https://github.com/coq/coq/wiki/Coq-Calls
+    link: https://rendez-vous.renater.fr/coq-call
+    notes: https://github.com/coq/coq/wiki/Coq-Calls
+  members:
+  - name: Matthieu Sozeau
+    github: mattam82
+    role: Project Leader
 - id: community
   name: Community
   description: The Community team is responsible for managing forums, social media, and community events.

data/pages/governance.md

@@ -75,13 +75,17 @@ It is the role of the Core team to resolve disputes that may arise in relation t
 the official Rocq Projects, specifically to ensure that
 these projects are able to progress in a coordinated way.
 
-The Rocq Core team has a formal [voting process](https://github.com/coq/coq/wiki/Core-Team-Voting-Process) 
+The Rocq Core team has a formal [voting process](#a1-voting-process)
 that can be used to resolve conflicts in case consensus cannot be reached.
 
-Yearly, the Core Team designate a Project Leader among them, who is in charge of representing the 
-Core Team and maintaing the long term vision of the Rocq Prover and official Rocq Projects. 
-The Project Leader is tacitly reconducted each calendar year, unless a Core Team member asks for a vote
-or the Project Leader decides to resign. The current Project Leader is Matthieu Sozeau.
+The Core Team elects a Project Leader among them, who is in charge of representing the 
+Core Team and maintaing the long term roadmap of the Rocq Prover and official Rocq Projects. 
+The current Project Leader is Matthieu Sozeau. The Project Leader's mandate is for one year, 
+renewable each year. The Project Leader is elected each calendar year on the anniversary date 
+of the Rocq 9.0 release, or the date of the previous Project Leader's resignation. If there is 
+a single candidate among the Core Team members, he or she is automatically elected. Otherwise
+the Core Team must proceed with a Condorcet vote on [Belenios](https://vote.belenios.org), 
+with a two weeks notice and 72hr voting window.
 
 It is the community's role to guide the decisions of the Core Team through active engagement,
 contributions, and discussions. To foster a healthy and growing community, the
@@ -91,6 +95,25 @@ It is anticipated that the Projects themselves will be self-managing and will
 resolve issues within their communities, without recourse to the Project Leader. Where
 the Project Leader needs to become involved, he/she will act as arbitrator.
 
+#### A.1 Voting process
+
+These rules were approved by the Coq Core Team on ???.
+
+To resolve certain conflicting situations, the Core Team can proceed to vote on a binary decision, 
+as an ultimate recourse in case consensus cannot be reached. The result binds the core team only 
+and it is its responsibility to enforce the decision.
+
+Each Core Team member has a vote (including the project leader).
+
+- Abstention and delegation of a vote are allowed.
+- Majority of >= 2/3 of casted votes (in Q)
+- Votes take place online, anonymously, within a 72hr voting window, using the [Belenios](https://vote.belenios.org) system.
+- The vote must be announced with precise options 2 weeks in advance by the project leader.
+- Decision to take a vote is taken by the project leader, taking input from the core team members.
+- In case a majority of >= 2/3 cannot be reached, the project leader can decide to launch a second 
+  vote with the same announcement conditions and same rules except it is to be decided by > 50% majority. 
+  The project leader's vote is decisive in case of a tie in this second round.
+
 ### B. Delegates
 
 The Project Leader may choose to delegate authority to others to manage a subproject and

src/global/url.ml

@@ -94,8 +94,10 @@ let news = "/news"
 let news_post v = "/news/" ^ v
 let jobs = "/jobs"
 let donation = "/donation"
-let governance = "/rocq-team"
-let governance_team id = "/rocq-team/" ^ id
+let rocq_team id =
+  match id with
+  | None -> "/rocq-team"
+  | Some id -> "/rocq-team/" ^ id
 let privacy_policy = "/policies/privacy-policy"
 let governance_policy = "/policies/governance"
 let code_of_conduct = "/policies/code-of-conduct"

src/rocqproverorg_frontend/components/footer.eml

@@ -21,6 +21,7 @@ let resources = [
 let ecosystem = [
   (Url.platform, "Platform");
   (Url.packages, "Packages");
+  (Url.rocq_team None, "Rocq Team");
   (Url.community, "Community");
   (Url.consortium, "Consortium");
   (Url.events, "Events");
@@ -29,7 +30,6 @@ let ecosystem = [
   ]
 
 let policies = [
-  (Url.governance, "Rocq Team");
   (Url.governance_policy, "Governance");
   (Url.privacy_policy, "Privacy");
   (Url.code_of_conduct, "Code of Conduct");

src/rocqproverorg_frontend/pages/about.eml

@@ -89,7 +89,7 @@ Layout.render
             All in all, more than 200 people have contributed to the development of Rocq.
           </p>
           <p>
-            The <a href="<%s Url.governance %>">Rocq Team</a> is responsible for the development of
+            The <a href="<%s Url.rocq_team None %>">Rocq Team</a> is responsible for the development of
             Rocq and integration of contributions. See <a href="/refman/changes.html">the changelog</a> for a detailed list of contributors in each release of Rocq and <a href="/refman/history.html">the history page in the reference manual</a> for the early history of Rocq.
           </p>
           <p>
@@ -106,7 +106,7 @@ Layout.render
           The new name, "the Rocq Prover", honors Inria Rocquencourt, the original site where the prover was developed.
           It also alludes to the mythological bird Roc (or Rokh), symbolizing strength and not so disconnected to a rooster.
           Furthermore, the name conveys a sense of solidity, and its unintended connection to music adds a pleasant resonance.
-          The new name was chosen by the <a href="<%s Url.governance_team "governance" %>#Core">Core team</a> after a poll of the users, see
+          The new name was chosen by the <a href="<%s Url.rocq_team (Some "governance") %>#Core">Core team</a> after a poll of the users, see
           <a href="https://coq.discourse.group/t/coq-community-survey-2022-results-part-iv-and-itp-paper-announcement/2001#renaming-coq-8">this page</a>
           for a detailed breakdown of the results.
           </p>

src/rocqproverorg_frontend/pages/governance.eml

@@ -10,7 +10,7 @@ let render_working_group (team : Data.Governance.team) member_label btn_class =
     </div>
     <p class="mb-2 text-white dark:text-dark-title"><%s team.description %></p>
     <div class="font-semibold my-6 text-white dark:text-dark-title"><%i count_members team %> <%s member_label %></div>
-    <a href="<%s Url.governance_team team.id %>" class="btn-transparent <%s btn_class %>">
+    <a href="<%s Url.rocq_team (Some team.id) %>" class="btn-transparent <%s btn_class %>">
       <span>Details</span>
       <svg xmlns="http://www.w3.org/2000/svg" class="h-4 w-4" fill="none" viewBox="0 0 24 24"
         stroke="currentColor">
@@ -24,7 +24,7 @@ let render_team_card (team: Data.Governance.team) member_label =
     <p class="text-title dark:text-dark-title text-lg mb-5"><%s team.name %></p>
     <p class="text-content dark:text-dark-content flex-grow text-base mb-5"><%s team.description %></p>
     <p class="text-content dark:text-dark-content text-base font-bold mb-2"><%i count_members team %> <%s member_label %></p>
-    <a href="<%s Url.governance_team team.id %>" class="flex gap-2 items-center text-base text-primary hover:text-primary-dark hover:underline dark:text-dark-primary dark:hover:underline py-2">
+    <a href="<%s Url.rocq_team (Some team.id) %>" class="flex gap-2 items-center text-base text-primary hover:text-primary-dark hover:underline dark:text-dark-primary dark:hover:underline py-2">
       Details
       <%s! Icons.arrow_right_circle "h-5 w-5" %>
     </a>

src/rocqproverorg_frontend/pages/governance_team.eml

@@ -113,7 +113,7 @@ Layout.render
           <path stroke-linecap="round" stroke-linejoin="round" stroke-width="2" d="M10 19l-7-7m0 0l7-7m-7 7h18">
           </path>
         </svg>
-        <a href="<%s Url.governance %>" class="hover:underline">Back to Governance</a>
+        <a href="<%s Url.rocq_team None %>" class="hover:underline">Back to Governance</a>
       </div>
       <div class="flex flex-col md:flex-row gap-8 mb-8 md:items-center">
         <div class="md:max-w-[70%]">
@@ -134,24 +134,24 @@ Layout.render
   </div>
 </div>
 <div class="bg-background dark:bg-dark-background">
-  <div class="py-8">
+  <div class="py-2">
     <div class="container-fluid">
       <% (match t.dev_meeting with | None -> () | Some dev_meeting -> %>
-      <h2 class="font-bold gradient mb-6 mt-12 md:mt-16 text-4xl text-title dark:text-dark-title">Dev Meeting</h2>
+      <h2 class="font-bold gradient mb-6 mt-6 md:mt-8 text-4xl text-title dark:text-dark-title">Dev Meeting</h2>
       <%s! render_dev_meeting dev_meeting "text-white mb-6" %>
       <% ); %>
 
       <% (match List.length t.members with | 0 -> () | _ -> %>
      <div class="">
-      <h2 class="font-bold gradient mb-6 mt-12 md:mt-16 text-4xl text-title dark:text-dark-title">People</h2>
+      <h2 class="font-bold gradient mb-6 mt-6 md:mt-8 text-4xl text-title dark:text-dark-title">People</h2>
       <div class="grid grid-cols-1 md:grid-cols-2 lg:grid-cols-3 gap-12 mb-4">
         <%s! t.members |> List.map (fun (member : Data.Governance.Member.t) -> render_team_member ~default_role:t.default_role member ) |> String.concat "\n" %>
       </div>
      </div>
       <% ); %>
 
       <% (match List.length t.subteams with | 0 -> () | _ -> %>
-      <h2 class="font-bold gradient mb-6 mt-12 md:mt-16 text-4xl text-title dark:text-dark-title">Teams</h2>
+      <h2 class="font-bold gradient mb-6 mt-6 md:mt-8 text-4xl text-title dark:text-dark-title">Teams</h2>
       <div class="flex flex-col gap-12">
         <% t.subteams |> List.iter (fun (team : Data.Governance.team) -> %>
         <%s! render_subteam team %>

src/rocqproverorg_web/lib/router.ml

@@ -54,8 +54,8 @@ let page_routes _t =
       Dream.get Url.jobs Handler.jobs;
       Dream.get Url.privacy_policy Handler.privacy_policy;
       Dream.get Url.code_of_conduct Handler.code_of_conduct;
-      Dream.get Url.governance Handler.governance;
-      Dream.get (Url.governance_team ":id") Handler.governance_team;
+      Dream.get (Url.rocq_team None) Handler.governance;
+      Dream.get (Url.rocq_team (Some ":id")) Handler.governance_team;
       Dream.get Url.governance_policy Handler.governance_policy;
       Dream.get Url.papers Handler.papers;
       Dream.get (Url.paper ":id") Handler.paper;

src/rocqproverorg_web/lib/sitemap.ml

@@ -18,7 +18,7 @@ let urls =
     Url.events;
     Url.exercises;
     Url.getting_started;
-    Url.governance;
+    Url.rocq_team None;
     Url.governance_policy;
     Url.index;
     Url.industrial_users;
@@ -43,7 +43,7 @@ let urlables =
     [
       Urlable (urls, to_url);
       Urlable (Changelog.all, fun r -> to_url @@ Url.changelog_entry r.slug);
-      Urlable (Governance.teams, fun r -> to_url @@ Url.governance_team r.id);
+      Urlable (Governance.teams, fun r -> to_url @@ Url.rocq_team (Some r.id));
       Urlable (News.all, fun r -> to_url @@ Url.news_post r.slug);
       Urlable (Release.all, fun r -> to_url @@ Url.release r.version);
       Urlable (Success_story.all, fun r -> to_url @@ Url.success_story r.slug);