Draft: nix

.github/workflows/test.yml

@@ -0,0 +1,16 @@
+name: "nix-build with tests"
+on:
+  pull_request:
+  push:
+jobs:
+  tests:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v4.2.2
+    - uses: cachix/install-nix-action@v31
+      with:
+        nix_path: nixpkgs=channel:nixos-unstable
+    - run:
+        nix-build copilot-bluespec
+    - run:
+        nix-build copilot-verifier

.gitignore

@@ -1,5 +1,6 @@
 dist
 dist-*
+result
 cabal-dev
 *.o
 *.hi

copilot-bluespec/README.md

@@ -25,6 +25,8 @@ $ cabal install copilot
 $ cabal install copilot-bluespec
 ```
 
+Test execution time is about 5 minutes.
+
 For more detailed instructions on how to install Copilot, please refer to the
 [Copilot website](https://copilot-language.github.io).
 

copilot-bluespec/default.nix

@@ -0,0 +1,34 @@
+{ sources ? import ../nix/sources.nix, ghc ? "ghc98" }:
+let
+  depOverlay = n: o: {
+    copilot-core = (import ../copilot-core { inherit sources ghc; }).copilot-core;
+  };
+  np = import sources.nixpkgs {};
+  bhp = np.haskell.packages.${ghc};
+
+  sourceRegexes = [
+    "^src.*$"
+    "^tests.*$"
+    "^.*\\.cabal$"
+    "^LICENSE$"
+  ];
+
+  externalDeps = [ np.bluespec np.removeReferencesTo ];
+  copilot-bluespec-base =
+    (hp.callCabal2nix "copilot-bluespec" (np.lib.sourceByRegex ./. sourceRegexes) {}
+    ).overrideAttrs(oa: {
+      propagatedBuildInputs = (oa.propagatedBuildInputs or []) ++ externalDeps;
+    });
+  copilot-bluespec-overlay = _n: _o: { copilot-bluespec = copilot-bluespec-base; };
+  hp = bhp.override (o: {
+    overrides =
+      builtins.foldl' np.lib.composeExtensions (o.overrides or (_: _: {}))
+        [ depOverlay copilot-bluespec-overlay ];
+  });
+  copilot-bluespec = hp.copilot-bluespec;
+in {
+  inherit np;
+  inherit hp;
+  inherit externalDeps;
+  inherit copilot-bluespec;
+}

copilot-bluespec/hie.yaml

@@ -0,0 +1,10 @@
+cradle:
+  multi:
+    - path: "./src"
+      config:
+        cradle:
+          cabal:
+    - path: "./tests"
+      config:
+        cradle:
+          cabal:

copilot-bluespec/shell.nix

@@ -0,0 +1,8 @@
+{}:
+let
+  inherit (import ./. {}) copilot-bluespec hp np externalDeps;
+in
+hp.shellFor {
+  packages = p: [ copilot-bluespec ];
+  nativeBuildInputs = (with np; [ cabal-install ghcid niv ]) ++ (with hp; [ haskell-language-server ]) ++ externalDeps;
+}

copilot-c99/default.nix

@@ -0,0 +1,28 @@
+{ sources ? import ../nix/sources.nix, ghc ? "ghc98" }:
+let
+  depOverlay = n: o: {
+    copilot-core = (import ../copilot-core { inherit sources ghc; }).copilot-core;
+  };
+  np = import sources.nixpkgs {};
+  bhp = np.haskell.packages.${ghc};
+
+  sourceRegexes = [
+    "^src.*$"
+    "^tests.*$"
+    "^.*\\.cabal$"
+    "^LICENSE$"
+  ];
+
+  copilot-c99-base = hp.callCabal2nix "copilot-c99" (np.lib.sourceByRegex ./. sourceRegexes) {};
+  copilot-c99-overlay = _n: _o: { copilot-c99 = copilot-c99-base; };
+  hp = bhp.override (o: {
+    overrides =
+      builtins.foldl' np.lib.composeExtensions (o.overrides or (_: _: {}))
+        [ depOverlay copilot-c99-overlay ];
+  });
+  copilot-c99 = hp.copilot-c99;
+in {
+  inherit np;
+  inherit hp;
+  inherit copilot-c99;
+}

copilot-core/default.nix

@@ -0,0 +1,18 @@
+{ sources ? import ../nix/sources.nix, ghc ? "ghc98" }:
+let
+  np = import sources.nixpkgs {};
+  hp = np.haskell.packages.${ghc};
+
+  sourceRegexes = [
+    "^src.*$"
+    "^tests.*$"
+    "^.*\\.cabal$"
+    "^LICENSE$"
+  ];
+
+  copilot-core = hp.callCabal2nix "copilot-core" (np.lib.sourceByRegex ./. sourceRegexes) {};
+in {
+  inherit np;
+  inherit hp;
+  inherit copilot-core;
+}

copilot-core/hie.yaml

@@ -0,0 +1,10 @@
+cradle:
+  multi:
+    - path: "./src"
+      config:
+        cradle:
+          cabal:
+    - path: "./tests"
+      config:
+        cradle:
+          cabal:

copilot-core/shell.nix

@@ -0,0 +1,8 @@
+{}:
+let
+  inherit (import ./. {}) copilot-core hp np;
+in
+hp.shellFor {
+  packages = p: [ copilot-core ];
+  nativeBuildInputs = (with np; [ cabal-install ghcid niv ]) ++ (with hp; [ haskell-language-server ]);
+}

copilot-interpreter/default.nix

@@ -0,0 +1,29 @@
+{ sources ? import ../nix/sources.nix, ghc ? "ghc98" }:
+let
+  depOverlay = n: o: {
+    copilot-core = (import ../copilot-core { inherit sources ghc; }).copilot-core;
+    copilot-prettyprinter = (import ../copilot-prettyprinter { inherit sources ghc; }).copilot-prettyprinter;
+  };
+  np = import sources.nixpkgs {};
+  bhp = np.haskell.packages.${ghc};
+
+  sourceRegexes = [
+    "^src.*$"
+    "^tests.*$"
+    "^.*\\.cabal$"
+    "^LICENSE$"
+  ];
+
+  copilot-interpreter-base = hp.callCabal2nix "copilot-interpreter" (np.lib.sourceByRegex ./. sourceRegexes) {};
+  copilot-interpreter-overlay = _n: _o: { copilot-interpreter = copilot-interpreter-base; };
+  hp = bhp.override (o: {
+    overrides =
+      builtins.foldl' np.lib.composeExtensions (o.overrides or (_: _: {}))
+        [ depOverlay copilot-interpreter-overlay ];
+  });
+  copilot-interpreter = hp.copilot-interpreter;
+in {
+  inherit np;
+  inherit hp;
+  inherit copilot-interpreter;
+}

copilot-interpreter/hie.yaml

@@ -0,0 +1,10 @@
+cradle:
+  multi:
+    - path: "./src"
+      config:
+        cradle:
+          cabal:
+    - path: "./tests"
+      config:
+        cradle:
+          cabal:

copilot-interpreter/shell.nix

@@ -0,0 +1,8 @@
+{}:
+let
+  inherit (import ./. {}) copilot-interpreter hp np;
+in
+hp.shellFor {
+  packages = p: [ copilot-interpreter ];
+  nativeBuildInputs = (with np; [ cabal-install ghcid niv ]) ++ (with hp; [ haskell-language-server ]);
+}

copilot-language/default.nix

@@ -0,0 +1,31 @@
+{ sources ? import ../nix/sources.nix, ghc ? "ghc98" }:
+let
+  depOverlay = n: o: {
+    copilot-core = (import ../copilot-core { inherit sources ghc; }).copilot-core;
+    copilot-interpreter = (import ../copilot-interpreter { inherit sources ghc; }).copilot-interpreter;
+    copilot-theorem = (import ../copilot-theorem { inherit sources ghc; }).copilot-theorem;
+    copilot-prettyprinter = (import ../copilot-prettyprinter { inherit sources ghc; }).copilot-prettyprinter;
+  };
+  np = import sources.nixpkgs {};
+  bhp = np.haskell.packages.${ghc};
+
+  sourceRegexes = [
+    "^src.*$"
+    "^tests.*$"
+    "^.*\\.cabal$"
+    "^LICENSE$"
+  ];
+
+  copilot-language-base = hp.callCabal2nix "copilot-language" (np.lib.sourceByRegex ./. sourceRegexes) {};
+  copilot-language-overlay = _n: _o: { copilot-language = copilot-language-base; };
+  hp = bhp.override (o: {
+    overrides =
+      builtins.foldl' np.lib.composeExtensions (o.overrides or (_: _: {}))
+        [ depOverlay copilot-language-overlay ];
+  });
+  copilot-language = hp.copilot-language;
+in {
+  inherit np;
+  inherit hp;
+  inherit copilot-language;
+}

copilot-language/hie.yaml

@@ -0,0 +1,10 @@
+cradle:
+  multi:
+    - path: "./src"
+      config:
+        cradle:
+          cabal:
+    - path: "./tests"
+      config:
+        cradle:
+          cabal:

copilot-language/shell.nix

@@ -0,0 +1,8 @@
+{}:
+let
+  inherit (import ./. {}) copilot-language hp np;
+in
+hp.shellFor {
+  packages = p: [ copilot-language ];
+  nativeBuildInputs = (with np; [ cabal-install ghcid niv ]) ++ (with hp; [ haskell-language-server ]);
+}

copilot-libraries/default.nix

@@ -0,0 +1,37 @@
+{ sources ? import ../nix/sources.nix, ghc ? "ghc98" }:
+let
+  depOverlay = n: o: {
+    copilot-language = (import ../copilot-language { inherit sources ghc; }).copilot-language;
+    copilot-interpreter = (import ../copilot-interpreter { inherit sources ghc; }).copilot-interpreter;
+    copilot-theorem = (import ../copilot-theorem { inherit sources ghc; }).copilot-theorem;
+  };
+  np = import sources.nixpkgs {};
+  bhp = np.haskell.packages.${ghc};
+
+  sourceRegexes = [
+    "^src.*$"
+    "^tests.*$"
+    "^.*\\.cabal$"
+    "^LICENSE$"
+  ];
+
+  importZ3 = drv:
+    drv.overrideAttrs (oa: {
+      propagatedBuildInputs = (oa.propagatedBuildInputs or []) ++ [np.z3];
+    });
+
+  copilot-libraries-base =
+    importZ3 (hp.callCabal2nix "copilot-libraries" (np.lib.sourceByRegex ./. sourceRegexes) {});
+
+  copilot-libraries-overlay = _n: _o: { copilot-libraries = copilot-libraries-base; };
+  hp = bhp.override (o: {
+    overrides =
+      builtins.foldl' np.lib.composeExtensions (o.overrides or (_: _: {}))
+        [ depOverlay copilot-libraries-overlay ];
+  });
+  copilot-libraries = hp.copilot-libraries;
+in {
+  inherit np;
+  inherit hp;
+  inherit copilot-libraries;
+}

copilot-libraries/hie.yaml

@@ -0,0 +1,10 @@
+cradle:
+  multi:
+    - path: "./src"
+      config:
+        cradle:
+          cabal:
+    - path: "./tests"
+      config:
+        cradle:
+          cabal:

copilot-libraries/shell.nix

@@ -0,0 +1,8 @@
+{}:
+let
+  inherit (import ./. {}) copilot-libraries hp np;
+in
+hp.shellFor {
+  packages = p: [ copilot-libraries ];
+  nativeBuildInputs = (with np; [ cabal-install ghcid niv ]) ++ (with hp; [ haskell-language-server ]);
+}

copilot-prettyprinter/default.nix

@@ -0,0 +1,28 @@
+{ sources ? import ../nix/sources.nix, ghc ? "ghc98" }:
+let
+  depOverlay = n: o: {
+    copilot-core = (import ../copilot-core { inherit sources ghc; }).copilot-core;
+  };
+  np = import sources.nixpkgs {};
+  bhp = np.haskell.packages.${ghc};
+
+  sourceRegexes = [
+    "^src.*$"
+    "^tests.*$"
+    "^.*\\.cabal$"
+    "^LICENSE$"
+  ];
+
+  copilot-prettyprinter-base = hp.callCabal2nix "copilot-prettyprinter" (np.lib.sourceByRegex ./. sourceRegexes) {};
+  copilot-prettyprinter-overlay = _n: _o: { copilot-prettyprinter = copilot-prettyprinter-base; };
+  hp = bhp.override (o: {
+    overrides =
+      builtins.foldl' np.lib.composeExtensions (o.overrides or (_: _: {}))
+        [ depOverlay copilot-prettyprinter-overlay ];
+  });
+  copilot-prettyprinter = hp.copilot-prettyprinter;
+in {
+  inherit np;
+  inherit hp;
+  inherit copilot-prettyprinter;
+}

copilot-prettyprinter/hie.yaml

@@ -0,0 +1,6 @@
+cradle:
+  multi:
+    - path: "./src"
+      config:
+        cradle:
+          cabal:

copilot-prettyprinter/shell.nix

@@ -0,0 +1,8 @@
+{}:
+let
+  inherit (import ./. {}) copilot-prettyprinter hp np;
+in
+hp.shellFor {
+  packages = p: [ copilot-prettyprinter ];
+  nativeBuildInputs = (with np; [ cabal-install ghcid niv ]) ++ (with hp; [ haskell-language-server ]);
+}

copilot-theorem/copilot-theorem.cabal

@@ -60,7 +60,7 @@ library
                           , random                >= 1.1 && < 1.3
                           , transformers          >= 0.5 && < 0.7
                           , xml                   >= 1.3 && < 1.4
-                          , what4                 >= 1.3 && < 1.8
+                          , what4                 >= 1.7 && < 1.8
 
                           , copilot-core          >= 4.6 && < 4.7
                           , copilot-prettyprinter >= 4.6 && < 4.7