From 68e1419cb8eca6e306ec0a75f37621ae7aefabed Mon Sep 17 00:00:00 2001 From: laMudri Date: Sat, 21 May 2016 16:02:15 +0100 Subject: [PATCH 1/4] Agda: prebuild all of the new builtin modules --- .../haskell-modules/hackage-packages.nix | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/pkgs/development/haskell-modules/hackage-packages.nix b/pkgs/development/haskell-modules/hackage-packages.nix index 2fb8e65450f..91649b56247 100644 --- a/pkgs/development/haskell-modules/hackage-packages.nix +++ b/pkgs/development/haskell-modules/hackage-packages.nix @@ -847,13 +847,22 @@ self: { ]; executableToolDepends = [ emacs ]; postInstall = '' - $out/bin/agda -c --no-main $(find $out/share -name Primitive.agda) + # Separate loops to avoid internal error + files=($out/share/*-ghc-*/Agda-*/lib/prim/Agda/{Primitive.agda,Builtin/*.agda}) + for f in "''${files[@]}" + do + $out/bin/agda $f + done + for f in "''${files[@]}" + do + $out/bin/agda -c --no-main $f + done $out/bin/agda-mode compile ''; homepage = "http://wiki.portal.chalmers.se/agda/"; description = "A dependently typed functional programming language and proof assistant"; license = "unknown"; - maintainers = with stdenv.lib.maintainers; [ abbradar ]; + maintainers = with stdenv.lib.maintainers; [ abbradar mudri ]; }) {inherit (pkgs) emacs;}; "Agda-executable" = callPackage From 072ce88eb9b3774321bd70103027a5561f22b72b Mon Sep 17 00:00:00 2001 From: laMudri Date: Sat, 21 May 2016 16:05:08 +0100 Subject: [PATCH 2/4] agda-stdlib: 2.4.2.3 -> v0.12 (for Agda-2.5.1) --- .../libraries/agda/agda-stdlib/default.nix | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/pkgs/development/libraries/agda/agda-stdlib/default.nix b/pkgs/development/libraries/agda/agda-stdlib/default.nix index 2a75b1fb700..47e426580ce 100644 --- a/pkgs/development/libraries/agda/agda-stdlib/default.nix +++ b/pkgs/development/libraries/agda/agda-stdlib/default.nix @@ -1,13 +1,12 @@ -{ stdenv, agda, fetchgit, ghcWithPackages }: +{ stdenv, agda, fetchurl, ghcWithPackages }: agda.mkDerivation (self: rec { - version = "2.4.2.3"; + version = "v0.12"; name = "agda-stdlib-${version}"; - src = fetchgit { - url = "git://github.com/agda/agda-stdlib"; - rev = "9c9b3cb28f9a7d39a256890a1469c1a3f7fc4faf"; - sha256 = "521899b820e70abbae7cb30008b87a2f8676bc6265b78865e42982fc2e5c972f"; + src = fetchurl { + url = "https://github.com/agda/agda-stdlib/archive/${version}.tar.gz"; + sha256 = "11qf87hxx3g0n8i6nkp4vqvh3i0gal6g812p0w2n4k7711nvrp9g"; }; nativeBuildInputs = [ (ghcWithPackages (self : [ self.filemanip ])) ]; @@ -22,6 +21,6 @@ agda.mkDerivation (self: rec { description = "A standard library for use with the Agda compiler"; license = stdenv.lib.licenses.mit; platforms = stdenv.lib.platforms.unix; - maintainers = with maintainers; [ jwiegley fuuzetsu ]; + maintainers = with maintainers; [ jwiegley fuuzetsu mudri ]; }; }) From 92b843f9a5eaa889b4453db078e0935752ef7ff0 Mon Sep 17 00:00:00 2001 From: laMudri Date: Sat, 21 May 2016 17:02:43 +0100 Subject: [PATCH 3/4] agda-prelude: 2014-09-27 -> 2016-04-18 --- pkgs/development/libraries/agda/agda-prelude/default.nix | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/pkgs/development/libraries/agda/agda-prelude/default.nix b/pkgs/development/libraries/agda/agda-prelude/default.nix index 9b67c5dbb5b..a2d29ff08dc 100644 --- a/pkgs/development/libraries/agda/agda-prelude/default.nix +++ b/pkgs/development/libraries/agda/agda-prelude/default.nix @@ -1,13 +1,13 @@ { stdenv, agda, fetchgit }: agda.mkDerivation (self: rec { - version = "d598f35d88596c5a63766a7188a0c0144e467c8c"; + version = "0dca24a81d417db2ae8fc871eccb7776f7eae952"; name = "agda-prelude-${version}"; src = fetchgit { url = "https://github.com/UlfNorell/agda-prelude.git"; rev = version; - sha256 = "bdcffb675d0ad1bafa2b47f581b6a9b90347ae739b6218f89f365fda2cc4f8c8"; + sha256 = "0gwfgvj96i1mx5v01bi46h567d1q1fbgvzv6z8zv91l2jhybwff5"; }; topSourceDirectories = [ "src" ]; @@ -18,6 +18,6 @@ agda.mkDerivation (self: rec { description = "Programming library for Agda"; license = stdenv.lib.licenses.mit; platforms = stdenv.lib.platforms.unix; - maintainers = with maintainers; [ fuuzetsu ]; + maintainers = with maintainers; [ fuuzetsu mudri ]; }; }) From 6343cf8ae7e593db58d476e36396ecb9670bd501 Mon Sep 17 00:00:00 2001 From: laMudri Date: Sat, 21 May 2016 23:24:49 +0100 Subject: [PATCH 4/4] Agda: marked some old packages as broken --- pkgs/development/libraries/agda/Agda-Sheaves/default.nix | 3 ++- .../libraries/agda/TotalParserCombinators/default.nix | 1 + pkgs/development/libraries/agda/agda-base/default.nix | 1 + pkgs/development/libraries/agda/bitvector/default.nix | 1 + 4 files changed, 5 insertions(+), 1 deletion(-) diff --git a/pkgs/development/libraries/agda/Agda-Sheaves/default.nix b/pkgs/development/libraries/agda/Agda-Sheaves/default.nix index 83066f5da63..b7634c36913 100644 --- a/pkgs/development/libraries/agda/Agda-Sheaves/default.nix +++ b/pkgs/development/libraries/agda/Agda-Sheaves/default.nix @@ -19,5 +19,6 @@ agda.mkDerivation (self: rec { 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 }; -}) \ No newline at end of file +}) diff --git a/pkgs/development/libraries/agda/TotalParserCombinators/default.nix b/pkgs/development/libraries/agda/TotalParserCombinators/default.nix index 8c299000065..226a39890c2 100644 --- a/pkgs/development/libraries/agda/TotalParserCombinators/default.nix +++ b/pkgs/development/libraries/agda/TotalParserCombinators/default.nix @@ -21,5 +21,6 @@ agda.mkDerivation (self: rec { license = stdenv.lib.licenses.mit; platforms = stdenv.lib.platforms.unix; maintainers = with maintainers; [ fuuzetsu ]; + broken = true; }; }) diff --git a/pkgs/development/libraries/agda/agda-base/default.nix b/pkgs/development/libraries/agda/agda-base/default.nix index cf73d7dea06..40eef932822 100644 --- a/pkgs/development/libraries/agda/agda-base/default.nix +++ b/pkgs/development/libraries/agda/agda-base/default.nix @@ -18,5 +18,6 @@ agda.mkDerivation (self: rec { 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/pkgs/development/libraries/agda/bitvector/default.nix b/pkgs/development/libraries/agda/bitvector/default.nix index 290a2f1206d..faa9fa5203c 100644 --- a/pkgs/development/libraries/agda/bitvector/default.nix +++ b/pkgs/development/libraries/agda/bitvector/default.nix @@ -19,5 +19,6 @@ agda.mkDerivation (self: rec { license = stdenv.lib.licenses.bsd3; platforms = stdenv.lib.platforms.unix; maintainers = with stdenv.lib.maintainers; [ fuuzetsu ]; + broken = true; }; })