Small proofs

.github/workflows/pcs.yml

@@ -6,18 +6,35 @@ on:
     paths:
       - 'misc/pcs.tex'
       - '.github/workflows/pcs.yml'
+  pull_request:
+    paths:
+      - 'misc/pcs.tex'
+      - '.github/workflows/pcs.yml'
   workflow_dispatch:
 
-permissions:
-  contents: write
-
 concurrency:
   group: pcs-${{ github.ref }}
   cancel-in-progress: true
 
 jobs:
+  check-pdf:
+    if: github.event_name == 'pull_request'
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+    steps:
+      - uses: actions/checkout@v4
+      - name: Compile LaTeX
+        uses: xu-cheng/latex-action@v3
+        with:
+          working_directory: misc
+          root_file: pcs.tex
+
   build-pdf:
+    if: github.event_name != 'pull_request'
     runs-on: ubuntu-latest
+    permissions:
+      contents: write
     steps:
       - uses: actions/checkout@v4
       - name: Compile LaTeX
@@ -26,7 +43,6 @@ jobs:
           working_directory: misc
           root_file: pcs.tex
       - name: Publish PDF as release asset
-        if: github.event_name != 'pull_request'
         uses: softprops/action-gh-release@v2
         with:
           tag_name: pcs-latest

.github/workflows/pdf.yml

@@ -7,18 +7,36 @@ on:
       - 'misc/doc.tex'
       - 'misc/images/**'
       - '.github/workflows/pdf.yml'
+  pull_request:
+    paths:
+      - 'misc/doc.tex'
+      - 'misc/images/**'
+      - '.github/workflows/pdf.yml'
   workflow_dispatch:
 
-permissions:
-  contents: write
-
 concurrency:
   group: pdf-${{ github.ref }}
   cancel-in-progress: true
 
 jobs:
+  check-pdf:
+    if: github.event_name == 'pull_request'
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+    steps:
+      - uses: actions/checkout@v4
+      - name: Compile LaTeX
+        uses: xu-cheng/latex-action@v3
+        with:
+          working_directory: misc
+          root_file: doc.tex
+
   build-pdf:
+    if: github.event_name != 'pull_request'
     runs-on: ubuntu-latest
+    permissions:
+      contents: write
     steps:
       - uses: actions/checkout@v4
       - name: Compile LaTeX
@@ -27,7 +45,6 @@ jobs:
           working_directory: misc
           root_file: doc.tex
       - name: Publish PDF as release asset
-        if: github.event_name != 'pull_request'
         uses: softprops/action-gh-release@v2
         with:
           tag_name: spec-latest

.github/workflows/ring-switching.yml

@@ -6,18 +6,35 @@ on:
     paths:
       - 'misc/ring-switching.tex'
       - '.github/workflows/ring-switching.yml'
+  pull_request:
+    paths:
+      - 'misc/ring-switching.tex'
+      - '.github/workflows/ring-switching.yml'
   workflow_dispatch:
 
-permissions:
-  contents: write
-
 concurrency:
   group: ring-switching-${{ github.ref }}
   cancel-in-progress: true
 
 jobs:
+  check-pdf:
+    if: github.event_name == 'pull_request'
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+    steps:
+      - uses: actions/checkout@v4
+      - name: Compile LaTeX
+        uses: xu-cheng/latex-action@v3
+        with:
+          working_directory: misc
+          root_file: ring-switching.tex
+
   build-pdf:
+    if: github.event_name != 'pull_request'
     runs-on: ubuntu-latest
+    permissions:
+      contents: write
     steps:
       - uses: actions/checkout@v4
       - name: Compile LaTeX
@@ -26,7 +43,6 @@ jobs:
           working_directory: misc
           root_file: ring-switching.tex
       - name: Publish PDF as release asset
-        if: github.event_name != 'pull_request'
         uses: softprops/action-gh-release@v2
         with:
           tag_name: ring-switching-latest

.github/workflows/rust.yml

@@ -0,0 +1,32 @@
+name: Rust
+
+on:
+  push:
+    branches: [ "main" ]
+  pull_request:
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+concurrency:
+  group: rust-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  release:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: dtolnay/rust-toolchain@stable
+        with:
+          components: clippy
+      - uses: Swatinem/rust-cache@v2
+      - name: Test
+        run: cargo test --release --workspace
+      - name: Clippy
+        run: cargo clippy --release --workspace --all-targets -- -D warnings
+      - name: Rustdoc
+        env:
+          RUSTDOCFLAGS: -D warnings
+        run: cargo doc --release --workspace --no-deps