Add 'nixpkgs/' from commit 'abf060725d7614bd3b9f96764262dfbc2f9c2199'

git-subtree-dir: nixpkgs
git-subtree-mainline: 4e31070265257dc67d120c27e0f75c2344fdfa9a
git-subtree-split: abf060725d7614bd3b9f96764262dfbc2f9c2199

11 files changed, 528 insertions, 0 deletions

diff --git a/nixpkgs/pkgs/development/libraries/agda/Agda-Sheaves/default.nix b/nixpkgs/pkgs/development/libraries/agda/Agda-Sheaves/default.nix
new file mode 100644
index 000000000000..6ab7455915cc
--- /dev/null
+++ b/nixpkgs/pkgs/development/libraries/agda/Agda-Sheaves/default.nix
@@ -0,0 +1,24 @@
+{ stdenv, agda, fetchgit }:
+
+agda.mkDerivation (self: rec {
+  version = "8a06162a8f0f7df308458db91d720cf8f7345d69";
+  name = "Agda-Sheaves-${version}";
+  src = fetchgit {
+    url = "https://github.com/jonsterling/Agda-Sheaves.git";
+    rev = version;
+    sha256 = "1gjffyyi4gk9z380yw2wm0jg0a01zy8dnw7jrcc7222swisk5s2d";
+  };
+
+  everythingFile = "sheaves.agda";
+  topSourceDirectories = [ "../$sourceRoot" ];
+  sourceDirectories = [];
+
+  meta = {
+    homepage = https://github.com/jonsterling/Agda-Sheaves;
+    description = "Sheaves in Agda";
+    license = stdenv.lib.licenses.cc-by-40;
+    platforms = stdenv.lib.platforms.unix;
+    maintainers = with stdenv.lib.maintainers; [ fuuzetsu ];
+    broken = true;  # replaced by constructive-sheaf-semantics
+  };
+})
diff --git a/nixpkgs/pkgs/development/libraries/agda/TotalParserCombinators/contextfile b/nixpkgs/pkgs/development/libraries/agda/TotalParserCombinators/contextfile
new file mode 100644
index 000000000000..46743cba3b67
--- /dev/null
+++ b/nixpkgs/pkgs/development/libraries/agda/TotalParserCombinators/contextfile
@@ -0,0 +1,259 @@
+
+Context:
+
+[Updated the code in response to changes to Agda.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20150319181310
+ Ignore-this: 52b9ff613d7f10b0c8f45591a0759d07
+] 
+
+[Rolled back most of "Updated the code in response to changes to Agda".
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20150319101420
+ Ignore-this: c2ea7bdf79848235fa3ea64ebda116eb
+ * One of the Agda changes has been reverted.
+] 
+
+[Removed an outdated comment.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20150217162945
+ Ignore-this: 3ff7732335750305fe220e65693f0cbf
+] 
+
+[Added the simplification "nonempty (return x) → fail".
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20150217161718
+ Ignore-this: 56ad6a68c314446d8986a8c1b49655d0
+] 
+
+[Added Nonempty.nonempty-return.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20150217161629
+ Ignore-this: 68829d3f9a248272c46848daa05ccfe3
+] 
+
+[Updated the copyright year range.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20150212154744
+ Ignore-this: 3410a12ca1f9de825b00e692b136d500
+] 
+
+[Updated the code in response to changes to Agda.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20150212152207
+ Ignore-this: 683b5eeca5fa9c8490bceaf68c23a204
+] 
+
+[Updated the copyright year range.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20141128223227
+ Ignore-this: 31d3f5e4fdd6fbfad9758d9bfd0d3a3e
+] 
+
+[Updated the code in response to changes to Agda and the library.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20141128223205
+ Ignore-this: 6392ec67aab2c534a7195abed55be47
+] 
+
+[Updated code to reflect changes to Agda.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20140425121055
+ Ignore-this: 54d80fd647cb897eef85f57e9172f7db
+] 
+
+[Workaround for (possible) Agda bug.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20140228200347
+ Ignore-this: b17884ad17a3bdb7faff678622365a8
+] 
+
+[Updated code to reflect changes to library API.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20130307134644
+ Ignore-this: 50d070a22a6796b9acdf19d44ba5de16
+] 
+
+[Updated code to reflect changes to Agda and the library API.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20130228122951
+ Ignore-this: 761dc4d85683a59cc3667a8706c88093
+] 
+
+[Turned _◇_ into a constructor.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20120316125431
+ Ignore-this: 41b492c3106a575f28f146253f78a5ae
+] 
+
+[Updated code to reflect changes to Agda.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20120316125416
+ Ignore-this: e77d817d8b391c3b4806119d10848eb3
+] 
+
+[Updated code to reflect changes to Agda.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20120215103344
+ Ignore-this: 467716429d5553cd122722108ea82a08
+] 
+
+[Modified a comment.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20120215103319
+ Ignore-this: e57d4911f692f8a96a80017d910efc5f
+] 
+
+[Updated code to reflect change to library API.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20111006160229
+ Ignore-this: 5359da54e7e6e0f92983fa3ecaccebf3
+] 
+
+[Updated code to reflect changes to Agda and the library API.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20111003170117
+ Ignore-this: cbdd35172e372779e12642985cf17268
+] 
+
+[Rolled back addition of inversion lemmas.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20110930150912
+ Ignore-this: 9c9b083f0afcf95aaaa55a01d871274e
+] 
+
+[Added inversion lemmas, implemented other lemmas using these lemmas.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20110930150842
+ Ignore-this: 19b832c3f9e14d1e713b5911c094a130
+ + This change was a response to a change to Agda's pattern matching
+   machinery. Subsequently the machinery was made more liberal again,
+   making this change unnecessary.
+] 
+
+[Updated code to reflect changes to library API.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20110517220158
+ Ignore-this: ea9771a5014a25cb20afc2118638f8b5
+] 
+
+[Updated code to reflect changes to Agda.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20110512124425
+ Ignore-this: 97b154661679f574f6ab914583b14580
+] 
+
+[Proved that many constructions preserve various preorders.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20110313012617
+ Ignore-this: 8008efaff967c228448baa33b82edb81
+] 
+
+[Updated code to reflect changes to library API.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20110313002106
+ Ignore-this: 94799ba1ae411e59fd8c6c7eac3b8dfb
+] 
+
+[Simplified TotalRecognisers.LeftRecursion.MatchingParentheses.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20110118102159
+ Ignore-this: 1e01a8092b0c0124979ffc5fe17a245c
+] 
+
+[Added TotalRecognisers.LeftRecursion.MatchingParentheses.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20110118102146
+ Ignore-this: 13a3bc91425364e26c3047561655bb25
+] 
+
+[Added a simplifying backend.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101229012716
+ Ignore-this: 9ac7ae21cd44c099633678a994fb9a3
+] 
+
+[Fixed another "bug" in the deep simplifier.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101229010854
+ Ignore-this: e258adf963436ef715242db23c6808e
+ + Sometimes the first layer of bind's right-hand argument was not
+   simplified.
+] 
+
+[Made simplify₁ public and changed its type.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101228235603
+ Ignore-this: d39b8453a15089126261e098080223c6
+] 
+
+[Deep simplification no longer adds casts.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101228192850
+ Ignore-this: 2ba016825adfa3a1e36922869eabfd39
+] 
+
+[The first constructor in a simplified parser can no longer be a cast.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101228175822
+ Ignore-this: ce3e38cc0b9a096aa436655c9013ae97
+] 
+
+[Modified the outline.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101228173414
+ Ignore-this: f8866e69f6d1a344e79fb6f708dfa4c
+] 
+
+[Added an example: a right recursive expression grammar.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101228173159
+ Ignore-this: 9a4d732b451cca08ba19aac5d115c678
+] 
+
+[Rearranged the code.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101228172209
+ Ignore-this: 50fa29406d0f150669ff3feec4dbe513
+] 
+
+[Renamed same-bag/set to (initial-bag-)cong.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101228170706
+ Ignore-this: dd3ce43d77dde74cc2428d2568dd2d30
+] 
+
+[Added TotalParserCombinators.Force.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101228153638
+ Ignore-this: 3b6ff6ea20df0c1293494f06845d17eb
+] 
+
+[Proved that uses of subst can be erased.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101228153621
+ Ignore-this: f503ba495b923ae521718b6957167128
+] 
+
+[The deep simplifier no longer skips layers.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101228141138
+ Ignore-this: 733a4a4a9aa0f890ad1740ecfc6a599f
+] 
+
+[Documented that the deep simplifier misses every second layer.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101228121910
+ Ignore-this: 8a0baf25b12f63f8748dbc1d16affacf
+] 
+
+[The simplifier now applies the token-bind rule more often.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101227165413
+ Ignore-this: 40132fa6f19602886bbe29aadd8a683c
+] 
+
+[Switched back to deep simplification, now with a proper proof.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101227125434
+ Ignore-this: ccc46e82f6f9c6c2a27ddb43d315f7dd
+] 
+
+[Simplified the soundness proof.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101227123839
+ Ignore-this: fb6826dd9836e34fc3bfdce2928ba13d
+] 
+
+[Made some _≈[_]P_ constructors conditionally coinductive.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101227123827
+ Ignore-this: f521f70475403697229051b62343a080
+ + The structure of the soundness proof was also changed.
+] 
+
+[Unified And, AsymmetricChoice and Not.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101225103109
+ Ignore-this: 5ae8b80e1505fe6e707bb2307d22688c
+] 
+
+[Modified some comments.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101225101051
+ Ignore-this: e812d8c3e9720895c368f7a286f8315c
+] 
+
+[Modified a comment.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101223202647
+ Ignore-this: 16ea5dc01a4cbe0fe38714b2e4b7ff6
+] 
+
+[Updated code to reflect changes to library API.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101107162658
+ Ignore-this: 9e38a10a9997c9825ece6ad9f871b673
+] 
+
+[Added an alternative backend for TotalRecognisers.Simple.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101020183743
+ Ignore-this: a111a89e0c237e132b649561000f53d6
+] 
+
+[TAG Code corresponding to the paper "Total Parser Combinators" (4).
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100928013815
+ Ignore-this: 45ccc28373ed3974047315613eb14833
+] 
diff --git a/nixpkgs/pkgs/development/libraries/agda/TotalParserCombinators/default.nix b/nixpkgs/pkgs/development/libraries/agda/TotalParserCombinators/default.nix
new file mode 100644
index 000000000000..ac9ce9dd84f4
--- /dev/null
+++ b/nixpkgs/pkgs/development/libraries/agda/TotalParserCombinators/default.nix
@@ -0,0 +1,26 @@
+{ stdenv, agda, fetchdarcs, AgdaStdlib }:
+
+agda.mkDerivation (self: rec {
+  version = "2015-03-19";
+  name = "TotalParserCombinators-${version}";
+
+  src = fetchdarcs {
+    url = "http://www.cse.chalmers.se/~nad/repos/parser-combinators.code/";
+    context = ./contextfile;
+    sha256 = "0jlbz8yni6i7vb2qsd41bdkpchqirvc5pavckaf97z7p4gqi2mlj";
+  };
+
+  buildDepends = [ AgdaStdlib ];
+  everythingFile = "TotalParserCombinators.agda";
+  sourceDirectories = [];
+  topSourceDirectories = [ "../$sourceRoot" ];
+
+  meta = with stdenv.lib; {
+    homepage = http://www.cse.chalmers.se/~nad/publications/danielsson-parser-combinators.html;
+    description = "A monadic parser combinator library which guarantees termination of parsing";
+    license = stdenv.lib.licenses.mit;
+    platforms = stdenv.lib.platforms.unix;
+    maintainers = with maintainers; [ fuuzetsu ];
+    broken = true;
+  };
+})
diff --git a/nixpkgs/pkgs/development/libraries/agda/agda-base/default.nix b/nixpkgs/pkgs/development/libraries/agda/agda-base/default.nix
new file mode 100644
index 000000000000..146e44182ed2
--- /dev/null
+++ b/nixpkgs/pkgs/development/libraries/agda/agda-base/default.nix
@@ -0,0 +1,23 @@
+{ stdenv, agda, fetchurl }:
+
+agda.mkDerivation (self: rec {
+  version = "0.1";
+  name = "agda-base-${version}";
+
+  src = fetchurl {
+    url = "https://github.com/pcapriotti/agda-base/archive/v${version}.tar.gz";
+    sha256 = "124h06p7jdiqr2x6r46sfab9r0cgb0fznr2qs5i1psl5yf3z74h8";
+  };
+
+  sourceDirectories = [ "./." ];
+  everythingFile = "README.agda";
+
+  meta = {
+    homepage = https://github.com/pcapriotti/agda-base;
+    description = "Base library for HoTT in Agda";
+    license = stdenv.lib.licenses.bsd3;
+    platforms = stdenv.lib.platforms.unix;
+    maintainers = with stdenv.lib.maintainers; [ fuuzetsu ];
+    broken = true;  # largely replaced by HoTT-Agda
+  };
+})
diff --git a/nixpkgs/pkgs/development/libraries/agda/agda-iowa-stdlib/default.nix b/nixpkgs/pkgs/development/libraries/agda/agda-iowa-stdlib/default.nix
new file mode 100644
index 000000000000..3ab4ed3e9623
--- /dev/null
+++ b/nixpkgs/pkgs/development/libraries/agda/agda-iowa-stdlib/default.nix
@@ -0,0 +1,27 @@
+{ stdenv, agda, fetchFromGitHub }:
+
+agda.mkDerivation (self: rec {
+  version = "1.4.0";
+  name = "agda-iowa-stdlib-${version}";
+
+  src = fetchFromGitHub {
+    owner = "cedille";
+    repo  = "ial";
+    rev = "v${version}";
+    sha256 = "1gwxpybxwdj5ipbb3gapm7r5hfl3g6sj9kp13954pdmx8d5b0gma";
+  };
+
+  sourceDirectories = [ "./." ];
+  buildPhase = ''
+    patchShebangs find-deps.sh
+    make
+  '';
+
+  meta = {
+    homepage = https://svn.divms.uiowa.edu/repos/clc/projects/agda/lib/;
+    description = "Agda standard library developed at Iowa";
+    license = stdenv.lib.licenses.free;
+    platforms = stdenv.lib.platforms.unix;
+    maintainers = with stdenv.lib.maintainers; [ fuuzetsu ];
+  };
+})
diff --git a/nixpkgs/pkgs/development/libraries/agda/agda-prelude/default.nix b/nixpkgs/pkgs/development/libraries/agda/agda-prelude/default.nix
new file mode 100644
index 000000000000..e3dcf765dfd4
--- /dev/null
+++ b/nixpkgs/pkgs/development/libraries/agda/agda-prelude/default.nix
@@ -0,0 +1,23 @@
+{ stdenv, agda, fetchgit }:
+
+agda.mkDerivation (self: rec {
+  version = "0dca24a81d417db2ae8fc871eccb7776f7eae952";
+  name = "agda-prelude-${version}";
+
+  src = fetchgit {
+    url = "https://github.com/UlfNorell/agda-prelude.git";
+    rev = version;
+    sha256 = "0gwfgvj96i1mx5v01bi46h567d1q1fbgvzv6z8zv91l2jhybwff5";
+  };
+
+  topSourceDirectories = [ "src" ];
+  everythingFile = "src/Prelude.agda";
+
+  meta = with stdenv.lib; {
+    homepage = https://github.com/UlfNorell/agda-prelude;
+    description = "Programming library for Agda";
+    license = stdenv.lib.licenses.mit;
+    platforms = stdenv.lib.platforms.unix;
+    maintainers = with maintainers; [ fuuzetsu mudri ];
+  };
+})
diff --git a/nixpkgs/pkgs/development/libraries/agda/agda-stdlib/default.nix b/nixpkgs/pkgs/development/libraries/agda/agda-stdlib/default.nix
new file mode 100644
index 000000000000..276e1531acdd
--- /dev/null
+++ b/nixpkgs/pkgs/development/libraries/agda/agda-stdlib/default.nix
@@ -0,0 +1,29 @@
+{ stdenv, agda, fetchFromGitHub, ghcWithPackages }:
+
+agda.mkDerivation (self: rec {
+  version = "0.17";
+  name = "agda-stdlib-${version}";
+
+  src = fetchFromGitHub {
+    repo = "agda-stdlib";
+    owner = "agda";
+    rev = "v${version}";
+    sha256 = "05c5zgj9fcaqz7z2l70jh48b3g4811vm7bccj0vd9r82wi02g3p1";
+  };
+
+  nativeBuildInputs = [ (ghcWithPackages (self : [ self.filemanip ])) ];
+  preConfigure = ''
+    runhaskell GenerateEverything.hs
+  '';
+
+  topSourceDirectories = [ "src" ];
+
+  meta = with stdenv.lib; {
+    homepage = http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary;
+    description = "A standard library for use with the Agda compiler";
+    license = stdenv.lib.licenses.mit;
+    platforms = stdenv.lib.platforms.unix;
+    broken = stdenv.isDarwin;
+    maintainers = with maintainers; [ jwiegley fuuzetsu mudri ];
+  };
+})
diff --git a/nixpkgs/pkgs/development/libraries/agda/bitvector/default.nix b/nixpkgs/pkgs/development/libraries/agda/bitvector/default.nix
new file mode 100644
index 000000000000..6306bb89b5c7
--- /dev/null
+++ b/nixpkgs/pkgs/development/libraries/agda/bitvector/default.nix
@@ -0,0 +1,24 @@
+{ stdenv, agda, fetchgit, AgdaStdlib }:
+
+agda.mkDerivation (self: rec {
+  version = "f1c173313f2a41d95a8dc6053f9365a24690e18d";
+  name = "bitvector-${version}";
+
+  src = fetchgit {
+    url = "https://github.com/copumpkin/bitvector.git";
+    rev = version;
+    sha256 = "0jb421lxvyxz26sxa81qjmn1gfcxfh0fmbq128f0kslqhiiaqfrh";
+  };
+
+  buildDepends = [ AgdaStdlib ];
+  sourceDirectories = [ "Data" ];
+
+  meta = {
+    homepage = https://github.com/copumpkin/bitvector;
+    description = "Sequences of bits and common operations on them";
+    license = stdenv.lib.licenses.bsd3;
+    platforms = stdenv.lib.platforms.unix;
+    maintainers = with stdenv.lib.maintainers; [ fuuzetsu ];
+    broken = true;
+  };
+})
diff --git a/nixpkgs/pkgs/development/libraries/agda/categories/default.nix b/nixpkgs/pkgs/development/libraries/agda/categories/default.nix
new file mode 100644
index 000000000000..ea232f2853d6
--- /dev/null
+++ b/nixpkgs/pkgs/development/libraries/agda/categories/default.nix
@@ -0,0 +1,24 @@
+{ stdenv, agda, fetchgit, AgdaStdlib }:
+
+agda.mkDerivation (self: rec {
+  version = "33409120d071656f5198c658145889ae2e86249c";
+  name = "categories-${version}";
+
+  src = fetchgit {
+    url = "https://github.com/copumpkin/categories.git";
+    rev = version;
+    sha256 = "15x834f7jn2s816b9vz8nm8p424ppzv6v9nayaawyl43qmaaaa5p";
+  };
+
+  buildDepends = [ AgdaStdlib ];
+  sourceDirectories = [ "Categories" "Graphs" ];
+
+  meta = {
+    homepage = https://github.com/copumpkin/categories;
+    description = "Categories parametrized by morphism equality, in Agda";
+    license = stdenv.lib.licenses.bsd3;
+    platforms = stdenv.lib.platforms.unix;
+    maintainers = with stdenv.lib.maintainers; [ fuuzetsu ];
+    broken = true; # doesn't work due to new agdastdlib, see #9471
+  };
+})
diff --git a/nixpkgs/pkgs/development/libraries/agda/pretty/contextfile b/nixpkgs/pkgs/development/libraries/agda/pretty/contextfile
new file mode 100644
index 000000000000..2ea20153bbcc
--- /dev/null
+++ b/nixpkgs/pkgs/development/libraries/agda/pretty/contextfile
@@ -0,0 +1,43 @@
+
+Context:
+
+[Updated the code in response to a change to Agda.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20150319181428
+ Ignore-this: f83c3dccfe25a2a5b9d0437d1dce0ec0
+] 
+
+[Rolled back most of "Updated the code in response to changes to Agda".
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20150319101413
+ Ignore-this: 5a26cf9cf83d0d146cca0c15c857d20c
+ * One of the Agda changes has been reverted.
+] 
+
+[Updated the code in response to changes to Agda.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20150217101656
+ Ignore-this: a12921aebbe0fb575ef391ba5789a391
+] 
+
+[Modified the copyright year range.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20150213144338
+ Ignore-this: 1d1b22457dd6dadcb47f5d7f3eea062
+] 
+
+[Restored Grammar.Abstract and Grammar.Non-terminal.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20130727225031
+ Ignore-this: ddccb15caa7a3c26e973997ffdb4eec1
+] 
+
+[Modified the copyright year range.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20141128164015
+ Ignore-this: b9c6dddc965738aa2a7670c4c18da67f
+] 
+
+[Updated the code to reflect changes to the library API.
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20141128163950
+ Ignore-this: 8094c47f23cef0fcc596ad0c18a92b56
+] 
+
+[TAG Correct-by-Construction Pretty-Printing (2013-07-28)
+Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20130727224432
+ Ignore-this: 6aab9b2e6b638457767c8821f3c27cb4
+] 
diff --git a/nixpkgs/pkgs/development/libraries/agda/pretty/default.nix b/nixpkgs/pkgs/development/libraries/agda/pretty/default.nix
new file mode 100644
index 000000000000..0e4f1da6e140
--- /dev/null
+++ b/nixpkgs/pkgs/development/libraries/agda/pretty/default.nix
@@ -0,0 +1,26 @@
+{ stdenv, agda, fetchdarcs, AgdaStdlib }:
+
+agda.mkDerivation (self: rec {
+  version = "2015-03-19";
+  name = "pretty-${version}";
+
+  src = fetchdarcs {
+    url = "http://www.cse.chalmers.se/~nad/repos/pretty/";
+    context = ./contextfile;
+    sha256 = "0zmwh9kln7ykpmkx1qhqz64qm2arq62b17vs5fswnxk7mqxsmrf0";
+  };
+
+  buildDepends = [ AgdaStdlib ];
+  everythingFile = "Pretty.agda";
+  sourceDirectories = [];
+  topSourceDirectories = [ "../$sourceRoot" ];
+
+  meta = with stdenv.lib; {
+    homepage = http://www.cse.chalmers.se/~nad/publications/danielsson-correct-pretty.html;
+    description = "Correct-by-Construction Pretty-Printing";
+    license = stdenv.lib.licenses.mit;
+    platforms = stdenv.lib.platforms.unix;
+    maintainers = with maintainers; [ fuuzetsu ];
+    broken = true; # 2018-04-11
+  };
+})