Try to import Utxow from formal-ledger

Hydra/Protocol/Main.lagda

@@ -69,6 +69,8 @@ module Hydra.Protocol.Main where
 
 open import Data.Nat
 
+open import Ledger.Utxo
+
 data HydraState : Set where
   Idle         : HydraState
   Open         : HydraState

flake.nix

@@ -14,13 +14,16 @@
         "x86_64-linux"
       ];
       perSystem = { pkgs, ... }:
+        let
+          agdaPackages = pkgs.callPackage ./initial-packages.nix { Agda = pkgs.haskellPackages.Agda; nixpkgs = inputs.nixpkgs; };
+        in
         rec {
           packages = {
-            hydra-agda-spec = pkgs.agdaPackages.mkDerivation { 
+            hydra-agda-spec = agdaPackages.mkDerivation { 
               pname = "hydra-formal-specification";
               version = "0.0.1";
               src = ./.;
-              buildInputs = [ pkgs.agdaPackages.standard-library ];
+              buildInputs = [ agdaPackages.standard-library agdaPackages.formal-ledger ];
               meta = { };
               buildPhase = ''
                 agda --latex Hydra/Protocol/Main.lagda

hydra-formal-specification.agda-lib

@@ -1,4 +1,5 @@
 name: hydra-formal-specification
 depend:
   standard-library
+  formal-ledger
 include: .

initial-packages.nix

@@ -0,0 +1,28 @@
+{ pkgs, lib, newScope, Agda, nixpkgs }:
+
+let
+  mkAgdaPackages = Agda: lib.makeScope newScope (mkAgdaPackages' Agda);
+  mkAgdaPackages' = Agda: self: let
+    inherit (self) callPackage;
+    inherit (callPackage "${nixpkgs}/pkgs/build-support/agda" {
+      inherit Agda self;
+      inherit (pkgs.haskellPackages) ghcWithPackages;
+    }) withPackages mkDerivation;
+  in {
+    inherit mkDerivation;
+
+    lib = lib.extend (final: prev: import "${nixpkgs}/pkgs/build-support/agda/lib.nix" { lib = prev; });
+
+    agda = withPackages [];
+
+    formal-ledger = callPackage ./nix/formal-ledger.nix { };
+
+    standard-library = callPackage ./nix/standard-library.nix { };
+      inherit (pkgs.haskellPackages) ghcWithPackages;
+
+    standard-library-classes = callPackage ./nix/standard-library-classes.nix { };
+
+    standard-library-meta = callPackage ./nix/standard-library-meta.nix { };
+
+  };
+in mkAgdaPackages Agda

nix/formal-ledger.nix

@@ -0,0 +1,18 @@
+{ lib, mkDerivation, fetchFromGitHub, standard-library, standard-library-classes, standard-library-meta }:
+
+mkDerivation rec {
+  version = "0.2.0";
+  pname = "formal-ledger";
+
+  src = (fetchFromGitHub {
+    owner = "IntersectMBO";
+    repo = "formal-ledger-specifications";
+    rev = "b1c45bca6da88db0c007a6bbd7eff9dd1892aa44";
+    sha256 = "sha256-Mzem6L5GkNbNt78XG7qnrz6+mWOpXRqGG8aEiXxMLuA=";
+  }) + "/src";
+
+  buildInputs = [ standard-library standard-library-classes standard-library-meta ];
+
+  meta = { };
+}
+

nix/standard-library-classes.nix

@@ -0,0 +1,21 @@
+{ lib, mkDerivation, fetchFromGitHub, standard-library }:
+
+mkDerivation rec {
+  version = "2.0";
+  pname = "standard-library-classes";
+
+  src = fetchFromGitHub {
+    owner = "omelkonian";
+    repo = "agda-stdlib-classes";
+    rev = "v${version}";
+    sha256 = "sha256-PcieRRnctjCzFCi+gUYAgyIAicMOAZPl8Sw35fZdt0E=";
+  };
+
+  buildInputs = [ standard-library ];
+
+  libraryFile = "agda-stdlib-classes.agda-lib";
+  everythingFile = "Classes.agda";
+
+  meta = { };
+}
+

nix/standard-library-meta.nix

@@ -0,0 +1,21 @@
+{ lib, mkDerivation, fetchFromGitHub, standard-library, standard-library-classes }:
+
+mkDerivation rec {
+  version = "2.0";
+  pname = "agda-stdlib-meta";
+
+  src = fetchFromGitHub {
+    owner = "input-output-hk";
+    repo = "stdlib-meta";
+    rev = "4fc4b1ed6e47d180516917d04be87cbacbf7d314";
+    sha256 = "T+9vwccbDO1IGBcGLjgV/fOt+IN14KEV9ct/J6nQCsM=";
+  };
+
+  buildInputs = [ standard-library standard-library-classes ];
+
+  libraryFile = "agda-stdlib-meta.agda-lib";
+  everythingFile = "Main.agda";
+
+  meta = { };
+}
+

nix/standard-library.nix

@@ -0,0 +1,30 @@
+{ lib, mkDerivation, fetchFromGitHub, ghcWithPackages, nixosTests }:
+
+mkDerivation rec {
+  pname = "standard-library";
+  version = "2.0";
+
+  src = fetchFromGitHub {
+    repo = "agda-stdlib";
+    owner = "agda";
+    rev = "v${version}";
+    hash = "sha256-TjGvY3eqpF+DDwatT7A78flyPcTkcLHQ1xcg+MKgCoE=";
+  };
+
+  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";
+    description = "Standard library for use with the Agda compiler";
+    license = lib.licenses.mit;
+    platforms = lib.platforms.unix;
+    maintainers = with maintainers; [ jwiegley mudri alexarice turion ];
+  };
+}