@@ -42,7 +42,6 @@ concurrency:
4242jobs :
4343 docs-generate-d2-diagrams :
4444 name : " Generate D2 Diagrams"
45- # Only run this job on pull_request or push triggers, not on workflow_run
4645 if : github.event_name == 'pull_request' || github.event_name == 'push'
4746 runs-on : ubuntu-latest
4847 permissions :
@@ -115,7 +114,6 @@ jobs:
115114
116115 viz-build :
117116 name : " Build Visualizer"
118- # Only run this job on pull_request or push triggers, not on workflow_run
119117 if : github.event_name == 'pull_request' || github.event_name == 'push'
120118 runs-on : ubuntu-latest
121119 steps :
@@ -148,225 +146,60 @@ jobs:
148146 name : visualizer
149147 path : ui/dist
150148
151- # This job handles PR and push events, and depends on viz-build
152- docs-build-pr-push :
153- name : " Build Docusaurus Site (PR/Push)"
149+ build-docusaurus-site :
150+ name : " Build Docusaurus Site"
154151 runs-on : ubuntu-latest
155152 needs : [viz-build]
156- if : github.event_name == 'pull_request' || github.event_name == 'push' || github.event_name == 'workflow_dispatch'
157- outputs :
158- has_changes : ${{ steps.check_changes.outputs.has_changes || github.event_name == 'workflow_dispatch' }}
159153 steps :
160154 - name : 📥 Checkout repository
161155 uses : actions/checkout@v4
162156 with :
163157 fetch-depth : 2
164158
165- - name : Debug workflow trigger info
166- run : |
167- echo "Event name: ${{ github.event_name }}"
168- echo "Ref: ${{ github.ref }}"
169-
170- - name : Check for site or visualizer changes
171- id : check_changes
172- run : |
173- if [ "${{ github.event_name }}" == "workflow_dispatch" ]; then
174- echo "Changes from manual trigger"
175- echo "has_changes=true" >> $GITHUB_OUTPUT
176- else
177- # For PR or push events, check for actual changes
178- SITE_CHANGES=$(git diff --name-only HEAD^ HEAD -- site/ || true)
179- VIZ_CHANGES=$(git diff --name-only HEAD^ HEAD -- ui/ || true)
180- if [ -z "$SITE_CHANGES" ] && [ -z "$VIZ_CHANGES" ]; then
181- echo "No changes in site or UI directory"
182- echo "has_changes=false" >> $GITHUB_OUTPUT
183- else
184- echo "Changes detected in site or UI directory:"
185- echo "$SITE_CHANGES"
186- echo "$VIZ_CHANGES"
187- echo "has_changes=true" >> $GITHUB_OUTPUT
188- fi
189- fi
190- shell : " bash"
191-
192159 - name : 🛠️ Setup Node.js
193- if : steps.check_changes.outputs.has_changes == 'true'
194160 uses : actions/setup-node@v4
195161 with :
196162 node-version : 22
197163 cache : " yarn"
198164 cache-dependency-path : ./site/yarn.lock
199165
200166 - name : 📦 Install dependencies
201- if : steps.check_changes.outputs.has_changes == 'true'
202167 working-directory : site
203168 run : yarn install
204169
205- # Handle visualizer integration
206170 - name : 👁️ Unpack visualizer
207- if : steps.check_changes.outputs.has_changes == 'true'
208171 uses : actions/download-artifact@v4
209172 with :
210173 name : visualizer
211174 path : site/static/visualizer
212175
213- # Download formal spec HTML
176+ # Only for workflow_run: Download formal spec HTML
214177 - name : 📥 Download formal spec HTML
215- if : steps.check_changes.outputs.has_changes == 'true '
178+ if : github.event_name == 'workflow_run '
216179 uses : actions/download-artifact@v4
217180 continue-on-error : true
218181 with :
219182 name : formal-spec-html
220183 path : formal-spec-html
221184
185+ # Only for workflow_run: Update formal spec
222186 - name : 📝 Update formal spec
223- if : steps.check_changes.outputs.has_changes == 'true '
187+ if : github.event_name == 'workflow_run '
224188 run : |
225- # Create formal spec directory if it doesn't exist
226189 mkdir -p site/static/formal-spec
227-
228- # Copy any files we found (even if none were found, this is a no-op)
229190 if [ -d "formal-spec-html" ] && [ -n "$(ls -A formal-spec-html/ 2>/dev/null)" ]; then
230- echo "Formal spec HTML files found - copying to site"
231191 cp -r formal-spec-html/* site/static/formal-spec/
232- else
233- echo "No formal spec HTML files found - continuing without them"
234192 fi
235193
194+ # Only for workflow_run: Enhance Agda documentation
236195 - name : 🔄 Enhance Agda documentation
237- if : steps.check_changes.outputs.has_changes == 'true '
196+ if : github.event_name == 'workflow_run '
238197 working-directory : site
239- timeout-minutes : 20
198+ timeout-minutes : 25
240199 run : |
241- # Process HTML files using the agda-web-docs-lib only if there are actual HTML files
242200 HTML_COUNT=$(find ./static/formal-spec -name '*.html' | wc -l)
243- echo "Found $HTML_COUNT HTML files"
244-
245201 if [ "$HTML_COUNT" -gt "0" ]; then
246- echo "Processing HTML files with agda-web-docs-lib"
247- echo "Available memory before processing:"
248- free -h
249-
250202 NODE_OPTIONS="--max-old-space-size=6144" npx agda-web-docs-lib process ./static/formal-spec ./agda-docs.config.json
251- else
252- echo "No HTML files found in formal-spec directory, skipping enhancement"
253- fi
254-
255- - name : 🏗️ Build Docusaurus site
256- if : steps.check_changes.outputs.has_changes == 'true'
257- working-directory : site
258- run : |
259- yarn build
260-
261- - name : Verify Docusaurus build
262- if : steps.check_changes.outputs.has_changes == 'true'
263- working-directory : site
264- run : |
265- if [ -z "$(ls -A build/)" ]; then
266- echo "Error: Docusaurus build directory is empty"
267- exit 1
268- fi
269- echo "Docusaurus build verified"
270- ls -la build/
271-
272- - name : 🚀 Upload Docusaurus build
273- if : steps.check_changes.outputs.has_changes == 'true'
274- uses : actions/upload-artifact@v4
275- with :
276- name : docusaurus-build
277- if-no-files-found : error
278- path : |
279- site/build/*
280-
281- # This job handles workflow_run events from formal-spec-listener
282- docs-build-workflow-run :
283- name : " Build Docusaurus Site (Workflow Run)"
284- runs-on : ubuntu-latest
285- # No dependency on viz-build for workflow_run events
286- if : github.event_name == 'workflow_run' && github.event.workflow_run.conclusion == 'success'
287- outputs :
288- has_changes : " true"
289- steps :
290- - name : 📥 Checkout repository
291- uses : actions/checkout@v4
292-
293- - name : Debug workflow trigger info
294- run : |
295- echo "Event name: ${{ github.event_name }}"
296- echo "Workflow run conclusion: ${{ github.event.workflow_run.conclusion }}"
297- echo "Workflow run name: ${{ github.event.workflow_run.name }}"
298- echo "Workflow run ID: ${{ github.event.workflow_run.id }}"
299- echo "Ref: ${{ github.ref }}"
300- echo "Event payload: ${{ toJSON(github.event) }}"
301-
302- - name : List available artifacts
303- run : |
304- echo "Listing artifacts in the formal-spec-listener workflow run"
305- curl -s -H "Authorization: token ${{ github.token }}" \
306- "https://api.github.com/repos/${{ github.repository }}/actions/runs/${{ github.event.workflow_run.id }}/artifacts" | \
307- jq '.artifacts[] | {name: .name, id: .id, created_at: .created_at, expired: .expired}'
308-
309- - name : 🛠️ Setup Node.js
310- uses : actions/setup-node@v4
311- with :
312- node-version : 22
313- cache : " yarn"
314- cache-dependency-path : ./site/yarn.lock
315-
316- - name : 📦 Install dependencies
317- working-directory : site
318- run : yarn install
319-
320- # Download formal spec HTML specifically from the workflow run
321- - name : 📥 Download formal spec HTML
322- uses : actions/download-artifact@v4
323- continue-on-error : false
324- with :
325- name : formal-spec-html
326- run-id : ${{ github.event.workflow_run.id }}
327- path : formal-spec-html
328- github-token : ${{ github.token }}
329-
330- - name : Check downloaded files
331- run : |
332- echo "Checking downloaded formal spec files..."
333- if [ -d "formal-spec-html" ]; then
334- echo "formal-spec-html directory exists"
335- ls -la formal-spec-html/
336- else
337- echo "formal-spec-html directory does not exist"
338- exit 1
339- fi
340-
341- - name : 📝 Update formal spec
342- run : |
343- # Create formal spec directory if it doesn't exist
344- mkdir -p site/static/formal-spec
345-
346- # Copy any files we found (even if none were found, this is a no-op)
347- if [ -d "formal-spec-html" ] && [ -n "$(ls -A formal-spec-html/ 2>/dev/null)" ]; then
348- echo "Formal spec HTML files found - copying to site"
349- cp -r formal-spec-html/* site/static/formal-spec/
350- else
351- echo "No formal spec HTML files found - continuing without them"
352- fi
353-
354- - name : 🔄 Enhance Agda documentation
355- working-directory : site
356- timeout-minutes : 20
357- run : |
358- # Process HTML files using the agda-web-docs-lib only if there are actual HTML files
359- HTML_COUNT=$(find ./static/formal-spec -name '*.html' | wc -l)
360- echo "Found $HTML_COUNT HTML files"
361-
362- if [ "$HTML_COUNT" -gt "0" ]; then
363- echo "Processing HTML files with agda-web-docs-lib"
364- echo "Available memory before processing:"
365- free -h
366-
367- NODE_OPTIONS="--max-old-space-size=6144" npx agda-web-docs-lib process ./static/formal-spec ./agda-docs.config.json
368- else
369- echo "No HTML files found in formal-spec directory, skipping enhancement"
370203 fi
371204
372205 - name : 🏗️ Build Docusaurus site
@@ -381,7 +214,6 @@ jobs:
381214 echo "Error: Docusaurus build directory is empty"
382215 exit 1
383216 fi
384- echo "Docusaurus build verified"
385217 ls -la build/
386218
387219 - name : 🚀 Upload Docusaurus build
@@ -394,14 +226,9 @@ jobs:
394226
395227 docs-publish :
396228 name : " Publish"
397- if : |
398- (github.ref == 'refs/heads/main' || github.event_name == 'workflow_run') &&
399- (
400- (needs.docs-build-pr-push.result == 'success' && needs.docs-build-pr-push.outputs.has_changes == 'true') ||
401- (needs.docs-build-workflow-run.result == 'success' && needs.docs-build-workflow-run.outputs.has_changes == 'true')
402- )
403229 runs-on : ubuntu-latest
404- needs : [docs-build-pr-push, docs-build-workflow-run]
230+ needs : [build-docusaurus-site]
231+ if : github.ref == 'refs/heads/main' || github.event_name == 'workflow_run'
405232 steps :
406233 - name : 📥 Download Docusaurus build
407234 uses : actions/download-artifact@v4
0 commit comments