Skip to content

Commit e50894d

Browse files
committed
Runs minimum workflow upon pull_request
#16
1 parent 409c31f commit e50894d

File tree

1 file changed

+12
-3
lines changed

1 file changed

+12
-3
lines changed

.github/workflows/blueprint.yml

Lines changed: 12 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
name: Compile blueprint
22

33
on:
4+
pull_request:
45
push:
56
branches:
67
- main # Trigger on pushes to the default branch
@@ -54,8 +55,9 @@ jobs:
5455

5556
- name: Build project API documentation
5657
run: ~/.elan/bin/lake -R -Kenv=dev build Analysis:docs
57-
58+
5859
- name: Check for `home_page` folder # this is meant to detect a Jekyll-based website
60+
if: github.event_name != 'pull_request'
5961
id: check_home_page
6062
run: |
6163
if [ -d home_page ]; then
@@ -67,6 +69,7 @@ jobs:
6769
fi
6870
6971
- name: Build blueprint and copy to `home_page/blueprint`
72+
if: github.event_name != 'pull_request'
7073
uses: xu-cheng/texlive-action@v2
7174
with:
7275
docker_image: ghcr.io/xu-cheng/texlive-full:20250101
@@ -88,40 +91,46 @@ jobs:
8891
cp -r blueprint/web home_page/blueprint
8992
9093
- name: Check declarations mentioned in the blueprint exist in Lean code
94+
if: github.event_name != 'pull_request'
9195
run: |
9296
~/.elan/bin/lake exe checkdecls blueprint/lean_decls
9397
9498
- name: Copy API documentation to `home_page/docs`
99+
if: github.event_name != 'pull_request'
95100
run: cp -r .lake/build/doc home_page/docs
96101

97102
- name: Remove unnecessary lake files from documentation in `home_page/docs`
103+
if: github.event_name != 'pull_request'
98104
run: |
99105
find home_page/docs -name "*.trace" -delete
100106
find home_page/docs -name "*.hash" -delete
101107
102108
- name: Bundle dependencies
109+
if: github.event_name != 'pull_request'
103110
uses: ruby/setup-ruby@v1
104111
with:
105112
working-directory: home_page
106113
ruby-version: "3.0" # Specify Ruby version
107114
bundler-cache: true # Enable caching for bundler
108115

109116
- name: Build website using Jekyll
110-
if: env.HOME_PAGE_EXISTS == 'true'
117+
if: github.event_name != 'pull_request' && env.HOME_PAGE_EXISTS == 'true'
111118
working-directory: home_page
112119
env:
113120
JEKYLL_GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
114121
run: JEKYLL_ENV=production bundle exec jekyll build # Note this will also copy the blueprint and API doc into home_page/_site
115122

116123
- name: "Upload website (API documentation, blueprint and any home page)"
124+
if: github.event_name != 'pull_request'
117125
uses: actions/upload-pages-artifact@v3
118126
with:
119127
path: ${{ env.HOME_PAGE_EXISTS == 'true' && 'home_page/_site' || 'home_page/' }}
120128

121129
- name: Deploy to GitHub Pages
130+
if: github.event_name != 'pull_request'
122131
id: deployment
123132
uses: actions/deploy-pages@v4
124133

125134
- name: Make sure the API documentation cache works
135+
if: github.event_name != 'pull_request'
126136
run: mv home_page/docs .lake/build/doc
127-

0 commit comments

Comments
 (0)