From 561fcf4c820c6db65b0efeba675680c54f9f2e41 Mon Sep 17 00:00:00 2001
From: Matthew Pickering <matthewtpickering@gmail.com>
Date: Fri, 12 Oct 2018 21:20:19 +0000
Subject: [PATCH 1/3] agdaIowaStdlib: 18734 -> 1.4.0

---
 .../libraries/agda/agda-iowa-stdlib/default.nix   | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

diff --git a/pkgs/development/libraries/agda/agda-iowa-stdlib/default.nix b/pkgs/development/libraries/agda/agda-iowa-stdlib/default.nix
index ce25521ad2e5..3ab4ed3e9623 100644
--- a/pkgs/development/libraries/agda/agda-iowa-stdlib/default.nix
+++ b/pkgs/development/libraries/agda/agda-iowa-stdlib/default.nix
@@ -1,13 +1,14 @@
-{ stdenv, agda, fetchsvn }:
+{ stdenv, agda, fetchFromGitHub }:
 
 agda.mkDerivation (self: rec {
-  version = "18734";
+  version = "1.4.0";
   name = "agda-iowa-stdlib-${version}";
 
-  src = fetchsvn {
-    url = "https://svn.divms.uiowa.edu/repos/clc/projects/agda/lib";
-    rev = version;
-    sha256 = "0aqib88m5n6aqb5lmns9nl62x40yqhg6zpj0zjxibbn4s4qjw9ky";
+  src = fetchFromGitHub {
+    owner = "cedille";
+    repo  = "ial";
+    rev = "v${version}";
+    sha256 = "1gwxpybxwdj5ipbb3gapm7r5hfl3g6sj9kp13954pdmx8d5b0gma";
   };
 
   sourceDirectories = [ "./." ];
@@ -22,7 +23,5 @@ agda.mkDerivation (self: rec {
     license = stdenv.lib.licenses.free;
     platforms = stdenv.lib.platforms.unix;
     maintainers = with stdenv.lib.maintainers; [ fuuzetsu ];
-
-    broken = true;
   };
 })

From 43ae33728bace6deb31042ab61efb196c1b8e2b0 Mon Sep 17 00:00:00 2001
From: Matthew Pickering <matthewtpickering@gmail.com>
Date: Fri, 12 Oct 2018 21:22:25 +0000
Subject: [PATCH 2/3] cedille: init at 1.0.0

---
 .../science/logic/cedille/default.nix         | 37 +++++++++++++++++++
 pkgs/top-level/all-packages.nix               |  4 ++
 2 files changed, 41 insertions(+)
 create mode 100644 pkgs/applications/science/logic/cedille/default.nix

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;
+  };
+}
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 8daf69f64f65..256e11ada728 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -1091,6 +1091,10 @@ with pkgs;
 
   cddl = callPackage ../development/tools/cddl { };
 
+  cedille = callPackage ../applications/science/logic/cedille
+                          { inherit (haskellPackages) alex happy Agda ghcWithPackages;
+                          };
+
   cfdyndns = callPackage ../applications/networking/dyndns/cfdyndns { };
 
   ckbcomp = callPackage ../tools/X11/ckbcomp { };

From 9e348b4613c734d114e85ec40b72119a3c5ffd4f Mon Sep 17 00:00:00 2001
From: Matthew Pickering <matthewtpickering@gmail.com>
Date: Sat, 13 Oct 2018 09:16:57 +0000
Subject: [PATCH 3/3] emacsPackages.cedille: init at 1.0.0

---
 .../editors/emacs-modes/cedille/default.nix   | 30 +++++++++++++++++++
 pkgs/top-level/all-packages.nix               |  2 ++
 2 files changed, 32 insertions(+)
 create mode 100644 pkgs/applications/editors/emacs-modes/cedille/default.nix

diff --git a/pkgs/applications/editors/emacs-modes/cedille/default.nix b/pkgs/applications/editors/emacs-modes/cedille/default.nix
new file mode 100644
index 000000000000..2d1cbb75981e
--- /dev/null
+++ b/pkgs/applications/editors/emacs-modes/cedille/default.nix
@@ -0,0 +1,30 @@
+{ stdenv, cedille, emacs }:
+
+stdenv.mkDerivation rec {
+  name    = "cedille-mode-${version}";
+  version = cedille.version;
+
+  src = cedille.src;
+
+  buildInputs = [ emacs ];
+
+  buildPhase = ":";
+
+  installPhase = ''
+    install -d $out/share/emacs/site-lisp
+    install se-mode/*.el se-mode/*.elc $out/share/emacs/site-lisp
+    install cedille-mode/*.el cedille-mode/*.elc $out/share/emacs/site-lisp
+    install *.el *.elc $out/share/emacs/site-lisp
+    substituteInPlace $out/share/emacs/site-lisp/cedille-mode.el \
+      --replace /usr/bin/cedille ${cedille}/bin/cedille \
+
+  '';
+
+  meta = {
+    description = "Emacs major mode for Cedille";
+    homepage    = cedille.meta.homepage;
+    license     = cedille.meta.license ;
+    platforms   = cedille.meta.platforms;
+    maintainers = cedille.meta.maintainers;
+  };
+}
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 256e11ada728..43c5dfb36f0b 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -16236,6 +16236,8 @@ with pkgs;
 
     calfw = callPackage ../applications/editors/emacs-modes/calfw { };
 
+    cedille = callPackage ../applications/editors/emacs-modes/cedille { cedille = pkgs.cedille; };
+
     coffee = callPackage ../applications/editors/emacs-modes/coffee { };
 
     colorTheme = callPackage ../applications/editors/emacs-modes/color-theme { };