Update nixpkgs and agda libraries (#14)

cardano-scaling · Jan 18, 2025 · 7355e7e · 7355e7e
1 parent 34ea745
commit 7355e7e
Show file tree

Hide file tree

Showing 9 changed files with 68 additions and 31 deletions.
diff --git a/flake.lock b/flake.lock
diff --git a/flake.nix b/flake.nix
@@ -25,6 +25,7 @@
           };
           agdaLibraries = with agdaPackages;
             [
+              abstract-set-theory
               formal-ledger
               standard-library
               standard-library-classes

diff --git a/hydra-protocol.agda-lib b/hydra-protocol.agda-lib
@@ -1,5 +1,6 @@
 name: hydra-protocol
 depend:
+  abstract-set-theory
   formal-ledger
   standard-library
   standard-library-classes

diff --git a/nix/initial-packages.nix b/nix/initial-packages.nix
@@ -17,6 +17,8 @@ let
 
       agda = withPackages [ ];
 
+      abstract-set-theory = callPackage ./pkgs/abstract-set-theory.nix { };
+
       formal-ledger = callPackage ./pkgs/formal-ledger.nix { };
 
       standard-library = callPackage ./pkgs/standard-library.nix { };

diff --git a/nix/pkgs/abstract-set-theory.nix b/nix/pkgs/abstract-set-theory.nix
@@ -0,0 +1,22 @@
+{ lib, mkDerivation, fetchFromGitHub, standard-library, standard-library-classes, standard-library-meta }:
+
+mkDerivation rec {
+  version = "0.1.0";
+  pname = "abstract-set-theory";
+
+  src = (fetchFromGitHub {
+    owner = "input-output-hk";
+    repo = "agda-sets";
+    rev = "751b3ee39122fe33022af41e6c94dc820afde19a";
+    sha256 = "sha256-0vjmNN8wuZXT4NM3aEv4z1Y+/6LpNfb7vzeajwZ3eFY=";
+  });
+
+  buildInputs = [ standard-library standard-library-classes standard-library-meta ];
+
+  everythingFile = "src/abstract-set-theory.agda";
+
+  libraryFile = "abstract-set-theory.agda-lib";
+
+  meta = { };
+}
+
diff --git a/nix/pkgs/formal-ledger.nix b/nix/pkgs/formal-ledger.nix
@@ -1,17 +1,17 @@
-{ lib, mkDerivation, fetchFromGitHub, standard-library, standard-library-classes, standard-library-meta }:
+{ lib, mkDerivation, fetchFromGitHub, abstract-set-theory, standard-library, standard-library-classes, standard-library-meta }:
 
 mkDerivation rec {
   version = "0.2.0";
   pname = "formal-ledger";
 
   src = (fetchFromGitHub {
-    owner = "locallycompact";
+    owner = "IntersectMBO";
     repo = "formal-ledger-specifications";
-    rev = "d2a1746ec6671ee7699487ae41b97b275160e71a";
-    sha256 = "sha256-2G9VEimSLFm4j/LdM+khJ43jTRwc3q7eQEdY6w5KvD8=";
+    rev = "cef3505f275900c51737071b5671e5dad47dc576";
+    sha256 = "sha256-KAyojB3uClt72fhOzw9iDSCGzlL8EUhEtK/Xizj5pyU=";
   }) + "/src";
 
-  buildInputs = [ standard-library standard-library-classes standard-library-meta ];
+  buildInputs = [ abstract-set-theory standard-library standard-library-classes standard-library-meta ];
 
   meta = { };
 }

diff --git a/nix/pkgs/standard-library-classes.nix b/nix/pkgs/standard-library-classes.nix
@@ -7,14 +7,14 @@ mkDerivation rec {
   src = fetchFromGitHub {
     owner = "omelkonian";
     repo = "agda-stdlib-classes";
-    rev = "v${version}";
-    sha256 = "sha256-PcieRRnctjCzFCi+gUYAgyIAicMOAZPl8Sw35fZdt0E=";
+    rev = "28df278381c94a25c54f6819524cd9f8cb99f092";
+    sha256 = "sha256-TdPJ3K4jyAIQgX1sUrqd0QeA72n2mkBVzlg8WfrqWWY=";
   };
 
   buildInputs = [ standard-library ];
 
   libraryFile = "agda-stdlib-classes.agda-lib";
-  everythingFile = "Classes.agda";
+  everythingFile = "standard-library-classes.agda";
 
   meta = { };
 }

diff --git a/nix/pkgs/standard-library-meta.nix b/nix/pkgs/standard-library-meta.nix
@@ -1,14 +1,14 @@
 { lib, mkDerivation, fetchFromGitHub, standard-library, standard-library-classes }:
 
 mkDerivation rec {
-  version = "2.0";
+  version = "2.1.1";
   pname = "agda-stdlib-meta";
 
   src = fetchFromGitHub {
-    owner = "input-output-hk";
-    repo = "stdlib-meta";
-    rev = "4fc4b1ed6e47d180516917d04be87cbacbf7d314";
-    sha256 = "T+9vwccbDO1IGBcGLjgV/fOt+IN14KEV9ct/J6nQCsM=";
+    owner = "agda";
+    repo = "agda-stdlib-meta";
+    rev = "v${version}";
+    sha256 = "sha256-qOoThYMG0dzjKvwmzzVZmGcerfb++MApbaGRzLEq3/4=";
   };
 
   buildInputs = [ standard-library standard-library-classes ];

diff --git a/nix/pkgs/standard-library.nix b/nix/pkgs/standard-library.nix
@@ -1,17 +1,23 @@
-{ lib, mkDerivation, fetchFromGitHub, ghcWithPackages, nixosTests }:
+{
+  lib,
+  mkDerivation,
+  fetchFromGitHub,
+  ghcWithPackages,
+  nixosTests,
+}:
 
 mkDerivation rec {
   pname = "standard-library";
-  version = "2.0";
+  version = "2.1.1";
 
   src = fetchFromGitHub {
     repo = "agda-stdlib";
     owner = "agda";
     rev = "v${version}";
-    hash = "sha256-TjGvY3eqpF+DDwatT7A78flyPcTkcLHQ1xcg+MKgCoE=";
+    hash = "sha256-4HfwNAkIhk1yC/oSxZ30xilzUM5/22nzbUSqTjcW5Ng=";
   };
 
-  nativeBuildInputs = [ (ghcWithPackages (self : [ self.filemanip ])) ];
+  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
@@ -25,6 +31,11 @@ mkDerivation rec {
     description = "Standard library for use with the Agda compiler";
     license = lib.licenses.mit;
     platforms = lib.platforms.unix;
-    maintainers = with maintainers; [ jwiegley mudri alexarice turion ];
+    maintainers = with maintainers; [
+      jwiegley
+      mudri
+      alexarice
+      turion
+    ];
   };
 }