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

git.iko.soy/Idris-dev

Better handling of optional main in package files

No default value is provided for main - in case it's missing, the appropriate error message is produced.

commit483fd4f1c9539f32808accf6cb0307658757781f authorBartosz Przygoda <bprzygoda@gmail.com> dateTue 2 Aug 2016, 23:41 (10 years ago) parent46c1cd5

11 files changed+39−11

compare with master

unifiedsplit

idris.cabal+6 src/Idris/Package.hs+13−7 src/Idris/Package/Common.hs+2−2 src/Idris/Package/Parser.hs+1−1 test/TestData.hs+3−1 test/pkg005/expected+1 test/pkg005/run+3 test/pkg005/test.ipkg+3 test/pkg006/expected+1 test/pkg006/run+3 test/pkg006/test.ipkg+3

idris.cabal+6

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

656656 test/pkg004/*.idr

657657 test/pkg004/expected

658658 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

659665

660666 test/proof001/run

661667 test/proof001/*.idr

src/Idris/Package.hs+13−7

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

8282 Left emsg -> do

8383 putStrLn emsg

8484 exitWith (ExitFailure 1)

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

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

8686 case m_ist of

8787 Nothing -> exitWith (ExitFailure 1)

8888 Just ist -> do

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

9191 Just _ -> exitWith (ExitFailure 1)

9292 _ -> return ()

9393 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)

9499

95100-- --------------------------------------------------------- [ Check Packages ]

96101

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

140145 case mergeOptions copts (idris_opts pkgdesc) of

141146 Left emsg -> ifail emsg

142147 Right opts -> do

143− let mod = idris_main pkgdesc

144− let f = toPath (showCG mod)

145148 putIState orig

146149 dir <- runIO getCurrentDirectory

147150 runIO $ setCurrentDirectory $ dir </> sourcedir pkgdesc

148−

149− if (f /= "")

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

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

151+ runMain opts (idris_main pkgdesc)

152152 runIO $ setCurrentDirectory dir

153153

154154 where

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

156156

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+

157163-- --------------------------------------------------------------- [ Cleaning ]

158164

159165-- | Clean Package build files

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

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

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

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

3232 , 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.

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

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

3636 } deriving (Show)

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

3939defaultPkg :: PkgDesc

4040defaultPkg = PkgDesc "" [] Nothing Nothing Nothing Nothing

4141 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 '=';

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

128128 main <- fst <$> iName []

129129 st <- get

130− put (st { idris_main = main })

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

131131

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

133133 src <- fst <$> identifier

test/TestData.hs+3−1

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

167167 [ ( 1, ANY ),

168168 ( 2, ANY ),

169169 ( 3, ANY ),

170− ( 4, ANY )]),

170+ ( 4, ANY ),

171+ ( 5, ANY ),

172+ ( 6, ANY )]),

171173 ("prelude", "Prelude",

172174 [ ( 1, ANY )]),

173175 ("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

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

3+executable = test