distance based graph matching #550
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: Documentation | |
| on: | |
| push: | |
| branches: | |
| - main | |
| tags: | |
| - "v*" | |
| pull_request: | |
| branches: | |
| - main | |
| workflow_dispatch: | |
| permissions: | |
| contents: write | |
| pages: write | |
| id-token: write | |
| concurrency: | |
| group: pages | |
| cancel-in-progress: false | |
| jobs: | |
| build: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout repository | |
| uses: actions/checkout@v4 | |
| with: | |
| fetch-depth: 0 # Fetch full history for versioning | |
| - name: Set up Python | |
| uses: actions/setup-python@v5 | |
| with: | |
| python-version: "3.11" | |
| - name: Install uv | |
| uses: astral-sh/setup-uv@v5 | |
| with: | |
| enable-cache: true | |
| - name: Install dependencies | |
| run: | | |
| uv sync --all-extras --dev | |
| - name: Configure Git | |
| run: | | |
| git config --global user.name "github-actions[bot]" | |
| git config --global user.email "github-actions[bot]@users.noreply.github.com" | |
| git remote set-url origin https://x-access-token:${GITHUB_TOKEN}@github.com/${GITHUB_REPOSITORY}.git | |
| - name: Build documentation for PR | |
| if: github.event_name == 'pull_request' | |
| run: | | |
| uv run mkdocs build --verbose | |
| - name: Deploy development docs | |
| if: github.ref == 'refs/heads/main' && github.event_name == 'push' | |
| run: | | |
| uv run mike deploy --push --update-aliases dev development | |
| uv run mike set-default --push dev | |
| - name: Deploy release docs | |
| if: startsWith(github.ref, 'refs/tags/v') | |
| run: | | |
| VERSION=${GITHUB_REF#refs/tags/v} | |
| uv run mike deploy --push --update-aliases $VERSION latest | |
| uv run mike set-default --push latest | |
| - name: Setup Pages | |
| if: github.ref == 'refs/heads/main' && github.event_name == 'push' | |
| uses: actions/configure-pages@v4 | |
| - name: Build site for Pages | |
| if: github.ref == 'refs/heads/main' && github.event_name == 'push' | |
| run: | | |
| uv run mkdocs build | |
| - name: Upload artifact | |
| if: github.ref == 'refs/heads/main' && github.event_name == 'push' | |
| uses: actions/upload-pages-artifact@v3 | |
| with: | |
| path: './site' | |
| deploy: | |
| if: github.ref == 'refs/heads/main' && github.event_name == 'push' | |
| environment: | |
| name: github-pages | |
| url: ${{ steps.deployment.outputs.page_url }} | |
| runs-on: ubuntu-latest | |
| needs: build | |
| steps: | |
| - name: Deploy to GitHub Pages | |
| id: deployment | |
| uses: actions/deploy-pages@v4 |