From 92fac419e78955c698f9610e2b5974d0eb61575a Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 2 May 2024 16:28:17 +0200
Subject: [PATCH] chore: CI: use large runners on Windows (#4050)

---
 .github/workflows/ci.yml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 97103f7b38..ca10235caa 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -54,7 +54,10 @@ jobs:
         with:
           script: |
             const quick = ${{ steps.set-quick.outputs.quick }};
-            console.log(`quick: ${quick}`)
+            console.log(`quick: ${quick}`);
+            // use large runners outside PRs where available (original repo)
+            // for now Windows only, which is the slowest non-debug job
+            let large = ${{ github.event_name != 'pull_request' && github.repository == 'leanprover/lean4' }} ? "-large" : "";
             let matrix = [
               {
                 // portable release build: use channel with older glibc (2.27)
@@ -135,7 +138,7 @@ jobs:
               },
               {
                 "name": "Windows",
-                "os": "windows-2022",
+                "os": `windows-2022${large}`,
                 "release": true,
                 "quick": false,
                 "shell": "msys2 {0}",