From 168d9a5f1e72dd109c53f844a9ba54795613276c Mon Sep 17 00:00:00 2001 From: Ingo Blechschmidt Date: Tue, 31 Jan 2023 22:33:20 +0100 Subject: [PATCH] agda: 2.6.2.2 -> 2.6.3 --- .../scripts/haskell/update-stackage.sh | 2 + pkgs/build-support/agda/default.nix | 7 ++++ .../configuration-hackage2nix/stackage.yaml | 1 - .../haskell-modules/hackage-packages.nix | 38 ------------------- .../agda/agda-categories/default.nix | 20 +++++++--- .../libraries/agda/agda-prelude/default.nix | 6 +-- .../libraries/agda/cubical/default.nix | 8 ++-- .../agda/standard-library/default.nix | 4 +- 8 files changed, 31 insertions(+), 55 deletions(-) diff --git a/maintainers/scripts/haskell/update-stackage.sh b/maintainers/scripts/haskell/update-stackage.sh index 426c371d1d35..95efeff732b6 100755 --- a/maintainers/scripts/haskell/update-stackage.sh +++ b/maintainers/scripts/haskell/update-stackage.sh @@ -63,11 +63,13 @@ sed -r \ -e '/ lsp-test /d' \ -e '/ hie-bios /d' \ -e '/ ShellCheck /d' \ + -e '/ Agda /d' \ < "${tmpfile_new}" >> $stackage_config # Explanations: # cabal2nix, distribution-nixpkgs, jailbreak-cabal, language-nix: These are our packages and we know what we are doing. # lsp, lsp-types, lsp-test, hie-bios: These are tightly coupled to hls which is not in stackage. They have no rdeps in stackage. # ShellCheck: latest version of command-line dev tool. +# Agda: The Agda community is fast-moving; we strive to always include the newest versions of Agda and the Agda packages in nixpkgs. if [[ "${1:-}" == "--do-commit" ]]; then git add $stackage_config diff --git a/pkgs/build-support/agda/default.nix b/pkgs/build-support/agda/default.nix index fed0f6cb3441..7eeaf73d07ce 100644 --- a/pkgs/build-support/agda/default.nix +++ b/pkgs/build-support/agda/default.nix @@ -81,6 +81,13 @@ let runHook postInstall ''; + # As documented at https://github.com/NixOS/nixpkgs/issues/172752, + # we need to set LC_ALL to an UTF-8-supporting locale. However, on + # darwin, it seems that there is no standard such locale; luckily, + # the referenced issue doesn't seem to surface on darwin. Hence let's + # set this only on non-darwin. + LC_ALL = lib.optionalString (!stdenv.isDarwin) "C.UTF-8"; + meta = if meta.broken or false then meta // { hydraPlatforms = lib.platforms.none; } else meta; # Retrieve all packages from the finished package set that have the current package as a dependency and build them diff --git a/pkgs/development/haskell-modules/configuration-hackage2nix/stackage.yaml b/pkgs/development/haskell-modules/configuration-hackage2nix/stackage.yaml index 31b5d417b84c..169a3664f1da 100644 --- a/pkgs/development/haskell-modules/configuration-hackage2nix/stackage.yaml +++ b/pkgs/development/haskell-modules/configuration-hackage2nix/stackage.yaml @@ -38,7 +38,6 @@ default-package-overrides: - aeson-value-parser ==0.19.7 - aeson-yak ==0.1.1.3 - aeson-yaml ==1.1.0.1 - - Agda ==2.6.2.2 - agda2lagda ==0.2021.6.1 - airship ==0.9.5 - al ==0.1.4.2 diff --git a/pkgs/development/haskell-modules/hackage-packages.nix b/pkgs/development/haskell-modules/hackage-packages.nix index 99210d057a82..61c19c5b320f 100644 --- a/pkgs/development/haskell-modules/hackage-packages.nix +++ b/pkgs/development/haskell-modules/hackage-packages.nix @@ -809,43 +809,6 @@ self: { }) {}; "Agda" = callPackage - ({ mkDerivation, aeson, alex, array, async, base, binary - , blaze-html, boxes, bytestring, Cabal, case-insensitive - , containers, data-hash, deepseq, directory, edit-distance, emacs - , equivalence, exceptions, filepath, ghc-compact, gitrev, happy - , hashable, hashtables, haskeline, monad-control, mtl, murmur-hash - , parallel, pretty, process, regex-tdfa, split, stm, strict - , template-haskell, text, time, transformers, unordered-containers - , uri-encode, zlib - }: - mkDerivation { - pname = "Agda"; - version = "2.6.2.2"; - sha256 = "0yjjbhc593ylrm4mq4j01nkdvh7xqsg5in30wxj4y53vf5hkggp5"; - revision = "2"; - editedCabalFile = "0mas4lsd093rg4w6js12cjmnz8227q5g0jhkhyrnr25jglqjz75n"; - isLibrary = true; - isExecutable = true; - enableSeparateDataOutput = true; - setupHaskellDepends = [ base Cabal directory filepath process ]; - libraryHaskellDepends = [ - aeson array async base binary blaze-html boxes bytestring - case-insensitive containers data-hash deepseq directory - edit-distance equivalence exceptions filepath ghc-compact gitrev - hashable hashtables haskeline monad-control mtl murmur-hash - parallel pretty process regex-tdfa split stm strict - template-haskell text time transformers unordered-containers - uri-encode zlib - ]; - libraryToolDepends = [ alex happy ]; - executableHaskellDepends = [ base directory filepath process ]; - executableToolDepends = [ emacs ]; - description = "A dependently typed functional programming language and proof assistant"; - license = "unknown"; - maintainers = [ lib.maintainers.abbradar lib.maintainers.turion ]; - }) {inherit (pkgs) emacs;}; - - "Agda_2_6_3" = callPackage ({ mkDerivation, aeson, alex, array, async, base, binary , blaze-html, boxes, bytestring, Cabal, case-insensitive , containers, data-hash, deepseq, directory, dlist, edit-distance @@ -877,7 +840,6 @@ self: { executableToolDepends = [ emacs ]; description = "A dependently typed functional programming language and proof assistant"; license = "unknown"; - hydraPlatforms = lib.platforms.none; maintainers = [ lib.maintainers.abbradar lib.maintainers.turion ]; }) {inherit (pkgs) emacs;}; diff --git a/pkgs/development/libraries/agda/agda-categories/default.nix b/pkgs/development/libraries/agda/agda-categories/default.nix index 12bc6e7e4e19..ff520fb85ef3 100644 --- a/pkgs/development/libraries/agda/agda-categories/default.nix +++ b/pkgs/development/libraries/agda/agda-categories/default.nix @@ -1,21 +1,29 @@ { lib, mkDerivation, fetchFromGitHub, standard-library }: mkDerivation rec { - version = "0.1.7.1"; + version = "0.1.7.1a"; pname = "agda-categories"; src = fetchFromGitHub { owner = "agda"; repo = "agda-categories"; rev = "v${version}"; - sha256 = "1acb693ad2nrmnn6jxsyrlkc0di3kk2ksj2w9wnyfxrgvfsil7rn"; + sha256 = "sha256-VlxRDxXg+unzYlACUU58JQUHXxtg0fI5dEQvlBRxJtU="; }; - # Remove this once new version of agda-categories is released which - # directly references standard-library-1.7.1 postPatch = '' - substituteInPlace agda-categories.agda-lib \ - --replace 'standard-library-1.7' 'standard-library-1.7.1' + # Remove this once agda-categories incorporates this fix or once Agda's + # versioning system gets an overhaul in general. Right now there is no middle + # ground between "no version constraint" and "exact match down to patch". We + # do not want to need to change this postPatch directive on each minor + # version update of the stdlib, so we get rid of the version constraint + # altogether. + sed -Ei 's/standard-library-[0-9.]+/standard-library/' agda-categories.agda-lib + + # The Makefile of agda-categories uses git(1) instead of find(1) to + # determine the list of source files. We cannot use git, as $PWD will not + # be a valid Git working directory. + find src -name '*.agda' | sed -e 's|^src/[/]*|import |' -e 's|/|.|g' -e 's/.agda//' -e '/import Everything/d' | LC_COLLATE='C' sort > Everything.agda ''; buildInputs = [ standard-library ]; diff --git a/pkgs/development/libraries/agda/agda-prelude/default.nix b/pkgs/development/libraries/agda/agda-prelude/default.nix index 693bad67d08e..573b13d3b4f9 100644 --- a/pkgs/development/libraries/agda/agda-prelude/default.nix +++ b/pkgs/development/libraries/agda/agda-prelude/default.nix @@ -1,14 +1,14 @@ { lib, mkDerivation, fetchFromGitHub }: mkDerivation rec { - version = "compat-2.6.2"; + version = "unstable-2022-01-14"; pname = "agda-prelude"; src = fetchFromGitHub { owner = "UlfNorell"; repo = "agda-prelude"; - rev = version; - sha256 = "0j2nip5fbn61fpkm3qz4dlazl4mzdv7qlgw9zm15bkcvaila0h14"; + rev = "3d143d6d0a3f75966602480665623e87233ff93e"; + hash = "sha256-ILhXDq788vrceMp5mCiQUMrJxeLPtS4yGtvMHMYxzg8="; }; preConfigure = '' diff --git a/pkgs/development/libraries/agda/cubical/default.nix b/pkgs/development/libraries/agda/cubical/default.nix index a69edded5b3d..5cd2a4a9a232 100644 --- a/pkgs/development/libraries/agda/cubical/default.nix +++ b/pkgs/development/libraries/agda/cubical/default.nix @@ -2,17 +2,15 @@ mkDerivation rec { pname = "cubical"; - version = "0.4"; + version = "unstable-2023-02-09"; src = fetchFromGitHub { repo = pname; owner = "agda"; - rev = "v${version}"; - hash = "sha256-bnHz5uZXZnn1Zd36tq/veA4yT7dhJ1c+AYpgdDfSRzE="; + rev = "6b1ce0b67fd94693c1a3e340c8e8765380de0edc"; + hash = "sha256-XRCaW94oAgy2GOnFiI9c5A8mEx7AzlbT4pFd+PMmc9o="; }; - LC_ALL = "C.UTF-8"; - # The cubical library has several `Everything.agda` files, which are # compiled through the make file they provide. nativeBuildInputs = [ ghc ]; diff --git a/pkgs/development/libraries/agda/standard-library/default.nix b/pkgs/development/libraries/agda/standard-library/default.nix index bad3a02470e4..76f69f54d719 100644 --- a/pkgs/development/libraries/agda/standard-library/default.nix +++ b/pkgs/development/libraries/agda/standard-library/default.nix @@ -2,13 +2,13 @@ mkDerivation rec { pname = "standard-library"; - version = "1.7.1"; + version = "1.7.2"; src = fetchFromGitHub { repo = "agda-stdlib"; owner = "agda"; rev = "v${version}"; - sha256 = "0khl12jvknsvjsq3l5cbp2b5qlw983qbymi1dcgfz9z0b92si3r0"; + hash = "sha256-vvbyfC5+Yyx18IDikSbAAcTHHtU6krlz45Fd2YlwsBg="; }; nativeBuildInputs = [ (ghcWithPackages (self : [ self.filemanip ])) ];