cedille: init at 1.0.0

1 files changed, 37 insertions, 0 deletions

diff --git a/pkgs/applications/science/logic/cedille/default.nix b/pkgs/applications/science/logic/cedille/default.nix
new file mode 100644
index 000000000000..5b99a47bb415
--- /dev/null
+++ b/pkgs/applications/science/logic/cedille/default.nix
@@ -0,0 +1,37 @@
+{ stdenv, lib, fetchFromGitHub, alex, happy, Agda, agdaIowaStdlib,
+  buildPlatform, buildPackages, ghcWithPackages }:
+stdenv.mkDerivation rec {
+  version = "1.0.0";
+  name = "cedille-${version}";
+  src = fetchFromGitHub {
+    owner = "cedille";
+    repo = "cedille";
+    rev = "v${version}";
+    sha256 = "08c2vgg8i6l3ws7hd5gsj89mki36lxm7x7s8hi1qa5gllq04a832";
+  };
+  buildInputs = [ alex happy Agda (ghcWithPackages (ps: [ps.ieee])) ];
+
+  LANG = "en_US.UTF-8";
+  LOCALE_ARCHIVE =
+    lib.optionalString (buildPlatform.libc == "glibc")
+      "${buildPackages.glibcLocales}/lib/locale/locale-archive";
+
+  postPatch = ''
+    patchShebangs create-libraries.sh
+    cp -r ${agdaIowaStdlib.src} ial
+    chmod -R 755 ial
+  '';
+
+  installPhase = ''
+    mkdir -p $out/bin
+    mv cedille $out/bin/cedille
+  '';
+
+  meta = {
+    description = "An interactive theorem-prover and dependently typed programming language, based on extrinsic (aka Curry-style) type theory.";
+    homepage = https://cedille.github.io/;
+    license = stdenv.lib.licenses.mit;
+    maintainers = [ stdenv.lib.maintainers.mpickering ];
+    platforms = stdenv.lib.platforms.unix;
+  };
+}