a75bd0f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #1280 from david-christiansen/testrunner

Add --testpkg option + tests section in ipkg files

commita75bd0f492d98e0ce01eeb216b8e2b25928dccf7 authorEdwin Brady <edwin.brady@gmail.com> dateWed 4 Jun 2014, 16:52 (12 years ago) parent42d0138 6ea7202

7 files changed+61−3

compare with master

unifiedsplit

CHANGELOG+6 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

CHANGELOG+6

@@ -1,3 +1,9 @@

1+New in 0.9.14:

2+--------------

3+* Support for running tests for a package with the tests section of .ipkg files and the

4+ --testpkg command-line option

17New in 0.9.13:

28--------------

39* IDE support for retrieving structured information about metavariables

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

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

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

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

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

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

104105 -- Misc options

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

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

src/Idris/REPL.hs+5

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

13521352getPkgMkDoc (PkgMkDoc str) = Just str

13531353getPkgMkDoc _ = Nothing

13541354

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

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

1357+getPkgTest (PkgTest f) = Just f

1358+getPkgTest _ = Nothing

1359+

13551360getCodegen :: Opt -> Maybe Codegen

13561361getCodegen (UseCodegen x) = Just x

13571362getCodegen _ = 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 ()