docs #221
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: "docs" | |
| on: | |
| pull_request: | |
| paths: | |
| - "**/*.d2" | |
| - "site/**" | |
| - "ui/**" | |
| push: | |
| branches: | |
| - main | |
| paths: | |
| - "**/*.d2" | |
| - "site/**" | |
| - "ui/**" | |
| workflow_run: | |
| workflows: ["Formal Spec Listener"] | |
| types: | |
| - completed | |
| branches: | |
| - main | |
| workflow_dispatch: # Allow manual triggering or via API | |
| inputs: | |
| source: | |
| description: "Source of the workflow dispatch" | |
| required: false | |
| default: "manual" | |
| # Global permissions | |
| permissions: | |
| contents: read | |
| pages: write | |
| actions: read | |
| # Prevent redundant workflow runs | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: true | |
| jobs: | |
| docs-generate-d2-diagrams: | |
| name: "Generate D2 Diagrams" | |
| # Only run this job on pull_request or push triggers, not on workflow_run | |
| if: github.event_name == 'pull_request' || github.event_name == 'push' | |
| runs-on: ubuntu-latest | |
| permissions: | |
| contents: write | |
| steps: | |
| - name: 📥 Checkout repository | |
| uses: actions/checkout@v4 | |
| with: | |
| ref: ${{ github.head_ref || github.ref_name }} | |
| fetch-depth: 2 # Needed to get previous commit for comparison | |
| - name: Cache D2 | |
| uses: actions/cache@v4 | |
| with: | |
| path: ~/.d2 | |
| key: ${{ runner.os }}-d2-${{ hashFiles('**/install.sh') }} | |
| restore-keys: | | |
| ${{ runner.os }}-d2- | |
| - name: Install D2 | |
| run: | | |
| if ! command -v d2 &> /dev/null; then | |
| curl -fsSL https://d2lang.com/install.sh | sh -s -- | |
| fi | |
| d2 --version | |
| - name: Generate PNG files for changed D2 files | |
| run: | | |
| # Get list of changed .d2 files | |
| CHANGED_FILES=$(git diff --name-only HEAD^ HEAD | grep '\.d2$' || true) | |
| if [ -z "$CHANGED_FILES" ]; then | |
| echo "No .d2 files were changed" | |
| exit 0 | |
| fi | |
| echo "Changed .d2 files:" | |
| echo "$CHANGED_FILES" | |
| # Process each changed file | |
| echo "$CHANGED_FILES" | while read -r file; do | |
| if [ -f "$file" ]; then | |
| output_file="${file%.d2}.png" | |
| echo "Converting $file to $output_file" | |
| d2 "$file" "$output_file" | |
| else | |
| echo "File $file does not exist, skipping" | |
| fi | |
| done | |
| - name: Check for changes | |
| id: changes | |
| run: | | |
| git add *.png | |
| if git diff --staged --quiet; then | |
| echo "No changes to commit" | |
| echo "has_changes=false" >> $GITHUB_OUTPUT | |
| else | |
| echo "Changes detected" | |
| echo "has_changes=true" >> $GITHUB_OUTPUT | |
| fi | |
| - name: Commit and push changes | |
| if: steps.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 "Auto-generate diagram PNGs [skip ci]" | |
| git push origin HEAD:${{ github.head_ref || github.ref_name }} | |
| viz-build: | |
| name: "Build Visualizer" | |
| # Only run this job on pull_request or push triggers, not on workflow_run | |
| if: github.event_name == 'pull_request' || github.event_name == 'push' | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: 📥 Checkout repository | |
| uses: actions/checkout@v4 | |
| with: | |
| lfs: true | |
| fetch-depth: 2 | |
| - name: 🛠️ Setup Node.js | |
| uses: actions/setup-node@v4 | |
| with: | |
| node-version: 22 | |
| cache: "yarn" | |
| cache-dependency-path: ./ui/yarn.lock | |
| - name: 📦 Install dependencies | |
| working-directory: ui | |
| run: yarn install | |
| - name: 🏗️ Build visualizer | |
| working-directory: ui | |
| run: | | |
| yarn build | |
| - name: 🚢 Upload visualizer static site | |
| id: upload_viz | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| name: visualizer | |
| path: ui/dist | |
| # This job handles PR and push events, and depends on viz-build | |
| docs-build-pr-push: | |
| name: "Build Docusaurus Site (PR/Push)" | |
| runs-on: ubuntu-latest | |
| needs: [viz-build] | |
| if: github.event_name == 'pull_request' || github.event_name == 'push' || github.event_name == 'workflow_dispatch' | |
| outputs: | |
| has_changes: ${{ steps.check_changes.outputs.has_changes || github.event_name == 'workflow_dispatch' }} | |
| steps: | |
| - name: 📥 Checkout repository | |
| uses: actions/checkout@v4 | |
| with: | |
| fetch-depth: 2 | |
| - name: Debug workflow trigger info | |
| run: | | |
| echo "Event name: ${{ github.event_name }}" | |
| echo "Ref: ${{ github.ref }}" | |
| - name: Check for site or visualizer changes | |
| id: check_changes | |
| run: | | |
| if [ "${{ github.event_name }}" == "workflow_dispatch" ]; then | |
| echo "Changes from manual trigger" | |
| echo "has_changes=true" >> $GITHUB_OUTPUT | |
| else | |
| # For PR or push events, check for actual changes | |
| SITE_CHANGES=$(git diff --name-only HEAD^ HEAD -- site/ || true) | |
| VIZ_CHANGES=$(git diff --name-only HEAD^ HEAD -- ui/ || true) | |
| if [ -z "$SITE_CHANGES" ] && [ -z "$VIZ_CHANGES" ]; then | |
| echo "No changes in site or UI directory" | |
| echo "has_changes=false" >> $GITHUB_OUTPUT | |
| else | |
| echo "Changes detected in site or UI directory:" | |
| echo "$SITE_CHANGES" | |
| echo "$VIZ_CHANGES" | |
| echo "has_changes=true" >> $GITHUB_OUTPUT | |
| fi | |
| fi | |
| shell: "bash" | |
| - name: 🛠️ Setup Node.js | |
| if: steps.check_changes.outputs.has_changes == 'true' | |
| uses: actions/setup-node@v4 | |
| with: | |
| node-version: 22 | |
| cache: "yarn" | |
| cache-dependency-path: ./site/yarn.lock | |
| - name: 📦 Install dependencies | |
| if: steps.check_changes.outputs.has_changes == 'true' | |
| working-directory: site | |
| run: yarn install | |
| # Handle visualizer integration | |
| - name: 👁️ Unpack visualizer | |
| if: steps.check_changes.outputs.has_changes == 'true' | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: visualizer | |
| path: site/static/visualizer | |
| # Download formal spec HTML | |
| - name: 📥 Download formal spec HTML | |
| if: steps.check_changes.outputs.has_changes == 'true' | |
| uses: actions/download-artifact@v4 | |
| continue-on-error: true | |
| with: | |
| name: formal-spec-html | |
| path: formal-spec-html | |
| - name: 📝 Update formal spec | |
| if: steps.check_changes.outputs.has_changes == 'true' | |
| run: | | |
| # Create formal spec directory if it doesn't exist | |
| mkdir -p site/static/formal-spec | |
| # Copy any files we found (even if none were found, this is a no-op) | |
| if [ -d "formal-spec-html" ] && [ -n "$(ls -A formal-spec-html/ 2>/dev/null)" ]; then | |
| echo "Formal spec HTML files found - copying to site" | |
| cp -r formal-spec-html/* site/static/formal-spec/ | |
| else | |
| echo "No formal spec HTML files found - continuing without them" | |
| fi | |
| - name: 🔄 Enhance Agda documentation | |
| working-directory: site | |
| timeout-minutes: 20 | |
| run: | | |
| # Process HTML files using the agda-web-docs-lib only if there are actual HTML files | |
| HTML_COUNT=$(find ./static/formal-spec -name '*.html' | wc -l) | |
| echo "Found $HTML_COUNT HTML files" | |
| if [ "$HTML_COUNT" -gt "0" ]; then | |
| echo "Processing HTML files with agda-web-docs-lib" | |
| echo "Available memory before processing:" | |
| free -h | |
| # Use more memory but only 1 worker to reduce overall memory usage | |
| NODE_OPTIONS="--max-old-space-size=24576" npx agda-web-docs-lib process ./static/formal-spec ./agda-docs.config.json --workers 1 | |
| else | |
| echo "No HTML files found in formal-spec directory, skipping enhancement" | |
| fi | |
| - name: 🏗️ Build Docusaurus site | |
| if: steps.check_changes.outputs.has_changes == 'true' | |
| working-directory: site | |
| run: | | |
| yarn build | |
| - name: Verify Docusaurus build | |
| if: steps.check_changes.outputs.has_changes == 'true' | |
| working-directory: site | |
| run: | | |
| if [ -z "$(ls -A build/)" ]; then | |
| echo "Error: Docusaurus build directory is empty" | |
| exit 1 | |
| fi | |
| echo "Docusaurus build verified" | |
| ls -la build/ | |
| - name: 🚀 Upload Docusaurus build | |
| if: steps.check_changes.outputs.has_changes == 'true' | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| name: docusaurus-build | |
| if-no-files-found: error | |
| path: | | |
| site/build/* | |
| # This job handles workflow_run events from formal-spec-listener | |
| docs-build-workflow-run: | |
| name: "Build Docusaurus Site (Workflow Run)" | |
| runs-on: ubuntu-latest | |
| # No dependency on viz-build for workflow_run events | |
| if: github.event_name == 'workflow_run' && github.event.workflow_run.conclusion == 'success' | |
| outputs: | |
| has_changes: "true" | |
| steps: | |
| - name: 📥 Checkout repository | |
| uses: actions/checkout@v4 | |
| - name: Debug workflow trigger info | |
| run: | | |
| echo "Event name: ${{ github.event_name }}" | |
| echo "Workflow run conclusion: ${{ github.event.workflow_run.conclusion }}" | |
| echo "Workflow run name: ${{ github.event.workflow_run.name }}" | |
| echo "Workflow run ID: ${{ github.event.workflow_run.id }}" | |
| echo "Ref: ${{ github.ref }}" | |
| - name: List available artifacts | |
| run: | | |
| echo "Listing artifacts in the formal-spec-listener workflow run" | |
| curl -s -H "Authorization: token ${{ github.token }}" \ | |
| "https://api.github.com/repos/${{ github.repository }}/actions/runs/${{ github.event.workflow_run.id }}/artifacts" | \ | |
| jq '.artifacts[] | {name: .name, id: .id, created_at: .created_at, expired: .expired}' | |
| - 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 | |
| # Download formal spec HTML specifically from the workflow run | |
| - name: 📥 Download formal spec HTML | |
| uses: actions/download-artifact@v4 | |
| continue-on-error: true | |
| with: | |
| name: formal-spec-html | |
| run-id: ${{ github.event.workflow_run.id }} | |
| path: formal-spec-html | |
| - name: 📝 Update formal spec | |
| run: | | |
| # Create formal spec directory if it doesn't exist | |
| mkdir -p site/static/formal-spec | |
| # Copy any files we found (even if none were found, this is a no-op) | |
| if [ -d "formal-spec-html" ] && [ -n "$(ls -A formal-spec-html/ 2>/dev/null)" ]; then | |
| echo "Formal spec HTML files found - copying to site" | |
| cp -r formal-spec-html/* site/static/formal-spec/ | |
| else | |
| echo "No formal spec HTML files found - continuing without them" | |
| fi | |
| - name: 🔄 Enhance Agda documentation | |
| working-directory: site | |
| timeout-minutes: 20 | |
| run: | | |
| # Process HTML files using the agda-web-docs-lib only if there are actual HTML files | |
| HTML_COUNT=$(find ./static/formal-spec -name '*.html' | wc -l) | |
| echo "Found $HTML_COUNT HTML files" | |
| if [ "$HTML_COUNT" -gt "0" ]; then | |
| echo "Processing HTML files with agda-web-docs-lib" | |
| echo "Available memory before processing:" | |
| free -h | |
| # Use more memory but only 1 worker to reduce overall memory usage | |
| NODE_OPTIONS="--max-old-space-size=24576" npx agda-web-docs-lib process ./static/formal-spec ./agda-docs.config.json --workers 1 | |
| else | |
| echo "No HTML files found in formal-spec directory, skipping enhancement" | |
| 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 | |
| echo "Docusaurus build verified" | |
| ls -la build/ | |
| - name: 🚀 Upload Docusaurus build | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| name: docusaurus-build | |
| if-no-files-found: error | |
| path: | | |
| site/build/* | |
| docs-publish: | |
| name: "Publish" | |
| if: | | |
| github.ref == 'refs/heads/main' && | |
| (needs.docs-build-pr-push.outputs.has_changes == 'true' || needs.docs-build-workflow-run.outputs.has_changes == 'true') | |
| runs-on: ubuntu-latest | |
| needs: [docs-build-pr-push, docs-build-workflow-run] | |
| steps: | |
| - name: 📥 Download Docusaurus build | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: docusaurus-build | |
| path: ./github-pages | |
| - name: 🚀 Publish GitHub Pages | |
| uses: peaceiris/actions-gh-pages@v4 | |
| with: | |
| github_token: ${{ github.token }} | |
| publish_dir: ./github-pages | |
| cname: leios.cardano-scaling.org |