e2a34a8 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add --testpkg option + tests section in IPKG files

Add a new section to IPKG files called "tests". This section should be a comma-separated list of fully qualified names of IO actions, the sequence of which in some way test an Idris package. When invoked as idris --testpkg IPKG, Idris will generate a module in a temporary directory that imports every module from the package IPKG and whose main function simply executes each specified test. The intention is to keep test specifications as low-level as possible, allowing user libraries to define a better mechanism on top of this.

commite2a34a8691d998daea24a74355fff632fb7b88ed authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateTue 3 Jun 2014, 19:08 (12 years ago) parent4d215c1

6 files changed+55−3

compare with master

unifiedsplit

main/Main.hs+4 src/Idris/AbsSyntaxTree.hs+1 src/Idris/CmdOptions.hs+1 src/Idris/REPL.hs+5 src/Pkg/PParser.hs+7−2 src/Pkg/Package.hs+37−1

main/Main.hs+4

@@ -63,6 +63,10 @@ runIdris opts = do

6363 [] -> return ()

6464 fs -> do runIO $ mapM_ documentPkg fs

6565 runIO $ exitWith ExitSuccess

66+ case opt getPkgTest opts of

67+ [] -> return ()

68+ fs -> do runIO $ mapM_ testPkg fs

69+ runIO $ exitWith ExitSuccess

6670 case opt getPkg opts of

6771 [] -> case opt getPkgREPL opts of

6872 [] -> idrisMain opts

src/Idris/AbsSyntaxTree.hs+1

@@ -373,6 +373,7 @@ data Opt = Filename String

373373 | PkgCheck String

374374 | PkgREPL String

375375 | PkgMkDoc String -- IdrisDoc

376+ | PkgTest String

376377 | WarnOnly

377378 | Pkg String

378379 | BCAsm String

src/Idris/CmdOptions.hs+1

@@ -61,6 +61,7 @@ parseFlags = many $

6161 <|> (PkgClean <$> strOption (long "clean" <> metavar "IPKG" <> help "Clean package"))

6262 <|> (PkgMkDoc <$> strOption (long "mkdoc" <> metavar "IPKG" <> help "Generate IdrisDoc for package"))

6363 <|> (PkgCheck <$> strOption (long "checkpkg" <> metavar "IPKG" <> help "Check package only"))

64+ <|> (PkgTest <$> strOption (long "testpkg" <> metavar "IPKG" <> help "Run tests for package"))

6465 -- Misc options

6566 <|> (BCAsm <$> strOption (long "bytecode"))

6667 <|> flag' (OutputTy Raw) (short 'S' <> long "codegenonly" <> help "Do no further compilation of code generator output")

src/Idris/REPL.hs+5

@@ -1350,6 +1350,11 @@ getPkgMkDoc :: Opt -- ^ Opt to extract

13501350getPkgMkDoc (PkgMkDoc str) = Just str

13511351getPkgMkDoc _ = Nothing

13521352

1353+getPkgTest :: Opt -- ^ the option to extract

1354+ -> Maybe String -- ^ the package file to test

1355+getPkgTest (PkgTest f) = Just f

1356+getPkgTest _ = Nothing

1357+

13531358getCodegen :: Opt -> Maybe Codegen

13541359getCodegen (UseCodegen x) = Just x

13551360getCodegen _ = Nothing

src/Pkg/PParser.hs+7−2

@@ -26,7 +26,8 @@ data PkgDesc = PkgDesc { pkgname :: String,

2626 sourcedir :: String,

2727 modules :: [Name],

2828 idris_main :: Name,

29− execout :: Maybe String

29+ execout :: Maybe String,

30+ idris_tests :: [Name]

3031 }

3132 deriving Show

3233

@@ -34,7 +35,7 @@ instance TokenParsing PParser where

3435 someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()

3536

3637

37−defaultPkg = PkgDesc "" [] [] Nothing [] "" [] (sUN "") Nothing

38+defaultPkg = PkgDesc "" [] [] Nothing [] "" [] (sUN "") Nothing []

3839

3940parseDesc :: FilePath -> IO PkgDesc

4041parseDesc fp = do p <- readFile fp

@@ -85,4 +86,8 @@ pClause = do reserved "executable"; lchar '=';

8586 mk <- iName []

8687 st <- get

8788 put (st { makefile = Just (show mk) })

89+ <|> do reserved "tests"; lchar '=';

90+ ts <- sepBy1 (iName []) (lchar ',')

91+ st <- get

92+ put st { idris_tests = idris_tests st ++ ts }

8893

src/Pkg/Package.hs+37−1

@@ -5,7 +5,7 @@ import System.Process

55import System.Directory

66import System.Exit

77import System.IO

8−import System.FilePath ((</>), addTrailingPathSeparator, takeFileName, takeDirectory)

8+import System.FilePath ((</>), addTrailingPathSeparator, takeFileName, takeDirectory, normalise)

99import System.Directory (createDirectoryIfMissing, copyFile)

1010

1111import Util.System

@@ -159,6 +159,42 @@ documentPkg fp =

159159 Left msg -> do putStrLn msg

160160 exitWith (ExitFailure 1)

161161

162+-- | Build a package with a sythesized main function that runs the tests

163+testPkg :: FilePath -> IO ()

164+testPkg fp

165+ = do pkgdesc <- parseDesc fp

166+ ok <- mapM (testLib True (pkgname pkgdesc)) (libdeps pkgdesc)

167+ when (and ok) $

168+ do dir <- getCurrentDirectory

169+ setCurrentDirectory $ dir </> sourcedir pkgdesc

170+ make (makefile pkgdesc)

171+ -- Get a temporary file to save the tests' source in

172+ (tmpn, tmph) <- tempIdr

173+ hPutStrLn tmph $

174+ "module Test_______\n" ++

175+ concat ["import " ++ show m ++ "\n"

176+ | m <- modules pkgdesc] ++

177+ "namespace Main\n" ++

178+ " main : IO ()\n" ++

179+ " main = do " ++

180+ concat [show t ++ "\n "

181+ | t <- idris_tests pkgdesc]

182+ hClose tmph

183+ (tmpn', tmph') <- tempfile

184+ hClose tmph'

185+ m_ist <- idris (Filename tmpn : NoREPL : Verbose : Output tmpn' : idris_opts pkgdesc)

186+ system tmpn'

187+ setCurrentDirectory dir

188+ case m_ist of

189+ Nothing -> exitWith (ExitFailure 1)

190+ Just ist -> do

191+ -- Quit with error code if problem building

192+ case errSpan ist of

193+ Just _ -> exitWith (ExitFailure 1)

194+ _ -> return ()

195+ where tempIdr :: IO (FilePath, Handle)

196+ tempIdr = do dir <- getTemporaryDirectory

197+ openTempFile (normalise dir) "idristests.idr"

162198

163199-- | Install package

164200installPkg :: PkgDesc -> IO ()