diff --git a/doc/languages-frameworks/agda.section.md b/doc/languages-frameworks/agda.section.md new file mode 100644 index 000000000000..7a5dc767b7c4 --- /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 a6f56d791c54..2414956995c0 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/nixos/tests/agda.nix b/nixos/tests/agda.nix new file mode 100644 index 000000000000..e158999e57d1 --- /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 f3e90f9bfa70..5caf1c958fb0 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 {}; avahi = handleTest ./avahi.nix {}; babeld = handleTest ./babeld.nix {}; diff --git a/pkgs/build-support/agda/default.nix b/pkgs/build-support/agda/default.nix index 0d054eaa5469..205aff555730 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-Sheaves/default.nix b/pkgs/development/libraries/agda/Agda-Sheaves/default.nix deleted file mode 100644 index 513b79e63938..000000000000 --- 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/development/libraries/agda/TotalParserCombinators/contextfile b/pkgs/development/libraries/agda/TotalParserCombinators/contextfile deleted file mode 100644 index 46743cba3b67..000000000000 --- 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 97cceebc1b64..000000000000 --- 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/development/libraries/agda/agda-base/default.nix b/pkgs/development/libraries/agda/agda-base/default.nix deleted file mode 100644 index 678b3a28dc7e..000000000000 --- 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/development/libraries/agda/agda-categories/default.nix b/pkgs/development/libraries/agda/agda-categories/default.nix new file mode 100644 index 000000000000..9eb68b5a64ac --- /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 turion ]; + }; +} diff --git a/pkgs/development/libraries/agda/agda-prelude/default.nix b/pkgs/development/libraries/agda/agda-prelude/default.nix index 86f21ad9b19c..2bec10c02dd1 100644 --- a/pkgs/development/libraries/agda/agda-prelude/default.nix +++ b/pkgs/development/libraries/agda/agda-prelude/default.nix @@ -1,23 +1,32 @@ -{ stdenv, agda, fetchgit }: +{ stdenv, mkDerivation, fetchFromGitHub }: -agda.mkDerivation (self: rec { - version = "eacc961c2c312b7443109a7872f99d55557df317"; - name = "agda-prelude-${version}"; +mkDerivation rec { + version = "compat-2.6.0"; + pname = "agda-prelude"; - src = fetchgit { - url = "https://github.com/UlfNorell/agda-prelude.git"; + src = fetchFromGitHub { + owner = "UlfNorell"; + repo = "agda-prelude"; rev = version; - sha256 = "0iql67hb1q0fn8dwkcx07brkdkxqfqrsbwjy71ndir0k7qzw7qv2"; + sha256 = "0brg61qrf8izqav80qpx77dbdxvlnsxyy0v7hmlrmhg68b5lp38y"; }; - topSourceDirectories = [ "src" ]; - 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; - maintainers = with maintainers; [ mudri ]; + # broken since Agda 2.6.1 + broken = true; + maintainers = with maintainers; [ mudri alexarice turion ]; }; -}) +} diff --git a/pkgs/development/libraries/agda/bitvector/default.nix b/pkgs/development/libraries/agda/bitvector/default.nix deleted file mode 100644 index bf9798557b10..000000000000 --- 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/development/libraries/agda/categories/default.nix b/pkgs/development/libraries/agda/categories/default.nix deleted file mode 100644 index fef01ee9be70..000000000000 --- 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/development/libraries/agda/agda-iowa-stdlib/default.nix b/pkgs/development/libraries/agda/iowa-stdlib/default.nix similarity index 58% rename from pkgs/development/libraries/agda/agda-iowa-stdlib/default.nix rename to pkgs/development/libraries/agda/iowa-stdlib/default.nix index 23013bfbc324..55cd6a742e54 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,17 +11,21 @@ agda.mkDerivation (self: rec { sha256 = "0dlis6v6nzbscf713cmwlx8h9n2gxghci8y21qak3hp18gkxdp0g"; }; - sourceDirectories = [ "./." ]; + libraryFile = ""; + libraryName = "IAL-1.3"; + buildPhase = '' patchShebangs find-deps.sh make ''; 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; - maintainers = with stdenv.lib.maintainers; [ ]; + # broken since Agda 2.6.1 + broken = true; + maintainers = with stdenv.lib.maintainers; [ alexarice turion ]; }; }) diff --git a/pkgs/development/libraries/agda/pretty/contextfile b/pkgs/development/libraries/agda/pretty/contextfile deleted file mode 100644 index 2ea20153bbcc..000000000000 --- 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 de4cfaa6637b..000000000000 --- 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/development/libraries/agda/agda-stdlib/default.nix b/pkgs/development/libraries/agda/standard-library/default.nix similarity index 63% rename from pkgs/development/libraries/agda/agda-stdlib/default.nix rename to pkgs/development/libraries/agda/standard-library/default.nix index 6647677f71c0..4bff585ac3a9 100644 --- a/pkgs/development/libraries/agda/agda-stdlib/default.nix +++ b/pkgs/development/libraries/agda/standard-library/default.nix @@ -1,14 +1,14 @@ -{ stdenv, agda, fetchFromGitHub, ghcWithPackages }: +{ stdenv, mkDerivation, fetchFromGitHub, ghcWithPackages }: -agda.mkDerivation (self: rec { - version = "1.1"; - name = "agda-stdlib-${version}"; +mkDerivation rec { + pname = "standard-library"; + version = "1.3"; src = fetchFromGitHub { repo = "agda-stdlib"; owner = "agda"; rev = "v${version}"; - sha256 = "190bxsy92ffmvwpmyyg3lxs91vyss2z25rqz1w79gkj56484cy64"; + sha256 = "18kl20z3bjfgx5m3nvrdj5776qmpi7jl2p12pqybsls2lf86m0d5"; }; nativeBuildInputs = [ (ghcWithPackages (self : [ self.filemanip ])) ]; @@ -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 turion ]; }; -}) +} diff --git a/pkgs/top-level/agda-packages.nix b/pkgs/top-level/agda-packages.nix new file mode 100644 index 000000000000..3f4d7db0c7c7 --- /dev/null +++ b/pkgs/top-level/agda-packages.nix @@ -0,0 +1,26 @@ +{ 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 { }; + + agda-categories = callPackage ../development/libraries/agda/agda-categories { }; + }; +in mkAgdaPackages Agda diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index 49bf7d9f815d..b85fd488f788 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -15176,31 +15176,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; }; - - agdaBase = callPackage ../development/libraries/agda/agda-base { }; - - 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; - }; - - AgdaSheaves = callPackage ../development/libraries/agda/Agda-Sheaves { }; - - bitvector = callPackage ../development/libraries/agda/bitvector { }; - - categories = callPackage ../development/libraries/agda/categories { }; - - pretty = callPackage ../development/libraries/agda/pretty { }; - - TotalParserCombinators = callPackage ../development/libraries/agda/TotalParserCombinators { }; + agda = agdaPackages.agda; ### DEVELOPMENT / LIBRARIES / JAVA diff --git a/pkgs/top-level/release.nix b/pkgs/top-level/release.nix index e0723523f4e5..60a4a679f161 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;