diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml new file mode 100644 index 00000000..10e23d42 --- /dev/null +++ b/.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 diff --git a/.gitignore b/.gitignore index f94ebc47..abe9b641 100644 --- a/.gitignore +++ b/.gitignore @@ -1,5 +1,6 @@ dist dist-* +result cabal-dev *.o *.hi diff --git a/cabal.project b/cabal.project deleted file mode 100644 index 812c95ba..00000000 --- a/cabal.project +++ /dev/null @@ -1,10 +0,0 @@ -packages: - copilot-bluespec/copilot-bluespec.cabal - copilot-c99/copilot-c99.cabal - copilot-core/copilot-core.cabal - copilot-interpreter/copilot-interpreter.cabal - copilot-language/copilot-language.cabal - copilot-libraries/copilot-libraries.cabal - copilot-prettyprinter/copilot-prettyprinter.cabal - copilot-theorem/copilot-theorem.cabal - copilot/copilot.cabal diff --git a/copilot-bluespec/README.md b/copilot-bluespec/README.md index e85d9e8c..b21f7612 100644 --- a/copilot-bluespec/README.md +++ b/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). diff --git a/copilot-bluespec/default.nix b/copilot-bluespec/default.nix new file mode 100644 index 00000000..e6edf53e --- /dev/null +++ b/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; +} diff --git a/copilot-bluespec/hie.yaml b/copilot-bluespec/hie.yaml new file mode 100644 index 00000000..20e14b24 --- /dev/null +++ b/copilot-bluespec/hie.yaml @@ -0,0 +1,10 @@ +cradle: + multi: + - path: "./src" + config: + cradle: + cabal: + - path: "./tests" + config: + cradle: + cabal: diff --git a/copilot-bluespec/shell.nix b/copilot-bluespec/shell.nix new file mode 100644 index 00000000..b30503d6 --- /dev/null +++ b/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; +} diff --git a/copilot-c99/default.nix b/copilot-c99/default.nix new file mode 100644 index 00000000..154b7057 --- /dev/null +++ b/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; +} diff --git a/copilot-core/default.nix b/copilot-core/default.nix new file mode 100644 index 00000000..b8ea8705 --- /dev/null +++ b/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; +} diff --git a/copilot-core/hie.yaml b/copilot-core/hie.yaml new file mode 100644 index 00000000..20e14b24 --- /dev/null +++ b/copilot-core/hie.yaml @@ -0,0 +1,10 @@ +cradle: + multi: + - path: "./src" + config: + cradle: + cabal: + - path: "./tests" + config: + cradle: + cabal: diff --git a/copilot-core/shell.nix b/copilot-core/shell.nix new file mode 100644 index 00000000..a46dae22 --- /dev/null +++ b/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 ]); +} diff --git a/copilot-interpreter/default.nix b/copilot-interpreter/default.nix new file mode 100644 index 00000000..0e1b300e --- /dev/null +++ b/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; +} diff --git a/copilot-interpreter/hie.yaml b/copilot-interpreter/hie.yaml new file mode 100644 index 00000000..20e14b24 --- /dev/null +++ b/copilot-interpreter/hie.yaml @@ -0,0 +1,10 @@ +cradle: + multi: + - path: "./src" + config: + cradle: + cabal: + - path: "./tests" + config: + cradle: + cabal: diff --git a/copilot-interpreter/shell.nix b/copilot-interpreter/shell.nix new file mode 100644 index 00000000..412ab618 --- /dev/null +++ b/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 ]); +} diff --git a/copilot-language/default.nix b/copilot-language/default.nix new file mode 100644 index 00000000..6524e8cb --- /dev/null +++ b/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; +} diff --git a/copilot-language/hie.yaml b/copilot-language/hie.yaml new file mode 100644 index 00000000..20e14b24 --- /dev/null +++ b/copilot-language/hie.yaml @@ -0,0 +1,10 @@ +cradle: + multi: + - path: "./src" + config: + cradle: + cabal: + - path: "./tests" + config: + cradle: + cabal: diff --git a/copilot-language/shell.nix b/copilot-language/shell.nix new file mode 100644 index 00000000..482083dc --- /dev/null +++ b/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 ]); +} diff --git a/copilot-libraries/default.nix b/copilot-libraries/default.nix new file mode 100644 index 00000000..33886020 --- /dev/null +++ b/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; +} diff --git a/copilot-libraries/hie.yaml b/copilot-libraries/hie.yaml new file mode 100644 index 00000000..20e14b24 --- /dev/null +++ b/copilot-libraries/hie.yaml @@ -0,0 +1,10 @@ +cradle: + multi: + - path: "./src" + config: + cradle: + cabal: + - path: "./tests" + config: + cradle: + cabal: diff --git a/copilot-libraries/shell.nix b/copilot-libraries/shell.nix new file mode 100644 index 00000000..1ce5439b --- /dev/null +++ b/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 ]); +} diff --git a/copilot-prettyprinter/default.nix b/copilot-prettyprinter/default.nix new file mode 100644 index 00000000..753ec1bf --- /dev/null +++ b/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; +} diff --git a/copilot-prettyprinter/hie.yaml b/copilot-prettyprinter/hie.yaml new file mode 100644 index 00000000..cea2181b --- /dev/null +++ b/copilot-prettyprinter/hie.yaml @@ -0,0 +1,6 @@ +cradle: + multi: + - path: "./src" + config: + cradle: + cabal: diff --git a/copilot-prettyprinter/shell.nix b/copilot-prettyprinter/shell.nix new file mode 100644 index 00000000..04487e86 --- /dev/null +++ b/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 ]); +} diff --git a/copilot-theorem/copilot-theorem.cabal b/copilot-theorem/copilot-theorem.cabal index b830f91a..30047cca 100644 --- a/copilot-theorem/copilot-theorem.cabal +++ b/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 diff --git a/copilot-theorem/default.nix b/copilot-theorem/default.nix new file mode 100644 index 00000000..493260e3 --- /dev/null +++ b/copilot-theorem/default.nix @@ -0,0 +1,35 @@ +{ 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; + what4 = bhp.what4_1_7; + }; + 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-theorem-base = importZ3 (hp.callCabal2nix "copilot-theorem" (np.lib.sourceByRegex ./. sourceRegexes) {}); + copilot-theorem-overlay = _n: _o: { copilot-theorem = copilot-theorem-base; }; + hp = bhp.override (o: { + overrides = + builtins.foldl' np.lib.composeExtensions (o.overrides or (_: _: {})) + [ depOverlay copilot-theorem-overlay ]; + }); + copilot-theorem = hp.copilot-theorem; +in { + inherit np; + inherit hp; + inherit copilot-theorem; +} diff --git a/copilot-theorem/hie.yaml b/copilot-theorem/hie.yaml new file mode 100644 index 00000000..20e14b24 --- /dev/null +++ b/copilot-theorem/hie.yaml @@ -0,0 +1,10 @@ +cradle: + multi: + - path: "./src" + config: + cradle: + cabal: + - path: "./tests" + config: + cradle: + cabal: diff --git a/copilot-theorem/shell.nix b/copilot-theorem/shell.nix new file mode 100644 index 00000000..6311168f --- /dev/null +++ b/copilot-theorem/shell.nix @@ -0,0 +1,8 @@ +{}: +let + inherit (import ./. {}) copilot-theorem hp np; +in +hp.shellFor { + packages = p: [ copilot-theorem ]; + nativeBuildInputs = (with np; [ cabal-install ghcid niv ]) ++ (with hp; [ haskell-language-server ]); +} diff --git a/copilot-verifier/copilot-verifier.cabal b/copilot-verifier/copilot-verifier.cabal index 9c6bed8d..ce149097 100644 --- a/copilot-verifier/copilot-verifier.cabal +++ b/copilot-verifier/copilot-verifier.cabal @@ -51,10 +51,10 @@ common bldflags crucible >= 0.7.1 && < 0.8, crucible-llvm >= 0.7 && < 0.8, crux >= 0.7.1 && < 0.8, - crux-llvm >= 0.9 && < 0.10, + crux-llvm >= 0.9 && < 0.11, filepath, lens, - llvm-pretty >= 0.12.1.0 && < 0.13, + llvm-pretty >= 0.12.1.0 && < 0.14, mtl, panic >= 0.3, parameterized-utils >= 2.1.4 && < 2.2, @@ -62,7 +62,7 @@ common bldflags text, transformers, vector, - what4 >= 1.6.1 && < 1.7 + what4 >= 1.6.1 && < 1.8 library import: bldflags diff --git a/copilot-verifier/default.nix b/copilot-verifier/default.nix new file mode 100644 index 00000000..5796d0da --- /dev/null +++ b/copilot-verifier/default.nix @@ -0,0 +1,49 @@ +{ sources ? import ../nix/sources.nix, ghc ? "ghc98" }: +let + depOverlay = n: o: { + copilot = (import ../copilot { inherit sources ghc; }).copilot; + copilot-core = (import ../copilot-core { inherit sources ghc; }).copilot-core; + copilot-c99 = (import ../copilot-c99 { inherit sources ghc; }).copilot-c99; + copilot-language = (import ../copilot-language { inherit sources ghc; }).copilot-language; + copilot-interpreter = (import ../copilot-interpreter { inherit sources ghc; }).copilot-interpreter; + copilot-libraries = (import ../copilot-libraries { inherit sources ghc; }).copilot-libraries; + copilot-prettyprinter = (import ../copilot-prettyprinter { inherit sources ghc; }).copilot-prettyprinter; + copilot-theorem = (import ../copilot-theorem { inherit sources ghc; }).copilot-theorem; + }; + np = import sources.nixpkgs {}; + bhp = np.haskell.packages.${ghc}; + + sourceRegexes = [ + "^src.*$" + "^exe.*$" + "^examples.*$" + "^test.*$" + "^.*\\.cabal$" + "^LICENSE$" + ]; + + # llvm and clang versions are coupled + externalDeps = [np.z3 np.clang_16 np.llvm_16]; + shellTuning = ''export CCC_OVERRIDE_OPTIONS=+-fno-wrapv + ''; + copilot-verifier-base = + (hp.callCabal2nix "copilot-verifier" (np.lib.sourceByRegex ./. sourceRegexes) {}).overrideAttrs + (oa: { + checkPhase = shellTuning + oa.checkPhase; + propagatedBuildInputs = (oa.propagatedBuildInputs or []) ++ externalDeps; + }); + + copilot-verifier-overlay = _n: _o: { copilot-verifier = copilot-verifier-base; }; + hp = bhp.override (o: { + overrides = + builtins.foldl' np.lib.composeExtensions (o.overrides or (_: _: {})) + [ depOverlay copilot-verifier-overlay ]; + }); + copilot-verifier = hp.copilot-verifier; +in { + inherit np; + inherit hp; + inherit externalDeps; + inherit shellTuning; + inherit copilot-verifier; +} diff --git a/copilot-verifier/hie.yaml b/copilot-verifier/hie.yaml new file mode 100644 index 00000000..a99a3847 --- /dev/null +++ b/copilot-verifier/hie.yaml @@ -0,0 +1,10 @@ +cradle: + multi: + - path: "./src" + config: + cradle: + cabal: + - path: "./test" + config: + cradle: + cabal: diff --git a/copilot-verifier/shell.nix b/copilot-verifier/shell.nix new file mode 100644 index 00000000..07c1e335 --- /dev/null +++ b/copilot-verifier/shell.nix @@ -0,0 +1,12 @@ +{}: +let + inherit (import ./. {}) copilot-verifier hp np externalDeps shellTuning; +in +hp.shellFor { + packages = p: [ copilot-verifier ]; + nativeBuildInputs = + (with np; [ cabal-install ghcid niv]) ++ + (with hp; [ haskell-language-server ]) ++ + externalDeps; + shellHook = shellTuning; +} diff --git a/copilot-visualizer/default.nix b/copilot-visualizer/default.nix new file mode 100644 index 00000000..7db132ae --- /dev/null +++ b/copilot-visualizer/default.nix @@ -0,0 +1,33 @@ +{ 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-core = (import ../copilot-core { inherit sources ghc; }).copilot-core; + copilot = (import ../copilot { inherit sources ghc; }).copilot; + copilot-prettyprinter = (import ../copilot-prettyprinter { inherit sources ghc; }).copilot-prettyprinter; + }; + np = import sources.nixpkgs {}; + bhp = np.haskell.packages.${ghc}; + + sourceRegexes = [ + "^src.*$" + "^data.*$" + "^examples.*$" + "^.*\\.cabal$" + "^LICENSE$" + ]; + + copilot-visualizer-base = hp.callCabal2nix "copilot-visualizer" (np.lib.sourceByRegex ./. sourceRegexes) {}; + copilot-visualizer-overlay = _n: _o: { copilot-visualizer = copilot-visualizer-base; }; + hp = bhp.override (o: { + overrides = + builtins.foldl' np.lib.composeExtensions (o.overrides or (_: _: {})) + [ depOverlay copilot-visualizer-overlay ]; + }); + copilot-visualizer = hp.copilot-visualizer; +in { + inherit np; + inherit hp; + inherit copilot-visualizer; +} diff --git a/copilot-visualizer/hie.yaml b/copilot-visualizer/hie.yaml new file mode 100644 index 00000000..cea2181b --- /dev/null +++ b/copilot-visualizer/hie.yaml @@ -0,0 +1,6 @@ +cradle: + multi: + - path: "./src" + config: + cradle: + cabal: diff --git a/copilot-visualizer/shell.nix b/copilot-visualizer/shell.nix new file mode 100644 index 00000000..d6d41df5 --- /dev/null +++ b/copilot-visualizer/shell.nix @@ -0,0 +1,8 @@ +{}: +let + inherit (import ./. {}) copilot-visualizer hp np; +in +hp.shellFor { + packages = p: [ copilot-visualizer ]; + nativeBuildInputs = (with np; [ cabal-install ghcid niv ]) ++ (with hp; [ haskell-language-server ]); +} diff --git a/copilot/default.nix b/copilot/default.nix new file mode 100644 index 00000000..6be9ccc0 --- /dev/null +++ b/copilot/default.nix @@ -0,0 +1,38 @@ +{ sources ? import ../nix/sources.nix, ghc ? "ghc98" }: +let + depOverlay = n: o: { + copilot-core = (import ../copilot-core { inherit sources ghc; }).copilot-core; + copilot-c99 = (import ../copilot-c99 { inherit sources ghc; }).copilot-c99; + copilot-language = (import ../copilot-language { inherit sources ghc; }).copilot-language; + copilot-libraries = (import ../copilot-libraries { inherit sources ghc; }).copilot-libraries; + copilot-prettyprinter = (import ../copilot-prettyprinter { inherit sources ghc; }).copilot-prettyprinter; + copilot-theorem = (import ../copilot-theorem { inherit sources ghc; }).copilot-theorem; + }; + np = import sources.nixpkgs {}; + bhp = np.haskell.packages.${ghc}; + + sourceRegexes = [ + "^src.*$" + "^examples.*$" + "^runtest$" + "^.*\\.cabal$" + "^LICENSE$" + ]; + + withExamples = drv: drv.overrideAttrs(oa: + { configureFlags = oa.configureFlags ++ [ "-f examples" ]; }); + + copilot-base = withExamples (hp.callCabal2nix "copilot" (np.lib.sourceByRegex ./. sourceRegexes) {}); + + copilot-overlay = _n: _o: { copilot = copilot-base; }; + hp = bhp.override (o: { + overrides = + builtins.foldl' np.lib.composeExtensions (o.overrides or (_: _: {})) + [ depOverlay copilot-overlay ]; + }); + copilot = hp.copilot; +in { + inherit np; + inherit hp; + inherit copilot; +} diff --git a/nix/sources.json b/nix/sources.json new file mode 100644 index 00000000..9d76be05 --- /dev/null +++ b/nix/sources.json @@ -0,0 +1,12 @@ +{ + "nixpkgs": { + "branch": "master", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "da5af46a09eeb2b1c8f4193d626727d5b7460601", + "sha256": "sha256:1hmj9mg81gy8c7v8j563793sckawyxnca60zlif7qpsri597hlhh", + "type": "tarball", + "url": "https://github.com/NixOS/nixpkgs/archive/da5af46a09eeb2b1c8f4193d626727d5b7460601.tar.gz", + "url_template": "https://github.com///archive/.tar.gz" + } +} diff --git a/nix/sources.nix b/nix/sources.nix new file mode 100644 index 00000000..fe3dadf7 --- /dev/null +++ b/nix/sources.nix @@ -0,0 +1,198 @@ +# This file has been generated by Niv. + +let + + # + # The fetchers. fetch_ fetches specs of type . + # + + fetch_file = pkgs: name: spec: + let + name' = sanitizeName name + "-src"; + in + if spec.builtin or true then + builtins_fetchurl { inherit (spec) url sha256; name = name'; } + else + pkgs.fetchurl { inherit (spec) url sha256; name = name'; }; + + fetch_tarball = pkgs: name: spec: + let + name' = sanitizeName name + "-src"; + in + if spec.builtin or true then + builtins_fetchTarball { name = name'; inherit (spec) url sha256; } + else + pkgs.fetchzip { name = name'; inherit (spec) url sha256; }; + + fetch_git = name: spec: + let + ref = + spec.ref or ( + if spec ? branch then "refs/heads/${spec.branch}" else + if spec ? tag then "refs/tags/${spec.tag}" else + abort "In git source '${name}': Please specify `ref`, `tag` or `branch`!" + ); + submodules = spec.submodules or false; + submoduleArg = + let + nixSupportsSubmodules = builtins.compareVersions builtins.nixVersion "2.4" >= 0; + emptyArgWithWarning = + if submodules + then + builtins.trace + ( + "The niv input \"${name}\" uses submodules " + + "but your nix's (${builtins.nixVersion}) builtins.fetchGit " + + "does not support them" + ) + { } + else { }; + in + if nixSupportsSubmodules + then { inherit submodules; } + else emptyArgWithWarning; + in + builtins.fetchGit + ({ url = spec.repo; inherit (spec) rev; inherit ref; } // submoduleArg); + + fetch_local = spec: spec.path; + + fetch_builtin-tarball = name: throw + ''[${name}] The niv type "builtin-tarball" is deprecated. You should instead use `builtin = true`. + $ niv modify ${name} -a type=tarball -a builtin=true''; + + fetch_builtin-url = name: throw + ''[${name}] The niv type "builtin-url" will soon be deprecated. You should instead use `builtin = true`. + $ niv modify ${name} -a type=file -a builtin=true''; + + # + # Various helpers + # + + # https://github.com/NixOS/nixpkgs/pull/83241/files#diff-c6f540a4f3bfa4b0e8b6bafd4cd54e8bR695 + sanitizeName = name: + ( + concatMapStrings (s: if builtins.isList s then "-" else s) + ( + builtins.split "[^[:alnum:]+._?=-]+" + ((x: builtins.elemAt (builtins.match "\\.*(.*)" x) 0) name) + ) + ); + + # The set of packages used when specs are fetched using non-builtins. + mkPkgs = sources: system: + let + sourcesNixpkgs = + import (builtins_fetchTarball { inherit (sources.nixpkgs) url sha256; }) { inherit system; }; + hasNixpkgsPath = builtins.any (x: x.prefix == "nixpkgs") builtins.nixPath; + hasThisAsNixpkgsPath = == ./.; + in + if builtins.hasAttr "nixpkgs" sources + then sourcesNixpkgs + else if hasNixpkgsPath && ! hasThisAsNixpkgsPath then + import { } + else + abort + '' + Please specify either (through -I or NIX_PATH=nixpkgs=...) or + add a package called "nixpkgs" to your sources.json. + ''; + + # The actual fetching function. + fetch = pkgs: name: spec: + + if ! builtins.hasAttr "type" spec then + abort "ERROR: niv spec ${name} does not have a 'type' attribute" + else if spec.type == "file" then fetch_file pkgs name spec + else if spec.type == "tarball" then fetch_tarball pkgs name spec + else if spec.type == "git" then fetch_git name spec + else if spec.type == "local" then fetch_local spec + else if spec.type == "builtin-tarball" then fetch_builtin-tarball name + else if spec.type == "builtin-url" then fetch_builtin-url name + else + abort "ERROR: niv spec ${name} has unknown type ${builtins.toJSON spec.type}"; + + # If the environment variable NIV_OVERRIDE_${name} is set, then use + # the path directly as opposed to the fetched source. + replace = name: drv: + let + saneName = stringAsChars (c: if (builtins.match "[a-zA-Z0-9]" c) == null then "_" else c) name; + ersatz = builtins.getEnv "NIV_OVERRIDE_${saneName}"; + in + if ersatz == "" then drv else + # this turns the string into an actual Nix path (for both absolute and + # relative paths) + if builtins.substring 0 1 ersatz == "/" then /. + ersatz else /. + builtins.getEnv "PWD" + "/${ersatz}"; + + # Ports of functions for older nix versions + + # a Nix version of mapAttrs if the built-in doesn't exist + mapAttrs = builtins.mapAttrs or ( + f: set: with builtins; + listToAttrs (map (attr: { name = attr; value = f attr set.${attr}; }) (attrNames set)) + ); + + # https://github.com/NixOS/nixpkgs/blob/0258808f5744ca980b9a1f24fe0b1e6f0fecee9c/lib/lists.nix#L295 + range = first: last: if first > last then [ ] else builtins.genList (n: first + n) (last - first + 1); + + # https://github.com/NixOS/nixpkgs/blob/0258808f5744ca980b9a1f24fe0b1e6f0fecee9c/lib/strings.nix#L257 + stringToCharacters = s: map (p: builtins.substring p 1 s) (range 0 (builtins.stringLength s - 1)); + + # https://github.com/NixOS/nixpkgs/blob/0258808f5744ca980b9a1f24fe0b1e6f0fecee9c/lib/strings.nix#L269 + stringAsChars = f: s: concatStrings (map f (stringToCharacters s)); + concatMapStrings = f: list: concatStrings (map f list); + concatStrings = builtins.concatStringsSep ""; + + # https://github.com/NixOS/nixpkgs/blob/8a9f58a375c401b96da862d969f66429def1d118/lib/attrsets.nix#L331 + optionalAttrs = cond: as: if cond then as else { }; + + # fetchTarball version that is compatible between all the versions of Nix + builtins_fetchTarball = { url, name ? null, sha256 }@attrs: + let + inherit (builtins) lessThan nixVersion fetchTarball; + in + if lessThan nixVersion "1.12" then + fetchTarball ({ inherit url; } // (optionalAttrs (name != null) { inherit name; })) + else + fetchTarball attrs; + + # fetchurl version that is compatible between all the versions of Nix + builtins_fetchurl = { url, name ? null, sha256 }@attrs: + let + inherit (builtins) lessThan nixVersion fetchurl; + in + if lessThan nixVersion "1.12" then + fetchurl ({ inherit url; } // (optionalAttrs (name != null) { inherit name; })) + else + fetchurl attrs; + + # Create the final "sources" from the config + mkSources = config: + mapAttrs + ( + name: spec: + if builtins.hasAttr "outPath" spec + then + abort + "The values in sources.json should not have an 'outPath' attribute" + else + spec // { outPath = replace name (fetch config.pkgs name spec); } + ) + config.sources; + + # The "config" used by the fetchers + mkConfig = + { sourcesFile ? if builtins.pathExists ./sources.json then ./sources.json else null + , sources ? if sourcesFile == null then { } else builtins.fromJSON (builtins.readFile sourcesFile) + , system ? builtins.currentSystem + , pkgs ? mkPkgs sources system + }: rec { + # The sources, i.e. the attribute set of spec name to spec + inherit sources; + + # The "pkgs" (evaluated nixpkgs) to use for e.g. non-builtin fetchers + inherit pkgs; + }; + +in +mkSources (mkConfig { }) // { __functor = _: settings: mkSources (mkConfig settings); }