alioth/nixpkgs
3
0
Fork 0
forked from mirrors/nixpkgs
Code Releases Activity

Merge pull request #76653 from alexarice/agda-rework

Browse source 
Agda rework
This commit is contained in:
Dmitry Kalinkin 2020-05-14 18:02:50 -04:00 committed by GitHub
parent efdeb1a0de 8ee4c3698c
commit 9943fd1a1d
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
20 changed files with 294 additions and 578 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

96
doc/languages-frameworks/agda.section.md Normal file
View file

@ -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).

1
doc/languages-frameworks/index.xml
View file

@ -5,6 +5,7 @@
<para>
The <link linkend="chap-stdenv">standard build environment</link> 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 <literal>stdenv</literal>. 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.
</para>
<xi:include href="agda.section.xml" />
<xi:include href="android.section.xml" />
<xi:include href="beam.xml" />
<xi:include href="bower.xml" />

41
nixos/tests/agda.nix Normal file
View file

@ -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")
'';
}
)

1
nixos/tests/all-tests.nix
View file

@ -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 {};

121
pkgs/build-support/agda/default.nix
View file

@ -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;
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
isAgdaPackage = true;
withPackages = arg: if builtins.isAttrs arg then withPackages' arg else withPackages' { pkgs = arg; };
buildInputs = [ Agda ] ++ self.buildDepends;
buildDepends = [];
buildDependsAgda = stdenv.lib.filter
(dep: dep ? isAgdaPackage && dep.isAgdaPackage)
self.buildDepends;
buildDependsAgdaShareAgda = map (x: x + "/share/agda") self.buildDependsAgda;
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;
# Not much choice here ;)
LANG = "en_US.UTF-8";
LOCALE_ARCHIVE = stdenv.lib.optionalString
stdenv.isLinux
"${glibcLocales}/lib/locale/locale-archive";
isAgdaDerivation = true;
everythingFile = "Everything.agda";
buildInputs = buildInputs ++ [ agdaWithArgs ];
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 = ''
buildPhase = if buildPhase != null then buildPhase else ''
runHook preBuild
${self.agdaWithArgs} ${self.everythingFile}
agda -i ${dirOf everythingFile} ${everythingFile}
runHook postBuild
'';
installPhase = let
srcFiles = self.sourceDirectories
++ map (x: x + "/*") self.topSourceDirectories;
in ''
installPhase = if installPhase != null then installPhase else ''
runHook preInstall
mkdir -p $out/share/agda
cp -pR ${concatStringsSep " " srcFiles} $out/share/agda
mkdir -p $out
find \( -name '*.agda' -or -name '*.agdai' -or -name '*.agda-lib' \) -exec cp -p --parents -t "$out" {} +
runHook postInstall
'';
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;
};
};
};
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';
}

24
pkgs/development/libraries/agda/Agda-Sheaves/default.nix
View file

@ -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
};
})

259
pkgs/development/libraries/agda/TotalParserCombinators/contextfile
View file

@ -1,259 +0,0 @@
Context:
[Updated the code in response to changes to Agda.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20150319181310
Ignore-this: 52b9ff613d7f10b0c8f45591a0759d07
]
[Rolled back most of "Updated the code in response to changes to Agda".
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20150319101420
Ignore-this: c2ea7bdf79848235fa3ea64ebda116eb
* One of the Agda changes has been reverted.
]
[Removed an outdated comment.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20150217162945
Ignore-this: 3ff7732335750305fe220e65693f0cbf
]
[Added the simplification "nonempty (return x) → fail".
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20150217161718
Ignore-this: 56ad6a68c314446d8986a8c1b49655d0
]
[Added Nonempty.nonempty-return.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20150217161629
Ignore-this: 68829d3f9a248272c46848daa05ccfe3
]
[Updated the copyright year range.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20150212154744
Ignore-this: 3410a12ca1f9de825b00e692b136d500
]
[Updated the code in response to changes to Agda.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20150212152207
Ignore-this: 683b5eeca5fa9c8490bceaf68c23a204
]
[Updated the copyright year range.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20141128223227
Ignore-this: 31d3f5e4fdd6fbfad9758d9bfd0d3a3e
]
[Updated the code in response to changes to Agda and the library.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20141128223205
Ignore-this: 6392ec67aab2c534a7195abed55be47
]
[Updated code to reflect changes to Agda.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20140425121055
Ignore-this: 54d80fd647cb897eef85f57e9172f7db
]
[Workaround for (possible) Agda bug.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20140228200347
Ignore-this: b17884ad17a3bdb7faff678622365a8
]
[Updated code to reflect changes to library API.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20130307134644
Ignore-this: 50d070a22a6796b9acdf19d44ba5de16
]
[Updated code to reflect changes to Agda and the library API.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20130228122951
Ignore-this: 761dc4d85683a59cc3667a8706c88093
]
[Turned _◇_ into a constructor.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20120316125431
Ignore-this: 41b492c3106a575f28f146253f78a5ae
]
[Updated code to reflect changes to Agda.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20120316125416
Ignore-this: e77d817d8b391c3b4806119d10848eb3
]
[Updated code to reflect changes to Agda.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20120215103344
Ignore-this: 467716429d5553cd122722108ea82a08
]
[Modified a comment.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20120215103319
Ignore-this: e57d4911f692f8a96a80017d910efc5f
]
[Updated code to reflect change to library API.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20111006160229
Ignore-this: 5359da54e7e6e0f92983fa3ecaccebf3
]
[Updated code to reflect changes to Agda and the library API.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20111003170117
Ignore-this: cbdd35172e372779e12642985cf17268
]
[Rolled back addition of inversion lemmas.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20110930150912
Ignore-this: 9c9b083f0afcf95aaaa55a01d871274e
]
[Added inversion lemmas, implemented other lemmas using these lemmas.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**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 <nils.anders.danielsson@gmail.com>**20110517220158
Ignore-this: ea9771a5014a25cb20afc2118638f8b5
]
[Updated code to reflect changes to Agda.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20110512124425
Ignore-this: 97b154661679f574f6ab914583b14580
]
[Proved that many constructions preserve various preorders.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20110313012617
Ignore-this: 8008efaff967c228448baa33b82edb81
]
[Updated code to reflect changes to library API.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20110313002106
Ignore-this: 94799ba1ae411e59fd8c6c7eac3b8dfb
]
[Simplified TotalRecognisers.LeftRecursion.MatchingParentheses.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20110118102159
Ignore-this: 1e01a8092b0c0124979ffc5fe17a245c
]
[Added TotalRecognisers.LeftRecursion.MatchingParentheses.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20110118102146
Ignore-this: 13a3bc91425364e26c3047561655bb25
]
[Added a simplifying backend.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101229012716
Ignore-this: 9ac7ae21cd44c099633678a994fb9a3
]
[Fixed another "bug" in the deep simplifier.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**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 <nils.anders.danielsson@gmail.com>**20101228235603
Ignore-this: d39b8453a15089126261e098080223c6
]
[Deep simplification no longer adds casts.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101228192850
Ignore-this: 2ba016825adfa3a1e36922869eabfd39
]
[The first constructor in a simplified parser can no longer be a cast.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101228175822
Ignore-this: ce3e38cc0b9a096aa436655c9013ae97
]
[Modified the outline.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101228173414
Ignore-this: f8866e69f6d1a344e79fb6f708dfa4c
]
[Added an example: a right recursive expression grammar.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101228173159
Ignore-this: 9a4d732b451cca08ba19aac5d115c678
]
[Rearranged the code.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101228172209
Ignore-this: 50fa29406d0f150669ff3feec4dbe513
]
[Renamed same-bag/set to (initial-bag-)cong.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101228170706
Ignore-this: dd3ce43d77dde74cc2428d2568dd2d30
]
[Added TotalParserCombinators.Force.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101228153638
Ignore-this: 3b6ff6ea20df0c1293494f06845d17eb
]
[Proved that uses of subst can be erased.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101228153621
Ignore-this: f503ba495b923ae521718b6957167128
]
[The deep simplifier no longer skips layers.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101228141138
Ignore-this: 733a4a4a9aa0f890ad1740ecfc6a599f
]
[Documented that the deep simplifier misses every second layer.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101228121910
Ignore-this: 8a0baf25b12f63f8748dbc1d16affacf
]
[The simplifier now applies the token-bind rule more often.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101227165413
Ignore-this: 40132fa6f19602886bbe29aadd8a683c
]
[Switched back to deep simplification, now with a proper proof.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101227125434
Ignore-this: ccc46e82f6f9c6c2a27ddb43d315f7dd
]
[Simplified the soundness proof.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101227123839
Ignore-this: fb6826dd9836e34fc3bfdce2928ba13d
]
[Made some _≈[_]P_ constructors conditionally coinductive.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101227123827
Ignore-this: f521f70475403697229051b62343a080
+ The structure of the soundness proof was also changed.
]
[Unified And, AsymmetricChoice and Not.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101225103109
Ignore-this: 5ae8b80e1505fe6e707bb2307d22688c
]
[Modified some comments.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101225101051
Ignore-this: e812d8c3e9720895c368f7a286f8315c
]
[Modified a comment.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101223202647
Ignore-this: 16ea5dc01a4cbe0fe38714b2e4b7ff6
]
[Updated code to reflect changes to library API.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101107162658
Ignore-this: 9e38a10a9997c9825ece6ad9f871b673
]
[Added an alternative backend for TotalRecognisers.Simple.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101020183743
Ignore-this: a111a89e0c237e132b649561000f53d6
]
[TAG Code corresponding to the paper "Total Parser Combinators" (4).
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100928013815
Ignore-this: 45ccc28373ed3974047315613eb14833
]

26
pkgs/development/libraries/agda/TotalParserCombinators/default.nix
View file

@ -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;
};
})

23
pkgs/development/libraries/agda/agda-base/default.nix
View file

@ -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
};
})

28
pkgs/development/libraries/agda/agda-categories/default.nix Normal file
View file

@ -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 ];
};
}

31
pkgs/development/libraries/agda/agda-prelude/default.nix
View file

@ -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 ];
};
})
}

24
pkgs/development/libraries/agda/bitvector/default.nix
View file

@ -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;
};
})

24
pkgs/development/libraries/agda/categories/default.nix
View file

@ -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
};
})

16
pkgs/development/libraries/agda/agda-iowa-stdlib/default.nix → pkgs/development/libraries/agda/iowa-stdlib/default.nix
View file

@ -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 ];
};
})

43
pkgs/development/libraries/agda/pretty/contextfile
View file

@ -1,43 +0,0 @@
Context:
[Updated the code in response to a change to Agda.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20150319181428
Ignore-this: f83c3dccfe25a2a5b9d0437d1dce0ec0
]
[Rolled back most of "Updated the code in response to changes to Agda".
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20150319101413
Ignore-this: 5a26cf9cf83d0d146cca0c15c857d20c
* One of the Agda changes has been reverted.
]
[Updated the code in response to changes to Agda.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20150217101656
Ignore-this: a12921aebbe0fb575ef391ba5789a391
]
[Modified the copyright year range.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20150213144338
Ignore-this: 1d1b22457dd6dadcb47f5d7f3eea062
]
[Restored Grammar.Abstract and Grammar.Non-terminal.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20130727225031
Ignore-this: ddccb15caa7a3c26e973997ffdb4eec1
]
[Modified the copyright year range.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20141128164015
Ignore-this: b9c6dddc965738aa2a7670c4c18da67f
]
[Updated the code to reflect changes to the library API.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20141128163950
Ignore-this: 8094c47f23cef0fcc596ad0c18a92b56
]
[TAG Correct-by-Construction Pretty-Printing (2013-07-28)
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20130727224432
Ignore-this: 6aab9b2e6b638457767c8821f3c27cb4
]

26
pkgs/development/libraries/agda/pretty/default.nix
View file

@ -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
};
})

16
pkgs/development/libraries/agda/agda-stdlib/default.nix → pkgs/development/libraries/agda/standard-library/default.nix
View file

@ -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 ];
};
})
}

26
pkgs/top-level/agda-packages.nix Normal file
View file

@ -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

25
pkgs/top-level/all-packages.nix
View file

@ -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

1
pkgs/top-level/release.nix
View file

@ -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;