Do more during CI run

Author: jkopanski

.github/workflows/cheshire.yml

@@ -0,0 +1,40 @@
+name: "Cheshire CI"
+on:
+  push:
+    branches:
+      - main
+
+jobs:
+  dev-shell:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v4
+    - uses: cachix/install-nix-action@v24
+    - uses: cachix/cachix-action@v15
+      with:
+        name: famisoft
+        authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
+    - run: nix develop --profile dev-shell -c true
+
+  checks:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v4
+    - uses: cachix/install-nix-action@v24
+    - uses: cachix/cachix-action@v15
+      with:
+        name: famisoft
+        skipPush: true
+    - run: nix flake check
+
+  typecheck:
+    runs-on: ubuntu-latest
+    needs: dev-shell
+    steps:
+    - uses: actions/checkout@v4
+    - uses: cachix/install-nix-action@v24
+    - uses: cachix/cachix-action@v15
+      with:
+        name: famisoft
+        skipPush: true
+    - run: nix build -L

.github/workflows/dev-shell.yml

@@ -15,11 +15,11 @@
   };
 
   outputs = inputs@{ self, nixpkgs, utils, ... }:
-    utils.lib.eachDefaultSystem (system:
+    (utils.lib.eachDefaultSystem (system:
       let
         pkgs = import nixpkgs {
           inherit system;
-          overlays = [ self.overlays.${system}.default ];
+          overlays = [ self.overlays.default ];
         };
         agdaWithLibraries = pkgs.agda.withPackages (p: [
           p.standard-library
@@ -37,43 +37,6 @@
           installPhase = ''mkdir "$out"'';
         };
 
-        overlays = rec {
-          agda = final: prev: {
-            haskellPackages = prev.haskellPackages.override {
-              overrides = hfinal: hprev:
-                let inherit (final.haskell.lib.compose)
-                  addBuildDepends enableCabalFlag overrideSrc;
-                in {
-                  Agda = final.lib.pipe hprev.Agda [
-                    (overrideSrc {
-                      src = inputs.agda;
-                      version = "2.7.0.1";
-                    })
-                    (addBuildDepends (with hfinal; [pqueue text-icu]))
-                    (enableCabalFlag "enable-cluster-counting")
-                  ];
-                };
-            };
-          };
-
-          standard-library = final: prev: {
-            agdaPackages = prev.agdaPackages.overrideScope (
-              finalAgda: prevAgda: {
-                standard-library = prevAgda.standard-library.overrideAttrs {
-                  version = "2.1";
-                  src = inputs.std-lib;
-                };
-              }
-            );
-          };
-
-          # pkgs.lib.composeExtensions, but how to get it without infinte recursion?
-          default = final: prev:
-            let agda' = agda final prev;
-                prev' = prev // agda';
-            in agda' // standard-library final prev';
-        };
-
         devShells.default = pkgs.mkShell {
           buildInputs = [
             agdaWithLibraries
@@ -98,5 +61,42 @@
           };
         };
       }
-    );
+    )) // {
+      overlays = rec {
+        agda = final: prev: {
+          haskellPackages = prev.haskellPackages.override {
+            overrides = hfinal: hprev:
+              let inherit (final.haskell.lib.compose)
+                addBuildDepends enableCabalFlag overrideSrc;
+              in {
+                Agda = final.lib.pipe hprev.Agda [
+                  (overrideSrc {
+                    src = inputs.agda;
+                    version = "2.7.0.1";
+                  })
+                  (addBuildDepends (with hfinal; [pqueue text-icu]))
+                  (enableCabalFlag "enable-cluster-counting")
+                ];
+              };
+          };
+        };
+
+        standard-library = final: prev: {
+          agdaPackages = prev.agdaPackages.overrideScope (
+            finalAgda: prevAgda: {
+              standard-library = prevAgda.standard-library.overrideAttrs {
+                version = "2.1";
+                src = inputs.std-lib;
+              };
+            }
+          );
+        };
+
+        # pkgs.lib.composeExtensions, but how to get it without infinte recursion?
+        default = final: prev:
+          let agda' = agda final prev;
+              prev' = prev // agda';
+          in agda' // standard-library final prev';
+      };
+    };
 }

flake.nix

@@ -361,7 +361,7 @@ module Cancellers {h : X ⇒ Y} {i : Y ⇒ X} (inv : h ∘ i ≈ id) where
     ∀ {f : Y ⇒ Z} {g : W ⇒ Y} →
     f ∘ g ≈ (f ∘ h) ∘ (i ∘ g)
   insertInner = ⟺ cancelInner
-  
+
 open Cancellers public
 
 -- operate in the 'center' instead (like pull/push)