idris-0.9.19: 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.

checkPkg Source


:: 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

cleanPkg Source


:: FilePath

Path to ipkg file.

-> IO () 

Clean Package build files

documentPkg Source


:: 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

testPkg :: FilePath -> IO () Source

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

installPkg :: PkgDesc -> IO () Source

Install package

rmIBC :: Name -> IO () Source

inPkgDir :: PkgDesc -> IO a -> IO a Source

make :: Maybe String -> IO () Source

Invoke a Makefile's default target.

clean :: Maybe String -> IO () Source

Invoke a Makefile's clean target.