module Agda.Compiler.CallCompiler where
import qualified Control.Exception as E
import Control.Monad.Trans
import Data.List as L
import System.Exit
import System.IO
import System.Process
import Agda.TypeChecking.Monad
import Agda.Utils.Impossible
#include "../undefined.h"
callCompiler
:: FilePath
-> [String]
-> TCM ()
callCompiler cmd args = do
merrors <- callCompiler' cmd args
case merrors of
Nothing -> return ()
Just errors -> typeError (CompilationError errors)
callCompiler'
:: FilePath
-> [String]
-> TCM (Maybe String)
callCompiler' cmd args = do
reportSLn "" 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 "" 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