Re-run Agda properly in plutus-metatheory

Two tricks:
- Run Agda in both a post-configure hook and a pre-build hook, so it
runs before Haddock and also before any build. This won't waste work due
to Agda being good at not redoing work.
- Put the Agda sources in `extra-source-files`, which apparently makes
Cabal rebuild if they change!

plutus-metatheory/.gitignore

@@ -1,4 +1,4 @@
 *.agdai
 *.lagda~
 *.agda~
-MAlonzo/*
+src/MAlonzo

plutus-metatheory/Setup.hs

@@ -4,15 +4,45 @@ import           Distribution.Simple
 import           Distribution.Simple.Setup
 import           Distribution.Types.LocalBuildInfo
 import           Distribution.Types.PackageDescription
+import           Distribution.Types.HookedBuildInfo
 import           Turtle
 
 main :: IO ()
 main = defaultMainWithHooks userhooks
 
 userhooks :: UserHooks
-userhooks = simpleUserHooks { postConf = postConf' }
+userhooks = simpleUserHooks {
+      postConf = \_ _ _ _ -> runAgda
+    , preBuild = \_ _ -> runAgda >> pure emptyHookedBuildInfo
+    }
+
+{- Note [Cabal hooks for Agda]
+We want to run Agda to generate some of the Haskell sources for this project.
+
+We do this with cabal hooks. The considerations are:
+- We need it to run before Haddock also
+- We want the Haskell to be regenerated if the Agda has changed before building the
+Haskell.
+
+This is tricky: the first point suggests having a post-configure hook, but then the
+second won't work, since Cabal won't detect that it needs to reconfigure if the
+Agda changes.
+
+The only way is to rely on Agda to do the change detection, and run it every time.
+That means we need a pre-build hook. But then it won't run before Haddock!
+
+So: we do both! Since Agda is reasonably good at not redoing work, we mostly don't
+pay the cost twice on the first configure/build sequence.
+-}
 
--- This adds a post-configure hook which calls Agda. No attempt is made to fail gracefully.
--- Post-configure seems like the right place, so it runs even if we're doing a non-build thing like Haddock.
 postConf' :: Args -> ConfigFlags -> PackageDescription -> LocalBuildInfo -> IO ()
-postConf' _ _ _ _ = void $ proc "agda" ["--compile", "--ghc-dont-call-ghc", "--local-interfaces", "src/Main.lagda"] empty
+postConf' _ _ _ _ = runAgda
+
+-- This adds a pre-build hook which calls Agda. No attempt is made to fail gracefully.
+-- Doing this before building ensures that the generated Haskell files are always up-to-date, since cabal won't
+-- track the dependency on the source Agda files, but Agda should do
+preBuild' :: Args -> BuildFlags -> IO ()
+preBuild' _ _ = runAgda
+
+runAgda :: IO ()
+runAgda = procs "agda" ["--compile", "--ghc-dont-call-ghc", "--local-interfaces", "src/Main.lagda"] empty

plutus-metatheory/plutus-metatheory.cabal

@@ -10,7 +10,12 @@ license-files:
 author:              James Chapman
 maintainer:          james.chapman@iohk.io
 category:            Development
-extra-source-files:  README.md, Plutus.agda-lib
+extra-source-files:
+  README.md,
+  Plutus.agda-lib,
+  -- This makes cabal rebuild if any of these files change, which allow the
+  -- custom setup to fire and rebuild the Haskell sources
+  src/**/*.lagda
 build-type:          Custom
 
 custom-setup
@@ -402,15 +407,15 @@ library
         MAlonzo.Code.IO.Primitive
         MAlonzo.Code.Relation.Binary.Construct.FromRel
         MAlonzo.Code.Relation.Binary.Reasoning.Base.Double
-                       
+
 executable plc-agda
   import: stuff
   hs-source-dirs: exe
   main-is: Main.hs
   build-depends:
     base -any,
     plutus-metatheory
-    
+
 test-suite test1
   import: stuff
   build-tool-depends: plutus-core:plc
@@ -436,7 +441,7 @@ test-suite test2
     plutus-metatheory,
     process -any,
     text -any
-    
+
 test-suite test3
   import: stuff
   hs-source-dirs: test
@@ -451,4 +456,4 @@ test-suite test3
     size-based -any,
     Stream -any,
     tasty -any,
-    tasty-hunit -any
+    tasty-hunit -any