From e47636cdcacf22b8274bee09ad385a4bd2e59a2d Mon Sep 17 00:00:00 2001
From: Garmelon <joscha@plugh.de>
Date: Tue, 5 May 2026 15:38:54 +0200
Subject: [PATCH] chore: fix CI for PRs from external repos (#13643)

Those action runs don't have access to the READ_RUNNERS_TOKEN secret, so
they should just fall back to the namespace runner.

Also, this PR removes the permission checks again. They are failing for
some non-user authors (e.g. copilot) and could be removed anyways by a
malicious actor in a PR.
---
 .github/workflows/ci.yml | 13 ++-----------
 1 file changed, 2 insertions(+), 11 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index fd9b7480a4..6a08faec37 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -228,6 +228,7 @@ jobs:
           fallback-runner: nscloud-ubuntu-24.04-amd64-8x16
           organization: leanprover
           primaries-required: 1
+          fallback-on-error: true
 
       - name: Configure build matrix
         id: set-matrix
@@ -242,17 +243,7 @@ jobs:
             let large = ${{ github.repository == 'leanprover/lean4' }};
             const isPr = "${{ github.event_name }}" == "pull_request";
             const isPushToMaster = "${{ github.event_name }}" == "push" && "${{ github.ref_name }}" == "master";
-
-            // Only users with write access may use the chonk runners.
-            const permission = await github.rest.repos.getCollaboratorPermissionLevel({
-              owner: context.repo.owner,
-              repo: context.repo.repo,
-              username: context.actor,
-            });
-            const trusted = ["admin", "write"].includes(permission.data.permission);
-            const chonk = trusted ? ${{ steps.runner-fallback.outputs.use-runner }} : "nscloud-ubuntu-24.04-amd64-8x16";
-            console.log(`trusted: ${trusted}, chonk: ${chonk}`);
-
+            const chonk = ${{ steps.runner-fallback.outputs.use-runner }};
             let matrix = [
               /* TODO: to be updated to new LLVM
               {