3acfea9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #3447 from jfdm/ipkg-warning-flag

3acfea9Jan de Muijnck-Hughes10 years ago

CHANGELOG.md+5

compare with master

unifiedsplit

@@ -36,6 +36,11 @@

36 Unicode-rendering issues on Windows (e.g., error messages stating

37 `commitBuffer: invalid argument (invalid character)`).

39++ Idris now has a `--warnipkg` flag to enable auditing of Idris

40+ packages during build time. Currently auditing check's the list of

41+ modules specified in the `iPKG` file with those presented in the

42+ package directory.

43+

39## Library Updates

44## Library Updates

41+ Terminating programs has been improved with more appropriate

46+ Terminating programs has been improved with more appropriate

docs/reference/packages.rst+2

@@ -138,6 +138,8 @@ Given an Idris package file ``text.ipkg`` it can be used with the Idris compiler

138

139+ ``idris --testpkg test.ipkg`` will compile and run any embedded tests you have specified in the ``tests`` parameter.

140

141+When building or install packages the commandline flag ``--warnipkg`` will audit the project and warn of any potentiable problems.

142+

141Once the test package has been installed, the command line option

143Once the test package has been installed, the command line option

142``--package test`` makes it accessible (abbreviated to ``-p test``).

144``--package test`` makes it accessible (abbreviated to ``-p test``).

143For example::

145For example::

src/Idris/AbsSyntaxTree.hs+1

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

523 | DefaultPartial

524 | WarnPartial

525 | WarnReach

526+ | AuditIPkg

526 | EvalTypes

527 | EvalTypes

527 | NoCoverage

528 | NoCoverage

528 | ErrContext

529 | ErrContext

src/Idris/CmdOptions.hs+1

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

126 <|> flag' DefaultPartial (long "partial")

127 <|> flag' WarnPartial (long "warnpartial" <> help "Warn about undeclared partial functions")

128 <|> flag' WarnReach (long "warnreach" <> help "Warn about reachable but inaccessible arguments")

129+ <|> flag' AuditIPkg (long "warnipkg" <> help "Warn about possible incorrect package specifications")

129 <|> flag' NoCoverage (long "nocoverage")

130 <|> flag' NoCoverage (long "nocoverage")

130 <|> flag' ErrContext (long "errorcontext")

131 <|> flag' ErrContext (long "errorcontext")

131

132

src/Idris/Package.hs+78−22

@@ -8,6 +8,26 @@ Maintainer : The Idris Community.

8{-# LANGUAGE CPP #-}

9module Idris.Package where

11+import System.Directory

12+import System.Directory (copyFile, createDirectoryIfMissing)

13+import System.Exit

14+import System.FilePath (addExtension, addTrailingPathSeparator, dropExtension,

15+ hasExtension, normalise, takeDirectory, takeExtension,

16+ takeFileName, (</>))

17+import System.IO

18+import System.Process

19+

20+import Util.System

21+

22+import Control.Monad

23+import Control.Monad.Trans.Except (runExceptT)

24+import Control.Monad.Trans.State.Strict (execStateT)

25+import Data.Either (partitionEithers)

26+import Data.Either (partitionEithers)

27+import Data.List

28+import Data.List.Split (splitOn)

29+import Data.Maybe (fromMaybe)

30+

11import Idris.AbsSyntax

31import Idris.AbsSyntax

12import Idris.Core.TT

32import Idris.Core.TT

13import Idris.Error (ifail)

33import Idris.Error (ifail)

@@ -17,28 +37,13 @@ import Idris.Imports

17import Idris.Main (idris, idrisMain)

37import Idris.Main (idris, idrisMain)

18import Idris.Output (pshow)

38import Idris.Output (pshow)

19import Idris.Output

39import Idris.Output

20−import Idris.Package.Common

21−import Idris.Package.Parser

22import Idris.Parser (loadModule)

40import Idris.Parser (loadModule)

23import Idris.REPL

41import Idris.REPL

24−import IRTS.System

26−import Util.System

43+import Idris.Package.Common

44+import Idris.Package.Parser

28−import Control.Monad

46+import IRTS.System

29−import Control.Monad.Trans.Except (runExceptT)

30−import Control.Monad.Trans.State.Strict (execStateT)

31−import Data.Either (partitionEithers)

32−import Data.List

33−import Data.List.Split (splitOn)

34−import Data.Maybe (fromMaybe)

35−import System.Directory

36−import System.Directory (copyFile, createDirectoryIfMissing)

37−import System.Exit

38−import System.FilePath (addExtension, addTrailingPathSeparator, hasExtension,

39− normalise, takeDirectory, takeFileName, (</>))

40−import System.IO

41−import System.Process

43-- To build a package:

48-- To build a package:

44-- * read the package description

49-- * read the package description

@@ -75,14 +80,18 @@ buildPkg copts warnonly (install, fp) = do

75 Left emsg -> do

80 Left emsg -> do

76 putStrLn emsg

81 putStrLn emsg

77 exitWith (ExitFailure 1)

82 exitWith (ExitFailure 1)

83+ Right opts -> do

84+ auditPackage (AuditIPkg `elem` opts) pkgdesc

78− Right opts -> buildMods opts (modules pkgdesc)

85+ buildMods opts (modules pkgdesc)

79 Just o -> do

86 Just o -> do

80 let exec = dir </> o

87 let exec = dir </> o

81 case mergeOptions copts (idx : NoREPL : Verbose 1 : Output exec : idris_opts pkgdesc) of

88 case mergeOptions copts (idx : NoREPL : Verbose 1 : Output exec : idris_opts pkgdesc) of

82 Left emsg -> do

89 Left emsg -> do

83 putStrLn emsg

90 putStrLn emsg

84 exitWith (ExitFailure 1)

91 exitWith (ExitFailure 1)

92+ Right opts -> do

93+ auditPackage (AuditIPkg `elem` opts) pkgdesc

85− Right opts -> buildMain opts (idris_main pkgdesc)

94+ buildMain opts (idris_main pkgdesc)

86 case m_ist of

95 case m_ist of

87 Nothing -> exitWith (ExitFailure 1)

96 Nothing -> exitWith (ExitFailure 1)

88 Just ist -> do

97 Just ist -> do

@@ -120,6 +129,7 @@ checkPkg copts warnonly quit fpath = do

120 putStrLn emsg

129 putStrLn emsg

121 exitWith (ExitFailure 1)

130 exitWith (ExitFailure 1)

122 Right opts -> do

131 Right opts -> do

132+ auditPackage (AuditIPkg `elem` opts) pkgdesc

123 buildMods opts (modules pkgdesc)

133 buildMods opts (modules pkgdesc)

124 when quit $ case res of

134 when quit $ case res of

125 Nothing -> exitWith (ExitFailure 1)

135 Nothing -> exitWith (ExitFailure 1)

@@ -301,10 +311,55 @@ installPkg altdests pkgdesc = inPkgDir pkgdesc $ do

301-- Methods for building, testing, installing, and removal of idris

311-- Methods for building, testing, installing, and removal of idris

302-- packages.

312-- packages.

303

313

314+auditPackage :: Bool -> PkgDesc -> IO ()

315+auditPackage False _ = return ()

316+auditPackage True ipkg = do

317+ cwd <- getCurrentDirectory

318+

319+ let ms = map (sourcedir ipkg </>) $ map (toPath . showCG) (modules ipkg)

320+ ms' <- mapM makeAbsolute ms

321+

322+ ifiles <- getIdrisFiles cwd

323+

324+ let ifiles' = map dropExtension ifiles

325+

326+ not_listed <- mapM makeRelativeToCurrentDirectory (ifiles' \\ ms')

327+

328+ putStrLn $ unlines $

329+ ["Warning: The following modules are not listed in your iPkg file:\n"]

330+ ++ map (\m -> unwords ["-", m]) not_listed

331+ ++ ["\nModules that are not listed, are not installed."]

332+

333+ where

334+ toPath n = foldl1' (</>) $ splitOn "." n

335+

336+ getIdrisFiles :: FilePath -> IO [FilePath]

337+ getIdrisFiles dir = do

338+ contents <- getDirectoryContents dir

339+ let contents' = filter (\fname -> fname /= "." && fname /= "..") contents

340+

341+ -- [ NOTE ] Directory >= 1.2.5.0 introduced `listDirectory` but later versions of directory appear to be causing problems with ghc 7.10.3 and cabal 1.22 in travis. Let's reintroduce the old ranges for directory to be sure.

342+

343+

344+ files <- forM contents (findRest dir)

345+ return $ filter (isIdrisFile) (concat files)

346+

347+ isIdrisFile :: FilePath -> Bool

348+ isIdrisFile fp = takeExtension fp == ".idr" || takeExtension fp == ".lidr"

349+

350+ findRest :: FilePath -> FilePath -> IO [FilePath]

351+ findRest dir fn = do

352+ path <- makeAbsolute (dir </> fn)

353+ isDir <- doesDirectoryExist path

354+ if isDir

355+ then getIdrisFiles path

356+ else return [path]

357+

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

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

305buildMods opts ns = do let f = map (toPath . showCG) ns

359buildMods opts ns = do let f = map (toPath . showCG) ns

306 idris (map Filename f ++ opts)

360 idris (map Filename f ++ opts)

361+ where

307− where toPath n = foldl1' (</>) $ splitOn "." n

362+ toPath n = foldl1' (</>) $ splitOn "." n

308

363

309testLib :: Bool -> String -> String -> IO Bool

364testLib :: Bool -> String -> String -> IO Bool

310testLib warn p f

365testLib warn p f

@@ -443,13 +498,14 @@ mergeOptions copts popts =

443 chkOpt o@(ImportDir _ ) = Right o

498 chkOpt o@(ImportDir _ ) = Right o

444 chkOpt o@(UseCodegen _) = Right o

499 chkOpt o@(UseCodegen _) = Right o

445 chkOpt o@(Verbose _) = Right o

500 chkOpt o@(Verbose _) = Right o

501+ chkOpt o@(AuditIPkg) = Right o

446 chkOpt o = Left (unwords ["\t", show o, "\n"])

502 chkOpt o = Left (unwords ["\t", show o, "\n"])

447

503

448 genErrMsg :: [String] -> String

504 genErrMsg :: [String] -> String

449 genErrMsg es = unlines

505 genErrMsg es = unlines

450 [ "Not all command line options can be used to override package options."

506 [ "Not all command line options can be used to override package options."

451 , "\nThe only changeable options are:"

507 , "\nThe only changeable options are:"

452− , "\t--log <lvl>, --total, --warnpartial, --warnreach"

508+ , "\t--log <lvl>, --total, --warnpartial, --warnreach, --warnipkg"

453 , "\t--ibcsubdir <path>, -i --idrispath <path>"

509 , "\t--ibcsubdir <path>, -i --idrispath <path>"

454 , "\t--logging-categories <cats>"

510 , "\t--logging-categories <cats>"

455 , "\nThe options need removing are:"

511 , "\nThe options need removing are:"

test/pkg001/expected+1−1

@@ -1,7 +1,7 @@

1Not all command line options can be used to override package options.

3The only changeable options are:

4− --log <lvl>, --total, --warnpartial, --warnreach

4+ --log <lvl>, --total, --warnpartial, --warnreach, --warnipkg

5 --ibcsubdir <path>, -i --idrispath <path>

6 --logging-categories <cats>