From 2d5ef3925b5dfcfe1b241a60594c7c25c4128ab1 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Wed, 9 Oct 2024 11:21:24 +0200
Subject: [PATCH 1/3] Update blueprint.yml

---
 leanblueprint/templates/blueprint.yml | 38 ++++++++++++++++++++++-----
 1 file changed, 31 insertions(+), 7 deletions(-)

diff --git a/leanblueprint/templates/blueprint.yml b/leanblueprint/templates/blueprint.yml
index 277a7ee..9ac1002 100644
--- a/leanblueprint/templates/blueprint.yml
+++ b/leanblueprint/templates/blueprint.yml
@@ -3,19 +3,40 @@ name: Compile blueprint
 on:
   push:
     branches:
-      - {| master_branch |} # Trigger on pushes to the default branch
-  workflow_dispatch:        # Allow manual triggering of the workflow from the GitHub Actions interface
+      - main
+    paths:
+      - '**/*.lean'
+      - '**/blueprint.yml'
+      - 'blueprint/**'
+      - 'home_page/**'
+      - 'lean-toolchain'
+      - 'lakefile.toml'
+      - 'lake-manifest.json'
+  pull_request:
+    branches:
+      - main
+    paths:
+      - '**/*.lean'
+      - '**/blueprint.yml'
+      - 'blueprint/**'
+      - 'home_page/**'
+      - 'lean-toolchain'
+      - 'lakefile.toml'
+      - 'lake-manifest.json'
+  workflow_dispatch: # Allow manual triggering of the workflow from the GitHub Actions interface
 
 # Cancel previous runs if a new commit is pushed to the same PR or branch
 concurrency:
   group: ${{ github.ref }}  # Group runs by the ref (branch or PR)
   cancel-in-progress: true  # Cancel any ongoing runs in the same group
 
-# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
+# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages and modify PR labels
 permissions:
-  contents: read  # Read access to repository contents
-  pages: write    # Write access to GitHub Pages
-  id-token: write # Write access to ID tokens
+  contents: read          # Read access to repository contents
+  pages: write            # Write access to GitHub Pages
+  id-token: write         # Write access to ID tokens
+  issues: write           # Write access to issues
+  pull-requests: write    # Write access to pull requests
 
 jobs:
   build_project:
@@ -100,6 +121,7 @@ jobs:
           find home_page/docs -name "*.hash" -delete
 
       - name: Bundle dependencies
+        if: github.event_name == 'push'
         uses: ruby/setup-ruby@v1
         with:
           working-directory: home_page
@@ -107,16 +129,18 @@ jobs:
           bundler-cache: true  # Enable caching for bundler
 
       - name: Build website using Jekyll
-        if: env.HOME_PAGE_EXISTS == 'true'
+        if: github.event_name == 'push' && env.HOME_PAGE_EXISTS == 'true'
         working-directory: home_page
         run: JEKYLL_ENV=production bundle exec jekyll build  # Note this will also copy the blueprint and API doc into home_page/_site
 
       - name: "Upload website (API documentation, blueprint and any home page)"
+        if: github.event_name == 'push'
         uses: actions/upload-pages-artifact@v3
         with:
           path: ${{ env.HOME_PAGE_EXISTS == 'true' && 'home_page/_site' || 'home_page/' }}
 
       - name: Deploy to GitHub Pages
+        if: github.event_name == 'push'
         id: deployment
         uses: actions/deploy-pages@v4
 

From 6671255a860abf3a0037e35d3e4eb47c3042cd62 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Wed, 9 Oct 2024 11:23:26 +0200
Subject: [PATCH 2/3] Update blueprint.yml

---
 leanblueprint/templates/blueprint.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/leanblueprint/templates/blueprint.yml b/leanblueprint/templates/blueprint.yml
index 9ac1002..77cc9aa 100644
--- a/leanblueprint/templates/blueprint.yml
+++ b/leanblueprint/templates/blueprint.yml
@@ -3,7 +3,7 @@ name: Compile blueprint
 on:
   push:
     branches:
-      - main
+      - {| master_branch |} # Trigger the workflow on push to the default branch
     paths:
       - '**/*.lean'
       - '**/blueprint.yml'
@@ -14,7 +14,7 @@ on:
       - 'lake-manifest.json'
   pull_request:
     branches:
-      - main
+      - {| master_branch |} # Trigger the workflow on pull requests to the default branch
     paths:
       - '**/*.lean'
       - '**/blueprint.yml'

From a9258fcc7d82f8d4620a1de7c9f7587a5c3cbd60 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Wed, 9 Oct 2024 11:27:41 +0200
Subject: [PATCH 3/3] Update blueprint.yml

---
 leanblueprint/templates/blueprint.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/leanblueprint/templates/blueprint.yml b/leanblueprint/templates/blueprint.yml
index 77cc9aa..364a339 100644
--- a/leanblueprint/templates/blueprint.yml
+++ b/leanblueprint/templates/blueprint.yml
@@ -30,7 +30,7 @@ concurrency:
   group: ${{ github.ref }}  # Group runs by the ref (branch or PR)
   cancel-in-progress: true  # Cancel any ongoing runs in the same group
 
-# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages and modify PR labels
+# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages and interaction with issues and pull requests
 permissions:
   contents: read          # Read access to repository contents
   pages: write            # Write access to GitHub Pages