AlgebraicFramework: Jordan/JB/JBW hierarchy, Stinespring dilation, trace-class infrastructure

.codespellignore

@@ -16,3 +16,7 @@ dOut
 SINIC
 ofSet
 mapP
+hTe
+hSA
+hsI
+hax

.github/workflows/alphaBuild.yml

@@ -13,9 +13,14 @@ jobs:
   alpha_build:
     name: Lean based style linters
     runs-on: ubuntu-latest
+    env:
+      LAKE_CACHE_DIR: .lake/cache
     steps:
 
+      # Full history so lake can look back for a commit with a cache, see build.yml
       - uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
 
       - name: Install elan
         run: |
@@ -29,10 +34,18 @@ jobs:
           lean --version
           lake --version
 
-      - name: build cache
+      - name: Mathlib build cache
         run: |
           lake exe cache get
 
+      # PhyslibAlpha has its own cache in the bucket so we pull that one
+      - name: PhyslibAlpha's build cache
+        env:
+          LAKE_CONFIG: ${{ github.workspace }}/lake-cache.toml
+        run: |
+          lake cache get --scope="physlib-master/$(tr '/:' '--' < lean-toolchain | tr -d '[:space:]')/alpha" \
+            || echo "no existing cache to restore -- building from scratch"
+
       - name: build PhyslibAlpha
         id: build
         uses: liskin/gh-problem-matcher-wrap@v3
@@ -50,6 +63,13 @@ jobs:
           linters: gcc
           run: env LEAN_ABORT_ON_PANIC=1 lake exe runPhyslibAlphaLinters
 
+      - name: Check no PhyslibAlpha in Physlib and QuantumInfo
+        run: env LEAN_ABORT_ON_PANIC=1 lake exe noAlphaImports
+
+      - name: Check PhyslibAlpha imports
+        run: env LEAN_ABORT_ON_PANIC=1 lake exe alphaFileImports
+
+
   style_lint:
     name: Python based linters
     runs-on: ubuntu-latest
@@ -73,16 +93,6 @@ jobs:
         with:
           python-version: 3.8
 
-      - name: Check PhyslibAlpha imports
-        run: |
-          chmod u+x scripts/PhyslibAlpha/alphaFileImports.py
-          ./scripts/PhyslibAlpha/alphaFileImports.py
-
-      - name: Check no PhyslibAlpha in Physlib and QuantumInfo
-        run: |
-          chmod u+x scripts/PhyslibAlpha/noAlphaImports.py
-          ./scripts/PhyslibAlpha/noAlphaImports.py
-
       - name: Python linters for PhyslibAlpha
         run: |
           chmod u+x scripts/PhyslibAlpha/alphaPythonLinters.sh

.github/workflows/build.yml

@@ -13,9 +13,15 @@ jobs:
   doc_lint:
     name: Lean based style linters
     runs-on: ubuntu-latest
+    env:
+      LAKE_CACHE_DIR: .lake/cache
     steps:
 
+      # Need the full history here, lake looks back through the commits to find
+      # one with a cache. A shallow clone only has one so it never finds anything.
       - uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
 
       - name: Install elan
         run: |
@@ -29,10 +35,19 @@ jobs:
           lean --version
           lake --version
 
-      - name: build cache
+      - name: Mathlib build cache
         run: |
           lake exe cache get
 
+      # Pulls the cache from the bucket so we only compile what the PR changed.
+      # No key needed as it is only reading. If it fails we just build from scratch.
+      - name: Physlib's build cache
+        env:
+          LAKE_CONFIG: ${{ github.workspace }}/lake-cache.toml
+        run: |
+          lake cache get --scope="physlib-master/$(tr '/:' '--' < lean-toolchain | tr -d '[:space:]')/physlib" \
+            || echo "no existing cache to restore -- building from scratch"
+
       - name: build Physlib
         id: build
         uses: liskin/gh-problem-matcher-wrap@v3

.github/workflows/pr_size_label.yaml

@@ -0,0 +1,85 @@
+name: PR size label
+
+on:
+  pull_request_target:
+    types: [opened, synchronize, reopened]
+
+# Limit permissions for GITHUB_TOKEN for the entire workflow
+permissions:
+  contents: read
+  pull-requests: write  # Only allow PR comments/labels
+  # All other permissions are implicitly 'none'
+
+jobs:
+  add_size_label:
+    name: Add size label
+    runs-on: ubuntu-latest
+    # Don't run on forks, where we wouldn't have permissions to add the label anyway.
+    if: github.repository == 'leanprover-community/physlib'
+    steps:
+      - name: Label PR by size
+        uses: actions/github-script@v7
+        with:
+          script: |
+            const SIZES = [
+              { label: 'small', color: '2ea44f', max: 100 },
+              { label: 'medium', color: 'f66a0a', max: 500 },
+              { label: 'large', color: 'd73a4a', max: Infinity },
+            ];
+
+            const { data: pr } = await github.rest.pulls.get({
+              owner: context.repo.owner,
+              repo: context.repo.repo,
+              pull_number: context.issue.number,
+            });
+
+            const changedLines = pr.additions + pr.deletions;
+            const target = SIZES.find(s => changedLines < s.max) ?? SIZES[SIZES.length - 1];
+
+            core.info(`PR #${pr.number}: ${changedLines} lines changed -> ${target.label}`);
+
+            // Ensure all three size labels exist with the right color, and remove
+            // any size label that isn't the one that currently applies.
+            for (const size of SIZES) {
+              try {
+                await github.rest.issues.getLabel({
+                  owner: context.repo.owner,
+                  repo: context.repo.repo,
+                  name: size.label,
+                });
+              } catch (err) {
+                if (err.status === 404) {
+                  await github.rest.issues.createLabel({
+                    owner: context.repo.owner,
+                    repo: context.repo.repo,
+                    name: size.label,
+                    color: size.color,
+                  });
+                } else {
+                  throw err;
+                }
+              }
+
+              if (size.label !== target.label) {
+                try {
+                  await github.rest.issues.removeLabel({
+                    owner: context.repo.owner,
+                    repo: context.repo.repo,
+                    issue_number: pr.number,
+                    name: size.label,
+                  });
+                } catch (err) {
+                  if (err.status !== 404) throw err;
+                }
+              }
+            }
+
+            const existingLabels = pr.labels.map(l => l.name);
+            if (!existingLabels.includes(target.label)) {
+              await github.rest.issues.addLabels({
+                owner: context.repo.owner,
+                repo: context.repo.repo,
+                issue_number: pr.number,
+                labels: [target.label],
+              });
+            }

.github/workflows/publish-cache.yml

@@ -0,0 +1,194 @@
+on:
+  push:
+    branches:
+      - master
+
+name: Publish build cache
+
+# Pulls the cache from the bucket and then does a build with the new changes that are being merged
+# Then it creates a new cache which is pushed to the web bucket where they can be accessed
+# by `lake exe get_cache`.
+
+jobs:
+  # `secrets` is not allowed in a job-level `if:` -- GitHub rejects the whole
+  # file. Gating on a `needs` output instead skips the build jobs when the
+  # bucket is not set up yet.
+  gate:
+    name: Check for cache credentials
+    runs-on: ubuntu-latest
+    outputs:
+      has_key: ${{ steps.check.outputs.has_key }}
+    steps:
+      - name: look for LAKE_CACHE_KEY
+        id: check
+        env:
+          LAKE_CACHE_KEY: ${{ secrets.LAKE_CACHE_KEY }}
+        run: |
+          set -euo pipefail
+          if [ -n "$LAKE_CACHE_KEY" ]; then
+            echo "has_key=true" >> "$GITHUB_OUTPUT"
+          else
+            echo "::notice::LAKE_CACHE_KEY is not set, so the build cache will not be published. See docs/cache-setup.md."
+            echo "has_key=false" >> "$GITHUB_OUTPUT"
+          fi
+
+  physlib:
+    name: Physlib + QuantumInfo
+    needs: gate
+    if: needs.gate.outputs.has_key == 'true'
+    runs-on: ubuntu-latest
+    env:
+      LAKE_CACHE_DIR: .lake/cache
+    steps:
+      # Full history so lake can look back for a commit with a cache,
+      # a shallow clone only has one so the restore below never finds anything
+      - uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
+
+      # Each job needs its own scope: Lake PUTs the revision mappings to
+      # <revisionEndpoint>/<scope>/<sha>.jsonl, so a shared scope would have
+      # one job overwrite the other's. The toolchain is in the scope because
+      # Lake ignores --toolchain for verbatim scopes.
+      # scripts/get_cache.lean builds the same strings -- keep them in step.
+      - name: compute cache scope
+        run: |
+          set -euo pipefail
+          TC="$(tr '/:' '--' < lean-toolchain | tr -d '[:space:]')"
+          echo "CACHE_SCOPE=physlib-master/$TC/physlib" >> "$GITHUB_ENV"
+
+      - name: Install elan
+        run: |
+          set -o pipefail
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
+          ~/.elan/bin/lean --version
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+
+      - name: build cache
+        run: |
+          lake exe cache get
+
+      # This reads the existing info in the bucket so that we only have to update whats changed
+      # If the bucket is empty we will have to build from scratch.
+      - name: restore Physlib's own cache
+        env:
+          LAKE_CONFIG: ${{ github.workspace }}/lake-cache.toml
+        run: |
+          lake cache get --scope="$CACHE_SCOPE" || echo "no existing cache to restore -- building from scratch"
+
+      - name: build Physlib
+        run: |
+          bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build -KCI | tee stdout.log"
+
+      # `--no-build` here does not build anything; it emits the
+      # input-to-output mappings for what was just built.
+      - name: stage build outputs for the cache
+        id: stage
+        continue-on-error: true
+        run: |
+          set -euo pipefail
+          mkdir -p ../lake-cache-staging
+          lake build --no-build -KCI -o .lake/outputs.jsonl
+          echo "mappings: $(wc -l < .lake/outputs.jsonl) entries"
+          lake cache stage .lake/outputs.jsonl ../lake-cache-staging
+          echo "staged: $(find ../lake-cache-staging -name '*.ltar' | wc -l) ltar files"
+
+      - name: publish to R2 cache
+        id: publish
+        if: steps.stage.outcome == 'success'
+        continue-on-error: true
+        env:
+          LAKE_CACHE_KEY_RAW: ${{ secrets.LAKE_CACHE_KEY }}
+          LAKE_CONFIG: ${{ github.workspace }}/lake-cache.toml
+        run: |
+          set -euo pipefail
+          # GitHub secrets commonly carry a trailing newline, which breaks the
+          # SigV4 signature. Trim it, and mask the value so it cannot surface
+          # in logs.
+          KEY="$(printf %s "$LAKE_CACHE_KEY_RAW" | sed -e 's/[[:space:]]*$//')"
+          echo "::add-mask::$KEY"
+          export LAKE_CACHE_KEY="$KEY"
+
+          lake cache put-staged ../lake-cache-staging \
+            --scope="$CACHE_SCOPE" \
+            --rev="${{ github.sha }}"
+
+      - name: warn if cache publish failed
+        if: steps.stage.outcome == 'failure' || steps.publish.outcome == 'failure'
+        run: echo "::warning::Physlib build cache was not published this run (staging or upload failed). Contributors will fall back to compiling from source until the next successful push."
+
+  physlib_alpha:
+    name: PhyslibAlpha
+    needs: gate
+    if: needs.gate.outputs.has_key == 'true'
+    runs-on: ubuntu-latest
+    env:
+      LAKE_CACHE_DIR: .lake/cache
+    steps:
+      # Full history, see the physlib job above
+      - uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
+
+      # Own scope, so this job does not overwrite the physlib job's mappings.
+      - name: compute cache scope
+        run: |
+          set -euo pipefail
+          TC="$(tr '/:' '--' < lean-toolchain | tr -d '[:space:]')"
+          echo "CACHE_SCOPE=physlib-master/$TC/alpha" >> "$GITHUB_ENV"
+
+      - name: Install elan
+        run: |
+          set -o pipefail
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
+          ~/.elan/bin/lean --version
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+
+      - name: build cache
+        run: |
+          lake exe cache get
+
+      # See the physlib job's "restore Physlib's own cache" step -- same
+      # idea, seeding from this job's own scope before its build.
+      - name: restore PhyslibAlpha's own cache
+        env:
+          LAKE_CONFIG: ${{ github.workspace }}/lake-cache.toml
+        run: |
+          lake cache get --scope="$CACHE_SCOPE" || echo "no existing cache to restore -- building from scratch"
+
+      - name: build PhyslibAlpha
+        run: |
+          bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build -KCI PhyslibAlpha | tee stdout.log"
+
+      # Stage the cache so it can be pushed to the bucket
+      - name: stage build outputs for the cache
+        id: stage
+        continue-on-error: true
+        run: |
+          set -euo pipefail
+          mkdir -p ../lake-cache-staging
+          lake build --no-build -KCI PhyslibAlpha -o .lake/outputs.jsonl
+          echo "mappings: $(wc -l < .lake/outputs.jsonl) entries"
+          lake cache stage .lake/outputs.jsonl ../lake-cache-staging
+          echo "staged: $(find ../lake-cache-staging -name '*.ltar' | wc -l) ltar files"
+
+      - name: publish to R2 cache
+        id: publish
+        if: steps.stage.outcome == 'success'
+        continue-on-error: true
+        env:
+          LAKE_CACHE_KEY_RAW: ${{ secrets.LAKE_CACHE_KEY }}
+          LAKE_CONFIG: ${{ github.workspace }}/lake-cache.toml
+        run: |
+          set -euo pipefail
+          KEY="$(printf %s "$LAKE_CACHE_KEY_RAW" | sed -e 's/[[:space:]]*$//')"
+          echo "::add-mask::$KEY"
+          export LAKE_CACHE_KEY="$KEY"
+
+          lake cache put-staged ../lake-cache-staging \
+            --scope="$CACHE_SCOPE" \
+            --rev="${{ github.sha }}"
+
+      - name: warn if cache publish failed
+        if: steps.stage.outcome == 'failure' || steps.publish.outcome == 'failure'
+        run: echo "::warning::PhyslibAlpha build cache was not published this run."