483fd4f · Idris-dev · git.iko.soy

idris.cabal+6

compare with master

unifiedsplit

@@ -656,6 +656,12 @@ Extra-source-files:

656 test/pkg004/*.idr

657 test/pkg004/expected

658 test/pkg004/*.ipkg

659+ test/pkg005/run

660+ test/pkg005/expected

661+ test/pkg005/*.ipkg

662+ test/pkg006/run

663+ test/pkg006/expected

664+ test/pkg006/*.ipkg

659

665

660 test/proof001/run

666 test/proof001/run

661 test/proof001/*.idr

667 test/proof001/*.idr

src/Idris/Package.hs+13−7

@@ -82,7 +82,7 @@ buildPkg copts warnonly (install, fp) = do

82 Left emsg -> do

83 putStrLn emsg

84 exitWith (ExitFailure 1)

85− Right opts -> buildMods opts [idris_main pkgdesc]

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

86 case m_ist of

87 Nothing -> exitWith (ExitFailure 1)

88 Just ist -> do

@@ -91,6 +91,11 @@ buildPkg copts warnonly (install, fp) = do

91 Just _ -> exitWith (ExitFailure 1)

92 _ -> return ()

93 when install $ installPkg (opt getIBCSubDir copts) pkgdesc

94+ where

95+ buildMain opts (Just mod) = buildMods opts [mod]

96+ buildMain _ Nothing = do

97+ putStrLn "Can't build an executable: No main module given"

98+ exitWith (ExitFailure 1)

94

99

95-- --------------------------------------------------------- [ Check Packages ]

100-- --------------------------------------------------------- [ Check Packages ]

96

101

@@ -140,20 +145,21 @@ replPkg copts fp = do

140 case mergeOptions copts (idris_opts pkgdesc) of

145 case mergeOptions copts (idris_opts pkgdesc) of

141 Left emsg -> ifail emsg

146 Left emsg -> ifail emsg

142 Right opts -> do

147 Right opts -> do

143− let mod = idris_main pkgdesc

144− let f = toPath (showCG mod)

145 putIState orig

148 putIState orig

146 dir <- runIO getCurrentDirectory

149 dir <- runIO getCurrentDirectory

147 runIO $ setCurrentDirectory $ dir </> sourcedir pkgdesc

150 runIO $ setCurrentDirectory $ dir </> sourcedir pkgdesc

148−

151+ runMain opts (idris_main pkgdesc)

149− if (f /= "")

150− then idrisMain ((Filename f) : opts)

151− else iputStrLn "Can't start REPL: no main module given"

152 runIO $ setCurrentDirectory dir

153

154 where

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

156

157+ runMain opts (Just mod) = do

158+ let f = toPath (showCG mod)

159+ idrisMain ((Filename f) : opts)

160+ runMain _ Nothing =

161+ iputStrLn "Can't start REPL: no main module given"

162+

157-- --------------------------------------------------------------- [ Cleaning ]

163-- --------------------------------------------------------------- [ Cleaning ]

158

164

159-- | Clean Package build files

165-- | Clean Package build files

src/Idris/Package/Common.hs+2−2

@@ -30,7 +30,7 @@ data PkgDesc = PkgDesc {

30 , idris_opts :: [Opt] -- ^ List of options to give the compiler.

31 , sourcedir :: String -- ^ Source directory for Idris files.

32 , modules :: [Name] -- ^ Modules provided by the package.

33− , idris_main :: Name -- ^ If an executable in which module can the Main namespace and function be found.

33+ , idris_main :: Maybe Name -- ^ If an executable in which module can the Main namespace and function be found.

34 , execout :: Maybe String -- ^ What to call the executable.

35 , idris_tests :: [Name] -- ^ Lists of tests to execute against the package.

36 } deriving (Show)

@@ -39,4 +39,4 @@ data PkgDesc = PkgDesc {

39defaultPkg :: PkgDesc

40defaultPkg = PkgDesc "" [] Nothing Nothing Nothing Nothing

41 Nothing Nothing Nothing Nothing

42− Nothing [] [] Nothing [] "" [] (sUN "") Nothing []

42+ Nothing [] [] Nothing [] "" [] Nothing Nothing []

src/Idris/Package/Parser.hs+1−1

@@ -127,7 +127,7 @@ pClause = do reserved "executable"; lchar '=';

127 <|> do reserved "main"; lchar '=';

128 main <- fst <$> iName []

129 st <- get

130− put (st { idris_main = main })

130+ put (st { idris_main = Just main })

131

132 <|> do reserved "sourcedir"; lchar '=';

133 src <- fst <$> identifier

test/TestData.hs+3−1

@@ -167,7 +167,9 @@ testFamiliesData = [

167 [ ( 1, ANY ),

168 ( 2, ANY ),

169 ( 3, ANY ),

170− ( 4, ANY )]),

170+ ( 4, ANY ),

171+ ( 5, ANY ),

172+ ( 6, ANY )]),

171 ("prelude", "Prelude",

173 ("prelude", "Prelude",

172 [ ( 1, ANY )]),

174 [ ( 1, ANY )]),

173 ("primitives", "Primitive types",

175 ("primitives", "Primitive types",

test/pkg005/expectednew file+1

@@ -0,0 +1 @@

1+Can't build an executable: No main module given

test/pkg005/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+### Test: Build IPKG, executable without main.

3+${IDRIS:-idris} $@ --build test.ipkg

test/pkg005/test.ipkgnew file+3

@@ -0,0 +1,3 @@

1+package test

2+

3+executable = test

test/pkg006/expectednew file+1

@@ -0,0 +1 @@

1+Can't start REPL: no main module given

test/pkg006/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+### Test: Launch REPL, IPKG executable without main.

3+${IDRIS:-idris} $@ --repl test.ipkg

test/pkg006/test.ipkgnew file+3

@@ -0,0 +1,3 @@

1+package test

2+

3+executable = test