970c833 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #782 from jfdm/feature/pkg-check-only

970c833Edwin Brady13 years ago

main/Main.hs+57−30

compare with master

unifiedsplit

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

53 when (ShowIncs `elem` opts) $ runIO showIncs

54 when (ShowLibs `elem` opts) $ runIO showLibs

55 when (ShowLibdir `elem` opts) $ runIO showLibdir

56+ case opt getPkgCheck opts of

57+ [] -> return ()

58+ fs -> do runIO $ mapM_ (checkPkg (WarnOnly `elem` opts)) fs

59+ runIO $ exitWith ExitSuccess

56 case opt getPkgClean opts of

60 case opt getPkgClean opts of

57 [] -> return ()

61 [] -> return ()

58 fs -> do runIO $ mapM_ cleanPkg fs

62 fs -> do runIO $ mapM_ cleanPkg fs

@@ -79,34 +83,57 @@ showIncs = do incFlags <- getIncFlags

79 putStrLn incFlags

83 putStrLn incFlags

80 exitWith ExitSuccess

84 exitWith ExitSuccess

86+usagemsghdr = "Idris version " ++ ver ++ ", (C) The Idris Community 2014"

87+

82−usagemsg = "Idris version " ++ ver ++ "\n" ++

88+usagemsg = usagemsghdr ++ "\n" ++

83− "--------------" ++ map (\x -> '-') ver ++ "\n" ++

89+ map (\x -> '-') usagemsghdr ++ "\n" ++

84− "Usage: idris [input file] [options]\n" ++

90+ "idris [OPTIONS] [FILE]\n\n" ++

85− "Options:\n" ++

91+ "Common flags:\n" ++

86− "\t--quiet Quiet mode (for editors)\n" ++

92+ "\t --install=IPKG Install Package\n" ++

87− "\t--[no]colour Control REPL colour highlighting\n" ++

93+ "\t --clean=IPKG Clean Package\n" ++

88− "\t--check Type check only\n" ++

94+ "\t --build=IPKG Build Package\n" ++

95+ "\t --exec=EXPR Execute as Idris\n" ++

96+ "\t --libdir Display library directory\n" ++

97+ "\t --link Display link directory\n" ++

98+ "\t --include Display the includes directory\n" ++

99+ "\t --nobanner Suppress the banner\n" ++

100+ "\t --color Force colored output\n" ++

101+ "\t --colour Force coloured output\n" ++

102+ "\t --nocolor Disable colored output\n" ++

103+ "\t --nocolour Disable coloured output\n" ++

104+ "\t --errorcontent Undocumented\n" ++

105+ "\t --nocoverage Undocumented\n" ++

89− "\t-o [file] Specify output filename\n" ++

106+ "\t -o --output=FILE Specify output file\n" ++

107+ "\t --check Undocumented\n" ++

108+ "\t --total Require functions to be total by default\n" ++

109+ "\t --partial Undocumented\n" ++

110+ "\t --warnpartial Warn about undeclared partial functions.\n" ++

111+ "\t --warn Undocumented\n" ++

112+ "\t --typecase Undocumented\n" ++

113+ "\t --typeintype Undocumented\n" ++

114+ "\t --nobasepkgs Undocumented\n" ++

115+ "\t --noprelude Undocumented\n" ++

116+ "\t --nobuiltins Undocumented\n" ++

117+ "\t -O --level=LEVEL Undocumented\n" ++

90− "\t-i [dir] Add directory to the list of import paths\n" ++

118+ "\t -i --idrispath=DIR Add directory to the list of import paths\n" ++

119+ "\t --package=ITEM Undocumented\n" ++

91− "\t--ibcsubdir [dir] Write IBC files into sub directory\n" ++

120+ "\t --ibcsubdir=FILE Write IBC files into sub directory\n" ++

92− "\t--noprelude Don't import the prelude\n" ++

121+ "\t --codegen=TARGET Select code generator: C, Java, bytecode," ++

93− "\t--total Require functions to be total by default\n" ++

122+ "\t javascript, node, or llvm\n" ++

94− "\t--warnpartial Warn about undeclared partial functions\n" ++

123+ "\t --mvn Create a maven project (for Java codegen)\n" ++

95− "\t--typeintype Disable universe checking\n" ++

124+ "\t --cpu=CPU Select tartget CPU e.g. corei& or cortex-m3" ++

96− "\t--log [level] Type debugging log level\n" ++

125+ "\t (for LLVM codegen)\n" ++

126+ "\t --target=TRIPLE Select target triple (for llvm codegen)\n" ++

97− "\t-S Do no further compilation of code generator output\n" ++

127+ "\t -S --codegenonly Do no further compilation of code generator output\n" ++

98− "\t-c Compile to object files rather than an executable\n" ++

128+ "\t -c --compileonly Compile to object fules rather than an executable\n" ++

99− "\t--mvn Create a maven project (for Java codegen)\n" ++

129+ "\t -X --extension=ITEM undocumented\n" ++

100− "\t--exec [expr] Execute the expression expr in the interpreter,\n" ++

130+ "\t --dumpdefuns Undocumented\n" ++

101− "\t defaulting to Main.main if none provided, and exit.\n" ++

131+ "\t --dumpcases Undocumented\n" ++

102− "\t--ideslave Ideslave mode (for editors; in/ouput wrapped in \n" ++

132+ "\t --log=LEVEL --loglevel Type Debugging log level\n" ++

103− "\t s-expressions)\n" ++

133+ "\t --ideslave Undocumented\n" ++

104− "\t--libdir Show library install directory and exit\n" ++

134+ "\t --client Undocumented\n" ++

105− "\t--link Show C library directories and exit (for C linking)\n" ++

135+ "\t -h --help Display help message\n" ++

106− "\t--include Show C include directories and exit (for C linking)\n" ++

136+ "\t -v --version Print version information\n" ++

107− "\t--codegen [cg] Select code generator: C, Java, bytecode, javascript,\n" ++

137+ "\t -V --Verbose Loud verbosity\n" ++

108− "\t node or llvm\n" ++

138+ "\t -q --quiet Quiet verbosity\n"

109− "\t--target [triple] Select target triple (for LLVM codegen)\n" ++

110− "\t--cpu [cpu] Select target CPU (e.g. corei7 or cortex-m3) (for LLVM codegen)\n"

111−

112

139

src/Idris/AbsSyntaxTree.hs+1

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

295 | PkgBuild String

296 | PkgInstall String

297 | PkgClean String

298+ | PkgCheck String

298 | WarnOnly

299 | WarnOnly

299 | Pkg String

300 | Pkg String

300 | BCAsm String

301 | BCAsm String

src/Idris/REPL.hs+7

@@ -1008,11 +1008,14 @@ parseArgs ("--verbose":ns) = Verbose : (parseArgs ns)

1008parseArgs ("--ibcsubdir":n:ns) = IBCSubDir n : (parseArgs ns)

1009parseArgs ("-i":n:ns) = ImportDir n : (parseArgs ns)

1010parseArgs ("--warn":ns) = WarnOnly : (parseArgs ns)

1011+-- Package Related options

1011parseArgs ("--package":n:ns) = Pkg n : (parseArgs ns)

1012parseArgs ("--package":n:ns) = Pkg n : (parseArgs ns)

1012parseArgs ("-p":n:ns) = Pkg n : (parseArgs ns)

1013parseArgs ("-p":n:ns) = Pkg n : (parseArgs ns)

1013parseArgs ("--build":n:ns) = PkgBuild n : (parseArgs ns)

1014parseArgs ("--build":n:ns) = PkgBuild n : (parseArgs ns)

1014parseArgs ("--install":n:ns) = PkgInstall n : (parseArgs ns)

1015parseArgs ("--install":n:ns) = PkgInstall n : (parseArgs ns)

1015parseArgs ("--clean":n:ns) = PkgClean n : (parseArgs ns)

1016parseArgs ("--clean":n:ns) = PkgClean n : (parseArgs ns)

1017+parseArgs ("--checkpkg":n:ns) = PkgCheck n : (parseArgs ns)

1018+-- Misc Options

1016parseArgs ("--bytecode":n:ns) = NoREPL : BCAsm n : (parseArgs ns)

1019parseArgs ("--bytecode":n:ns) = NoREPL : BCAsm n : (parseArgs ns)

1017parseArgs ("-S":ns) = OutputTy Raw : (parseArgs ns)

1020parseArgs ("-S":ns) = OutputTy Raw : (parseArgs ns)

1018parseArgs ("-c":ns) = OutputTy Object : (parseArgs ns)

1021parseArgs ("-c":ns) = OutputTy Object : (parseArgs ns)

@@ -1327,6 +1330,10 @@ getPkgClean :: Opt -> Maybe String

1327getPkgClean (PkgClean str) = Just str

1330getPkgClean (PkgClean str) = Just str

1328getPkgClean _ = Nothing

1331getPkgClean _ = Nothing

1329

1332

1333+getPkgCheck :: Opt -> Maybe String

1334+getPkgCheck (PkgCheck str) = Just str

1335+getPkgCheck _ = Nothing

1336+

1330getCodegen :: Opt -> Maybe Codegen

1337getCodegen :: Opt -> Maybe Codegen

1331getCodegen (UseCodegen x) = Just x

1338getCodegen (UseCodegen x) = Just x

1332getCodegen _ = Nothing

1339getCodegen _ = Nothing

src/Pkg/Package.hs+41−2

@@ -24,13 +24,14 @@ import Pkg.PParser

25import Paths_idris (getDataDir)

27+-- | Run the package through the idris compiler.

28+--

27-- To build a package:

29-- To build a package:

28-- * read the package description

30-- * read the package description

29-- * check all the library dependencies exist

31-- * check all the library dependencies exist

30-- * invoke the makefile if there is one

32-- * invoke the makefile if there is one

31-- * invoke idris on each module, with idris_opts

33-- * invoke idris on each module, with idris_opts

32-- * install everything into datadir/pname, if install flag is set

34-- * install everything into datadir/pname, if install flag is set

33−

34buildPkg :: Bool -> (Bool, FilePath) -> IO ()

35buildPkg :: Bool -> (Bool, FilePath) -> IO ()

35buildPkg warnonly (install, fp)

36buildPkg warnonly (install, fp)

36 = do pkgdesc <- parseDesc fp

37 = do pkgdesc <- parseDesc fp

@@ -63,7 +64,33 @@ buildPkg warnonly (install, fp)

63 putStrLn $ "\t" ++ show ms

64 putStrLn $ "\t" ++ show ms

64 exitWith (ExitFailure 1)

65 exitWith (ExitFailure 1)

67+-- | Type check packages only

68+--

69+-- This differs from build in that executables are not built, if the

70+-- package contains an executable.

71+checkPkg :: Bool -- ^ Show Warnings

72+ -> FilePath -- ^ Path to ipkg file.

73+ -> IO ()

74+checkPkg warnonly fpath

75+ = do pkgdesc <-parseDesc fpath

76+ ok <- mapM (testLib warnonly (pkgname pkgdesc)) (libdeps pkgdesc)

77+ when (and ok) $

78+ do dir <- getCurrentDirectory

79+ setCurrentDirectory $ dir </> sourcedir pkgdesc

80+ make (makefile pkgdesc)

81+ res <- buildMods (NoREPL : Verbose : idris_opts pkgdesc)

82+ (modules pkgdesc)

83+ setCurrentDirectory dir

84+ case res of

85+ Nothing -> exitWith (ExitFailure 1)

86+ Just res' -> do

87+ case errLine res' of

88+ Just _ -> exitWith (ExitFailure 1)

89+ _ -> return ()

90+

91+-- | Clean Package build files

66−cleanPkg :: FilePath -> IO ()

92+cleanPkg :: FilePath -- ^ Path to ipkg file.

93+ -> IO ()

67cleanPkg fp

94cleanPkg fp

68 = do pkgdesc <- parseDesc fp

95 = do pkgdesc <- parseDesc fp

69 dir <- getCurrentDirectory

96 dir <- getCurrentDirectory

@@ -74,6 +101,7 @@ cleanPkg fp

74 Nothing -> return ()

101 Nothing -> return ()

75 Just s -> rmFile $ dir </> s

102 Just s -> rmFile $ dir </> s

103

104+-- | Install package

77installPkg :: PkgDesc -> IO ()

105installPkg :: PkgDesc -> IO ()

78installPkg pkgdesc

106installPkg pkgdesc

79 = do dir <- getCurrentDirectory

107 = do dir <- getCurrentDirectory

@@ -83,6 +111,11 @@ installPkg pkgdesc

83 Just o -> return () -- do nothing, keep executable locally, for noe

111 Just o -> return () -- do nothing, keep executable locally, for noe

84 mapM_ (installObj (pkgname pkgdesc)) (objs pkgdesc)

112 mapM_ (installObj (pkgname pkgdesc)) (objs pkgdesc)

113

114+

115+-- ---------------------------------------------------------- [ Helper Methods ]

116+-- Methods for building, testing, installing, and removal of idris

117+-- packages.

118+

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

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

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

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

88-- putStrLn $ "MODULE: " ++ show f

121-- putStrLn $ "MODULE: " ++ show f

@@ -122,6 +155,7 @@ installIBC p m = do let f = toIBCFile m

122 where getDest (UN n) = ""

155 where getDest (UN n) = ""

123 getDest (NS n ns) = foldl1' (</>) (reverse (getDest n : map str ns))

156 getDest (NS n ns) = foldl1' (</>) (reverse (getDest n : map str ns))

124

157

158+

125installObj :: String -> String -> IO ()

159installObj :: String -> String -> IO ()

126installObj p o = do d <- getTargetDir

160installObj p o = do d <- getTargetDir

127 let destdir = addTrailingPathSeparator (d </> p)

161 let destdir = addTrailingPathSeparator (d </> p)

@@ -136,12 +170,17 @@ mkDirCmd = "mkdir "

136mkDirCmd = "mkdir -p "

170mkDirCmd = "mkdir -p "

137#endif

171#endif

138

172

173+-- ------------------------------------------------------- [ Makefile Commands ]

174+-- | Invoke a Makefile's default target.

139make :: Maybe String -> IO ()

175make :: Maybe String -> IO ()

140make Nothing = return ()

176make Nothing = return ()

141make (Just s) = do system $ "make -f " ++ s

177make (Just s) = do system $ "make -f " ++ s

142 return ()

178 return ()

143

179

180+-- | Invoke a Makefile's clean target.

144clean :: Maybe String -> IO ()

181clean :: Maybe String -> IO ()

145clean Nothing = return ()

182clean Nothing = return ()

146clean (Just s) = do system $ "make -f " ++ s ++ " clean"

183clean (Just s) = do system $ "make -f " ++ s ++ " clean"

147 return ()

184 return ()

185+

186+-- --------------------------------------------------------------------- [ EOF ]