{-# LANGUAGE CPP #-}
module Agda.Compiler.CallCompiler where
import qualified Control.Exception as E
import Control.Monad.Trans
import Data.List ( intercalate )
import qualified Data.List as List
import System.Exit
import System.IO
import System.Process
import Agda.TypeChecking.Monad
#include "undefined.h"
import Agda.Utils.Impossible
callCompiler
:: Bool
-> FilePath
-> [String]
-> TCM ()
callCompiler doCall cmd args =
if doCall then do
merrors <- callCompiler' cmd args
case merrors of
Nothing -> return ()
Just errors -> typeError (CompilationError errors)
else
reportSLn "compile.cmd" 1 $ "NOT calling: " ++ intercalate " " (cmd : args)
callCompiler'
:: FilePath
-> [String]
-> TCM (Maybe String)
callCompiler' cmd args = do
reportSLn "compile.cmd" 1 $ "Calling: " ++ intercalate " " (cmd : args)
(_, out, err, p) <-
liftIO $ createProcess
(proc cmd args) { std_err = CreatePipe
, std_out = CreatePipe
}
case out of
Nothing -> __IMPOSSIBLE__
Just out -> forkTCM $ do
liftIO $ hSetBinaryMode out False
progressInfo <- liftIO $ hGetContents out
mapM_ (reportSLn "compile.output" 1) $ lines progressInfo
errors <- liftIO $ case err of
Nothing -> __IMPOSSIBLE__
Just err -> do
hSetBinaryMode err False
hGetContents err
exitcode <- liftIO $ do
_ <- E.evaluate (length errors)
waitForProcess p
case exitcode of
ExitFailure _ -> return $ Just errors
_ -> return Nothing