diff --git a/flake.nix b/flake.nix index 3780f466..5d960cc0 100644 --- a/flake.nix +++ b/flake.nix @@ -1,57 +1,31 @@ { description = "Agda2hs"; - inputs.nixpkgs.url = github:NixOS/nixpkgs; - inputs.flake-utils.url = github:numtide/flake-utils; + inputs.nixpkgs.url = "github:NixOS/nixpkgs"; + inputs.flake-utils.url = "github:numtide/flake-utils"; - outputs = {self, nixpkgs, flake-utils}: - flake-utils.lib.eachDefaultSystem (system: + outputs = + { + self, + nixpkgs, + flake-utils, + }: + flake-utils.lib.eachDefaultSystem ( + system: let - pkgs = import nixpkgs {inherit system;}; - - agda2hs-lib = pkgs.agdaPackages.mkDerivation - { pname = "agda2hs"; - meta = {}; - version = "1.3"; - preBuild = '' - echo "{-# OPTIONS --sized-types #-}" > Everything.agda - echo "module Everything where" >> Everything.agda - find lib -name '*.agda' | sed -e 's/lib\///;s/\//./g;s/\.agda$//;s/^/import /' >> Everything.agda - ''; - src = ./.; - }; - # options provides a way to jailbreak for packages that use agda2hs - agda2hs-pkg = options: - pkgs.haskellPackages.haskellSrc2nix { - name = "agda2hs"; - src = ./.; - extraCabal2nixOptions = options; #"--jailbreak" - }; - agda2hs-hs = pkgs.haskellPackages.callPackage (agda2hs-pkg "") {}; - agda2hs-expr = import ./agda2hs.nix; - agda2hs = pkgs.callPackage agda2hs-expr { - inherit self; - agda2hs = agda2hs-hs; - inherit (pkgs.haskellPackages) ghcWithPackages; - }; - in { - packages = { - inherit agda2hs-lib; - inherit (agda2hs) agda2hs; - default = agda2hs.agda2hs; - }; - lib = { - inherit (agda2hs) withPackages; - inherit agda2hs-pkg agda2hs-hs agda2hs-expr; + pkgs = import nixpkgs { inherit system; }; + packages = import ./nix/default.nix { inherit pkgs; }; + lib = import ./nix/lib.nix { inherit pkgs; }; + in + { + packages = packages // { + default = packages.agda2hs; }; - devShells.default = pkgs.haskellPackages.shellFor { - packages = p: [agda2hs-hs]; - buildInputs = with pkgs.haskellPackages; [ - cabal-install - cabal2nix - haskell-language-server - pkgs.agda - ]; + inherit lib; + devShells.default = import ./nix/shell.nix { + inherit pkgs; + inherit (lib) agda2hs-hs; }; - }); + } + ); } diff --git a/agda2hs.nix b/nix/agda2hs.nix similarity index 76% rename from agda2hs.nix rename to nix/agda2hs.nix index ef54cd9a..216bdefa 100644 --- a/agda2hs.nix +++ b/nix/agda2hs.nix @@ -1,3 +1,6 @@ +# this file should be very close to a copy of nixpkgs/pkgs/build-support/agda/default.nix +# I think I took the version from https://github.com/NixOS/nixpkgs/blob/bbe6402ecacfc3a0e2c65e3527c2cbe148b98ff8/pkgs/build-support/agda/default.nix +# but it would be nice to expose this in upstream so that we don't have to duplicate the file {stdenv, lib, self, agda2hs, runCommandNoCC, makeWrapper, writeText, mkShell, ghcWithPackages}: with lib.strings; let diff --git a/nix/default.nix b/nix/default.nix new file mode 100644 index 00000000..3fd59667 --- /dev/null +++ b/nix/default.nix @@ -0,0 +1,23 @@ +{ + pkgs ? import { }, + ... +}: +let + lib = import ./lib.nix { inherit pkgs; }; + version = "1.3"; + agdalib = pkgs.agdaPackages.mkDerivation { + pname = "agda2hs"; + meta = { }; + version = version; + preBuild = '' + echo "{-# OPTIONS --sized-types #-}" > Everything.agda + echo "module Everything where" >> Everything.agda + find lib -name '*.agda' | sed -e 's/lib\///;s/\//./g;s/\.agda$//;s/^/import /' >> Everything.agda + ''; + src = ../.; + }; +in +{ + inherit (lib) agda2hs; + agda2hs-lib = agdalib; +} diff --git a/nix/lib.nix b/nix/lib.nix new file mode 100644 index 00000000..d19a46e6 --- /dev/null +++ b/nix/lib.nix @@ -0,0 +1,29 @@ +{ + pkgs ? import { }, + ... +}: +let + hsrc = + options: + pkgs.haskellPackages.haskellSrc2nix { + name = "agda2hs"; + src = ../.; + extraCabal2nixOptions = options; # "--jailbreak" + }; + hpkg = pkgs.haskellPackages.callPackage (hsrc "") { }; + expr = import ./agda2hs.nix; + agda2hs = pkgs.lib.makeScope pkgs.newScope ( + self: + pkgs.callPackage expr { + agda2hs = hpkg; + inherit self; + inherit (pkgs.haskellPackages) ghcWithPackages; + } + ); +in +{ + agda2hs-pkg = hsrc; + agda2hs-hs = hpkg; + agda2hs-expr = expr; + inherit (agda2hs) agda2hs withPackages; +} diff --git a/nix/shell.nix b/nix/shell.nix new file mode 100644 index 00000000..e18485d6 --- /dev/null +++ b/nix/shell.nix @@ -0,0 +1,10 @@ +{ pkgs, agda2hs-hs }: +pkgs.haskellPackages.shellFor { + packages = p: [ agda2hs-hs ]; + buildInputs = with pkgs.haskellPackages; [ + cabal-install + cabal2nix + haskell-language-server + pkgs.agda + ]; +} diff --git a/shell.nix b/shell.nix deleted file mode 100644 index 8ce098ad..00000000 --- a/shell.nix +++ /dev/null @@ -1,33 +0,0 @@ -{ nixpkgs ? import {}, compiler ? "default", doBenchmark ? false }: - -let - - inherit (nixpkgs) pkgs; - - f = { mkDerivation, Agda, base, containers, haskell-src-exts - , stdenv - }: - mkDerivation { - pname = "agda2hs"; - version = "1.0"; - src = ./.; - isLibrary = false; - isExecutable = true; - executableHaskellDepends = [ - Agda base containers haskell-src-exts - ]; - description = "Compiling Agda code to readable Haskell"; - license = stdenv.lib.licenses.bsd3; - }; - - haskellPackages = if compiler == "default" - then pkgs.haskellPackages - else pkgs.haskell.packages.${compiler}; - - variant = if doBenchmark then pkgs.haskell.lib.doBenchmark else pkgs.lib.id; - - drv = variant (haskellPackages.callPackage f {}); - -in - - if pkgs.lib.inNixShell then drv.env else drv