a75bd0f · Idris-dev · git.iko.soy

CHANGELOG+6

compare with master

unifiedsplit

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

5+

6+

1New in 0.9.13:

7New in 0.9.13:

2--------------

8--------------

3* IDE support for retrieving structured information about metavariables

9* IDE support for retrieving structured information about metavariables

main/Main.hs+4

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

63 [] -> return ()

64 fs -> do runIO $ mapM_ documentPkg fs

65 runIO $ exitWith ExitSuccess

66+ case opt getPkgTest opts of

67+ [] -> return ()

68+ fs -> do runIO $ mapM_ testPkg fs

69+ runIO $ exitWith ExitSuccess

66 case opt getPkg opts of

70 case opt getPkg opts of

67 [] -> case opt getPkgREPL opts of

71 [] -> case opt getPkgREPL opts of

68 [] -> idrisMain opts

72 [] -> idrisMain opts

src/Idris/AbsSyntaxTree.hs+1

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

373 | PkgCheck String

374 | PkgREPL String

375 | PkgMkDoc String -- IdrisDoc

376+ | PkgTest String

376 | WarnOnly

377 | WarnOnly

377 | Pkg String

378 | Pkg String

378 | BCAsm String

379 | BCAsm String

src/Idris/CmdOptions.hs+1

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

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

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

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

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

104 -- Misc options

105 -- Misc options

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

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

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

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

1352getPkgMkDoc (PkgMkDoc str) = Just str

1353getPkgMkDoc _ = Nothing

1354

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+

1355getCodegen :: Opt -> Maybe Codegen

1360getCodegen :: Opt -> Maybe Codegen

1356getCodegen (UseCodegen x) = Just x

1361getCodegen (UseCodegen x) = Just x

1357getCodegen _ = Nothing

1362getCodegen _ = Nothing

src/Pkg/PParser.hs+7−2

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

26 sourcedir :: String,

27 modules :: [Name],

28 idris_main :: Name,

29− execout :: Maybe String

29+ execout :: Maybe String,

30+ idris_tests :: [Name]

30 }

31 }

31 deriving Show

32 deriving Show

32

33

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

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

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

35

36

37

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

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

38

39

39parseDesc :: FilePath -> IO PkgDesc

40parseDesc :: FilePath -> IO PkgDesc

40parseDesc fp = do p <- readFile fp

41parseDesc fp = do p <- readFile fp

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

85 mk <- iName []

86 mk <- iName []

86 st <- get

87 st <- get

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

88 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 }

88

93

src/Pkg/Package.hs+37−1

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

5import System.Directory

6import System.Exit

7import System.IO

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

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

9import System.Directory (createDirectoryIfMissing, copyFile)

10

11import Util.System

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

159 Left msg -> do putStrLn msg

160 exitWith (ExitFailure 1)

161

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"

162

198

163-- | Install package

199-- | Install package

164installPkg :: PkgDesc -> IO ()

200installPkg :: PkgDesc -> IO ()