diff --git a/doc/languages-frameworks/agda.section.md b/doc/languages-frameworks/agda.section.md index d5a1c6ef08a3..6d4d973ed612 100644 --- a/doc/languages-frameworks/agda.section.md +++ b/doc/languages-frameworks/agda.section.md @@ -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} diff --git a/pkgs/build-support/agda/default.nix b/pkgs/build-support/agda/default.nix index b4609940fedc..aeb214727ef6 100644 --- a/pkgs/build-support/agda/default.nix +++ b/pkgs/build-support/agda/default.nix @@ -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 ''; diff --git a/pkgs/build-support/agda/lib.nix b/pkgs/build-support/agda/lib.nix index 4bdb80a6ca00..c11c17e668a9 100644 --- a/pkgs/build-support/agda/lib.nix +++ b/pkgs/build-support/agda/lib.nix @@ -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: diff --git a/pkgs/development/haskell-modules/configuration-nix.nix b/pkgs/development/haskell-modules/configuration-nix.nix index 89357c07eab0..0cb803f1c80c 100644 --- a/pkgs/development/haskell-modules/configuration-nix.nix +++ b/pkgs/development/haskell-modules/configuration-nix.nix @@ -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 diff --git a/pkgs/development/libraries/agda/1lab/default.nix b/pkgs/development/libraries/agda/1lab/default.nix index e21e9537f759..6dfcc4ac2a84 100644 --- a/pkgs/development/libraries/agda/1lab/default.nix +++ b/pkgs/development/libraries/agda/1lab/default.nix @@ -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; diff --git a/pkgs/development/libraries/agda/agda-categories/default.nix b/pkgs/development/libraries/agda/agda-categories/default.nix index 60a74c353f3e..b59255e887f8 100644 --- a/pkgs/development/libraries/agda/agda-categories/default.nix +++ b/pkgs/development/libraries/agda/agda-categories/default.nix @@ -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 ]; diff --git a/pkgs/development/libraries/agda/agda-prelude/default.nix b/pkgs/development/libraries/agda/agda-prelude/default.nix index 15f27998bec2..8cc002793456 100644 --- a/pkgs/development/libraries/agda/agda-prelude/default.nix +++ b/pkgs/development/libraries/agda/agda-prelude/default.nix @@ -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"; diff --git a/pkgs/development/libraries/agda/agdarsec/default.nix b/pkgs/development/libraries/agda/agdarsec/default.nix index 257172ad3178..876b3b271695 100644 --- a/pkgs/development/libraries/agda/agdarsec/default.nix +++ b/pkgs/development/libraries/agda/agdarsec/default.nix @@ -16,13 +16,6 @@ mkDerivation rec { sha256 = "02fqkycvicw6m2xsz8p01aq8n3gj2d2gyx8sgj15l46f8434fy0x"; }; - everythingFile = "./index.agda"; - - includePaths = [ - "src" - "examples" - ]; - buildInputs = [ standard-library ]; meta = with lib; { diff --git a/pkgs/development/libraries/agda/cubical-mini/default.nix b/pkgs/development/libraries/agda/cubical-mini/default.nix index 385d99b96ada..1a9107f6b4e6 100644 --- a/pkgs/development/libraries/agda/cubical-mini/default.nix +++ b/pkgs/development/libraries/agda/cubical-mini/default.nix @@ -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 = [ diff --git a/pkgs/development/libraries/agda/cubical/default.nix b/pkgs/development/libraries/agda/cubical/default.nix index 32cf1063383b..72bb3c3a501d 100644 --- a/pkgs/development/libraries/agda/cubical/default.nix +++ b/pkgs/development/libraries/agda/cubical/default.nix @@ -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; { diff --git a/pkgs/development/libraries/agda/functional-linear-algebra/default.nix b/pkgs/development/libraries/agda/functional-linear-algebra/default.nix index 40ec014ca129..a2d5cae4f6f5 100644 --- a/pkgs/development/libraries/agda/functional-linear-algebra/default.nix +++ b/pkgs/development/libraries/agda/functional-linear-algebra/default.nix @@ -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 = '' diff --git a/pkgs/development/libraries/agda/generics/default.nix b/pkgs/development/libraries/agda/generics/default.nix index 71219e334612..e2eefb445e9d 100644 --- a/pkgs/development/libraries/agda/generics/default.nix +++ b/pkgs/development/libraries/agda/generics/default.nix @@ -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"; diff --git a/pkgs/development/libraries/agda/standard-library/default.nix b/pkgs/development/libraries/agda/standard-library/default.nix index f05158d56a1c..976d84157836 100644 --- a/pkgs/development/libraries/agda/standard-library/default.nix +++ b/pkgs/development/libraries/agda/standard-library/default.nix @@ -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"; diff --git a/pkgs/top-level/agda-packages.nix b/pkgs/top-level/agda-packages.nix index a943c2c52cfd..1289445a5872 100644 --- a/pkgs/top-level/agda-packages.nix +++ b/pkgs/top-level/agda-packages.nix @@ -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 { };