From 229ef0ea8a94ee889790851264397e285624879b Mon Sep 17 00:00:00 2001 From: Alex Rice Date: Sun, 29 Dec 2019 12:11:14 +0000 Subject: [PATCH 01/14] TotalParserCombinators: remove broken package --- .../agda/TotalParserCombinators/contextfile | 259 ------------------ .../agda/TotalParserCombinators/default.nix | 26 -- pkgs/top-level/all-packages.nix | 2 - 3 files changed, 287 deletions(-) delete mode 100644 pkgs/development/libraries/agda/TotalParserCombinators/contextfile delete mode 100644 pkgs/development/libraries/agda/TotalParserCombinators/default.nix diff --git a/pkgs/development/libraries/agda/TotalParserCombinators/contextfile b/pkgs/development/libraries/agda/TotalParserCombinators/contextfile deleted file mode 100644 index 46743cba3b6..00000000000 --- a/pkgs/development/libraries/agda/TotalParserCombinators/contextfile +++ /dev/null @@ -1,259 +0,0 @@ - -Context: - -[Updated the code in response to changes to Agda. -Nils Anders Danielsson **20150319181310 - Ignore-this: 52b9ff613d7f10b0c8f45591a0759d07 -] - -[Rolled back most of "Updated the code in response to changes to Agda". -Nils Anders Danielsson **20150319101420 - Ignore-this: c2ea7bdf79848235fa3ea64ebda116eb - * One of the Agda changes has been reverted. -] - -[Removed an outdated comment. -Nils Anders Danielsson **20150217162945 - Ignore-this: 3ff7732335750305fe220e65693f0cbf -] - -[Added the simplification "nonempty (return x) → fail". -Nils Anders Danielsson **20150217161718 - Ignore-this: 56ad6a68c314446d8986a8c1b49655d0 -] - -[Added Nonempty.nonempty-return. -Nils Anders Danielsson **20150217161629 - Ignore-this: 68829d3f9a248272c46848daa05ccfe3 -] - -[Updated the copyright year range. -Nils Anders Danielsson **20150212154744 - Ignore-this: 3410a12ca1f9de825b00e692b136d500 -] - -[Updated the code in response to changes to Agda. -Nils Anders Danielsson **20150212152207 - Ignore-this: 683b5eeca5fa9c8490bceaf68c23a204 -] - -[Updated the copyright year range. -Nils Anders Danielsson **20141128223227 - Ignore-this: 31d3f5e4fdd6fbfad9758d9bfd0d3a3e -] - -[Updated the code in response to changes to Agda and the library. -Nils Anders Danielsson **20141128223205 - Ignore-this: 6392ec67aab2c534a7195abed55be47 -] - -[Updated code to reflect changes to Agda. -Nils Anders Danielsson **20140425121055 - Ignore-this: 54d80fd647cb897eef85f57e9172f7db -] - -[Workaround for (possible) Agda bug. -Nils Anders Danielsson **20140228200347 - Ignore-this: b17884ad17a3bdb7faff678622365a8 -] - -[Updated code to reflect changes to library API. -Nils Anders Danielsson **20130307134644 - Ignore-this: 50d070a22a6796b9acdf19d44ba5de16 -] - -[Updated code to reflect changes to Agda and the library API. -Nils Anders Danielsson **20130228122951 - Ignore-this: 761dc4d85683a59cc3667a8706c88093 -] - -[Turned _◇_ into a constructor. -Nils Anders Danielsson **20120316125431 - Ignore-this: 41b492c3106a575f28f146253f78a5ae -] - -[Updated code to reflect changes to Agda. -Nils Anders Danielsson **20120316125416 - Ignore-this: e77d817d8b391c3b4806119d10848eb3 -] - -[Updated code to reflect changes to Agda. -Nils Anders Danielsson **20120215103344 - Ignore-this: 467716429d5553cd122722108ea82a08 -] - -[Modified a comment. -Nils Anders Danielsson **20120215103319 - Ignore-this: e57d4911f692f8a96a80017d910efc5f -] - -[Updated code to reflect change to library API. -Nils Anders Danielsson **20111006160229 - Ignore-this: 5359da54e7e6e0f92983fa3ecaccebf3 -] - -[Updated code to reflect changes to Agda and the library API. -Nils Anders Danielsson **20111003170117 - Ignore-this: cbdd35172e372779e12642985cf17268 -] - -[Rolled back addition of inversion lemmas. -Nils Anders Danielsson **20110930150912 - Ignore-this: 9c9b083f0afcf95aaaa55a01d871274e -] - -[Added inversion lemmas, implemented other lemmas using these lemmas. -Nils Anders Danielsson **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 **20110517220158 - Ignore-this: ea9771a5014a25cb20afc2118638f8b5 -] - -[Updated code to reflect changes to Agda. -Nils Anders Danielsson **20110512124425 - Ignore-this: 97b154661679f574f6ab914583b14580 -] - -[Proved that many constructions preserve various preorders. -Nils Anders Danielsson **20110313012617 - Ignore-this: 8008efaff967c228448baa33b82edb81 -] - -[Updated code to reflect changes to library API. -Nils Anders Danielsson **20110313002106 - Ignore-this: 94799ba1ae411e59fd8c6c7eac3b8dfb -] - -[Simplified TotalRecognisers.LeftRecursion.MatchingParentheses. -Nils Anders Danielsson **20110118102159 - Ignore-this: 1e01a8092b0c0124979ffc5fe17a245c -] - -[Added TotalRecognisers.LeftRecursion.MatchingParentheses. -Nils Anders Danielsson **20110118102146 - Ignore-this: 13a3bc91425364e26c3047561655bb25 -] - -[Added a simplifying backend. -Nils Anders Danielsson **20101229012716 - Ignore-this: 9ac7ae21cd44c099633678a994fb9a3 -] - -[Fixed another "bug" in the deep simplifier. -Nils Anders Danielsson **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 **20101228235603 - Ignore-this: d39b8453a15089126261e098080223c6 -] - -[Deep simplification no longer adds casts. -Nils Anders Danielsson **20101228192850 - Ignore-this: 2ba016825adfa3a1e36922869eabfd39 -] - -[The first constructor in a simplified parser can no longer be a cast. -Nils Anders Danielsson **20101228175822 - Ignore-this: ce3e38cc0b9a096aa436655c9013ae97 -] - -[Modified the outline. -Nils Anders Danielsson **20101228173414 - Ignore-this: f8866e69f6d1a344e79fb6f708dfa4c -] - -[Added an example: a right recursive expression grammar. -Nils Anders Danielsson **20101228173159 - Ignore-this: 9a4d732b451cca08ba19aac5d115c678 -] - -[Rearranged the code. -Nils Anders Danielsson **20101228172209 - Ignore-this: 50fa29406d0f150669ff3feec4dbe513 -] - -[Renamed same-bag/set to (initial-bag-)cong. -Nils Anders Danielsson **20101228170706 - Ignore-this: dd3ce43d77dde74cc2428d2568dd2d30 -] - -[Added TotalParserCombinators.Force. -Nils Anders Danielsson **20101228153638 - Ignore-this: 3b6ff6ea20df0c1293494f06845d17eb -] - -[Proved that uses of subst can be erased. -Nils Anders Danielsson **20101228153621 - Ignore-this: f503ba495b923ae521718b6957167128 -] - -[The deep simplifier no longer skips layers. -Nils Anders Danielsson **20101228141138 - Ignore-this: 733a4a4a9aa0f890ad1740ecfc6a599f -] - -[Documented that the deep simplifier misses every second layer. -Nils Anders Danielsson **20101228121910 - Ignore-this: 8a0baf25b12f63f8748dbc1d16affacf -] - -[The simplifier now applies the token-bind rule more often. -Nils Anders Danielsson **20101227165413 - Ignore-this: 40132fa6f19602886bbe29aadd8a683c -] - -[Switched back to deep simplification, now with a proper proof. -Nils Anders Danielsson **20101227125434 - Ignore-this: ccc46e82f6f9c6c2a27ddb43d315f7dd -] - -[Simplified the soundness proof. -Nils Anders Danielsson **20101227123839 - Ignore-this: fb6826dd9836e34fc3bfdce2928ba13d -] - -[Made some _≈[_]P_ constructors conditionally coinductive. -Nils Anders Danielsson **20101227123827 - Ignore-this: f521f70475403697229051b62343a080 - + The structure of the soundness proof was also changed. -] - -[Unified And, AsymmetricChoice and Not. -Nils Anders Danielsson **20101225103109 - Ignore-this: 5ae8b80e1505fe6e707bb2307d22688c -] - -[Modified some comments. -Nils Anders Danielsson **20101225101051 - Ignore-this: e812d8c3e9720895c368f7a286f8315c -] - -[Modified a comment. -Nils Anders Danielsson **20101223202647 - Ignore-this: 16ea5dc01a4cbe0fe38714b2e4b7ff6 -] - -[Updated code to reflect changes to library API. -Nils Anders Danielsson **20101107162658 - Ignore-this: 9e38a10a9997c9825ece6ad9f871b673 -] - -[Added an alternative backend for TotalRecognisers.Simple. -Nils Anders Danielsson **20101020183743 - Ignore-this: a111a89e0c237e132b649561000f53d6 -] - -[TAG Code corresponding to the paper "Total Parser Combinators" (4). -Nils Anders Danielsson **20100928013815 - Ignore-this: 45ccc28373ed3974047315613eb14833 -] diff --git a/pkgs/development/libraries/agda/TotalParserCombinators/default.nix b/pkgs/development/libraries/agda/TotalParserCombinators/default.nix deleted file mode 100644 index 97cceebc1b6..00000000000 --- a/pkgs/development/libraries/agda/TotalParserCombinators/default.nix +++ /dev/null @@ -1,26 +0,0 @@ -{ 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; [ ]; - broken = true; - }; -}) diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index bbcdaf3a5a7..49fda77d53b 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -15152,8 +15152,6 @@ in pretty = callPackage ../development/libraries/agda/pretty { }; - TotalParserCombinators = callPackage ../development/libraries/agda/TotalParserCombinators { }; - ### DEVELOPMENT / LIBRARIES / JAVA commonsBcel = callPackage ../development/libraries/java/commons/bcel { }; From 99fa0644c9a3cf8f3a9d24c37895e0942259d898 Mon Sep 17 00:00:00 2001 From: Alex Rice Date: Sun, 29 Dec 2019 12:11:49 +0000 Subject: [PATCH 02/14] Agda-Sheaves: remove broken package --- .../libraries/agda/Agda-Sheaves/default.nix | 24 ------------------- pkgs/top-level/all-packages.nix | 2 -- 2 files changed, 26 deletions(-) delete mode 100644 pkgs/development/libraries/agda/Agda-Sheaves/default.nix diff --git a/pkgs/development/libraries/agda/Agda-Sheaves/default.nix b/pkgs/development/libraries/agda/Agda-Sheaves/default.nix deleted file mode 100644 index 513b79e6393..00000000000 --- a/pkgs/development/libraries/agda/Agda-Sheaves/default.nix +++ /dev/null @@ -1,24 +0,0 @@ -{ 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; [ ]; - broken = true; # replaced by constructive-sheaf-semantics - }; -}) diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index 49fda77d53b..6117b5fe7a5 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -15144,8 +15144,6 @@ in inherit (haskellPackages) ghcWithPackages; }; - AgdaSheaves = callPackage ../development/libraries/agda/Agda-Sheaves { }; - bitvector = callPackage ../development/libraries/agda/bitvector { }; categories = callPackage ../development/libraries/agda/categories { }; From 781a9273a8d998b78fcd47b4f5facaeab7fc8e14 Mon Sep 17 00:00:00 2001 From: Alex Rice Date: Sun, 29 Dec 2019 12:12:26 +0000 Subject: [PATCH 03/14] pretty: remove broken package --- .../libraries/agda/pretty/contextfile | 43 ------------------- .../libraries/agda/pretty/default.nix | 26 ----------- pkgs/top-level/all-packages.nix | 2 - 3 files changed, 71 deletions(-) delete mode 100644 pkgs/development/libraries/agda/pretty/contextfile delete mode 100644 pkgs/development/libraries/agda/pretty/default.nix diff --git a/pkgs/development/libraries/agda/pretty/contextfile b/pkgs/development/libraries/agda/pretty/contextfile deleted file mode 100644 index 2ea20153bbc..00000000000 --- a/pkgs/development/libraries/agda/pretty/contextfile +++ /dev/null @@ -1,43 +0,0 @@ - -Context: - -[Updated the code in response to a change to Agda. -Nils Anders Danielsson **20150319181428 - Ignore-this: f83c3dccfe25a2a5b9d0437d1dce0ec0 -] - -[Rolled back most of "Updated the code in response to changes to Agda". -Nils Anders Danielsson **20150319101413 - Ignore-this: 5a26cf9cf83d0d146cca0c15c857d20c - * One of the Agda changes has been reverted. -] - -[Updated the code in response to changes to Agda. -Nils Anders Danielsson **20150217101656 - Ignore-this: a12921aebbe0fb575ef391ba5789a391 -] - -[Modified the copyright year range. -Nils Anders Danielsson **20150213144338 - Ignore-this: 1d1b22457dd6dadcb47f5d7f3eea062 -] - -[Restored Grammar.Abstract and Grammar.Non-terminal. -Nils Anders Danielsson **20130727225031 - Ignore-this: ddccb15caa7a3c26e973997ffdb4eec1 -] - -[Modified the copyright year range. -Nils Anders Danielsson **20141128164015 - Ignore-this: b9c6dddc965738aa2a7670c4c18da67f -] - -[Updated the code to reflect changes to the library API. -Nils Anders Danielsson **20141128163950 - Ignore-this: 8094c47f23cef0fcc596ad0c18a92b56 -] - -[TAG Correct-by-Construction Pretty-Printing (2013-07-28) -Nils Anders Danielsson **20130727224432 - Ignore-this: 6aab9b2e6b638457767c8821f3c27cb4 -] diff --git a/pkgs/development/libraries/agda/pretty/default.nix b/pkgs/development/libraries/agda/pretty/default.nix deleted file mode 100644 index de4cfaa6637..00000000000 --- a/pkgs/development/libraries/agda/pretty/default.nix +++ /dev/null @@ -1,26 +0,0 @@ -{ 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; [ ]; - broken = true; # 2018-04-11 - }; -}) diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index 6117b5fe7a5..0fafb6d5642 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -15148,8 +15148,6 @@ in categories = callPackage ../development/libraries/agda/categories { }; - pretty = callPackage ../development/libraries/agda/pretty { }; - ### DEVELOPMENT / LIBRARIES / JAVA commonsBcel = callPackage ../development/libraries/java/commons/bcel { }; From 36840c5ff7813de552dedb894e4d9b6ae4e519a8 Mon Sep 17 00:00:00 2001 From: Alex Rice Date: Sun, 29 Dec 2019 12:13:23 +0000 Subject: [PATCH 04/14] categories: remove broken package --- .../libraries/agda/categories/default.nix | 24 ------------------- pkgs/top-level/all-packages.nix | 2 -- 2 files changed, 26 deletions(-) delete mode 100644 pkgs/development/libraries/agda/categories/default.nix diff --git a/pkgs/development/libraries/agda/categories/default.nix b/pkgs/development/libraries/agda/categories/default.nix deleted file mode 100644 index fef01ee9be7..00000000000 --- a/pkgs/development/libraries/agda/categories/default.nix +++ /dev/null @@ -1,24 +0,0 @@ -{ 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; [ ]; - broken = true; # doesn't work due to new agdastdlib, see #9471 - }; -}) diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index 0fafb6d5642..919c78bc00f 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -15146,8 +15146,6 @@ in bitvector = callPackage ../development/libraries/agda/bitvector { }; - categories = callPackage ../development/libraries/agda/categories { }; - ### DEVELOPMENT / LIBRARIES / JAVA commonsBcel = callPackage ../development/libraries/java/commons/bcel { }; From a519f22c03d65045996b77e89bb50c07728c85fd Mon Sep 17 00:00:00 2001 From: Alex Rice Date: Sun, 29 Dec 2019 12:13:52 +0000 Subject: [PATCH 05/14] bitvector: remove broken package --- .../libraries/agda/bitvector/default.nix | 24 ------------------- pkgs/top-level/all-packages.nix | 2 -- 2 files changed, 26 deletions(-) delete mode 100644 pkgs/development/libraries/agda/bitvector/default.nix diff --git a/pkgs/development/libraries/agda/bitvector/default.nix b/pkgs/development/libraries/agda/bitvector/default.nix deleted file mode 100644 index bf9798557b1..00000000000 --- a/pkgs/development/libraries/agda/bitvector/default.nix +++ /dev/null @@ -1,24 +0,0 @@ -{ 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; [ ]; - broken = true; - }; -}) diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index 919c78bc00f..f8dfe935f55 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -15144,8 +15144,6 @@ in inherit (haskellPackages) ghcWithPackages; }; - bitvector = callPackage ../development/libraries/agda/bitvector { }; - ### DEVELOPMENT / LIBRARIES / JAVA commonsBcel = callPackage ../development/libraries/java/commons/bcel { }; From 6cbaa256fab7df0d213be5caa14a6a29c9a47ed0 Mon Sep 17 00:00:00 2001 From: Alex Rice Date: Sun, 29 Dec 2019 12:25:43 +0000 Subject: [PATCH 06/14] agda-base: remove broken package --- .../libraries/agda/agda-base/default.nix | 23 ------------------- pkgs/top-level/all-packages.nix | 2 -- 2 files changed, 25 deletions(-) delete mode 100644 pkgs/development/libraries/agda/agda-base/default.nix diff --git a/pkgs/development/libraries/agda/agda-base/default.nix b/pkgs/development/libraries/agda/agda-base/default.nix deleted file mode 100644 index 678b3a28dc7..00000000000 --- a/pkgs/development/libraries/agda/agda-base/default.nix +++ /dev/null @@ -1,23 +0,0 @@ -{ 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; [ ]; - broken = true; # largely replaced by HoTT-Agda - }; -}) diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index f8dfe935f55..ea1a0791762 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -15134,8 +15134,6 @@ in inherit (haskellPackages) Agda; }; - agdaBase = callPackage ../development/libraries/agda/agda-base { }; - agdaIowaStdlib = callPackage ../development/libraries/agda/agda-iowa-stdlib { }; agdaPrelude = callPackage ../development/libraries/agda/agda-prelude { }; From d30e2468e0c7875d3d4d47404f52647ccea76fcf Mon Sep 17 00:00:00 2001 From: Alex Rice Date: Sun, 29 Dec 2019 12:14:16 +0000 Subject: [PATCH 07/14] agda: rework builder --- doc/languages-frameworks/agda.section.md | 96 ++++++++++++ doc/languages-frameworks/index.xml | 1 + pkgs/build-support/agda/default.nix | 141 ++++++++---------- .../libraries/agda/agda-prelude/default.nix | 16 +- .../default.nix | 12 +- .../default.nix | 12 +- pkgs/top-level/agda-packages.nix | 24 +++ pkgs/top-level/all-packages.nix | 13 +- pkgs/top-level/release.nix | 1 + 9 files changed, 205 insertions(+), 111 deletions(-) create mode 100644 doc/languages-frameworks/agda.section.md rename pkgs/development/libraries/agda/{agda-iowa-stdlib => iowa-stdlib}/default.nix (71%) rename pkgs/development/libraries/agda/{agda-stdlib => standard-library}/default.nix (74%) create mode 100644 pkgs/top-level/agda-packages.nix diff --git a/doc/languages-frameworks/agda.section.md b/doc/languages-frameworks/agda.section.md new file mode 100644 index 00000000000..7a5dc767b7c --- /dev/null +++ b/doc/languages-frameworks/agda.section.md @@ -0,0 +1,96 @@ +--- +title: Agda +author: Alex Rice (alexarice) +date: 2020-01-06 +--- +# Agda + +## How to use Agda + +Agda can be installed from `agda`: +``` +$ nix-env -iA agda +``` + +To use agda with libraries, the `agda.withPackages` function can be used. This function either takes: ++ A list of packages, ++ or a function which returns a list of packages when given the `agdaPackages` attribute set, ++ or an attribute set containing a list of packages and a GHC derivation for compilation (see below). + +For example, suppose we wanted a version of agda which has access to the standard library. This can be obtained with the expressions: + +``` +agda.withPackages [ agdaPackages.standard-library ] +``` + +or + +``` +agda.withPackages (p: [ p.standard-library ]) +``` + +or can be called as in the [Compiling Agda](#compiling-agda) section. + +If you want to use a library in your home directory (for instance if it is a development version) then typecheck it manually (using `agda.withPackages` if necessary) and then override the `src` attribute of the package to point to your local repository. + +Agda will not by default use these libraries. To tell agda to use the library we have some options: +- Call `agda` with the library flag: +``` +$ agda -l standard-library -i . MyFile.agda +``` +- Write a `my-library.agda-lib` file for the project you are working on which may look like: +``` +name: my-library +include: . +depends: standard-library +``` +- Create the file `~/.agda/defaults` and add any libraries you want to use by default. + +More information can be found in the [official Agda documentation on library management](https://agda.readthedocs.io/en/v2.6.1/tools/package-system.html). + +## Compiling Agda +Agda modules can be compiled with the `--compile` flag. A version of `ghc` with `ieee` is made available to the Agda program via the `--with-compiler` flag. +This can be overridden by a different version of `ghc` as follows: + +``` +agda.withPackages { + pkgs = [ ... ]; + ghc = haskell.compiler.ghcHEAD; +} +``` + +## Writing Agda packages +To write a nix derivation for an agda library, first check that the library has a `*.agda-lib` file. + +A derivation can then be written using `agdaPackages.mkDerivation`. This has similar arguments to `stdenv.mkDerivation` with the following additions: ++ `everythingFile` can be used to specify the location of the `Everything.agda` file, defaulting to `./Everything.agda`. If this file does not exist then either it should be patched in or the `buildPhase` should be overridden (see below). ++ `libraryName` should be the name that appears in the `*.agda-lib` file, defaulting to `pname`. ++ `libraryFile` should be the file name of the `*.agda-lib` file, defaulting to `${libraryName}.agda-lib`. + +The build phase for `agdaPackages.mkDerivation` simply runs `agda` on the `Everything.agda` file. If something else is needed to build the package (e.g. `make`) then the `buildPhase` should be overridden (or a `preBuild` or `configurePhase` can be used if there are steps that need to be done prior to checking the `Everything.agda` file). `agda` and the Agda libraries contained in `buildInputs` are made available during the build phase. The install phase simply copies all `.agda`, `.agdai` and `.agda-lib` files to the output directory. Again, this can be overridden. + +To add an agda package to `nixpkgs`, the derivation should be written to `pkgs/development/libraries/agda/${library-name}/` and an entry should be added to `pkgs/top-level/agda-packages.nix`. Here it is called in a scope with access to all other agda libraries, so the top line of the `default.nix` can look like: +``` +{ mkDerivation, standard-library, fetchFromGitHub }: +``` +and `mkDerivation` should be called instead of `agdaPackages.mkDerivation`. Here is an example skeleton derivation for iowa-stdlib: + +``` +mkDerivation { + version = "1.5.0"; + pname = "iowa-stdlib"; + + src = ... + + libraryFile = ""; + libraryName = "IAL-1.3"; + + buildPhase = '' + patchShebangs find-deps.sh + make + ''; +} +``` +This library has a file called `.agda-lib`, and so we give an empty string to `libraryFile` as nothing precedes `.agda-lib` in the filename. This file contains `name: IAL-1.3`, and so we let `libraryName = "IAL-1.3"`. This library does not use an `Everything.agda` file and instead has a Makefile, so there is no need to set `everythingFile` and we set a custom `buildPhase`. + +When writing an agda package it is essential to make sure that no `.agda-lib` file gets added to the store as a single file (for example by using `writeText`). This causes agda to think that the nix store is a agda library and it will attempt to write to it whenever it typechecks something. See [https://github.com/agda/agda/issues/4613](https://github.com/agda/agda/issues/4613). diff --git a/doc/languages-frameworks/index.xml b/doc/languages-frameworks/index.xml index 9364c764bbf..97202751f7d 100644 --- a/doc/languages-frameworks/index.xml +++ b/doc/languages-frameworks/index.xml @@ -5,6 +5,7 @@ The standard build environment makes it easy to build typical Autotools-based packages with very little code. Any other kind of package can be accomodated by overriding the appropriate phases of stdenv. However, there are specialised functions in Nixpkgs to easily build packages for other programming languages, such as Perl or Haskell. These are described in this chapter. + diff --git a/pkgs/build-support/agda/default.nix b/pkgs/build-support/agda/default.nix index 0d054eaa546..205aff55573 100644 --- a/pkgs/build-support/agda/default.nix +++ b/pkgs/build-support/agda/default.nix @@ -1,90 +1,71 @@ -# Builder for Agda packages. Mostly inspired by the cabal builder. +# Builder for Agda packages. -{ stdenv, Agda, glibcLocales -, writeShellScriptBin -, extension ? (self: super: {}) -}: +{ stdenv, lib, self, Agda, runCommandNoCC, makeWrapper, writeText, mkShell, ghcWithPackages }: -with stdenv.lib.strings; +with lib.strings; let - defaults = self : { - # There is no Hackage for Agda so we require src. - inherit (self) src name; - - isAgdaPackage = true; - - buildInputs = [ Agda ] ++ self.buildDepends; - buildDepends = []; - - buildDependsAgda = stdenv.lib.filter - (dep: dep ? isAgdaPackage && dep.isAgdaPackage) - self.buildDepends; - buildDependsAgdaShareAgda = map (x: x + "/share/agda") self.buildDependsAgda; - - # Not much choice here ;) - LANG = "en_US.UTF-8"; - LOCALE_ARCHIVE = stdenv.lib.optionalString - stdenv.isLinux - "${glibcLocales}/lib/locale/locale-archive"; - - everythingFile = "Everything.agda"; - - propagatedBuildInputs = self.buildDependsAgda; - propagatedUserEnvPkgs = self.buildDependsAgda; - - # Immediate source directories under which modules can be found. - sourceDirectories = [ ]; - - # This is used if we have a top-level element that only serves - # as the container for the source and we only care about its - # contents. The directories put here will have their - # *contents* copied over as opposed to sourceDirectories which - # would make a direct copy of the whole thing. - topSourceDirectories = [ "src" ]; - - # FIXME: `dirOf self.everythingFile` is what we really want, not hardcoded "./" - includeDirs = self.buildDependsAgdaShareAgda - ++ self.sourceDirectories ++ self.topSourceDirectories - ++ [ "." ]; - buildFlags = stdenv.lib.concatMap (x: ["-i" x]) self.includeDirs; - - agdaWithArgs = "${Agda}/bin/agda ${toString self.buildFlags}"; - - buildPhase = '' - runHook preBuild - ${self.agdaWithArgs} ${self.everythingFile} - runHook postBuild + withPackages' = { + pkgs, + ghc ? ghcWithPackages (p: with p; [ ieee ]) + }: let + pkgs' = if builtins.isList pkgs then pkgs else pkgs self; + library-file = writeText "libraries" '' + ${(concatMapStringsSep "\n" (p: "${p}/${p.libraryFile}") pkgs')} ''; + pname = "agdaWithPackages"; + version = Agda.version; + in runCommandNoCC "${pname}-${version}" { + inherit pname version; + nativeBuildInputs = [ makeWrapper ]; + passthru.unwrapped = Agda; + } '' + mkdir -p $out/bin + makeWrapper ${Agda}/bin/agda $out/bin/agda \ + --add-flags "--with-compiler=${ghc}/bin/ghc" \ + --add-flags "--library-file=${library-file}" \ + --add-flags "--local-interfaces" + makeWrapper ${Agda}/bin/agda-mode $out/bin/agda-mode + ''; # Local interfaces has been added for now: See https://github.com/agda/agda/issues/4526 - installPhase = let - srcFiles = self.sourceDirectories - ++ map (x: x + "/*") self.topSourceDirectories; - in '' - runHook preInstall - mkdir -p $out/share/agda - cp -pR ${concatStringsSep " " srcFiles} $out/share/agda - runHook postInstall - ''; + withPackages = arg: if builtins.isAttrs arg then withPackages' arg else withPackages' { pkgs = arg; }; - passthru = { - env = stdenv.mkDerivation { - name = "interactive-${self.name}"; - inherit (self) LANG LOCALE_ARCHIVE; - AGDA_PACKAGE_PATH = concatMapStrings (x: x + ":") self.buildDependsAgdaShareAgda; - buildInputs = let - # Makes a wrapper available to the user. Very useful in - # nix-shell where all dependencies are -i'd. - agdaWrapper = writeShellScriptBin "agda" '' - exec ${self.agdaWithArgs} "$@" - ''; - in [agdaWrapper] ++ self.buildDepends; + + defaults = + { pname + , buildInputs ? [] + , everythingFile ? "./Everything.agda" + , libraryName ? pname + , libraryFile ? "${libraryName}.agda-lib" + , buildPhase ? null + , installPhase ? null + , ... + }: let + agdaWithArgs = withPackages (builtins.filter (p: p ? isAgdaDerivation) buildInputs); + in + { + inherit libraryName libraryFile; + + isAgdaDerivation = true; + + buildInputs = buildInputs ++ [ agdaWithArgs ]; + + buildPhase = if buildPhase != null then buildPhase else '' + runHook preBuild + agda -i ${dirOf everythingFile} ${everythingFile} + runHook postBuild + ''; + + installPhase = if installPhase != null then installPhase else '' + runHook preInstall + mkdir -p $out + find \( -name '*.agda' -or -name '*.agdai' -or -name '*.agda-lib' \) -exec cp -p --parents -t "$out" {} + + runHook postInstall + ''; }; - }; - }; in -{ mkDerivation = args: let - super = defaults self // args self; - self = super // extension self super; - in stdenv.mkDerivation self; +{ + mkDerivation = args: stdenv.mkDerivation (args // defaults args); + + inherit withPackages withPackages'; } diff --git a/pkgs/development/libraries/agda/agda-prelude/default.nix b/pkgs/development/libraries/agda/agda-prelude/default.nix index 86f21ad9b19..1709ce314d9 100644 --- a/pkgs/development/libraries/agda/agda-prelude/default.nix +++ b/pkgs/development/libraries/agda/agda-prelude/default.nix @@ -1,16 +1,16 @@ -{ stdenv, agda, fetchgit }: +{ stdenv, mkDerivation, fetchFromGitHub }: -agda.mkDerivation (self: rec { +mkDerivation rec { version = "eacc961c2c312b7443109a7872f99d55557df317"; - name = "agda-prelude-${version}"; + pname = "agda-prelude"; - src = fetchgit { - url = "https://github.com/UlfNorell/agda-prelude.git"; + src = fetchFromGitHub { + owner = "UlfNorell"; + repo = "agda-prelude"; rev = version; sha256 = "0iql67hb1q0fn8dwkcx07brkdkxqfqrsbwjy71ndir0k7qzw7qv2"; }; - topSourceDirectories = [ "src" ]; everythingFile = "src/Prelude.agda"; meta = with stdenv.lib; { @@ -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; [ mudri ]; + maintainers = with maintainers; [ mudri alexarice ]; }; -}) +} diff --git a/pkgs/development/libraries/agda/agda-iowa-stdlib/default.nix b/pkgs/development/libraries/agda/iowa-stdlib/default.nix similarity index 71% rename from pkgs/development/libraries/agda/agda-iowa-stdlib/default.nix rename to pkgs/development/libraries/agda/iowa-stdlib/default.nix index 23013bfbc32..9cda6ceec13 100644 --- a/pkgs/development/libraries/agda/agda-iowa-stdlib/default.nix +++ b/pkgs/development/libraries/agda/iowa-stdlib/default.nix @@ -1,8 +1,8 @@ -{ stdenv, agda, fetchFromGitHub }: +{ stdenv, mkDerivation, fetchFromGitHub }: -agda.mkDerivation (self: rec { +mkDerivation (rec { version = "1.5.0"; - name = "agda-iowa-stdlib-${version}"; + pname = "iowa-stdlib"; src = fetchFromGitHub { owner = "cedille"; @@ -11,7 +11,9 @@ agda.mkDerivation (self: rec { sha256 = "0dlis6v6nzbscf713cmwlx8h9n2gxghci8y21qak3hp18gkxdp0g"; }; - sourceDirectories = [ "./." ]; + libraryFile = ""; + libraryName = "IAL-1.3"; + buildPhase = '' patchShebangs find-deps.sh make @@ -22,6 +24,6 @@ agda.mkDerivation (self: rec { description = "Agda standard library developed at Iowa"; license = stdenv.lib.licenses.free; platforms = stdenv.lib.platforms.unix; - maintainers = with stdenv.lib.maintainers; [ ]; + maintainers = with stdenv.lib.maintainers; [ alexarice ]; }; }) diff --git a/pkgs/development/libraries/agda/agda-stdlib/default.nix b/pkgs/development/libraries/agda/standard-library/default.nix similarity index 74% rename from pkgs/development/libraries/agda/agda-stdlib/default.nix rename to pkgs/development/libraries/agda/standard-library/default.nix index 6647677f71c..6d85d560a9b 100644 --- a/pkgs/development/libraries/agda/agda-stdlib/default.nix +++ b/pkgs/development/libraries/agda/standard-library/default.nix @@ -1,8 +1,8 @@ -{ stdenv, agda, fetchFromGitHub, ghcWithPackages }: +{ stdenv, mkDerivation, fetchFromGitHub, ghcWithPackages }: -agda.mkDerivation (self: rec { +mkDerivation rec { + pname = "standard-library"; version = "1.1"; - name = "agda-stdlib-${version}"; src = fetchFromGitHub { repo = "agda-stdlib"; @@ -16,13 +16,11 @@ agda.mkDerivation (self: rec { runhaskell GenerateEverything.hs ''; - topSourceDirectories = [ "src" ]; - meta = with stdenv.lib; { homepage = "https://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; - maintainers = with maintainers; [ jwiegley mudri ]; + maintainers = with maintainers; [ jwiegley mudri alexarice ]; }; -}) +} diff --git a/pkgs/top-level/agda-packages.nix b/pkgs/top-level/agda-packages.nix new file mode 100644 index 00000000000..5bd57b5dec8 --- /dev/null +++ b/pkgs/top-level/agda-packages.nix @@ -0,0 +1,24 @@ +{ pkgs, lib, callPackage, newScope, Agda }: + +let + mkAgdaPackages = Agda: lib.makeScope newScope (mkAgdaPackages' Agda); + mkAgdaPackages' = Agda: self: let + callPackage = self.callPackage; + inherit (callPackage ../build-support/agda { + inherit Agda self; + inherit (pkgs.haskellPackages) ghcWithPackages; + }) withPackages mkDerivation; + in { + inherit mkDerivation; + + agda = withPackages [] // { inherit withPackages; }; + + standard-library = callPackage ../development/libraries/agda/standard-library { + inherit (pkgs.haskellPackages) ghcWithPackages; + }; + + iowa-stdlib = callPackage ../development/libraries/agda/iowa-stdlib { }; + + agda-prelude = callPackage ../development/libraries/agda/agda-prelude { }; + }; +in mkAgdaPackages Agda diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index ea1a0791762..8c1414803ee 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -15128,19 +15128,10 @@ in ### DEVELOPMENT / LIBRARIES / AGDA - agda = callPackage ../build-support/agda { - glibcLocales = if pkgs.stdenv.isLinux then pkgs.glibcLocales else null; - extension = self : super : { }; + agdaPackages = callPackage ./agda-packages.nix { inherit (haskellPackages) Agda; }; - - agdaIowaStdlib = callPackage ../development/libraries/agda/agda-iowa-stdlib { }; - - agdaPrelude = callPackage ../development/libraries/agda/agda-prelude { }; - - AgdaStdlib = callPackage ../development/libraries/agda/agda-stdlib { - inherit (haskellPackages) ghcWithPackages; - }; + agda = agdaPackages.agda; ### DEVELOPMENT / LIBRARIES / JAVA diff --git a/pkgs/top-level/release.nix b/pkgs/top-level/release.nix index e0723523f4e..60a4a679f16 100644 --- a/pkgs/top-level/release.nix +++ b/pkgs/top-level/release.nix @@ -181,6 +181,7 @@ let haskell.compiler = packagePlatforms pkgs.haskell.compiler; haskellPackages = packagePlatforms pkgs.haskellPackages; idrisPackages = packagePlatforms pkgs.idrisPackages; + agdaPackages = packagePlatforms pkgs.agdaPackages; tests = packagePlatforms pkgs.tests; From c2814be3a329288a391c9436493ab6dcaa36f3ce Mon Sep 17 00:00:00 2001 From: Alex Rice Date: Sun, 29 Dec 2019 13:20:59 +0000 Subject: [PATCH 08/14] agda-prelude: update --- .../libraries/agda/agda-prelude/default.nix | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/pkgs/development/libraries/agda/agda-prelude/default.nix b/pkgs/development/libraries/agda/agda-prelude/default.nix index 1709ce314d9..bdc1b27cef4 100644 --- a/pkgs/development/libraries/agda/agda-prelude/default.nix +++ b/pkgs/development/libraries/agda/agda-prelude/default.nix @@ -1,23 +1,32 @@ { stdenv, mkDerivation, fetchFromGitHub }: mkDerivation rec { - version = "eacc961c2c312b7443109a7872f99d55557df317"; + version = "compat-2.6.0"; pname = "agda-prelude"; src = fetchFromGitHub { owner = "UlfNorell"; repo = "agda-prelude"; rev = version; - sha256 = "0iql67hb1q0fn8dwkcx07brkdkxqfqrsbwjy71ndir0k7qzw7qv2"; + sha256 = "0brg61qrf8izqav80qpx77dbdxvlnsxyy0v7hmlrmhg68b5lp38y"; }; - everythingFile = "src/Prelude.agda"; + preConfigure = '' + cd test + make everything + mv Everything.agda .. + cd .. + ''; + + everythingFile = "./Everything.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; + # broken since Agda 2.6.1 + broken = true; maintainers = with maintainers; [ mudri alexarice ]; }; } From 6c1cdedb6d6203aff485422c1b84cde6df7add57 Mon Sep 17 00:00:00 2001 From: Alex Rice Date: Sun, 29 Dec 2019 17:22:00 +0000 Subject: [PATCH 09/14] agda-categories: init at 0.1 --- .../agda/agda-categories/default.nix | 28 +++++++++++++++++++ pkgs/top-level/agda-packages.nix | 2 ++ 2 files changed, 30 insertions(+) create mode 100644 pkgs/development/libraries/agda/agda-categories/default.nix diff --git a/pkgs/development/libraries/agda/agda-categories/default.nix b/pkgs/development/libraries/agda/agda-categories/default.nix new file mode 100644 index 00000000000..11f8d71f1cd --- /dev/null +++ b/pkgs/development/libraries/agda/agda-categories/default.nix @@ -0,0 +1,28 @@ +{ lib, mkDerivation, fetchFromGitHub, standard-library }: + +mkDerivation rec { + version = "0.1"; + pname = "agda-categories"; + + src = fetchFromGitHub { + owner = "agda"; + repo = "agda-categories"; + rev = "release/v${version}"; + sha256 = "0m4pjy92jg6zfziyv0bxv5if03g8k4413ld8c3ii2xa8bzfn04m2"; + }; + + buildInputs = [ standard-library ]; + + meta = with lib; { + inherit (src.meta) homepage; + description = "A new Categories library"; + license = licenses.bsd3; + platforms = platforms.unix; + # agda categories takes a lot of memory to build. + # This can be removed if this is eventually fixed upstream. + hydraPlatforms = []; + # Waiting for release 0.2 for this to work + broken = true; + maintainers = with maintainers; [ alexarice ]; + }; +} diff --git a/pkgs/top-level/agda-packages.nix b/pkgs/top-level/agda-packages.nix index 5bd57b5dec8..3f4d7db0c7c 100644 --- a/pkgs/top-level/agda-packages.nix +++ b/pkgs/top-level/agda-packages.nix @@ -20,5 +20,7 @@ let iowa-stdlib = callPackage ../development/libraries/agda/iowa-stdlib { }; agda-prelude = callPackage ../development/libraries/agda/agda-prelude { }; + + agda-categories = callPackage ../development/libraries/agda/agda-categories { }; }; in mkAgdaPackages Agda From a7cd372a3e913bf526e4f72847ad1bbda23cc811 Mon Sep 17 00:00:00 2001 From: Alex Rice Date: Sun, 5 Jan 2020 23:34:35 +0000 Subject: [PATCH 10/14] agda.standard-library: 1.1 -> 1.3 --- pkgs/development/libraries/agda/standard-library/default.nix | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/pkgs/development/libraries/agda/standard-library/default.nix b/pkgs/development/libraries/agda/standard-library/default.nix index 6d85d560a9b..1b76aefe6fc 100644 --- a/pkgs/development/libraries/agda/standard-library/default.nix +++ b/pkgs/development/libraries/agda/standard-library/default.nix @@ -2,13 +2,13 @@ mkDerivation rec { pname = "standard-library"; - version = "1.1"; + version = "1.3"; src = fetchFromGitHub { repo = "agda-stdlib"; owner = "agda"; rev = "v${version}"; - sha256 = "190bxsy92ffmvwpmyyg3lxs91vyss2z25rqz1w79gkj56484cy64"; + sha256 = "18kl20z3bjfgx5m3nvrdj5776qmpi7jl2p12pqybsls2lf86m0d5"; }; nativeBuildInputs = [ (ghcWithPackages (self : [ self.filemanip ])) ]; From 11750651110696c4da6357adeea62d452ef6837c Mon Sep 17 00:00:00 2001 From: Alex Rice Date: Sat, 21 Mar 2020 11:58:44 +0000 Subject: [PATCH 11/14] agda.iowa-stdlib: mark broken --- pkgs/development/libraries/agda/iowa-stdlib/default.nix | 2 ++ 1 file changed, 2 insertions(+) diff --git a/pkgs/development/libraries/agda/iowa-stdlib/default.nix b/pkgs/development/libraries/agda/iowa-stdlib/default.nix index 9cda6ceec13..6fa45f58e78 100644 --- a/pkgs/development/libraries/agda/iowa-stdlib/default.nix +++ b/pkgs/development/libraries/agda/iowa-stdlib/default.nix @@ -24,6 +24,8 @@ mkDerivation (rec { description = "Agda standard library developed at Iowa"; license = stdenv.lib.licenses.free; platforms = stdenv.lib.platforms.unix; + # broken since Agda 2.6.1 + broken = true; maintainers = with stdenv.lib.maintainers; [ alexarice ]; }; }) From b78a5a0e79808550e450d8c5aba142309fe15fa3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Manuel=20B=C3=A4renz?= Date: Sun, 19 Apr 2020 20:01:37 +0200 Subject: [PATCH 12/14] agda: Added test --- nixos/tests/agda.nix | 41 +++++++++++++++++++++++++++++++++++++++ nixos/tests/all-tests.nix | 1 + 2 files changed, 42 insertions(+) create mode 100644 nixos/tests/agda.nix diff --git a/nixos/tests/agda.nix b/nixos/tests/agda.nix new file mode 100644 index 00000000000..e158999e57d --- /dev/null +++ b/nixos/tests/agda.nix @@ -0,0 +1,41 @@ +import ./make-test-python.nix ({ pkgs, ... }: + +let + hello-world = pkgs.writeText "hello-world" '' + open import IO + + main = run(putStrLn "Hello World!") + ''; +in +{ + name = "agda"; + meta = with pkgs.stdenv.lib.maintainers; { + maintainers = [ alexarice turion ]; + }; + + machine = { pkgs, ... }: { + environment.systemPackages = [ + (pkgs.agda.withPackages { + pkgs = p: [ p.standard-library ]; + }) + ]; + virtualisation.memorySize = 2000; # Agda uses a lot of memory + }; + + testScript = '' + # Minimal script that typechecks + machine.succeed("touch TestEmpty.agda") + machine.succeed("agda TestEmpty.agda") + + # Minimal script that actually uses the standard library + machine.succeed('echo "import IO" > TestIO.agda') + machine.succeed("agda -l standard-library -i . TestIO.agda") + + # # Hello world + machine.succeed( + "cp ${hello-world} HelloWorld.agda" + ) + machine.succeed("agda -l standard-library -i . -c HelloWorld.agda") + ''; +} +) diff --git a/nixos/tests/all-tests.nix b/nixos/tests/all-tests.nix index cbfdf3ad9c2..c4d7e38f54e 100644 --- a/nixos/tests/all-tests.nix +++ b/nixos/tests/all-tests.nix @@ -23,6 +23,7 @@ in { _3proxy = handleTest ./3proxy.nix {}; acme = handleTest ./acme.nix {}; + agda = handleTest ./agda.nix {}; atd = handleTest ./atd.nix {}; automysqlbackup = handleTest ./automysqlbackup.nix {}; avahi = handleTest ./avahi.nix {}; From 43fb96efe89c2215a58b576ee70e8b8ca0413897 Mon Sep 17 00:00:00 2001 From: Keshav Kini Date: Sat, 2 May 2020 13:25:18 -0700 Subject: [PATCH 13/14] iowa-stdlib: update homepage URL The old homepage URL, which was hosted inside the old SVN server, isn't publicly accessible anymore. Since the project has officially moved to github, it seems better to set the github repo as the homepage. --- pkgs/development/libraries/agda/iowa-stdlib/default.nix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pkgs/development/libraries/agda/iowa-stdlib/default.nix b/pkgs/development/libraries/agda/iowa-stdlib/default.nix index 6fa45f58e78..3cd1921be2d 100644 --- a/pkgs/development/libraries/agda/iowa-stdlib/default.nix +++ b/pkgs/development/libraries/agda/iowa-stdlib/default.nix @@ -20,7 +20,7 @@ mkDerivation (rec { ''; meta = { - homepage = "https://svn.divms.uiowa.edu/repos/clc/projects/agda/lib/"; + homepage = "https://github.com/cedille/ial"; description = "Agda standard library developed at Iowa"; license = stdenv.lib.licenses.free; platforms = stdenv.lib.platforms.unix; From 8ee4c3698c573e76cdb6617356ef21a3013a18ae Mon Sep 17 00:00:00 2001 From: Alex Rice Date: Thu, 14 May 2020 20:50:00 +0100 Subject: [PATCH 14/14] Agda: Add turion as maintainer --- pkgs/development/libraries/agda/agda-categories/default.nix | 2 +- pkgs/development/libraries/agda/agda-prelude/default.nix | 2 +- pkgs/development/libraries/agda/iowa-stdlib/default.nix | 2 +- pkgs/development/libraries/agda/standard-library/default.nix | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/pkgs/development/libraries/agda/agda-categories/default.nix b/pkgs/development/libraries/agda/agda-categories/default.nix index 11f8d71f1cd..9eb68b5a64a 100644 --- a/pkgs/development/libraries/agda/agda-categories/default.nix +++ b/pkgs/development/libraries/agda/agda-categories/default.nix @@ -23,6 +23,6 @@ mkDerivation rec { hydraPlatforms = []; # Waiting for release 0.2 for this to work broken = true; - maintainers = with maintainers; [ alexarice ]; + maintainers = with maintainers; [ alexarice turion ]; }; } diff --git a/pkgs/development/libraries/agda/agda-prelude/default.nix b/pkgs/development/libraries/agda/agda-prelude/default.nix index bdc1b27cef4..2bec10c02dd 100644 --- a/pkgs/development/libraries/agda/agda-prelude/default.nix +++ b/pkgs/development/libraries/agda/agda-prelude/default.nix @@ -27,6 +27,6 @@ mkDerivation rec { platforms = stdenv.lib.platforms.unix; # broken since Agda 2.6.1 broken = true; - maintainers = with maintainers; [ mudri alexarice ]; + maintainers = with maintainers; [ mudri alexarice turion ]; }; } diff --git a/pkgs/development/libraries/agda/iowa-stdlib/default.nix b/pkgs/development/libraries/agda/iowa-stdlib/default.nix index 3cd1921be2d..55cd6a742e5 100644 --- a/pkgs/development/libraries/agda/iowa-stdlib/default.nix +++ b/pkgs/development/libraries/agda/iowa-stdlib/default.nix @@ -26,6 +26,6 @@ mkDerivation (rec { platforms = stdenv.lib.platforms.unix; # broken since Agda 2.6.1 broken = true; - maintainers = with stdenv.lib.maintainers; [ alexarice ]; + maintainers = with stdenv.lib.maintainers; [ alexarice turion ]; }; }) diff --git a/pkgs/development/libraries/agda/standard-library/default.nix b/pkgs/development/libraries/agda/standard-library/default.nix index 1b76aefe6fc..4bff585ac3a 100644 --- a/pkgs/development/libraries/agda/standard-library/default.nix +++ b/pkgs/development/libraries/agda/standard-library/default.nix @@ -21,6 +21,6 @@ mkDerivation 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 mudri alexarice ]; + maintainers = with maintainers; [ jwiegley mudri alexarice turion ]; }; }