Fix CI

.github/workflows/ci.yml

@@ -2,19 +2,20 @@ name: CI
 
 on:
   push:
-    branches: [master]
+    branches: [dev]
   pull_request:
   workflow_dispatch:
 
-# A newer push to the same branch supersedes an in-flight run; master runs are
-# never cancelled, since those are the ones that populate the build cache.
+permissions:
+  contents: read
+
 concurrency:
-  group: ${{ github.workflow }}-${{ github.ref }}
-  cancel-in-progress: ${{ github.ref != 'refs/heads/master' }}
+  group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }}
+  cancel-in-progress: true
 
 jobs:
   build:
-    name: Build and self-check
+    name: Build and test
     runs-on: ubuntu-latest
     timeout-minutes: 60
     steps:
@@ -35,6 +36,15 @@ jobs:
       - name: Build Lean4Lean.Experimental
         run: lake build Lean4Lean.Experimental
 
+      # Enforce the trusted sorry frontier: fail if any `Theory`/`Verify`
+      # declaration gains, loses, or renames a `sorry` versus the allowlist in
+      # `Lean4Lean/Audit/SorryFrontier.lean`. Asks the compiled environment which
+      # declarations use `sorryAx`, so it can't drift over comments or string
+      # literals the way a source grep can. Not a default target, so it is built
+      # explicitly here; the surface it imports is already built above.
+      - name: Check sorry frontier
+        run: lake build Lean4Lean.Audit.SorryFrontier
+
       # `lake build` only establishes that lean4lean compiles; these check that it still
       # *works*. The two modes exercise different code paths, so both are worth running.
 

.github/workflows/nix.yml

@@ -2,7 +2,7 @@ name: Nix
 
 on:
   push:
-    branches: [master]
+    branches: [dev]
   pull_request:
   workflow_dispatch:
 
@@ -14,50 +14,43 @@ concurrency:
   cancel-in-progress: true
 
 jobs:
-  # Cheap gates first: formatting and whole-flake evaluation for every
-  # declared system, without building anything.
-  eval:
-    runs-on: ubuntu-latest
+  # Packaging-compatibility gate: build the shipped outputs and every flake
+  # check on x86_64-linux (the only supported system). ci.yml is the primary
+  # lean-action build and test. The other systems in flake.nix stay declared
+  # but are not built here, so they never gate CI.
+  nix-test:
+    name: Nix Tests
+    runs-on: warp-ubuntu-latest-x64-8x
     steps:
       - uses: actions/checkout@v7
-      - name: Sorry frontier
-        run: perl .github/scripts/check_sorry_frontier.pl
-      - uses: DeterminateSystems/nix-installer-action@v20
-      - name: Check formatting
-        run: nix fmt --accept-flake-config -- --check flake.nix
-      - name: Evaluate all systems
-        run: nix flake check --all-systems --no-build --accept-flake-config
-
-  # Build the shipped outputs and run every check (proofs, the
-  # downstream-consumer fixture, and the CLI smoke/no-arg regression
-  # tests) on Linux.
-  check-linux:
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v7
-      - uses: DeterminateSystems/nix-installer-action@v20
-      - uses: cachix/cachix-action@v16
+      - uses: cachix/install-nix-action@v31
+        with:
+          nix_path: nixpkgs=channel:nixos-unstable
+          github_access_token: ${{ secrets.GITHUB_TOKEN }}
+      - uses: cachix/cachix-action@v17
         with:
           name: argumentcomputer
           authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
-          # Only push from trusted master builds; PRs stay read-only.
-          skipPush: ${{ github.ref != 'refs/heads/master' }}
-      - name: Build packages
-        run: nix build --accept-flake-config --no-link --print-build-logs .#lake-dependency .#lake-dependency-full .#lean4lean
-      - name: Flake checks
-        run: nix flake check --accept-flake-config --print-build-logs
+      - name: Check formatting
+        run: nix fmt --accept-flake-config -- --check flake.nix
+      # Shipped outputs: the CLI and the downstream Lake-dependency artifact.
+      - run: nix build --print-build-logs --accept-flake-config .#lean4lean .#lake-dependency
+      # Builds every check (proofs + sorry frontier, tests, consumer fixture,
+      # CLI regressions) and evaluates the rest of the flake.
+      - run: nix flake check --print-build-logs --accept-flake-config
 
-  # One Darwin runner exercising the wrapper and the consumer fixture,
-  # per the improvement plan; the full check matrix stays on Linux.
-  build-darwin:
-    runs-on: macos-latest
+  # Verify the dev shell provides a working Lake toolchain.
+  nix-devshell:
+    name: Nix devShell
+    runs-on: warp-ubuntu-latest-x64-8x
     steps:
       - uses: actions/checkout@v7
-      - uses: DeterminateSystems/nix-installer-action@v20
-      - uses: cachix/cachix-action@v16
+      - uses: cachix/install-nix-action@v31
+        with:
+          nix_path: nixpkgs=channel:nixos-unstable
+          github_access_token: ${{ secrets.GITHUB_TOKEN }}
+      - uses: cachix/cachix-action@v17
         with:
           name: argumentcomputer
           authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
-          skipPush: ${{ github.ref != 'refs/heads/master' }}
-      - name: Build wrapper and consumer check
-        run: nix build --accept-flake-config --no-link --print-build-logs .#lean4lean .#checks.aarch64-darwin.downstream-consumer .#checks.aarch64-darwin.cli-smoke
+      - run: nix develop --accept-flake-config --command bash -c "lake build"