Only require two approvals for changes to doc/, library/ or verifast-proofs/ (model-checking#351)

We are making a lot of changes to our `scripts/` and
`.github/workflows/` folders to improve automation. These changes are
low-risk; we have no plans to upstream them and they're not part of the
public-facing challenge effort. Update our workflow to require two
committee approvals iff `doc/`, `library/` or `verifast-proofs/` are
modified, and otherwise just require one.

See carolynzech#35 and
carolynzech#36 for test runs on my fork.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: Carolyn Zech

.github/workflows/pr_approval.yml

@@ -73,6 +73,21 @@ jobs:
               return;
             }
 
+            // Get the list of changed files
+            const { data: changedFiles } = await github.rest.pulls.listFiles({
+              owner,
+              repo,
+              pull_number,
+            });
+
+            // Check if any files in doc/, library/ or verifast-proofs/ are modified
+            const affectsDocs = changedFiles.some(file => file.filename.startsWith('doc/'));
+            const affectsLibrary = changedFiles.some(file => file.filename.startsWith('library/'));
+            const affectsVerifast = changedFiles.some(file => file.filename.startsWith('verifast-proofs/'));
+            // Require two approvals iff one of the above folders are modified; otherwise, one is sufficient.
+            const requiresTwoApprovals = affectsDocs || affectsLibrary || affectsVerifast;
+            const requiredApprovals = requiresTwoApprovals ? 2 : 1;
+
             // Get all reviews with pagination
             async function getAllReviews() {
               let allReviews = [];
@@ -113,23 +128,27 @@ jobs:
                 .map(review => review.user.login)
             );
 
-            const requiredApprovals = 2;
             const committeeApprovers = Array.from(approvers)
               .filter(approver => requiredApprovers.includes(approver));
             const currentCountfromCommittee = committeeApprovers.length;
 
-            // Core logic that checks if the approvers are in the committee
-            const conclusion = (currentCountfromCommittee >= 2) ? 'success' : 'failure';
+            // Check if we have enough approvals
+            const conclusion = (currentCountfromCommittee >= requiredApprovals) ? 'success' : 'failure';
 
             console.log('PR Approval Status');
+            console.log('Modified folders:');
+            console.log(`- doc/: ${affectsDocs ? 'yes' : 'no'}`);
+            console.log(`- library/: ${affectsLibrary ? 'yes' : 'no'}`);
+            console.log(`- verifast-proofs/: ${affectsVerifast ? 'yes' : 'no'}`);
+            console.log(`Required approvals from committee: ${requiredApprovals}`);
             console.log(`PR has ${approvers.size} total approvals and ${currentCountfromCommittee} required approvals from the committee.`);
             
             console.log(`Committee Members: [${requiredApprovers.join(', ')}]`);
             console.log(`Committee Approvers: ${committeeApprovers.length === 0 ? 'NONE' : `[${committeeApprovers.join(', ')}]`}`);
             console.log(`All Approvers: ${approvers.size === 0 ? 'NONE' : `[${Array.from(approvers).join(', ')}]`}`);
             
             if (conclusion === 'failure') {
-              core.setFailed(`PR needs 2 approvals from committee members, but it has ${currentCountfromCommittee}`);
+              core.setFailed(`PR needs ${requiredApprovals} approval${requiredApprovals > 1 ? 's' : ''} from committee members, but it has ${currentCountfromCommittee}`);
             } else {
               core.info('PR approval check passed successfully.');
             }