docs #217
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 | |
| docs-build: | |
| name: "Build Docusaurus Site" | |
| runs-on: ubuntu-latest | |
| needs: [viz-build] | |
| # For workflow_run events, we don't need viz-build | |
| if: | | |
| github.event_name == 'pull_request' || | |
| github.event_name == 'push' || | |
| github.event_name == 'workflow_dispatch' || | |
| (github.event_name == 'workflow_run' && github.event.workflow_run.conclusion == 'success') | |
| outputs: | |
| has_changes: ${{ steps.check_changes.outputs.has_changes || github.event_name == 'workflow_run' || github.event_name == 'workflow_dispatch' }} | |
| steps: | |
| - name: 📥 Checkout repository | |
| uses: actions/checkout@v4 | |
| with: | |
| fetch-depth: 2 | |
| - name: Check for site or visualizer changes | |
| id: check_changes | |
| run: | | |
| if [ "${{ github.event_name }}" == "workflow_run" ] || [ "${{ github.event_name }}" == "workflow_dispatch" ]; then | |
| echo "Changes detected from formal-spec workflow or 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' && (github.event_name == 'pull_request' || github.event_name == 'push') | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: visualizer | |
| path: site/static/visualizer | |
| # Download formal spec HTML - unified approach for all event types | |
| - 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 | |
| run-id: ${{ github.event_name == 'workflow_run' && github.event.workflow_run.id || '' }} | |
| 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 | |
| # Check if we have files to copy | |
| if [ -z "$(ls -A formal-spec-html/ 2>/dev/null)" ]; then | |
| echo "No formal spec HTML files found - using placeholder" | |
| echo "<html><body><h1>Formal Specification</h1><p>Formal specification documentation is being updated. Please check back later.</p></body></html>" > site/static/formal-spec/index.html | |
| else | |
| # Copy the HTML files | |
| cp -r formal-spec-html/* site/static/formal-spec/ | |
| fi | |
| - name: 🔄 Enhance Agda documentation | |
| if: steps.check_changes.outputs.has_changes == 'true' | |
| working-directory: site | |
| run: | | |
| # Process HTML files using the agda-web-docs-lib only if there are actual HTML files | |
| if [ -d "./static/formal-spec" ] && [ "$(find ./static/formal-spec -name '*.html' | grep -v index.html | wc -l)" -gt "0" ]; then | |
| NODE_OPTIONS="--max-old-space-size=16384" npx agda-web-docs-lib process ./static/formal-spec ./agda-docs.config.json | |
| 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/* | |
| docs-publish: | |
| name: "Publish" | |
| if: | | |
| github.ref == 'refs/heads/main' && | |
| needs.docs-build.outputs.has_changes == 'true' | |
| runs-on: ubuntu-latest | |
| needs: docs-build | |
| 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 |