Use Agda Haskell lib instead of MAlonzo (#6562)

Co-authored-by: zeme <[email protected]>

nix/agda.nix

@@ -0,0 +1,147 @@
+{ repoRoot, inputs, pkgs, system, lib }:
+
+rec {
+
+  agda-stdlib = agda-packages.standard-library.overrideAttrs (oldAtts: rec {
+
+    version = "1.7.3";
+
+    src = pkgs.fetchFromGitHub {
+      repo = "agda-stdlib";
+      owner = "agda";
+      rev = "v${version}";
+      sha256 = "sha256-vtL6VPvTXhl/mepulUm8SYyTjnGsqno4RHDmTIy22Xg=";
+    };
+
+    # This is preConfigure is copied from more recent nixpkgs that also
+    # uses version 1.7 of standard-library. Old nixpkgs (that used 1.4)
+    # had a preConfigure step that worked with 1.7. Less old nixpkgs
+    # (that used 1.6) had a preConfigure step that attempts to `rm`
+    # files that are now in the .gitignore list for 1.
+    preConfigure = ''
+      runhaskell GenerateEverything.hs
+      # We will only build/consider Everything.agda, in particular we don't want Everything*.agda
+      # do be copied to the store.
+      rm EverythingSafe.agda
+    '';
+  });
+
+
+  # We want to keep control of which version of Agda we use, so we supply our own and override
+  # the one from nixpkgs.
+  #
+  # The Agda builder needs a derivation with:
+  # - The 'agda' executable
+  # - The 'agda-mode' executable
+  # - A 'version' attribute
+  #
+  # So we stitch one together here.
+  #
+  # Furthermore, the agda builder uses a `ghcWithPackages` that has to have ieee754 available.
+  # We'd like it to use the same GHC as we have, if nothing else just to avoid depending on
+  # another GHC from nixpkgs! Sadly, this one is harder to override, and we just hack
+  # it into pkgs.haskellPackages in a fragile way. Annoyingly, this also means we have to ensure
+  # we have a few extra packages that it uses in our Haskell package set.
+  agda-packages =
+    let
+      Agda = agda-project.hsPkgs.Agda;
+
+      frankenAgdaBin = pkgs.symlinkJoin {
+        name = "agda";
+        version = Agda.identifier.version;
+        paths = [
+          Agda.components.exes.agda
+          Agda.components.exes.agda-mode
+        ];
+      };
+
+      frankenAgda = frankenAgdaBin // {
+        # Newer Agda is built with enableSeparateBinOutput, hence this hacky workaround.
+        # https://github.com/NixOS/nixpkgs/commit/294245f7501e0a8e69b83346a4fa5afd4ed33ab3
+        bin = frankenAgdaBin;
+      };
+
+      frankenPkgs =
+        pkgs //
+        {
+          haskellPackages = pkgs.haskellPackages //
+          {
+            inherit (agda-project) ghcWithPackages;
+          };
+        };
+    in
+    pkgs.agdaPackages.override {
+      Agda = frankenAgda;
+      pkgs = frankenPkgs;
+    };
+
+
+  # Agda is a huge pain. They have a special custom setup that compiles the
+  # interface files for the Agda that ships with the compiler. These go in
+  # the data files for the *library*, but they require the *executable* to
+  # compile them, which depends on the library! They get away with it by
+  # using the old-style builds and building everything together, we can't
+  # do that.
+  # So we work around it:
+  # - turn off the custom setup
+  # - manually compile the executable (fortunately it has no extra dependencies!)
+  #   and do the compilation at the end of the library derivation.
+  # In addition, depending on whether we are cross-compiling or not, the
+  # compiler-nix-name handed to us by haskell.nix will be different, so we need
+  # to pass it in.
+  agda-project-module-patch = { compiler-nix-name }: {
+    packages.Agda.doHaddock = lib.mkForce false;
+    packages.Agda.package.buildType = lib.mkForce "Simple";
+    packages.Agda.components.library.enableSeparateDataOutput = lib.mkForce true;
+    packages.Agda.components.library.postInstall = ''
+      # Compile the executable using the package DB we've just made, which contains
+      # the main Agda library
+      ${compiler-nix-name} src/main/Main.hs -package-db=$out/package.conf.d -o agda
+
+      # Find all the files in $data
+      shopt -s globstar
+      files=($data/**/*.agda)
+      for f in "''${files[@]}" ; do
+        echo "Compiling $f"
+        # This is what the custom setup calls in the end
+        ./agda --no-libraries --local-interfaces $f
+      done
+    '';
+  };
+
+
+  agda-project-module-patch-default = agda-project-module-patch {
+    compiler-nix-name = "ghc";
+  };
+
+
+  agda-project-module-patch-musl64 = agda-project-module-patch {
+    compiler-nix-name = "x86_64-unknown-linux-musl-ghc";
+  };
+
+
+  agda-with-stdlib = agda-packages.agda.withPackages [ agda-stdlib ];
+
+
+  agda-project = pkgs.haskell-nix.hackage-project {
+    name = "Agda";
+    version = "2.6.4.3";
+    compiler-nix-name = "ghc96";
+    cabalProjectLocal = "extra-packages: ieee754, filemanip";
+    modules = [ agda-project-module-patch-default ];
+  };
+
+
+  # TODO this is a bit of a hack, but it's the only way to get the uplc
+  # executable to find the metatheory and the stdandard library.
+  shell-hook-exports = ''
+    export AGDA_STDLIB_SRC="${agda-stdlib}/src"
+    export PLUTUS_METHATHEORY_SRC="./plutus-metatheory/src"
+  '';
+
+
+  wrap-program-args = ''
+    --set AGDA_STDLIB_SRC "${agda-stdlib}/src" \
+    --set PLUTUS_METHATHEORY_SRC "./plutus-metatheory/src"
+  '';
+}

nix/build-latex-doc.nix

@@ -16,7 +16,7 @@ repoRoot.nix.build-latex {
 
 
   buildInputs = lib.optionals withAgda [
-    repoRoot.nix.agda-with-stdlib
+    repoRoot.nix.agda.agda-with-stdlib
   ];
 
 

nix/outputs.nix

@@ -35,7 +35,6 @@ in
   {
     packages.plutus-metatheory-site = repoRoot.nix.plutus-metatheory-site;
     packages.pre-commit-check = ghc96.pre-commit-check;
-    packages.agda-project = repoRoot.nix.agda-project.hsPkgs.Agda.components.exes.agda;
   }
 
   (lib.optionalAttrs (system == "x86_64-linux" || system == "x86_64-darwin")
@@ -64,9 +63,7 @@ in
   (lib.optionalAttrs (system == "aarch64-darwin")
     {
       # Plausibly if things build on x86 darwin then they'll build on aarch darwin.
-      # Se we only build roots and devshells on aarch to avoid overloading the builders.
-      # Note: We can't build the 9.6 shell on aarch64-darwin
-      # because of https://github.com/well-typed/cborg/issues/311
+      # Se we only build roots and dev sshells on aarch to avoid overloading the builders.
       hydraJobs.ghc810.devShell = ghc810.devShell;
       hydraJobs.ghc96.devShell = ghc96.devShell;
       hydraJobs.ghc98.devShell = ghc98.devShell;

nix/plutus-metatheory-site.nix

@@ -21,7 +21,7 @@ let
   plutus-metatheory-agda-html = pkgs.stdenv.mkDerivation {
     name = "plutus-metatheory-doc";
     src = lib.cleanSource (inputs.self + /plutus-metatheory);
-    buildInputs = [ repoRoot.nix.agda-with-stdlib ];
+    buildInputs = [ repoRoot.nix.agda.agda-with-stdlib ];
     dontInstall = true;
 
     # Jekyll requires the _layouts folder to be in the same directory as the

nix/project.nix

@@ -4,7 +4,10 @@
 
 let
   cabalProject = pkgs.haskell-nix.cabalProject' ({ config, pkgs, ... }:
-    let isCrossCompiling = pkgs.stdenv.hostPlatform != pkgs.stdenv.buildPlatform; in
+    let
+      isCompilingMingwW64 = pkgs.stdenv.hostPlatform.system == "x86_64-windows" && pkgs.stdenv.hostPlatform.libc == "msvcrt";
+      isCompilingMusl64 = pkgs.stdenv.hostPlatform.system == "x86_64-linux" && pkgs.stdenv.hostPlatform.libc == "musl";
+    in
     {
       name = "plutus";
 
@@ -41,19 +44,32 @@ let
       };
 
       modules = [
+
+        (
+          lib.mkIf (!isCompilingMingwW64 && !isCompilingMusl64) repoRoot.nix.agda.agda-project-module-patch-default
+        )
+
+        (
+          lib.mkIf isCompilingMusl64 repoRoot.nix.agda.agda-project-module-patch-musl64
+        )
+
         # Common
         {
           packages = {
             # plutus-metatheory needs agda with the stdlib around for the custom setup
             # I can't figure out a way to apply this as a blanket change for all the
             # components in the package, oh well
-            plutus-metatheory.components.library.build-tools = [ repoRoot.nix.agda-with-stdlib ];
-            plutus-metatheory.components.exes.plc-agda.build-tools = [ repoRoot.nix.agda-with-stdlib ];
-            plutus-metatheory.components.tests.test-NEAT.build-tools = [ repoRoot.nix.agda-with-stdlib ];
+            plutus-metatheory.components.library.build-tools = [ repoRoot.nix.agda.agda-with-stdlib ];
+            plutus-metatheory.components.exes.plc-agda.build-tools = [ repoRoot.nix.agda.agda-with-stdlib ];
+            plutus-metatheory.components.tests.test-NEAT.build-tools = [ repoRoot.nix.agda.agda-with-stdlib ];
+
+            plutus-executables.components.exes.uplc.build-tools = [ repoRoot.nix.agda.agda-with-stdlib ];
+            plutus-executables.components.exes.uplc.postInstall = ''
+              wrapProgram $out/bin/uplc ${repoRoot.nix.agda.wrap-program-args}
+            '';
 
-            plutus-executables.components.exes.uplc.build-tools = [ repoRoot.nix.agda-with-stdlib ];
-            plutus-executables.components.tests.test-simple.build-tools = [ repoRoot.nix.agda-with-stdlib ];
-            plutus-executables.components.tests.test-detailed.build-tools = [ repoRoot.nix.agda-with-stdlib ];
+            plutus-executables.components.tests.test-simple.build-tools = [ repoRoot.nix.agda.agda-with-stdlib ];
+            plutus-executables.components.tests.test-detailed.build-tools = [ repoRoot.nix.agda.agda-with-stdlib ];
 
             plutus-core.components.benchmarks.update-cost-model = {
               build-tools = [ repoRoot.nix.r-with-packages ];

nix/shell.nix

@@ -29,7 +29,7 @@ in
   welcomeMessage = "🤟 \\033[1;34mWelcome to Plutus\\033[0m 🤟";
 
   packages = [
-    repoRoot.nix.agda-with-stdlib
+    repoRoot.nix.agda.agda-with-stdlib
 
     # R environment
     repoRoot.nix.r-with-packages
@@ -92,6 +92,7 @@ in
 
   shellHook = ''
     ${builtins.readFile certEnv}
+    ${repoRoot.nix.agda.shell-hook-exports}
   '';
 
   preCommit = {

nix/unraveling-recursion-paper.nix

@@ -35,7 +35,7 @@ repoRoot.nix.build-latex {
   };
 
   buildInputs = [
-    repoRoot.nix.agda-with-stdlib
+    repoRoot.nix.agda.agda-with-stdlib
     pkgs.zip
   ];