{-|
Module      : Idris.Package
Description : Functionality for working with Idris packages.

License     : BSD3
Maintainer  : The Idris Community.
-}
{-# LANGUAGE CPP #-}
module Idris.Package where

import System.Directory
import System.Environment
import System.Exit
import System.FilePath (addExtension, addTrailingPathSeparator, dropExtension,
                        hasExtension, takeDirectory, takeExtension,
                        takeFileName, (</>))
import System.IO
import System.Process

import Util.System

import Control.Monad
import Control.Monad.Trans.Except (runExceptT)
import Control.Monad.Trans.State.Strict (execStateT)
import Data.Either (partitionEithers)
import Data.List
import Data.List.Split (splitOn)

import Idris.AbsSyntax
import Idris.Core.TT
import Idris.Error (ifail)
import Idris.IBC
import Idris.IdrisDoc
import Idris.Imports
import Idris.Main (idris, idrisMain)
import Idris.Options
import Idris.Output
import Idris.Parser (loadModule)

import Idris.Package.Common
import Idris.Package.Parser

import IRTS.System

-- To build a package:
-- * read the package description
-- * check all the library dependencies exist
-- * invoke the makefile if there is one
-- * invoke idris on each module, with idris_opts
-- * install everything into datadir/pname, if install flag is set

getPkgDesc :: FilePath -> IO PkgDesc
getPkgDesc :: String -> IO PkgDesc
getPkgDesc = String -> IO PkgDesc
parseDesc

--  --------------------------------------------------------- [ Build Packages ]

-- | Run the package through the idris compiler.
buildPkg :: [Opt]            -- ^ Command line options
         -> Bool             -- ^ Provide Warnings
         -> (Bool, FilePath) -- ^ (Should we install, Location of iPKG file)
         -> IO ()
buildPkg :: [Opt] -> Bool -> (Bool, String) -> IO ()
buildPkg [Opt]
copts Bool
warnonly (Bool
install, String
fp) = do
  PkgDesc
pkgdesc <- String -> IO PkgDesc
parseDesc String
fp
  String
dir <- IO String
getCurrentDirectory
  let idx' :: String
idx' = PkgName -> String
pkgIndex forall a b. (a -> b) -> a -> b
$ PkgDesc -> PkgName
pkgname PkgDesc
pkgdesc
      idx :: Opt
idx  = String -> Opt
PkgIndex forall a b. (a -> b) -> a -> b
$ case forall a. (Opt -> Maybe a) -> [Opt] -> [a]
opt Opt -> Maybe String
getIBCSubDir [Opt]
copts of
        (String
ibcsubdir:[String]
_) -> String
ibcsubdir String -> String -> String
</> String
idx'
        []            -> String
idx'
  [Bool]
oks <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Bool -> PkgName -> String -> IO Bool
testLib Bool
warnonly (PkgDesc -> PkgName
pkgname PkgDesc
pkgdesc)) (PkgDesc -> [String]
libdeps PkgDesc
pkgdesc)
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
oks) forall a b. (a -> b) -> a -> b
$ do
    Maybe IState
m_ist <- forall a. PkgDesc -> IO a -> IO a
inPkgDir PkgDesc
pkgdesc forall a b. (a -> b) -> a -> b
$ do

      Maybe String -> IO ()
make (PkgDesc -> Maybe String
makefile PkgDesc
pkgdesc)
      case (PkgDesc -> Maybe String
execout PkgDesc
pkgdesc) of
        Maybe String
Nothing -> do
          case [Opt] -> [Opt] -> Either String [Opt]
mergeOptions [Opt]
copts (Opt
idx forall a. a -> [a] -> [a]
: Opt
NoREPL forall a. a -> [a] -> [a]
: Int -> Opt
Verbose Int
1 forall a. a -> [a] -> [a]
: PkgDesc -> [Opt]
idris_opts PkgDesc
pkgdesc) of
            Left String
emsg -> do
              String -> IO ()
putStrLn String
emsg
              forall a. ExitCode -> IO a
exitWith (Int -> ExitCode
ExitFailure Int
1)
            Right [Opt]
opts -> do
              Bool -> PkgDesc -> IO ()
auditPackage (Opt
AuditIPkg forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Opt]
opts) PkgDesc
pkgdesc
              [Opt] -> [Name] -> IO (Maybe IState)
buildMods [Opt]
opts (PkgDesc -> [Name]
modules PkgDesc
pkgdesc)
        Just String
o -> do
          let exec :: String
exec = String
dir String -> String -> String
</> String
o
          case [Opt] -> [Opt] -> Either String [Opt]
mergeOptions [Opt]
copts (Opt
idx forall a. a -> [a] -> [a]
: Opt
NoREPL forall a. a -> [a] -> [a]
: Int -> Opt
Verbose Int
1 forall a. a -> [a] -> [a]
: String -> Opt
Output String
exec forall a. a -> [a] -> [a]
: PkgDesc -> [Opt]
idris_opts PkgDesc
pkgdesc) of
            Left String
emsg -> do
              String -> IO ()
putStrLn String
emsg
              forall a. ExitCode -> IO a
exitWith (Int -> ExitCode
ExitFailure Int
1)
            Right [Opt]
opts -> do
              Bool -> PkgDesc -> IO ()
auditPackage (Opt
AuditIPkg forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Opt]
opts) PkgDesc
pkgdesc
              [Opt] -> Maybe Name -> IO (Maybe IState)
buildMain [Opt]
opts (PkgDesc -> Maybe Name
idris_main PkgDesc
pkgdesc)
    case Maybe IState
m_ist of
      Maybe IState
Nothing  -> forall a. ExitCode -> IO a
exitWith (Int -> ExitCode
ExitFailure Int
1)
      Just IState
ist -> do
        -- Quit with error code if there was a problem
        case IState -> Maybe FC
errSpan IState
ist of
          Just FC
_ -> forall a. ExitCode -> IO a
exitWith (Int -> ExitCode
ExitFailure Int
1)
          Maybe FC
_      -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
install forall a b. (a -> b) -> a -> b
$ [String] -> PkgDesc -> IO ()
installPkg (forall a. (Opt -> Maybe a) -> [Opt] -> [a]
opt Opt -> Maybe String
getIBCSubDir [Opt]
copts) PkgDesc
pkgdesc
  where
    buildMain :: [Opt] -> Maybe Name -> IO (Maybe IState)
buildMain [Opt]
opts (Just Name
mod) = [Opt] -> [Name] -> IO (Maybe IState)
buildMods [Opt]
opts [Name
mod]
    buildMain [Opt]
_ Maybe Name
Nothing = do
      String -> IO ()
putStrLn String
"Can't build an executable: No main module given"
      forall a. ExitCode -> IO a
exitWith (Int -> ExitCode
ExitFailure Int
1)

--  --------------------------------------------------------- [ Check Packages ]

-- | Type check packages only
--
-- This differs from build in that executables are not built, if the
-- package contains an executable.
checkPkg :: [Opt]     -- ^ Command line Options
         -> Bool      -- ^ Show Warnings
         -> Bool      -- ^ quit on failure
         -> FilePath  -- ^ Path to ipkg file.
         -> IO ()
checkPkg :: [Opt] -> Bool -> Bool -> String -> IO ()
checkPkg [Opt]
copts Bool
warnonly Bool
quit String
fpath = do
  PkgDesc
pkgdesc <- String -> IO PkgDesc
parseDesc String
fpath
  [Bool]
oks <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Bool -> PkgName -> String -> IO Bool
testLib Bool
warnonly (PkgDesc -> PkgName
pkgname PkgDesc
pkgdesc)) (PkgDesc -> [String]
libdeps PkgDesc
pkgdesc)
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
oks) forall a b. (a -> b) -> a -> b
$ do
    Maybe IState
res <- forall a. PkgDesc -> IO a -> IO a
inPkgDir PkgDesc
pkgdesc forall a b. (a -> b) -> a -> b
$ do
      Maybe String -> IO ()
make (PkgDesc -> Maybe String
makefile PkgDesc
pkgdesc)

      case [Opt] -> [Opt] -> Either String [Opt]
mergeOptions [Opt]
copts (Opt
NoREPL forall a. a -> [a] -> [a]
: Int -> Opt
Verbose Int
1 forall a. a -> [a] -> [a]
: PkgDesc -> [Opt]
idris_opts PkgDesc
pkgdesc) of
        Left String
emsg -> do
          String -> IO ()
putStrLn String
emsg
          forall a. ExitCode -> IO a
exitWith (Int -> ExitCode
ExitFailure Int
1)
        Right [Opt]
opts -> do
          Bool -> PkgDesc -> IO ()
auditPackage (Opt
AuditIPkg forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Opt]
opts) PkgDesc
pkgdesc
          [Opt] -> [Name] -> IO (Maybe IState)
buildMods [Opt]
opts (PkgDesc -> [Name]
modules PkgDesc
pkgdesc)
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
quit forall a b. (a -> b) -> a -> b
$ case Maybe IState
res of
                  Maybe IState
Nothing -> forall a. ExitCode -> IO a
exitWith (Int -> ExitCode
ExitFailure Int
1)
                  Just IState
res' -> do
                    case IState -> Maybe FC
errSpan IState
res' of
                      Just FC
_ -> forall a. ExitCode -> IO a
exitWith (Int -> ExitCode
ExitFailure Int
1)
                      Maybe FC
_      -> forall (m :: * -> *) a. Monad m => a -> m a
return ()

--  ------------------------------------------------------------------- [ REPL ]

-- | Check a package and start a REPL.
--
-- This function only works with packages that have a main module.
--
replPkg :: [Opt]    -- ^ Command line Options
        -> FilePath -- ^ Path to ipkg file.
        -> Idris ()
replPkg :: [Opt] -> String -> Idris ()
replPkg [Opt]
copts String
fp = do
    IState
orig <- Idris IState
getIState
    forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ [Opt] -> Bool -> Bool -> String -> IO ()
checkPkg [Opt]
copts Bool
False Bool
False String
fp
    PkgDesc
pkgdesc <- forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ String -> IO PkgDesc
parseDesc String
fp -- bzzt, repetition!

    case [Opt] -> [Opt] -> Either String [Opt]
mergeOptions [Opt]
copts (PkgDesc -> [Opt]
idris_opts PkgDesc
pkgdesc) of
      Left String
emsg  -> forall a. String -> Idris a
ifail String
emsg
      Right [Opt]
opts -> do

        IState -> Idris ()
putIState IState
orig
        String
dir <- forall a. IO a -> Idris a
runIO IO String
getCurrentDirectory
        forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ String -> IO ()
setCurrentDirectory forall a b. (a -> b) -> a -> b
$ String
dir String -> String -> String
</> PkgDesc -> String
sourcedir PkgDesc
pkgdesc
        [Opt] -> Maybe Name -> Idris ()
runMain [Opt]
opts (PkgDesc -> Maybe Name
idris_main PkgDesc
pkgdesc)
        forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ String -> IO ()
setCurrentDirectory String
dir

  where
    toPath :: String -> String
toPath String
n = forall a. (a -> a -> a) -> [a] -> a
foldl1' String -> String -> String
(</>) forall a b. (a -> b) -> a -> b
$ forall a. Eq a => [a] -> [a] -> [[a]]
splitOn String
"." String
n

    runMain :: [Opt] -> Maybe Name -> Idris ()
runMain [Opt]
opts (Just Name
mod) = do
      let f :: String
f = String -> String
toPath (Name -> String
showCG Name
mod)
      [Opt] -> Idris ()
idrisMain ((String -> Opt
Filename String
f) forall a. a -> [a] -> [a]
: [Opt]
opts)
    runMain [Opt]
_ Maybe Name
Nothing =
      String -> Idris ()
iputStrLn String
"Can't start REPL: no main module given"

--  --------------------------------------------------------------- [ Cleaning ]

-- | Clean Package build files
cleanPkg :: [Opt]    -- ^ Command line options.
         -> FilePath -- ^ Path to ipkg file.
         -> IO ()
cleanPkg :: [Opt] -> String -> IO ()
cleanPkg [Opt]
copts String
fp = do
  PkgDesc
pkgdesc <- String -> IO PkgDesc
parseDesc String
fp
  String
dir <- IO String
getCurrentDirectory
  forall a. PkgDesc -> IO a -> IO a
inPkgDir PkgDesc
pkgdesc forall a b. (a -> b) -> a -> b
$ do
    Maybe String -> IO ()
clean (PkgDesc -> Maybe String
makefile PkgDesc
pkgdesc)
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Name -> IO ()
rmIBC (PkgDesc -> [Name]
modules PkgDesc
pkgdesc)
    PkgName -> IO ()
rmIdx (PkgDesc -> PkgName
pkgname PkgDesc
pkgdesc)
    case PkgDesc -> Maybe String
execout PkgDesc
pkgdesc of
      Maybe String
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
      Just String
s -> String -> IO ()
rmExe forall a b. (a -> b) -> a -> b
$ String
dir String -> String -> String
</> String
s

--  ------------------------------------------------------ [ Generate IdrisDoc ]


-- | Generate IdrisDoc for package
-- TODO: Handle case where module does not contain a matching namespace
--       E.g. from prelude.ipkg: IO, Prelude.Chars, Builtins
--
-- Issue number #1572 on the issue tracker
--       https://github.com/idris-lang/Idris-dev/issues/1572
documentPkg :: [Opt]           -- ^ Command line options.
            -> (Bool,FilePath) -- ^ (Should we install?, Path to ipkg file).
            -> IO ()
documentPkg :: [Opt] -> (Bool, String) -> IO ()
documentPkg [Opt]
copts (Bool
install,String
fp) = do
  PkgDesc
pkgdesc        <- String -> IO PkgDesc
parseDesc String
fp
  String
cd             <- IO String
getCurrentDirectory
  let pkgDir :: String
pkgDir      = String
cd String -> String -> String
</> String -> String
takeDirectory String
fp
      outputDir :: String
outputDir   = String
cd String -> String -> String
</> PkgName -> String
unPkgName (PkgDesc -> PkgName
pkgname PkgDesc
pkgdesc) forall a. [a] -> [a] -> [a]
++ String
"_doc"
      popts :: [Opt]
popts       = Opt
NoREPL forall a. a -> [a] -> [a]
: Int -> Opt
Verbose Int
1 forall a. a -> [a] -> [a]
: PkgDesc -> [Opt]
idris_opts PkgDesc
pkgdesc
      mods :: [Name]
mods        = PkgDesc -> [Name]
modules PkgDesc
pkgdesc
      fs :: [String]
fs          = forall a b. (a -> b) -> [a] -> [b]
map (forall a. (a -> a -> a) -> [a] -> a
foldl1' String -> String -> String
(</>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Eq a => [a] -> [a] -> [[a]]
splitOn String
"." forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> String
showCG) [Name]
mods
  String -> IO ()
setCurrentDirectory forall a b. (a -> b) -> a -> b
$ String
pkgDir String -> String -> String
</> PkgDesc -> String
sourcedir PkgDesc
pkgdesc
  Maybe String -> IO ()
make (PkgDesc -> Maybe String
makefile PkgDesc
pkgdesc)
  String -> IO ()
setCurrentDirectory String
pkgDir
  case [Opt] -> [Opt] -> Either String [Opt]
mergeOptions [Opt]
copts [Opt]
popts of
    Left String
emsg -> do
      String -> IO ()
putStrLn String
emsg
      forall a. ExitCode -> IO a
exitWith (Int -> ExitCode
ExitFailure Int
1)
    Right [Opt]
opts -> do
      let run :: StateT a (ExceptT e m) a -> a -> m (Either e a)
run StateT a (ExceptT e m) a
l       = forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT StateT a (ExceptT e m) a
l
          load :: [String] -> Idris ()
load []     = forall (m :: * -> *) a. Monad m => a -> m a
return ()
          load (String
f:[String]
fs) = do String -> IBCPhase -> Idris (Maybe String)
loadModule String
f IBCPhase
IBC_Building; [String] -> Idris ()
load [String]
fs
          loader :: Idris ()
loader      = do
            [Opt] -> Idris ()
idrisMain [Opt]
opts
            String -> Idris ()
addImportDir (PkgDesc -> String
sourcedir PkgDesc
pkgdesc)
            [String] -> Idris ()
load [String]
fs
      Either Err IState
idrisImplementation  <- forall {m :: * -> *} {a} {e} {a}.
Monad m =>
StateT a (ExceptT e m) a -> a -> m (Either e a)
run Idris ()
loader IState
idrisInit
      String -> IO ()
setCurrentDirectory String
cd
      case Either Err IState
idrisImplementation of
        Left  Err
err -> do
          String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ IState -> Err -> String
pshow IState
idrisInit Err
err
          forall a. ExitCode -> IO a
exitWith (Int -> ExitCode
ExitFailure Int
1)
        Right IState
ist -> do
          String
iDocDir   <- IO String
getIdrisDocDir
          String
pkgDocDir <- String -> IO String
makeAbsolute (String
iDocDir String -> String -> String
</> PkgName -> String
unPkgName (PkgDesc -> PkgName
pkgname PkgDesc
pkgdesc))
          let out_dir :: String
out_dir = if Bool
install then String
pkgDocDir else String
outputDir
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
install forall a b. (a -> b) -> a -> b
$ do
              String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"Attempting to install IdrisDocs for", forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ PkgDesc -> PkgName
pkgname PkgDesc
pkgdesc, String
"in:", String
out_dir]

          Either String ()
docRes <- IState -> [Name] -> String -> IO (Either String ())
generateDocs IState
ist [Name]
mods String
out_dir
          case Either String ()
docRes of
            Right ()
_  -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
            Left String
msg -> do
              String -> IO ()
putStrLn String
msg
              forall a. ExitCode -> IO a
exitWith (Int -> ExitCode
ExitFailure Int
1)

--  ------------------------------------------------------------------- [ Test ]

-- | Build a package with a sythesized main function that runs the tests
testPkg :: [Opt]     -- ^ Command line options.
        -> FilePath  -- ^ Path to ipkg file.
        -> IO ExitCode
testPkg :: [Opt] -> String -> IO ExitCode
testPkg [Opt]
copts String
fp = do
  PkgDesc
pkgdesc <- String -> IO PkgDesc
parseDesc String
fp
  [Bool]
ok <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Bool -> PkgName -> String -> IO Bool
testLib Bool
True (PkgDesc -> PkgName
pkgname PkgDesc
pkgdesc)) (PkgDesc -> [String]
libdeps PkgDesc
pkgdesc)
  if forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
ok
    then do
      (Maybe IState
m_ist, ExitCode
exitCode) <- forall a. PkgDesc -> IO a -> IO a
inPkgDir PkgDesc
pkgdesc forall a b. (a -> b) -> a -> b
$ do
        Maybe String -> IO ()
make (PkgDesc -> Maybe String
makefile PkgDesc
pkgdesc)
        -- Get a temporary file to save the tests' source in
        (String
tmpn, Handle
tmph) <- String -> IO (String, Handle)
tempfile String
".idr"
        Handle -> String -> IO ()
hPutStrLn Handle
tmph forall a b. (a -> b) -> a -> b
$
            String
"module Test_______\n" forall a. [a] -> [a] -> [a]
++
            forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"import " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
m forall a. [a] -> [a] -> [a]
++ String
"\n" | Name
m <- PkgDesc -> [Name]
modules PkgDesc
pkgdesc]
                forall a. [a] -> [a] -> [a]
++ String
"namespace Main\n"
                forall a. [a] -> [a] -> [a]
++ String
"  main : IO ()\n"
                forall a. [a] -> [a] -> [a]
++ String
"  main = do "
                forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ forall a. Show a => a -> String
show Name
t forall a. [a] -> [a] -> [a]
++ String
"\n            "
                          | Name
t <- PkgDesc -> [Name]
idris_tests PkgDesc
pkgdesc]
        Handle -> IO ()
hClose Handle
tmph
        (String
tmpn', Handle
tmph') <- String -> IO (String, Handle)
tempfile String
""
        Handle -> IO ()
hClose Handle
tmph'
        let popts :: [Opt]
popts = (String -> Opt
Filename String
tmpn forall a. a -> [a] -> [a]
: Opt
NoREPL forall a. a -> [a] -> [a]
: Int -> Opt
Verbose Int
1 forall a. a -> [a] -> [a]
: String -> Opt
Output String
tmpn' forall a. a -> [a] -> [a]
: PkgDesc -> [Opt]
idris_opts PkgDesc
pkgdesc)
        case [Opt] -> [Opt] -> Either String [Opt]
mergeOptions [Opt]
copts [Opt]
popts of
          Left String
emsg -> do
            String -> IO ()
putStrLn String
emsg
            forall a. ExitCode -> IO a
exitWith (Int -> ExitCode
ExitFailure Int
1)
          Right [Opt]
opts -> do
            Maybe IState
m_ist    <- [Opt] -> IO (Maybe IState)
idris [Opt]
opts
            let texe :: String
texe = if Bool
isWindows then String -> String -> String
addExtension String
tmpn' String
".exe" else String
tmpn'
            ExitCode
exitCode <- String -> [String] -> IO ExitCode
rawSystem String
texe []
            forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe IState
m_ist, ExitCode
exitCode)
      case Maybe IState
m_ist of
        Maybe IState
Nothing  -> forall a. ExitCode -> IO a
exitWith (Int -> ExitCode
ExitFailure Int
1)
        Just IState
ist -> do
          -- Quit with error code if problem building
          case IState -> Maybe FC
errSpan IState
ist of
            Just FC
_ -> forall a. ExitCode -> IO a
exitWith (Int -> ExitCode
ExitFailure Int
1)
            Maybe FC
_      -> forall (m :: * -> *) a. Monad m => a -> m a
return ExitCode
exitCode
    else forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> ExitCode
ExitFailure Int
1)

--  ----------------------------------------------------------- [ Installation ]

-- | Install package
installPkg :: [String]  -- ^ Alternate install location
           -> PkgDesc   -- ^ iPKG file.
           -> IO ()
installPkg :: [String] -> PkgDesc -> IO ()
installPkg [String]
altdests PkgDesc
pkgdesc = forall a. PkgDesc -> IO a -> IO a
inPkgDir PkgDesc
pkgdesc forall a b. (a -> b) -> a -> b
$ do
  String
d <- IO String
getIdrisLibDir
  let destdir :: String
destdir = case [String]
altdests of
                  []     -> String
d
                  (String
d':[String]
_) -> String
d'
  case (PkgDesc -> Maybe String
execout PkgDesc
pkgdesc) of
    Maybe String
Nothing -> do
      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (String -> PkgName -> Name -> IO ()
installIBC String
destdir (PkgDesc -> PkgName
pkgname PkgDesc
pkgdesc)) (PkgDesc -> [Name]
modules PkgDesc
pkgdesc)
      String -> PkgName -> IO ()
installIdx String
destdir (PkgDesc -> PkgName
pkgname PkgDesc
pkgdesc)
    Just String
o -> forall (m :: * -> *) a. Monad m => a -> m a
return () -- do nothing, keep executable locally, for noe

  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (String -> PkgName -> String -> IO ()
installObj String
destdir (PkgDesc -> PkgName
pkgname PkgDesc
pkgdesc)) (PkgDesc -> [String]
objs PkgDesc
pkgdesc)

-- ---------------------------------------------------------- [ Helper Methods ]
-- Methods for building, testing, installing, and removal of idris
-- packages.

auditPackage :: Bool -> PkgDesc -> IO ()
auditPackage :: Bool -> PkgDesc -> IO ()
auditPackage Bool
False PkgDesc
_    = forall (m :: * -> *) a. Monad m => a -> m a
return ()
auditPackage Bool
True  PkgDesc
ipkg = do
    String
cwd <- IO String
getCurrentDirectory

    let ms :: [String]
ms = forall a b. (a -> b) -> [a] -> [b]
map (PkgDesc -> String
sourcedir PkgDesc
ipkg String -> String -> String
</>) forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (String -> String
toPath forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> String
showCG) (PkgDesc -> [Name]
modules PkgDesc
ipkg)
    [String]
ms' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM String -> IO String
makeAbsolute [String]
ms

    [String]
ifiles <- String -> IO [String]
getIdrisFiles String
cwd

    let ifiles' :: [String]
ifiles' = forall a b. (a -> b) -> [a] -> [b]
map String -> String
dropExtension [String]
ifiles

    [String]
not_listed <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM String -> IO String
makeRelativeToCurrentDirectory ([String]
ifiles' forall a. Eq a => [a] -> [a] -> [a]
\\ [String]
ms')

    String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines forall a b. (a -> b) -> a -> b
$
         [String
"Warning: The following modules are not listed in your iPkg file:\n"]
      forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (\String
m -> [String] -> String
unwords [String
"-", String
m]) [String]
not_listed
      forall a. [a] -> [a] -> [a]
++ [String
"\nModules that are not listed, are not installed."]

  where
    toPath :: String -> String
toPath String
n = forall a. (a -> a -> a) -> [a] -> a
foldl1' String -> String -> String
(</>) forall a b. (a -> b) -> a -> b
$ forall a. Eq a => [a] -> [a] -> [[a]]
splitOn String
"." String
n

    getIdrisFiles :: FilePath -> IO [FilePath]
    getIdrisFiles :: String -> IO [String]
getIdrisFiles String
dir = do
      [String]
contents <- String -> IO [String]
getDirectoryContents String
dir

      -- [ NOTE ] Directory >= 1.2.5.0 introduced `listDirectory` but later versions of directory appear to be causing problems with ghc 7.10.3 and cabal 1.22 in travis. Let's reintroduce the old ranges for directory to be sure.

      [[String]]
files <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [String]
contents (String -> String -> IO [String]
findRest String
dir)
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter (String -> Bool
isIdrisFile) (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[String]]
files)

    isIdrisFile :: FilePath -> Bool
    isIdrisFile :: String -> Bool
isIdrisFile String
fp = String -> String
takeExtension String
fp forall a. Eq a => a -> a -> Bool
== String
".idr" Bool -> Bool -> Bool
|| String -> String
takeExtension String
fp forall a. Eq a => a -> a -> Bool
== String
".lidr"

    findRest :: FilePath -> FilePath -> IO [FilePath]
    findRest :: String -> String -> IO [String]
findRest String
dir String
fn = do
      String
path <- String -> IO String
makeAbsolute (String
dir String -> String -> String
</> String
fn)
      Bool
isDir <- String -> IO Bool
doesDirectoryExist String
path
      if Bool
isDir
        then String -> IO [String]
getIdrisFiles String
path
        else forall (m :: * -> *) a. Monad m => a -> m a
return [String
path]

buildMods :: [Opt] -> [Name] -> IO (Maybe IState)
buildMods :: [Opt] -> [Name] -> IO (Maybe IState)
buildMods [Opt]
opts [Name]
ns = do let f :: [String]
f = forall a b. (a -> b) -> [a] -> [b]
map (String -> String
toPath forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> String
showCG) [Name]
ns
                       [Opt] -> IO (Maybe IState)
idris (forall a b. (a -> b) -> [a] -> [b]
map String -> Opt
Filename [String]
f forall a. [a] -> [a] -> [a]
++ [Opt]
opts)
    where
      toPath :: String -> String
toPath String
n = forall a. (a -> a -> a) -> [a] -> a
foldl1' String -> String -> String
(</>) forall a b. (a -> b) -> a -> b
$ forall a. Eq a => [a] -> [a] -> [[a]]
splitOn String
"." String
n

testLib :: Bool -> PkgName -> String -> IO Bool
testLib :: Bool -> PkgName -> String -> IO Bool
testLib Bool
warn PkgName
p String
f
    = do String
d <- IO String
getIdrisCRTSDir
         String
gcc <- IO String
getCC
         (String
tmpf, Handle
tmph) <- String -> IO (String, Handle)
tempfile String
""
         Handle -> IO ()
hClose Handle
tmph
         let libtest :: String
libtest = String
d String -> String -> String
</> String
"libtest.c"
         ExitCode
e <- String -> [String] -> IO ExitCode
rawSystem String
gcc [String
libtest, String
"-l" forall a. [a] -> [a] -> [a]
++ String
f, String
"-o", String
tmpf]
         case ExitCode
e of
            ExitCode
ExitSuccess -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
            ExitCode
_ -> do if Bool
warn
                       then do String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"Not building " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PkgName
p forall a. [a] -> [a] -> [a]
++
                                          String
" due to missing library " forall a. [a] -> [a] -> [a]
++ String
f
                               forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
                       else forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"Missing library " forall a. [a] -> [a] -> [a]
++ String
f

rmIBC :: Name -> IO ()
rmIBC :: Name -> IO ()
rmIBC Name
m = String -> IO ()
rmFile forall a b. (a -> b) -> a -> b
$ Name -> String
toIBCFile Name
m

rmIdx :: PkgName -> IO ()
rmIdx :: PkgName -> IO ()
rmIdx PkgName
p = do let f :: String
f = PkgName -> String
pkgIndex PkgName
p
             Bool
ex <- String -> IO Bool
doesFileExist String
f
             forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
ex forall a b. (a -> b) -> a -> b
$ String -> IO ()
rmFile String
f

rmExe :: String -> IO ()
rmExe :: String -> IO ()
rmExe String
p = do
            String
fn <- forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ if Bool
isWindows Bool -> Bool -> Bool
&& Bool -> Bool
not (String -> Bool
hasExtension String
p)
                                then String -> String -> String
addExtension String
p String
".exe" else String
p
            String -> IO ()
rmFile String
fn

toIBCFile :: Name -> String
toIBCFile (UN Text
n) = Text -> String
str Text
n forall a. [a] -> [a] -> [a]
++ String
".ibc"
toIBCFile (NS Name
n [Text]
ns) = forall a. (a -> a -> a) -> [a] -> a
foldl1' String -> String -> String
(</>) (forall a. [a] -> [a]
reverse (Name -> String
toIBCFile Name
n forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map Text -> String
str [Text]
ns))

installIBC :: String -> PkgName -> Name -> IO ()
installIBC :: String -> PkgName -> Name -> IO ()
installIBC String
dest PkgName
p Name
m = do
    let f :: String
f = Name -> String
toIBCFile Name
m
    let destdir :: String
destdir = String
dest String -> String -> String
</> PkgName -> String
unPkgName PkgName
p String -> String -> String
</> Name -> String
getDest Name
m
    String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"Installing " forall a. [a] -> [a] -> [a]
++ String
f forall a. [a] -> [a] -> [a]
++ String
" to " forall a. [a] -> [a] -> [a]
++ String
destdir
    Bool -> String -> IO ()
createDirectoryIfMissing Bool
True String
destdir
    String -> String -> IO ()
copyFile String
f (String
destdir String -> String -> String
</> String -> String
takeFileName String
f)
    forall (m :: * -> *) a. Monad m => a -> m a
return ()
  where
    getDest :: Name -> String
getDest (UN Text
n) = String
""
    getDest (NS Name
n [Text]
ns) = forall a. (a -> a -> a) -> [a] -> a
foldl1' String -> String -> String
(</>) (forall a. [a] -> [a]
reverse (Name -> String
getDest Name
n forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map Text -> String
str [Text]
ns))

installIdx :: String -> PkgName -> IO ()
installIdx :: String -> PkgName -> IO ()
installIdx String
dest PkgName
p = do
  let f :: String
f = PkgName -> String
pkgIndex PkgName
p
  let destdir :: String
destdir = String
dest String -> String -> String
</> PkgName -> String
unPkgName PkgName
p
  String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"Installing " forall a. [a] -> [a] -> [a]
++ String
f forall a. [a] -> [a] -> [a]
++ String
" to " forall a. [a] -> [a] -> [a]
++ String
destdir
  Bool -> String -> IO ()
createDirectoryIfMissing Bool
True String
destdir
  String -> String -> IO ()
copyFile String
f (String
destdir String -> String -> String
</> String -> String
takeFileName String
f)
  forall (m :: * -> *) a. Monad m => a -> m a
return ()

installObj :: String -> PkgName -> String -> IO ()
installObj :: String -> PkgName -> String -> IO ()
installObj String
dest PkgName
p String
o = do
  let destdir :: String
destdir = String -> String
addTrailingPathSeparator (String
dest String -> String -> String
</> PkgName -> String
unPkgName PkgName
p)
  String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"Installing " forall a. [a] -> [a] -> [a]
++ String
o forall a. [a] -> [a] -> [a]
++ String
" to " forall a. [a] -> [a] -> [a]
++ String
destdir
  Bool -> String -> IO ()
createDirectoryIfMissing Bool
True String
destdir
  String -> String -> IO ()
copyFile String
o (String
destdir String -> String -> String
</> String -> String
takeFileName String
o)
  forall (m :: * -> *) a. Monad m => a -> m a
return ()

#ifdef mingw32_HOST_OS
mkDirCmd = "mkdir "
#else
mkDirCmd :: String
mkDirCmd = String
"mkdir -p "
#endif

inPkgDir :: PkgDesc -> IO a -> IO a
inPkgDir :: forall a. PkgDesc -> IO a -> IO a
inPkgDir PkgDesc
pkgdesc IO a
action =
  do String
dir <- IO String
getCurrentDirectory
     forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (PkgDesc -> String
sourcedir PkgDesc
pkgdesc forall a. Eq a => a -> a -> Bool
/= String
"") forall a b. (a -> b) -> a -> b
$
       do String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"Entering directory `" forall a. [a] -> [a] -> [a]
++ (String
"." String -> String -> String
</> PkgDesc -> String
sourcedir PkgDesc
pkgdesc) forall a. [a] -> [a] -> [a]
++ String
"'"
          String -> IO ()
setCurrentDirectory forall a b. (a -> b) -> a -> b
$ String
dir String -> String -> String
</> PkgDesc -> String
sourcedir PkgDesc
pkgdesc
     a
res <- IO a
action
     forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (PkgDesc -> String
sourcedir PkgDesc
pkgdesc forall a. Eq a => a -> a -> Bool
/= String
"") forall a b. (a -> b) -> a -> b
$
       do String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"Leaving directory `" forall a. [a] -> [a] -> [a]
++ (String
"." String -> String -> String
</> PkgDesc -> String
sourcedir PkgDesc
pkgdesc) forall a. [a] -> [a] -> [a]
++ String
"'"
          String -> IO ()
setCurrentDirectory String
dir
     forall (m :: * -> *) a. Monad m => a -> m a
return a
res

-- ------------------------------------------------------- [ Makefile Commands ]
-- | Invoke a Makefile's target with an enriched system environment
makeTarget :: Maybe String -> Maybe String -> IO ()
makeTarget :: Maybe String -> Maybe String -> IO ()
makeTarget Maybe String
_ Maybe String
Nothing = forall (m :: * -> *) a. Monad m => a -> m a
return ()
makeTarget Maybe String
mtgt (Just String
s) = do String
incFlags <- forall a. [a] -> [[a]] -> [a]
intercalate String
" " forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO [String]
getIncFlags
                              String
libFlags <- forall a. [a] -> [[a]] -> [a]
intercalate String
" " forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO [String]
getLibFlags
                              [(String, String)]
newEnv <- (forall a. [a] -> [a] -> [a]
++ [(String
"IDRIS_INCLUDES", String
incFlags),
                                             (String
"IDRIS_LDFLAGS", String
libFlags)]) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO [(String, String)]
getEnvironment
                              let cmdLine :: String
cmdLine = case Maybe String
mtgt of
                                              Maybe String
Nothing -> String
"make -f " forall a. [a] -> [a] -> [a]
++ String
s
                                              Just String
tgt -> String
"make -f " forall a. [a] -> [a] -> [a]
++ String
s forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ String
tgt
                              (Maybe Handle
_, Maybe Handle
_, Maybe Handle
_, ProcessHandle
r) <- CreateProcess
-> IO (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
createProcess (String -> CreateProcess
shell String
cmdLine) { env :: Maybe [(String, String)]
env = forall a. a -> Maybe a
Just [(String, String)]
newEnv }
                              ProcessHandle -> IO ExitCode
waitForProcess ProcessHandle
r
                              forall (m :: * -> *) a. Monad m => a -> m a
return ()


-- | Invoke a Makefile's default target.
make :: Maybe String -> IO ()
make :: Maybe String -> IO ()
make = Maybe String -> Maybe String -> IO ()
makeTarget forall a. Maybe a
Nothing

-- | Invoke a Makefile's clean target.
clean :: Maybe String -> IO ()
clean :: Maybe String -> IO ()
clean = Maybe String -> Maybe String -> IO ()
makeTarget (forall a. a -> Maybe a
Just String
"clean")

-- | Merge an option list representing the command line options into
-- those specified for a package description.
--
-- This is not a complete union between the two options sets. First,
-- to prevent important package specified options from being
-- overwritten. Second, the semantics for this merge are not fully
-- defined.
--
-- A discussion for this is on the issue tracker:
--     https://github.com/idris-lang/Idris-dev/issues/1448
--
mergeOptions :: [Opt] -- ^ The command line options
             -> [Opt] -- ^ The package options
             -> Either String [Opt]
mergeOptions :: [Opt] -> [Opt] -> Either String [Opt]
mergeOptions [Opt]
copts [Opt]
popts =
    case forall a b. [Either a b] -> ([a], [b])
partitionEithers (forall a b. (a -> b) -> [a] -> [b]
map Opt -> Either String Opt
chkOpt ([Opt] -> [Opt]
normaliseOpts [Opt]
copts)) of
      ([], [Opt]
copts') -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ [Opt]
copts' forall a. [a] -> [a] -> [a]
++ [Opt]
popts
      ([String]
es, [Opt]
_)      -> forall a b. a -> Either a b
Left  forall a b. (a -> b) -> a -> b
$ [String] -> String
genErrMsg [String]
es
  where
    normaliseOpts :: [Opt] -> [Opt]
    normaliseOpts :: [Opt] -> [Opt]
normaliseOpts = forall a. (a -> Bool) -> [a] -> [a]
filter Opt -> Bool
filtOpt

    filtOpt :: Opt -> Bool
    filtOpt :: Opt -> Bool
filtOpt (PkgBuild        String
_) = Bool
False
    filtOpt (PkgInstall      String
_) = Bool
False
    filtOpt (PkgClean        String
_) = Bool
False
    filtOpt (PkgCheck        String
_) = Bool
False
    filtOpt (PkgREPL         String
_) = Bool
False
    filtOpt (PkgDocBuild     String
_) = Bool
False
    filtOpt (PkgDocInstall   String
_) = Bool
False
    filtOpt (PkgTest         String
_) = Bool
False
    filtOpt Opt
_                   = Bool
True

    chkOpt :: Opt -> Either String Opt
    chkOpt :: Opt -> Either String Opt
chkOpt o :: Opt
o@(OLogging Int
_)     = forall a b. b -> Either a b
Right Opt
o
    chkOpt o :: Opt
o@(OLogCats [LogCat]
_)     = forall a b. b -> Either a b
Right Opt
o
    chkOpt o :: Opt
o@(Opt
DefaultTotal)   = forall a b. b -> Either a b
Right Opt
o
    chkOpt o :: Opt
o@(Opt
DefaultPartial) = forall a b. b -> Either a b
Right Opt
o
    chkOpt o :: Opt
o@(Opt
WarnPartial)    = forall a b. b -> Either a b
Right Opt
o
    chkOpt o :: Opt
o@(Opt
WarnReach)      = forall a b. b -> Either a b
Right Opt
o
    chkOpt o :: Opt
o@(IBCSubDir String
_)    = forall a b. b -> Either a b
Right Opt
o
    chkOpt o :: Opt
o@(ImportDir String
_ )   = forall a b. b -> Either a b
Right Opt
o
    chkOpt o :: Opt
o@(UseCodegen Codegen
_)   = forall a b. b -> Either a b
Right Opt
o
    chkOpt o :: Opt
o@(Verbose Int
_)      = forall a b. b -> Either a b
Right Opt
o
    chkOpt o :: Opt
o@(Opt
AuditIPkg)      = forall a b. b -> Either a b
Right Opt
o
    chkOpt o :: Opt
o@(Opt
DumpHighlights) = forall a b. b -> Either a b
Right Opt
o
    chkOpt Opt
o                  = forall a b. a -> Either a b
Left ([String] -> String
unwords [String
"\t", forall a. Show a => a -> String
show Opt
o, String
"\n"])

    genErrMsg :: [String] -> String
    genErrMsg :: [String] -> String
genErrMsg [String]
es = [String] -> String
unlines
        [ String
"Not all command line options can be used to override package options."
        , String
"\nThe only changeable options are:"
        , String
"\t--log <lvl>, --total, --warnpartial, --warnreach, --warnipkg"
        , String
"\t--ibcsubdir <path>, -i --idrispath <path>"
        , String
"\t--logging-categories <cats>"
        , String
"\t--highlight"
        , String
"\nThe options need removing are:"
        , [String] -> String
unlines [String]
es
        ]

-- --------------------------------------------------------------------- [ EOF ]