gador/nixpkgs
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

agda: fixes for 2.8.0 (#424180)

Browse Source
This commit is contained in:
Philip Taron
2025-07-17 14:56:33 -07:00
committed by GitHub
parent 32e5230d01 1288f57e55
commit 1d2cfef5e9
14 changed files with 50 additions and 107 deletions
Download Patch File Download Diff File Expand all files Collapse all files
doc/languages-frameworks/agda.section.md
+15 -32
View File
@@ -125,11 +125,10 @@ To install Agda without GHC, use `ghc = null;`.
## Writing Agda packages {#writing-agda-packages}
To write a nix derivation for an Agda library, first check that the library has a `*.agda-lib` file.
To write a nix derivation for an Agda library, first check that the library has a (single) `*.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`.
@@ -152,9 +151,9 @@ agdaPackages.mkDerivation {
### Building Agda packages {#building-agda-packages}
The default build phase for `agdaPackages.mkDerivation` runs `agda` on the `Everything.agda` file.
The default build phase for `agdaPackages.mkDerivation` runs `agda --build-library`.
If something else is needed to build the package (e.g. `make`) then the `buildPhase` should be overridden.
Additionally, a `preBuild` or `configurePhase` can be used if there are steps that need to be done prior to checking the `Everything.agda` file.
Additionally, a `preBuild` or `configurePhase` can be used if there are steps that need to be done prior to checking the library.
`agda` and the Agda libraries contained in `buildInputs` are made available during the build phase.
### Installing Agda packages {#installing-agda-packages}
@@ -182,7 +181,7 @@ the Agda package set is small and can (still) be maintained by hand.
### Adding Agda packages to Nixpkgs {#adding-agda-packages-to-nixpkgs}
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:
To add an Agda package to `nixpkgs`, the derivation should be written to `pkgs/development/libraries/agda/${library-name}/default.nix` 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 derivation could look like:
```nix
{
@@ -190,45 +189,29 @@ To add an Agda package to `nixpkgs`, the derivation should be written to `pkgs/d
standard-library,
fetchFromGitHub,
}:
{ }
mkDerivation {
pname = "my-library";
version = "1.0";
src = <...>;
buildInputs = [ standard-library ];
meta = <...>;
}
```
You can look at other files under `pkgs/development/libraries/agda/` for more inspiration.
Note that the derivation function is called with `mkDerivation` set to `agdaPackages.mkDerivation`, therefore you
could use a similar set as in your `default.nix` from [Writing Agda Packages](#writing-agda-packages) with
`agdaPackages.mkDerivation` replaced with `mkDerivation`.
Here is an example skeleton derivation for iowa-stdlib:
```nix
mkDerivation {
version = "1.5.0";
pname = "iowa-stdlib";
src = <...>;
libraryFile = "";
libraryName = "IAL-1.3";
buildPhase = ''
runHook preBuild
patchShebangs find-deps.sh
make
runHook postBuild
'';
}
```
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).
In the pull request adding this library,
you can test whether it builds correctly by writing in a comment:
```
@ofborg build agdaPackages.iowa-stdlib
@ofborg build agdaPackages.my-library
```
### Maintaining Agda packages {#agda-maintaining-packages}
pkgs/build-support/agda/default.nix
+3 -9
View File
@@ -90,8 +90,6 @@ let
pname,
meta,
buildInputs ? [ ],
everythingFile ? "./Everything.agda",
includePaths ? [ ],
libraryName ? pname,
libraryFile ? "${libraryName}.agda-lib",
buildPhase ? null,
@@ -100,17 +98,14 @@ let
...
}:
let
agdaWithArgs = withPackages (filter (p: p ? isAgdaDerivation) buildInputs);
includePathArgs = concatMapStrings (path: "-i" + path + " ") (
includePaths ++ [ (dirOf everythingFile) ]
);
agdaWithPkgs = withPackages (filter (p: p ? isAgdaDerivation) buildInputs);
in
{
inherit libraryName libraryFile;
isAgdaDerivation = true;
buildInputs = buildInputs ++ [ agdaWithArgs ];
buildInputs = buildInputs ++ [ agdaWithPkgs ];
buildPhase =
if buildPhase != null then
@@ -118,8 +113,7 @@ let
else
''
runHook preBuild
agda ${includePathArgs} ${everythingFile}
rm ${everythingFile} ${lib.interfaceFile Agda.version everythingFile}
agda --build-library
runHook postBuild
'';
pkgs/build-support/agda/lib.nix
+2 -2
View File
@@ -6,8 +6,8 @@
* The resulting path may not be normalized.
*
* Examples:
* interfaceFile pkgs.agda.version "./Everything.agda" == "_build/2.6.4.3/agda/./Everything.agdai"
* interfaceFile pkgs.agda.version "src/Everything.lagda.tex" == "_build/2.6.4.3/agda/src/Everything.agdai"
* interfaceFile pkgs.agda.version "./Foo.agda" == "_build/AGDA_VERSION/agda/./Foo.agdai"
* interfaceFile pkgs.agda.version "src/Foo.lagda.tex" == "_build/AGDA_VERSION/agda/src/Foo.agdai"
*/
interfaceFile =
agdaVersion: agdaFile:
pkgs/development/haskell-modules/configuration-nix.nix
+12
View File
@@ -1412,6 +1412,18 @@ builtins.intersectAttrs super {
(overrideCabal { mainProgram = "agda"; })
# Split outputs to reduce closure size
enableSeparateBinOutput
# Build the primitive library to generate its interface files.
# These are needed in order to use Agda in Nix builds.
(overrideCabal (drv: {
postInstall =
drv.postInstall or ""
+ ''
agdaExe=''${bin:-$out}/bin/agda
echo "Generating Agda core library interface files..."
(cd "$("$agdaExe" --print-agda-data-dir)/lib/prim" && "$agdaExe" --build-library)
'';
}))
];
# ats-format uses cli-setup in Setup.hs which is quite happy to write
pkgs/development/libraries/agda/1lab/default.nix
+3 -14
View File
@@ -6,13 +6,13 @@
mkDerivation rec {
pname = "1lab";
version = "unstable-2024-08-05";
version = "unstable-2025-07-01";
src = fetchFromGitHub {
owner = "the1lab";
repo = pname;
rev = "7cc9bf7bbe90be5491e0d64da90a36afa29a540b";
hash = "sha256-hOyf6ZzejDAFDRj6liFZsBc9bKdxV5bzTPP4kGXIhW0=";
rev = "e9c2ad2b3ba9cefad36e72cb9d732117c68ac862";
hash = "sha256-wKh77+xCdfMtnq9jMlpdnEptGO+/WVNlQFa1TDbdUGs=";
};
postPatch = ''
@@ -23,19 +23,8 @@ mkDerivation rec {
shopt -s globstar extglob
files=(src/**/*.@(agda|lagda.md))
sed -Ei '/OPTIONS/s/ -v ?[^ #]+//g' "''${files[@]}"
# Generate all-pages manually instead of building the build script.
mkdir -p _build
for f in "''${files[@]}"; do
f=''${f#src/} f=''${f%%.*} f=''${f//\//.}
echo "open import $f"
done > _build/all-pages.agda
'';
libraryName = "1lab";
libraryFile = "1lab.agda-lib";
everythingFile = "_build/all-pages.agda";
meta = with lib; {
description = "A formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory ";
homepage = src.meta.homepage;
pkgs/development/libraries/agda/agda-categories/default.nix
-5
View File
@@ -24,11 +24,6 @@ mkDerivation rec {
# 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
'';
buildInputs = [ standard-library ];
pkgs/development/libraries/agda/agda-prelude/default.nix
-7
View File
@@ -15,13 +15,6 @@ mkDerivation {
hash = "sha256-ab+KojzRbkUTAFNH5OA78s0F5SUuXTbliai6badveg4=";
};
preConfigure = ''
cd test
make everything
mv Everything.agda ..
cd ..
'';
meta = with lib; {
homepage = "https://github.com/UlfNorell/agda-prelude";
description = "Programming library for Agda";
pkgs/development/libraries/agda/agdarsec/default.nix
-7
View File
@@ -16,13 +16,6 @@ mkDerivation rec {
sha256 = "02fqkycvicw6m2xsz8p01aq8n3gj2d2gyx8sgj15l46f8434fy0x";
};
everythingFile = "./index.agda";
includePaths = [
"src"
"examples"
];
buildInputs = [ standard-library ];
meta = with lib; {
pkgs/development/libraries/agda/cubical-mini/default.nix
+3 -3
View File
@@ -8,13 +8,13 @@
mkDerivation rec {
pname = "cubical-mini";
version = "nightly-20241214";
version = "0.5-unstable-2025-06-13";
src = fetchFromGitHub {
repo = pname;
owner = "cmcmA20";
rev = "ab18320018ddc0055db60d4bb5560d31909c5b78";
hash = "sha256-32qXY9KbProdPwqHxSkwO74Oqx65rTzoXtH2SpRB3OM=";
rev = "1776874d13d0b811e6eeb70d0e5a52b4d2a978d2";
hash = "sha256-UxWOS+uzP9aAaMdSueA2CAuzWkImGAoKxroarcgpk+w=";
};
nativeBuildInputs = [
pkgs/development/libraries/agda/cubical/default.nix
+4 -8
View File
@@ -2,7 +2,6 @@
lib,
mkDerivation,
fetchFromGitHub,
ghc,
}:
mkDerivation rec {
@@ -16,13 +15,10 @@ mkDerivation rec {
hash = "sha256-KwwN2g2naEo4/rKTz2L/0Guh5LxymEYP53XQzJ6eMjM=";
};
# 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
postPatch = ''
# This imports the Everything files, which we don't generate.
# TODO: remove for the next release
rm -rf Cubical/README.agda Cubical/Talks/EPA2020.agda
'';
meta = with lib; {
pkgs/development/libraries/agda/functional-linear-algebra/default.nix
-4
View File
@@ -18,10 +18,6 @@ mkDerivation rec {
sha256 = "sha256-3nme/eH4pY6bD0DkhL4Dj/Vp/WnZqkQtZTNk+n1oAyY=";
};
preConfigure = ''
sh generate-everything.sh
'';
meta = with lib; {
homepage = "https://github.com/ryanorendorff/functional-linear-algebra";
description = ''
pkgs/development/libraries/agda/generics/default.nix
+4 -1
View File
@@ -20,7 +20,10 @@ mkDerivation rec {
standard-library
];
# everythingFile = "./README.agda";
# Agda expects a single .agda-lib file.
preBuild = ''
rm tests.agda-lib
'';
meta = with lib; {
description = "Library for datatype-generic programming in Agda";
pkgs/development/libraries/agda/standard-library/default.nix
+3 -12
View File
@@ -2,29 +2,20 @@
lib,
mkDerivation,
fetchFromGitHub,
ghcWithPackages,
nixosTests,
}:
mkDerivation rec {
pname = "standard-library";
version = "2.2";
version = "2.2-unstable-2025-07-03";
src = fetchFromGitHub {
repo = "agda-stdlib";
owner = "agda";
rev = "v${version}";
hash = "sha256-/Fy5EOSbVNXt6Jq0yKSnlNPW4SYfn+eCTAYFnMZrbR0=";
rev = "6f8af9452e7fac27bc3b3ad068793b538f07668e";
hash = "sha256-LD6KasmQ9ZHRNQJ0N4wjyc6JiSkZpmyqQq9B0Wta1n0=";
};
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";
pkgs/top-level/agda-packages.nix
+1 -3
View File
@@ -28,9 +28,7 @@ let
agda = withPackages [ ];
standard-library = callPackage ../development/libraries/agda/standard-library {
inherit (pkgs.haskellPackages) ghcWithPackages;
};
standard-library = callPackage ../development/libraries/agda/standard-library { };
iowa-stdlib = callPackage ../development/libraries/agda/iowa-stdlib { };