diff options
Diffstat (limited to 'nixpkgs/pkgs/development/libraries/agda')
9 files changed, 289 insertions, 0 deletions
diff --git a/nixpkgs/pkgs/development/libraries/agda/1lab/default.nix b/nixpkgs/pkgs/development/libraries/agda/1lab/default.nix new file mode 100644 index 000000000000..89b0fb60c365 --- /dev/null +++ b/nixpkgs/pkgs/development/libraries/agda/1lab/default.nix @@ -0,0 +1,35 @@ +{ lib, mkDerivation, fetchFromGitHub }: + +mkDerivation rec { + pname = "1lab"; + version = "unstable-2023-12-04"; + + src = fetchFromGitHub { + owner = "plt-amy"; + repo = pname; + rev = "47c2a96220b4d14419e5ddb973bc1fa06933e723"; + hash = "sha256-0U6s6sXdynk2IWRBDXBJCf7Gc+gE8AhR1PXZl0DS4yU="; + }; + + postPatch = '' + # We don't need anything in support; avoid installing LICENSE.agda + rm -rf support + + # Remove verbosity options as they make Agda take longer and use more memory. + shopt -s globstar extglob + sed -Ei '/OPTIONS/s/ -v ?[^ #]+//g' src/**/*.@(agda|lagda.md) + ''; + + libraryName = "1lab"; + libraryFile = "1lab.agda-lib"; + everythingFile = "src/index.lagda.md"; + + meta = with lib; { + description = + "A formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory "; + homepage = src.meta.homepage; + license = licenses.agpl3; + platforms = platforms.unix; + maintainers = with maintainers; [ ncfavier ]; + }; +} 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..11c129badd64 --- /dev/null +++ b/nixpkgs/pkgs/development/libraries/agda/agda-categories/default.nix @@ -0,0 +1,42 @@ +{ lib, mkDerivation, fetchFromGitHub, standard-library }: + +mkDerivation rec { + version = "0.2.0"; + pname = "agda-categories"; + + src = fetchFromGitHub { + owner = "agda"; + repo = "agda-categories"; + rev = "v${version}"; + sha256 = "sha256-GQuQxzYSQxAIVSJ1vf0blRC0juoxAqD1AHW66H/6NSk="; + }; + + postPatch = '' + # Remove this once agda-categories incorporates this fix or once Agda's + # versioning system gets an overhaul in general. Right now there is no middle + # ground between "no version constraint" and "exact match down to patch". We + # do not want to need to change this postPatch directive on each minor + # version update of the stdlib, so we get rid of the version constraint + # altogether. + sed -Ei 's/standard-library-[0-9.]+/standard-library/' agda-categories.agda-lib + + # The Makefile of agda-categories uses git(1) instead of find(1) to + # determine the list of source files. We cannot use git, as $PWD will not + # be a valid Git working directory. + find src -name '*.agda' | sed -e 's|^src/[/]*|import |' -e 's|/|.|g' -e 's/.agda//' -e '/import Everything/d' | LC_COLLATE='C' sort > Everything.agda + ''; + + # agda: Heap exhausted; + # agda: Current maximum heap size is 4294967296 bytes (4096 MB). + GHCRTS = "-M5G"; + + 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..fcc100e7a7bb --- /dev/null +++ b/nixpkgs/pkgs/development/libraries/agda/agda-prelude/default.nix @@ -0,0 +1,28 @@ +{ lib, mkDerivation, fetchFromGitHub }: + +mkDerivation rec { + version = "unstable-2023-10-04"; + pname = "agda-prelude"; + + src = fetchFromGitHub { + owner = "UlfNorell"; + repo = "agda-prelude"; + rev = "ff3b13253612caf0784a06e2d7d0f30be16c32e4"; + hash = "sha256-A05uDv3fJqKncea9AL6eQa0XAskLZwAIUl1OAOVeP8I="; + }; + + 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..34730ae17f4e --- /dev/null +++ b/nixpkgs/pkgs/development/libraries/agda/agdarsec/default.nix @@ -0,0 +1,29 @@ +{ 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 ]; + broken = true; + }; +} 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..50ca17a10a25 --- /dev/null +++ b/nixpkgs/pkgs/development/libraries/agda/cubical/default.nix @@ -0,0 +1,31 @@ +{ lib, mkDerivation, fetchFromGitHub, ghc }: + +mkDerivation rec { + pname = "cubical"; + version = "0.6"; + + src = fetchFromGitHub { + repo = pname; + owner = "agda"; + rev = "v${version}"; + hash = "sha256-2quAZ/j7kQaFkh9W5Bj1y7YQj9BT7FwHqVWyj8T4AH8="; + }; + + # The cubical library has several `Everything.agda` files, which are + # compiled through the make file they provide. + nativeBuildInputs = [ ghc ]; + buildPhase = '' + runHook preBuild + make + runHook postBuild + ''; + + 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 ncfavier ]; + }; +} 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..c91896993ce5 --- /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.5.0"; + pname = "functional-linear-algebra"; + + buildInputs = [ standard-library ]; + + src = fetchFromGitHub { + repo = "functional-linear-algebra"; + owner = "ryanorendorff"; + rev = "v${version}"; + sha256 = "sha256-3nme/eH4pY6bD0DkhL4Dj/Vp/WnZqkQtZTNk+n1oAyY="; + }; + + 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..d7b49893b96f --- /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 = "2.0"; + + src = fetchFromGitHub { + repo = "agda-stdlib"; + owner = "agda"; + rev = "v${version}"; + hash = "sha256-TjGvY3eqpF+DDwatT7A78flyPcTkcLHQ1xcg+MKgCoE="; + }; + + nativeBuildInputs = [ (ghcWithPackages (self : [ self.filemanip ])) ]; + preConfigure = '' + runhaskell GenerateEverything.hs --include-deprecated + # 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 ]; + }; +} |