0a6fb1f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Don't install packages if there are metavariables

Fixes #756 Also fixes #696 since that was due to package building not propagating errors to the caller!

commit0a6fb1f4f8cfc658497774de77ed1abe187153fb authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 30 Dec 2013, 14:24 (13 years ago) parenta811211

3 files changed+37−13

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+4 src/Idris/REPL.hs+16−9 src/Pkg/Package.hs+17−4

src/Idris/AbsSyntax.hs+4

@@ -337,6 +337,10 @@ solveDeferred n = do i <- getIState

337337 filter (\(n', _) -> n/=n')

338338 (idris_metavars i) }

339339

340+getUndefined :: Idris [Name]

341+getUndefined = do i <- getIState

342+ return (map fst (idris_metavars i) \\ primDefs)

343+

340344ihPrintResult :: Handle -> String -> Idris ()

341345ihPrintResult h s = do i <- getIState

342346 case idris_outputmode i of

src/Idris/REPL.hs+16−9

@@ -1029,11 +1029,12 @@ replSettings hFile = setComplete replCompletion $ defaultSettings {

10291029 }

10301030

10311031-- invoke as if from command line

1032−idris :: [Opt] -> IO ()

1032+idris :: [Opt] -> IO (Maybe IState)

10331033idris opts = do res <- runErrorT $ execStateT (idrisMain opts) idrisInit

10341034 case res of

1035− Left err -> putStrLn $ pshow idrisInit err

1036− Right ist -> return ()

1035+ Left err -> do putStrLn $ pshow idrisInit err

1036+ return Nothing

1037+ Right ist -> return (Just ist)

10371038

10381039

10391040loadInputs :: Handle -> [FilePath] -> Idris ()

@@ -1054,7 +1055,7 @@ loadInputs h inputs

10541055 -- so that they don't interfere with each other when checking

10551056

10561057 let ninputs = zip [1..] inputs

1057− ifiles <- mapM (\(num, input) ->

1058+ ifiles <- mapWhileOK (\(num, input) ->

10581059 do putIState ist

10591060 v <- verbose

10601061 -- when v $ iputStrLn $ "(" ++ show num ++ "/" ++

@@ -1080,7 +1081,7 @@ loadInputs h inputs

10801081 when (not loadCode) $ tryLoad $ nub (concat ifiles)

10811082 _ -> return ()

10821083 putIState inew)

1083− (\e -> case e of

1084+ (\e -> do case e of

10841085 At f _ -> do setErrLine (fc_line f)

10851086 iputStrLn (show e)

10861087 ProgramLineComment -> return () -- fail elsewhere

@@ -1090,14 +1091,20 @@ loadInputs h inputs

10901091 tryLoad :: [IFileType] -> Idris ()

10911092 tryLoad [] = return ()

10921093 tryLoad (f : fs) = do loadFromIFile h f

1093− inew <- getIState

1094− case errLine inew of

1095− Nothing -> tryLoad fs

1096− _ -> return () -- error, stop

1094+ ok <- noErrors

1095+ when ok $ tryLoad fs

10971096

10981097 ibc (IBC _ _) = True

10991098 ibc _ = False

11001099

1100+ -- Like mapM, but give up when there's an error

1101+ mapWhileOK f [] = return []

1102+ mapWhileOK f (x : xs) = do x' <- f x

1103+ ok <- noErrors

1104+ if ok then do xs' <- mapWhileOK f xs

1105+ return (x' : xs')

1106+ else return [x']

1107+

11011108idrisMain :: [Opt] -> Idris ()

11021109idrisMain opts =

11031110 do let inputs = opt getFile opts

src/Pkg/Package.hs+17−4

@@ -39,7 +39,7 @@ buildPkg warnonly (install, fp)

3939 do dir <- getCurrentDirectory

4040 setCurrentDirectory $ dir </> sourcedir pkgdesc

4141 make (makefile pkgdesc)

42− case (execout pkgdesc) of

42+ m_ist <- case (execout pkgdesc) of

4343 Nothing -> buildMods (NoREPL : Verbose : idris_opts pkgdesc)

4444 (modules pkgdesc)

4545 Just o -> do let exec = dir </> o

@@ -47,7 +47,21 @@ buildPkg warnonly (install, fp)

4747 (NoREPL : Verbose : Output exec : idris_opts pkgdesc)

4848 [idris_main pkgdesc]

4949 setCurrentDirectory dir

50− when install $ installPkg pkgdesc

50+ case m_ist of

51+ Nothing -> exitWith (ExitFailure 1)

52+ Just ist -> do

53+ -- Quit with error code if there was a problem

54+ case errLine ist of

55+ Just _ -> exitWith (ExitFailure 1)

56+ _ -> return ()

57+ -- Also give up if there are metavariables to solve

58+ case (map fst (idris_metavars ist) \\ primDefs) of

59+ [] -> when install $ installPkg pkgdesc

60+ ms -> do if install

61+ then putStrLn "Can't install: there are undefined metavariables:"

62+ else putStrLn "There are undefined metavariables:"

63+ putStrLn $ "\t" ++ show ms

64+ exitWith (ExitFailure 1)

5165

5266cleanPkg :: FilePath -> IO ()

5367cleanPkg fp

@@ -69,11 +83,10 @@ installPkg pkgdesc

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

7084 mapM_ (installObj (pkgname pkgdesc)) (objs pkgdesc)

7185

72−buildMods :: [Opt] -> [Name] -> IO ()

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

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

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

7589 idris (map Filename f ++ opts)

76− return ()

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

7891

7992testLib :: Bool -> String -> String -> IO Bool