feat(Channel): add Schmidt singular values #8125
Workflow file for this run
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: Lint blueprint | |
| on: | |
| push: | |
| branches: | |
| - main | |
| paths: | |
| - '**.lean' | |
| - 'lakefile.*' | |
| - 'lean-toolchain' | |
| - 'lake-manifest.json' | |
| - '.github/workflows/lint-blueprint.yml' | |
| - 'blueprint/src/**' | |
| - 'blueprint/.chktexrc' | |
| - 'blueprint/latexindent.yaml' | |
| - 'scripts/blueprint_bibtex.py' | |
| - 'scripts/blueprint_lean_sync.py' | |
| - 'scripts/check_reader_facing_prose.py' | |
| pull_request: | |
| types: [opened, synchronize, reopened] | |
| paths: | |
| - '**.lean' | |
| - 'lakefile.*' | |
| - 'lean-toolchain' | |
| - 'lake-manifest.json' | |
| - '.github/workflows/lint-blueprint.yml' | |
| - 'blueprint/src/**' | |
| - 'blueprint/.chktexrc' | |
| - 'blueprint/latexindent.yaml' | |
| - 'scripts/blueprint_bibtex.py' | |
| - 'scripts/blueprint_lean_sync.py' | |
| - 'scripts/check_reader_facing_prose.py' | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: true | |
| jobs: | |
| lint-blueprint: | |
| runs-on: ubuntu-latest | |
| name: Check blueprint compiles without errors | |
| steps: | |
| - uses: actions/checkout@v6 | |
| with: | |
| fetch-depth: 0 | |
| - name: Check reader-facing prose patterns | |
| if: github.event_name == 'pull_request' | |
| env: | |
| BASE_REF: origin/${{ github.event.pull_request.base.ref }} | |
| run: | | |
| git fetch --no-tags origin "+refs/heads/${{ github.event.pull_request.base.ref }}:refs/remotes/origin/${{ github.event.pull_request.base.ref }}" | |
| python3 scripts/check_reader_facing_prose.py --root . --diff-base "$BASE_REF" --ci | |
| - name: Detect changed Lean files | |
| id: changed-lean-files | |
| if: github.event_name == 'pull_request' | |
| env: | |
| BASE_REF: origin/${{ github.event.pull_request.base.ref }} | |
| run: | | |
| git fetch --no-tags origin "+refs/heads/${{ github.event.pull_request.base.ref }}:refs/remotes/origin/${{ github.event.pull_request.base.ref }}" | |
| changed_lean_paths="$(git diff --merge-base --name-only "$BASE_REF" -- \ | |
| TNLean.lean 'TNLean/**/*.lean' lakefile.* lean-toolchain lake-manifest.json)" | |
| if [ -n "$changed_lean_paths" ]; then | |
| has_changed_lean=true | |
| else | |
| has_changed_lean=false | |
| while IFS= read -r tex_file; do | |
| if [ -f "$tex_file" ] && grep -Eq '\\lean\{|\\uses\{|\\leanok|\\notready' "$tex_file"; then | |
| has_changed_lean=true | |
| break | |
| fi | |
| base_tex="$(git show "$BASE_REF:$tex_file" 2>/dev/null || true)" | |
| if [ -n "$base_tex" ] \ | |
| && grep -Eq '\\lean\{|\\uses\{|\\leanok|\\notready' <<< "$base_tex"; then | |
| has_changed_lean=true | |
| break | |
| fi | |
| done < <(git diff --merge-base --name-only "$BASE_REF" -- \ | |
| 'blueprint/src/**/*.tex' 'blueprint/src/*.tex') | |
| fi | |
| echo "has_changed_lean=$has_changed_lean" >> "$GITHUB_OUTPUT" | |
| - name: Set up Lean toolchain | |
| id: lean-setup | |
| if: github.event_name != 'pull_request' || steps.changed-lean-files.outputs.has_changed_lean == 'true' | |
| continue-on-error: true | |
| timeout-minutes: 6 | |
| uses: texra-ai/lean-env-action@v1 | |
| - name: Install blueprint system dependencies | |
| uses: texra-ai/lean-env-action/blueprint-system-deps@v1 | |
| - name: Install blueprint Python dependencies | |
| uses: texra-ai/lean-env-action/leanblueprint@v1 | |
| - name: Check tensor-network diagram macros | |
| run: | | |
| cd blueprint/src | |
| PYTHONPATH=Packages python3 Packages/tn_diagrams.py \ | |
| --check \ | |
| --check-peps-usage \ | |
| --smoke-render | |
| - name: Lint LaTeX (chktex) | |
| run: | | |
| cd blueprint/src | |
| find . -name '*.tex' -not -path '*/Packages/*' -print0 \ | |
| | xargs -0 -r chktex -q -l ../.chktexrc | |
| # TODO: drop continue-on-error after a separate mechanical PR has run | |
| # `latexindent -l blueprint/latexindent.yaml -w -s` over blueprint/src. | |
| - name: Check LaTeX formatting (latexindent) | |
| continue-on-error: true | |
| timeout-minutes: 5 | |
| run: | | |
| set -e | |
| status=0 | |
| while IFS= read -r f; do | |
| if ! latexindent -k -s -l blueprint/latexindent.yaml "$f" > /dev/null; then | |
| echo "::warning file=$f::not formatted to blueprint/latexindent.yaml; run 'latexindent -l blueprint/latexindent.yaml -w -s \"$f\"' locally to fix" | |
| status=1 | |
| fi | |
| done < <(find blueprint/src -name '*.tex' -not -path '*/Packages/*') | |
| exit $status | |
| - name: Build blueprint bibliography | |
| run: python3 scripts/blueprint_bibtex.py | |
| - name: Run leanblueprint web and check for errors | |
| working-directory: blueprint | |
| run: | | |
| set -o pipefail | |
| tmp_output_file="$(mktemp)" | |
| # Run leanblueprint, streaming output to the log and capturing it to a file | |
| set +o pipefail | |
| leanblueprint web 2>&1 | tee "$tmp_output_file" | |
| cmd_status=${PIPESTATUS[0]} | |
| set -o pipefail | |
| # Check for blueprint ERROR lines in the captured output | |
| if grep -q "^ERROR:" "$tmp_output_file"; then | |
| echo "::error::Blueprint has unresolved labels (see ERROR lines above)" | |
| exit 1 | |
| fi | |
| if grep -q "WARNING: File not found:" "$tmp_output_file"; then | |
| echo "::warning::Blueprint has missing file references (see WARNING lines above)" | |
| fi | |
| # If leanblueprint itself failed, propagate its exit status | |
| if [ "$cmd_status" -ne 0 ]; then | |
| exit "$cmd_status" | |
| fi | |
| - name: Generate lean_decls from blueprint .tex files | |
| id: lean-decls | |
| run: python3 scripts/blueprint_lean_sync.py --root . --update-lean-decls | |
| - name: Check blueprint and Lean source stay in sync | |
| if: steps.lean-decls.outcome == 'success' | |
| run: python3 scripts/blueprint_lean_sync.py --root . --ci | |
| - name: Fetch PR base ref for diff | |
| id: fetch-base-ref | |
| if: github.event_name == 'pull_request' && steps.lean-setup.outcome == 'success' | |
| env: | |
| BASE_REF: ${{ github.event.pull_request.base.ref }} | |
| run: git fetch --no-tags origin "$BASE_REF" | |
| - name: Error on changed Lean declarations missing blueprint entries | |
| if: github.event_name == 'pull_request' && steps.lean-setup.outcome == 'success' | |
| env: | |
| BASE_REF: origin/${{ github.event.pull_request.base.ref }} | |
| run: | | |
| python3 - <<'PY' | |
| import os | |
| import subprocess | |
| base_ref = os.environ["BASE_REF"] | |
| changed = subprocess.check_output( | |
| [ | |
| "git", | |
| "diff", | |
| "--merge-base", | |
| "--name-only", | |
| "--diff-filter=AMR", | |
| base_ref, | |
| "--", | |
| "TNLean.lean", | |
| "TNLean/**/*.lean", | |
| ], | |
| text=True, | |
| ) | |
| changed_lean_files = [line for line in changed.splitlines() if line.endswith(".lean")] | |
| if not changed_lean_files: | |
| print("No changed TNLean/*.lean files in this pull request.") | |
| raise SystemExit(0) | |
| subprocess.run( | |
| [ | |
| "python3", | |
| "scripts/blueprint_lean_sync.py", | |
| "--root", | |
| ".", | |
| "--warn-missing-blueprint", | |
| "--diff-base", | |
| base_ref, | |
| "--changed-files", | |
| *changed_lean_files, | |
| ], | |
| check=True, | |
| ) | |
| PY | |
| - name: Check blueprint Lean declarations | |
| if: steps.lean-setup.outcome == 'success' && steps.lean-decls.outcome == 'success' | |
| continue-on-error: true | |
| timeout-minutes: 10 | |
| run: | | |
| if ! lake exe checkdecls blueprint/lean_decls; then | |
| echo "::warning::Some blueprint/lean_decls entries have no matching Lean declaration yet (this is expected while formalization is in progress)" | |
| fi |