module Agda.Compiler.CallCompiler where
import qualified Control.Exception as E
import Control.Monad.Trans
import System.Exit
import System.IO
import System.Process
import Agda.TypeChecking.Monad
import Agda.Utils.Impossible
callCompiler
:: Bool
-> FilePath
-> [String]
-> Maybe FilePath
-> Maybe TextEncoding
-> TCM ()
callCompiler :: Bool
-> [Char]
-> [[Char]]
-> Maybe [Char]
-> Maybe TextEncoding
-> TCM ()
callCompiler Bool
doCall [Char]
cmd [[Char]]
args Maybe [Char]
cwd Maybe TextEncoding
enc =
if Bool
doCall then do
Maybe [Char]
merrors <- [Char]
-> [[Char]]
-> Maybe [Char]
-> Maybe TextEncoding
-> TCM (Maybe [Char])
callCompiler' [Char]
cmd [[Char]]
args Maybe [Char]
cwd Maybe TextEncoding
enc
case Maybe [Char]
merrors of
Maybe [Char]
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just [Char]
errors -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError ([Char] -> TypeError
CompilationError [Char]
errors)
else
forall (m :: * -> *).
MonadDebug m =>
[Char] -> VerboseLevel -> [Char] -> m ()
reportSLn [Char]
"compile.cmd" VerboseLevel
1 forall a b. (a -> b) -> a -> b
$ [Char]
"NOT calling: " forall a. [a] -> [a] -> [a]
++ [[Char]] -> [Char]
unwords ([Char]
cmd forall a. a -> [a] -> [a]
: [[Char]]
args)
callCompiler'
:: FilePath
-> [String]
-> Maybe FilePath
-> Maybe TextEncoding
-> TCM (Maybe String)
callCompiler' :: [Char]
-> [[Char]]
-> Maybe [Char]
-> Maybe TextEncoding
-> TCM (Maybe [Char])
callCompiler' [Char]
cmd [[Char]]
args Maybe [Char]
cwd Maybe TextEncoding
enc = do
forall (m :: * -> *).
MonadDebug m =>
[Char] -> VerboseLevel -> [Char] -> m ()
reportSLn [Char]
"compile.cmd" VerboseLevel
1 forall a b. (a -> b) -> a -> b
$ [Char]
"Calling: " forall a. [a] -> [a] -> [a]
++ [[Char]] -> [Char]
unwords ([Char]
cmd forall a. a -> [a] -> [a]
: [[Char]]
args)
(Maybe Handle
_, Maybe Handle
out, Maybe Handle
err, ProcessHandle
p) <-
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ CreateProcess
-> IO (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
createProcess
([Char] -> [[Char]] -> CreateProcess
proc [Char]
cmd [[Char]]
args) { std_err :: StdStream
std_err = StdStream
CreatePipe
, std_out :: StdStream
std_out = StdStream
CreatePipe
, cwd :: Maybe [Char]
cwd = Maybe [Char]
cwd
}
case Maybe Handle
out of
Maybe Handle
Nothing -> forall a. HasCallStack => a
__IMPOSSIBLE__
Just Handle
out -> forall a. TCM a -> TCM ()
forkTCM forall a b. (a -> b) -> a -> b
$ do
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ Handle -> Bool -> IO ()
hSetBinaryMode Handle
out Bool
False
case Maybe TextEncoding
enc of
Maybe TextEncoding
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just TextEncoding
enc -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ Handle -> TextEncoding -> IO ()
hSetEncoding Handle
out TextEncoding
enc
[Char]
progressInfo <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ Handle -> IO [Char]
hGetContents Handle
out
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall (m :: * -> *).
MonadDebug m =>
[Char] -> VerboseLevel -> [Char] -> m ()
reportSLn [Char]
"compile.output" VerboseLevel
1) forall a b. (a -> b) -> a -> b
$ [Char] -> [[Char]]
lines [Char]
progressInfo
[Char]
errors <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ case Maybe Handle
err of
Maybe Handle
Nothing -> forall a. HasCallStack => a
__IMPOSSIBLE__
Just Handle
err -> do
Handle -> Bool -> IO ()
hSetBinaryMode Handle
err Bool
False
case Maybe TextEncoding
enc of
Maybe TextEncoding
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just TextEncoding
enc -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ Handle -> TextEncoding -> IO ()
hSetEncoding Handle
err TextEncoding
enc
Handle -> IO [Char]
hGetContents Handle
err
ExitCode
exitcode <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ do
VerboseLevel
_ <- forall a. a -> IO a
E.evaluate (forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [Char]
errors)
ProcessHandle -> IO ExitCode
waitForProcess ProcessHandle
p
case ExitCode
exitcode of
ExitFailure VerboseLevel
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just [Char]
errors
ExitCode
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing