about summary refs log tree commit diff
path: root/nixpkgs/pkgs/development/libraries/agda
diff options
context:
space:
mode:
Diffstat (limited to 'nixpkgs/pkgs/development/libraries/agda')
-rw-r--r--nixpkgs/pkgs/development/libraries/agda/agda-categories/default.nix23
-rw-r--r--nixpkgs/pkgs/development/libraries/agda/agda-prelude/default.nix28
-rw-r--r--nixpkgs/pkgs/development/libraries/agda/agdarsec/default.nix28
-rw-r--r--nixpkgs/pkgs/development/libraries/agda/cubical/default.nix33
-rw-r--r--nixpkgs/pkgs/development/libraries/agda/functional-linear-algebra/default.nix30
-rw-r--r--nixpkgs/pkgs/development/libraries/agda/generic/default.nix33
-rw-r--r--nixpkgs/pkgs/development/libraries/agda/iowa-stdlib/default.nix31
-rw-r--r--nixpkgs/pkgs/development/libraries/agda/standard-library/default.nix30
8 files changed, 236 insertions, 0 deletions
diff --git a/nixpkgs/pkgs/development/libraries/agda/agda-categories/default.nix b/nixpkgs/pkgs/development/libraries/agda/agda-categories/default.nix
new file mode 100644
index 000000000000..267ee041bdc1
--- /dev/null
+++ b/nixpkgs/pkgs/development/libraries/agda/agda-categories/default.nix
@@ -0,0 +1,23 @@
+{ lib, mkDerivation, fetchFromGitHub, standard-library }:
+
+mkDerivation rec {
+  version = "0.1.7.1";
+  pname = "agda-categories";
+
+  src = fetchFromGitHub {
+    owner = "agda";
+    repo = "agda-categories";
+    rev = "v${version}";
+    sha256 = "1acb693ad2nrmnn6jxsyrlkc0di3kk2ksj2w9wnyfxrgvfsil7rn";
+  };
+
+  buildInputs = [ standard-library ];
+
+  meta = with lib; {
+    inherit (src.meta) homepage;
+    description = "A new Categories library";
+    license = licenses.bsd3;
+    platforms = platforms.unix;
+    maintainers = with maintainers; [ alexarice turion ];
+  };
+}
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..693bad67d08e
--- /dev/null
+++ b/nixpkgs/pkgs/development/libraries/agda/agda-prelude/default.nix
@@ -0,0 +1,28 @@
+{ lib, mkDerivation, fetchFromGitHub }:
+
+mkDerivation rec {
+  version = "compat-2.6.2";
+  pname = "agda-prelude";
+
+  src = fetchFromGitHub {
+    owner = "UlfNorell";
+    repo = "agda-prelude";
+    rev = version;
+    sha256 = "0j2nip5fbn61fpkm3qz4dlazl4mzdv7qlgw9zm15bkcvaila0h14";
+  };
+
+  preConfigure = ''
+    cd test
+    make everything
+    mv Everything.agda ..
+    cd ..
+  '';
+
+  meta = with lib; {
+    homepage = "https://github.com/UlfNorell/agda-prelude";
+    description = "Programming library for Agda";
+    license = lib.licenses.mit;
+    platforms = lib.platforms.unix;
+    maintainers = with maintainers; [ mudri alexarice turion ];
+  };
+}
diff --git a/nixpkgs/pkgs/development/libraries/agda/agdarsec/default.nix b/nixpkgs/pkgs/development/libraries/agda/agdarsec/default.nix
new file mode 100644
index 000000000000..ccdf65f96570
--- /dev/null
+++ b/nixpkgs/pkgs/development/libraries/agda/agdarsec/default.nix
@@ -0,0 +1,28 @@
+{ lib, mkDerivation, fetchFromGitHub
+, standard-library }:
+
+mkDerivation rec {
+  pname = "agdarsec";
+  version = "0.4.1";
+
+  src = fetchFromGitHub {
+    owner = "gallais";
+    repo = "agdarsec";
+    rev = "v${version}";
+    sha256 = "02fqkycvicw6m2xsz8p01aq8n3gj2d2gyx8sgj15l46f8434fy0x";
+  };
+
+  everythingFile = "./index.agda";
+
+  includePaths = [ "src" "examples" ];
+
+  buildInputs = [ standard-library ];
+
+  meta = with lib; {
+    homepage = "https://gallais.github.io/agdarsec/";
+    description = "Total Parser Combinators in Agda";
+    license = licenses.gpl3;
+    platforms = platforms.unix;
+    maintainers = with maintainers; [ turion ];
+  };
+}
diff --git a/nixpkgs/pkgs/development/libraries/agda/cubical/default.nix b/nixpkgs/pkgs/development/libraries/agda/cubical/default.nix
new file mode 100644
index 000000000000..8e654444dd6a
--- /dev/null
+++ b/nixpkgs/pkgs/development/libraries/agda/cubical/default.nix
@@ -0,0 +1,33 @@
+{ lib, mkDerivation, fetchFromGitHub, ghc, glibcLocales }:
+
+mkDerivation rec {
+  pname = "cubical";
+  version = "0.3pred5030a9";
+
+  src = fetchFromGitHub {
+    repo = pname;
+    owner = "agda";
+    rev = "d5030a9c89070255fc575add4e9f37b97e6a0c0c";
+    sha256 = "18achbxap4ikydigmz3m3xjfn3i9dw4rn8yih82vrlc01j02nqpi";
+  };
+
+  LC_ALL = "en_US.UTF-8";
+
+  preConfigure = ''export AGDA_EXEC=agda'';
+
+  # The cubical library has several `Everything.agda` files, which are
+  # compiled through the make file they provide.
+  nativeBuildInputs = [ ghc glibcLocales ];
+  buildPhase = ''
+    make
+  '';
+
+  meta = with lib; {
+    description =
+      "A cubical type theory library for use with the Agda compiler";
+    homepage = src.meta.homepage;
+    license = licenses.mit;
+    platforms = platforms.unix;
+    maintainers = with maintainers; [ alexarice ryanorendorff ];
+  };
+}
diff --git a/nixpkgs/pkgs/development/libraries/agda/functional-linear-algebra/default.nix b/nixpkgs/pkgs/development/libraries/agda/functional-linear-algebra/default.nix
new file mode 100644
index 000000000000..083741d58e94
--- /dev/null
+++ b/nixpkgs/pkgs/development/libraries/agda/functional-linear-algebra/default.nix
@@ -0,0 +1,30 @@
+{ fetchFromGitHub, lib, mkDerivation, standard-library }:
+
+mkDerivation rec {
+  version = "0.4";
+  pname = "functional-linear-algebra";
+
+  buildInputs = [ standard-library ];
+
+  src = fetchFromGitHub {
+    repo = "functional-linear-algebra";
+    owner = "ryanorendorff";
+    rev = "v${version}";
+    sha256 = "05jk3792k9xf8iiwzm2hwlvd25f2pqqr3gppmqjf8xb9199i8fk0";
+  };
+
+  preConfigure = ''
+    sh generate-everything.sh
+  '';
+
+  meta = with lib; {
+    homepage = "https://github.com/ryanorendorff/functional-linear-algebra";
+    description = ''
+      Formalizing linear algebra in Agda by representing matrices as functions
+      from one vector space to another.
+    '';
+    license = licenses.bsd3;
+    platforms = platforms.unix;
+    maintainers = with maintainers; [ ryanorendorff ];
+  };
+}
diff --git a/nixpkgs/pkgs/development/libraries/agda/generic/default.nix b/nixpkgs/pkgs/development/libraries/agda/generic/default.nix
new file mode 100644
index 000000000000..855dd0f33c51
--- /dev/null
+++ b/nixpkgs/pkgs/development/libraries/agda/generic/default.nix
@@ -0,0 +1,33 @@
+{ lib, mkDerivation, fetchFromGitHub, standard-library }:
+
+mkDerivation rec {
+  pname = "generic";
+  version = "0.1.0.2";
+
+  src = fetchFromGitHub {
+    owner = "effectfully";
+    repo = "Generic";
+    rev = "v${version}";
+    sha256 = "05igsd2gaj6h9bkqwp8llhvn4qvc5gmi03x4fnz096ba8m6x8s3n";
+  };
+
+  buildInputs = [
+    standard-library
+  ];
+
+  preBuild = ''
+    echo "module Everything where" > Everything.agda
+    find src -name '*.agda' | sed -e 's/src\///;s/\//./g;s/\.agda$//;s/^/import /' >> Everything.agda
+  '';
+
+  meta = with lib; {
+    # Remove if a version compatible with agda 2.6.2 is made
+    broken = true;
+    description =
+      "A library for doing generic programming in Agda";
+    homepage = src.meta.homepage;
+    license = licenses.mit;
+    platforms = platforms.unix;
+    maintainers = with maintainers; [ alexarice turion ];
+  };
+}
diff --git a/nixpkgs/pkgs/development/libraries/agda/iowa-stdlib/default.nix b/nixpkgs/pkgs/development/libraries/agda/iowa-stdlib/default.nix
new file mode 100644
index 000000000000..1383cff9e55a
--- /dev/null
+++ b/nixpkgs/pkgs/development/libraries/agda/iowa-stdlib/default.nix
@@ -0,0 +1,31 @@
+{ lib, mkDerivation, fetchFromGitHub }:
+
+mkDerivation (rec {
+  version = "1.5.0";
+  pname = "iowa-stdlib";
+
+  src = fetchFromGitHub {
+    owner = "cedille";
+    repo  = "ial";
+    rev = "v${version}";
+    sha256 = "0dlis6v6nzbscf713cmwlx8h9n2gxghci8y21qak3hp18gkxdp0g";
+  };
+
+  libraryFile = "";
+  libraryName = "IAL-1.3";
+
+  buildPhase = ''
+    patchShebangs find-deps.sh
+    make
+  '';
+
+  meta = {
+    homepage = "https://github.com/cedille/ial";
+    description = "Agda standard library developed at Iowa";
+    license = lib.licenses.free;
+    platforms = lib.platforms.unix;
+    # broken since Agda 2.6.1
+    broken = true;
+    maintainers = with lib.maintainers; [ alexarice turion ];
+  };
+})
diff --git a/nixpkgs/pkgs/development/libraries/agda/standard-library/default.nix b/nixpkgs/pkgs/development/libraries/agda/standard-library/default.nix
new file mode 100644
index 000000000000..99cb863a598d
--- /dev/null
+++ b/nixpkgs/pkgs/development/libraries/agda/standard-library/default.nix
@@ -0,0 +1,30 @@
+{ lib, mkDerivation, fetchFromGitHub, ghcWithPackages, nixosTests }:
+
+mkDerivation rec {
+  pname = "standard-library";
+  version = "1.7";
+
+  src = fetchFromGitHub {
+    repo = "agda-stdlib";
+    owner = "agda";
+    rev = "v${version}";
+    sha256 = "14h3jprm6924g9576v25axn9v6xnip354hvpzlcqsc5qqyj7zzjs";
+  };
+
+  nativeBuildInputs = [ (ghcWithPackages (self : [ self.filemanip ])) ];
+  preConfigure = ''
+    runhaskell GenerateEverything.hs
+    # We will only build/consider Everything.agda, in particular we don't want Everything*.agda
+    # do be copied to the store.
+    rm EverythingSafe.agda
+  '';
+
+  passthru.tests = { inherit (nixosTests) agda; };
+  meta = with lib; {
+    homepage = "https://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary";
+    description = "A standard library for use with the Agda compiler";
+    license = lib.licenses.mit;
+    platforms = lib.platforms.unix;
+    maintainers = with maintainers; [ jwiegley mudri alexarice turion ];
+  };
+}