idris-0.9.15: Functional Programming Language with Dependent Types

Safe HaskellNone




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

buildPkg :: Bool -> (Bool, FilePath) -> IO ()Source

Run the package through the idris compiler.



:: Bool

Show Warnings

-> Bool

quit on failure

-> FilePath

Path to ipkg file.

-> IO () 

Type check packages only

This differs from build in that executables are not built, if the package contains an executable.

replPkg :: FilePath -> Idris ()Source

Check a package and start a REPL



:: FilePath

Path to ipkg file.

-> IO () 

Clean Package build files



:: FilePath

Path to .ipkg file.

-> IO () 

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.comidris-langIdris-devissues1572

testPkg :: FilePath -> IO ()Source

Build a package with a sythesized main function that runs the tests

installPkg :: PkgDesc -> IO ()Source

Install package

buildMods :: [Opt] -> [Name] -> IO (Maybe IState)Source

testLib :: Bool -> String -> String -> IO BoolSource

rmIBC :: Name -> IO ()Source

toIBCFile :: Name -> [Char]Source

installIBC :: String -> Name -> IO ()Source

installObj :: String -> String -> IO ()Source

mkDirCmd :: [Char]Source

make :: Maybe String -> IO ()Source

Invoke a Makefile's default target.

clean :: Maybe String -> IO ()Source

Invoke a Makefile's clean target.