From bfe7f645c4473c5c5a51c24efa622e1e6d076844 Mon Sep 17 00:00:00 2001
From: Brian W Bush <brian.bush@iohk.io>
Date: Mon, 19 Feb 2024 11:15:20 -0700
Subject: [PATCH] Revised shell variables so `make` works inside/outside `nix
 develop`.

---
 Makefile        |  8 ++++++--
 nix/agda2hs.nix | 22 +---------------------
 nix/shell.nix   |  3 ++-
 3 files changed, 9 insertions(+), 24 deletions(-)

diff --git a/Makefile b/Makefile
index 445139f99..b36cedce4 100644
--- a/Makefile
+++ b/Makefile
@@ -18,13 +18,17 @@ typecheck: $(HSFILES) $(LHSFILES)
 
 # From https://stackoverflow.com/questions/34621364/makefile-compile-o-from-c-files
 $(HSDIR)/%.hs: %.agda
-	@$(AGDA2HS) --library-file=$(AGDA_LIBS) --compile-dir=$(HSDIR)/src $^
+	@$(AGDA2HS) --local-interfaces --library-file=$(AGDA_LIBS) --compile-dir=$(HSDIR)/src $^
 
 # FIXME: this obviously won't scale...
 $(HSDIR)/src/Peras/SmallStep.hs: src/Peras/SmallStep.lagda.md
-	@$(AGDA2HS) --library-file=$(AGDA_LIBS) --compile-dir=$(HSDIR)/src $^
+	@$(AGDA2HS) --local-interfaces --library-file=$(AGDA_LIBS) --compile-dir=$(HSDIR)/src $^
 
 .PHONY : clean veryclean
 clean:
 	@echo "Removing .agdai files"
 	@find src -name \*.agdai -delete;
+
+veryclean:
+	@echo "Removing generated.hs files"
+	@rm $(HSFILES) $(LHSFILES)
diff --git a/nix/agda2hs.nix b/nix/agda2hs.nix
index 4ccf6a7ea..44190b1a0 100644
--- a/nix/agda2hs.nix
+++ b/nix/agda2hs.nix
@@ -17,26 +17,6 @@ let
   };
 
   agdaLib = repoRoot.nix.agda-packages.mkDerivation {
-    pname = "agda2hs";
-    version = "1.2";
-    src = inputs.agda2nix;
-    meta = {
-      description = "agda2hs";
-    };
-    everythingFile = "./lib/Everything.agda";
-    preBuild = ''
-      # This won't compile without `--sized-types`.
-      sed -i '/^flags:/s/$/ --sized-types/' agda2hs.agda-lib
-      # Create the missing everything file.
-      find lib -type f -name \*.agda | sed -e 's/^lib\//import /; s/\.agda$// ; s/\//./g' > Everything.agda
-      sed -i '1imodule Everything where' Everything.agda
-      mv Everything.agda lib/
-      # Remove extraneous files.
-      rm -rf test tutorials
-    '';
-  };
-
-  altAgdaLib = repoRoot.nix.agda-packages.mkDerivation {
     pname = "agda2hs";
     version = "1.2";
     src = inputs.agda2nix;
@@ -60,5 +40,5 @@ in
 
 {
   exe = haskellProject.hsPkgs.agda2hs.components.exes.agda2hs;
-  lib = altAgdaLib;
+  lib = agdaLib;
 }
diff --git a/nix/shell.nix b/nix/shell.nix
index d28724dd7..53e9e8b70 100644
--- a/nix/shell.nix
+++ b/nix/shell.nix
@@ -59,11 +59,12 @@ cabalProject:
     # Agda hook.
     echo "${repoRoot.nix.agda-stdlib}/standard-library.agda-lib" > .libraries
     echo "${repoRoot.nix.agda2hs.lib}/agda2hs.agda-lib" >> .libraries
-    export AGDA_LIBS="--local-interfaces --library-file=$PWD/.libraries"
+    export AGDA_LIBS="$PWD/.libraries"
     # Rust hook.
     export RUSTC_VERSION=$(rustup toolchain list | sed -n -e '/ (default)$/{s/ (default)$//;p}')
     export PATH=''${CARGO_HOME:-~/.cargo}/bin:$PATH
     export PATH=''${RUSTUP_HOME:-~/.rustup}/toolchains/$RUSTC_VERSION/bin/:$PATH
+    echo "NOTE: 'make' will use the libraries file '$AGDA_LIBS' unless 'AGDA_LIBS' is set differently."
   '';
 
   tools = {