agda: 2.6.2.2 -> 2.6.3

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

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

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

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

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

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 = ''

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

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