Use env vars; broken agda compilation

IntersectMBO · Oct 24, 2024 · c58efc2 · c58efc2
1 parent b26f932
commit c58efc2
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 14 deletions.
diff --git a/plutus-executables/executables/uplc/Main.hs b/plutus-executables/executables/uplc/Main.hs
@@ -51,6 +51,7 @@ import Flat (unflat)
 import Options.Applicative
 import Prettyprinter ((<+>))
 import System.Exit (exitFailure)
+import System.FilePath ((</>))
 import System.IO (hPrint, stderr)
 import Text.Read (readMaybe)
 
@@ -85,6 +86,7 @@ import Data.ByteString (ByteString)
 import Data.List (isInfixOf, isSuffixOf)
 import Data.Map.Strict qualified as Map
 import Data.Text (Text)
+import Data.Text qualified as Text
 import Data.Traversable (forM)
 import PlutusCore.Crypto.BLS12_381.G1 qualified as BLS12_381.G1
 import PlutusCore.Crypto.BLS12_381.G2 qualified as BLS12_381.G2
@@ -330,17 +332,17 @@ runAgda certName rawTrace = do
         case parseTraceResult of
           Right (res, _) -> res
           Left err       -> error $ show err
-  -- path <- getEnv "PATH"
-  -- let paths = splitOn ":" path
-  --     agdaStdLib = head $ filter (isInfixOf "standard-library-1.7.3") paths
-  -- print paths
-  let inputFile = HAgda.File.AbsolutePath "/home/ana/Workspace/IOG/plutus/plutus-metatheory/src/Test.agda"
+  stdlibPath <- getEnv "AGDA_STDLIB_SRC"
+  metatheoryPath <- getEnv "PLUTUS_METHATHEORY_SRC"
+  print stdlibPath
+  print metatheoryPath
+  let inputFile = HAgda.File.AbsolutePath (Text.pack $ metatheoryPath </> "Test.agda") -- "/home/ana/Workspace/IOG/plutus/plutus-metatheory/src/Test.agda"
   runTCMPrettyErrors $ do
     let opts =
           defaultOptions
             { optIncludePaths =
-                [ "/home/ana/Workspace/IOG/plutus/plutus-metatheory/src"
-                , "/nix/store/g9vi7hzrp1cqgm21355549yyqcpkjnxx-standard-library-1.7.3/src"
+                [ metatheoryPath -- "/home/ana/Workspace/IOG/plutus/plutus-metatheory/src"
+                , stdlibPath -- "/nix/store/g9vi7hzrp1cqgm21355549yyqcpkjnxx-standard-library-1.7.3/src"
                 ]
             , optLocalInterfaces = True
             }
@@ -355,7 +357,6 @@ runAgda certName rawTrace = do
     decisionProcedureResult <- evalInCurrent DefaultCompute internalisedTrace
     final <- prettyTCM decisionProcedureResult
     liftIO $ writeFile (certName ++ ".agda") (show final)
-    return ()
 
 instance AgdaUnparse AgdaFFI.UTerm where
   agdaUnparse =
@@ -405,7 +406,7 @@ instance AgdaUnparse ByteString where
   agdaUnparse = show  -- maybe this should be encoded some other way
 
 instance AgdaUnparse () where
-  agdaUnparse _ = "⊤"
+  agdaUnparse _ = "tt"
 
 instance AgdaUnparse a => AgdaUnparse [a] where
   agdaUnparse l = "(" ++ foldr (\x xs -> agdaUnparse x ++ " ∷ " ++ xs) "[]" l ++ ")"

diff --git a/plutus-executables/plutus-executables.cabal b/plutus-executables/plutus-executables.cabal
@@ -81,16 +81,17 @@ executable plc
     , plutus-core:plutus-core-execlib
 
 executable uplc
-  import:             lang, os-support
-  main-is:            uplc/Main.hs
-  hs-source-dirs:     executables
+  import:         lang, os-support
+  main-is:        uplc/Main.hs
+  hs-source-dirs: executables
   build-depends:
-    , Agda                                            ==2.6.4
-    , base                                            >=4.9   && <5
+    , Agda                             ==2.6.4
+    , base                             >=4.9   && <5
     , bytestring
     , containers
     , criterion
     , deepseq
+    , filepath
     , flat                             ^>=0.6
     , haskeline
     , mtl