Formal Spec Listener #25
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: "Formal Spec Listener" | |
| on: | |
| repository_dispatch: | |
| types: [formal-spec-updated] | |
| workflow_dispatch: # Allow manual triggering for testing | |
| jobs: | |
| download-artifacts: | |
| name: "Download Formal Spec Artifacts" | |
| runs-on: ubuntu-latest | |
| outputs: | |
| artifacts-available: ${{ steps.check-artifacts.outputs.available }} | |
| download-successful: ${{ steps.validate-download.outputs.successful }} | |
| steps: | |
| - name: 📥 Checkout repository | |
| uses: actions/checkout@v4 | |
| - name: 🔍 List available artifacts in formal-spec repo | |
| id: list_artifacts | |
| run: | | |
| echo "Checking for artifacts in formal-spec repo..." | |
| echo "Event payload: ${{ toJSON(github.event.client_payload) }}" | |
| ARTIFACTS=$(curl -s -H "Authorization: token ${{ secrets.LEIOS_TRIGGER_PAT }}" \ | |
| "https://api.github.com/repos/input-output-hk/ouroboros-leios-formal-spec/actions/artifacts") | |
| echo "Available artifacts:" | |
| echo "$ARTIFACTS" | jq '.artifacts[] | {name: .name, id: .id, created_at: .created_at, expired: .expired, workflow_run: .workflow_run.id}' || true | |
| # Find the most recent formal-spec-html artifact ID | |
| ARTIFACT_ID=$(echo "$ARTIFACTS" | jq -r '.artifacts[] | select(.name=="formal-spec-html" and .expired==false) | .id' | head -n 1) | |
| if [ -n "$ARTIFACT_ID" ]; then | |
| echo "Found formal-spec-html artifact with ID: $ARTIFACT_ID" | |
| echo "artifact_id=$ARTIFACT_ID" >> $GITHUB_OUTPUT | |
| else | |
| echo "No valid formal-spec-html artifact found" | |
| fi | |
| - name: 📥 Download formal spec HTML by run ID | |
| id: download_by_run | |
| if: github.event.client_payload.run_id != '' | |
| uses: actions/download-artifact@v4 | |
| continue-on-error: true | |
| with: | |
| name: formal-spec-html | |
| repository: input-output-hk/ouroboros-leios-formal-spec | |
| run-id: ${{ github.event.client_payload.run_id }} | |
| path: formal-spec-html | |
| github-token: ${{ secrets.LEIOS_TRIGGER_PAT }} | |
| - name: 📥 Download formal spec HTML by artifact ID (fallback) | |
| id: download_by_id | |
| if: steps.download_by_run.outcome != 'success' && steps.list_artifacts.outputs.artifact_id != '' | |
| uses: dawidd6/action-download-artifact@v6 | |
| continue-on-error: true | |
| with: | |
| name: formal-spec-html | |
| repo: input-output-hk/ouroboros-leios-formal-spec | |
| workflow: formal-spec.yaml | |
| path: formal-spec-html | |
| github_token: ${{ secrets.LEIOS_TRIGGER_PAT }} | |
| search_artifacts: true | |
| if_no_artifact_found: warn | |
| - name: ✅ Validate download and create placeholder if needed | |
| id: validate-download | |
| run: | | |
| mkdir -p formal-spec-html | |
| # Check if we successfully downloaded files | |
| if [ -n "$(ls -A formal-spec-html 2>/dev/null)" ]; then | |
| echo "Using downloaded formal spec HTML" | |
| echo "Files in formal-spec-html directory:" | |
| ls -la formal-spec-html/ | |
| echo "successful=true" >> $GITHUB_OUTPUT | |
| else | |
| echo "No formal spec HTML available, creating placeholder" | |
| echo "<html><body><h1>Formal Specification</h1><p>Formal specification documentation is being updated. Please check back later.</p></body></html>" > formal-spec-html/index.html | |
| echo "successful=false" >> $GITHUB_OUTPUT | |
| fi | |
| - name: 🔍 Check artifacts availability | |
| id: check-artifacts | |
| run: | | |
| if [ -d "formal-spec-html" ] && [ -n "$(ls -A formal-spec-html/ 2>/dev/null)" ]; then | |
| echo "available=true" >> $GITHUB_OUTPUT | |
| else | |
| echo "available=false" >> $GITHUB_OUTPUT | |
| fi | |
| - name: 📤 Upload artifacts for next job | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| name: formal-spec-html-processed | |
| path: formal-spec-html/ | |
| retention-days: 1 | |
| update-formal-spec: | |
| name: "Update Formal Spec in Repository" | |
| runs-on: ubuntu-latest | |
| needs: download-artifacts | |
| if: needs.download-artifacts.outputs.artifacts-available == 'true' | |
| steps: | |
| - name: 📥 Checkout repository | |
| uses: actions/checkout@v4 | |
| with: | |
| token: ${{ secrets.GITHUB_TOKEN || github.token }} | |
| - name: 📥 Download artifacts from previous job | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: formal-spec-html-processed | |
| path: formal-spec-html | |
| - name: 🛠️ Setup Node.js | |
| uses: actions/setup-node@v4 | |
| with: | |
| node-version: 22 | |
| cache: "npm" | |
| cache-dependency-path: ./site/package-lock.json | |
| - name: 📦 Install dependencies | |
| working-directory: site | |
| run: npm ci | |
| - name: 📝 Update formal spec directory | |
| run: | | |
| # Clear existing formal spec files | |
| rm -rf site/static/formal-spec/* | |
| if [ -d "formal-spec-html" ] && [ -n "$(ls -A formal-spec-html/ 2>/dev/null)" ]; then | |
| cp -r formal-spec-html/* site/static/formal-spec/ | |
| fi | |
| - name: 🔄 Enhance Agda documentation | |
| uses: will-break-it/agda-web-docs-lib@v1 | |
| with: | |
| input-dir: site/static/formal-spec | |
| config-file: site/agda-docs.config.json | |
| cache-dependency-path: site/package-lock.json | |
| node-options: "--max-old-space-size=8192" | |
| - name: 🔍 Check for changes | |
| id: check-changes | |
| run: | | |
| git add site/static/formal-spec/ | |
| if git diff --staged --quiet; then | |
| echo "No changes to commit" | |
| echo "has_changes=false" >> $GITHUB_OUTPUT | |
| else | |
| echo "Changes detected in formal spec" | |
| echo "has_changes=true" >> $GITHUB_OUTPUT | |
| fi | |
| - name: 💾 Commit and push changes | |
| if: steps.check-changes.outputs.has_changes == 'true' | |
| run: | | |
| git config --global user.name 'github-actions[bot]' | |
| git config --global user.email 'github-actions[bot]@users.noreply.github.com' | |
| git commit -m "Update formal specification documentation | |
| - Updated from ouroboros-leios-formal-spec repository | |
| - Run ID: ${{ github.event.client_payload.run_id || 'manual' }} | |
| - Triggered by: ${{ github.event_name }}" | |
| git push |