formal-spec-updated #17
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: | |
| process-formal-spec: | |
| name: "Process Formal Spec Update" | |
| runs-on: ubuntu-latest | |
| outputs: | |
| spec_updated: "true" | |
| steps: | |
| - name: 📥 Checkout repository | |
| uses: actions/checkout@v4 | |
| # Try to download directly from GitHub API to see artifacts in the formal-spec repo | |
| - 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: Check download and create placeholder if needed | |
| 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/ | |
| 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 | |
| fi | |
| # Prepare Docusaurus site with formal spec | |
| - name: 📥 Checkout repository (again for site) | |
| uses: actions/checkout@v4 | |
| with: | |
| fetch-depth: 2 | |
| - name: 🛠️ Setup Node.js | |
| uses: actions/setup-node@v4 | |
| with: | |
| node-version: 22 | |
| cache: "yarn" | |
| cache-dependency-path: ./site/yarn.lock | |
| - name: 📦 Install dependencies | |
| working-directory: site | |
| run: yarn install | |
| - name: 📝 Update formal spec | |
| run: | | |
| mkdir -p 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 | |
| working-directory: site | |
| timeout-minutes: 25 | |
| run: | | |
| HTML_COUNT=$(find ./static/formal-spec -name '*.html' | wc -l) | |
| if [ "$HTML_COUNT" -gt "0" ]; then | |
| NODE_OPTIONS="--max-old-space-size=6144" npx agda-web-docs-lib process ./static/formal-spec ./agda-docs.config.json | |
| fi | |
| - name: 🏗️ Build Docusaurus site | |
| working-directory: site | |
| run: | | |
| yarn build | |
| - name: Verify Docusaurus build | |
| working-directory: site | |
| run: | | |
| if [ -z "$(ls -A build/)" ]; then | |
| echo "Error: Docusaurus build directory is empty" | |
| exit 1 | |
| fi | |
| ls -la build/ | |
| - name: 🚀 Publish GitHub Pages | |
| uses: peaceiris/actions-gh-pages@v4 | |
| with: | |
| github_token: ${{ secrets.GITHUB_TOKEN || github.token }} | |
| publish_dir: site/build | |
| cname: leios.cardano-scaling.org |