8d07967 · Idris-dev · git.iko.soy

idris.cabal+4

compare with master

unifiedsplit

@@ -444,6 +444,10 @@ Extra-source-files:

444 test/totality006/run

445 test/totality006/*.idr

446 test/totality006/expected

447+ test/totality007/run

448+ test/totality007/*.ipkg

449+ test/totality007/src/*.idr

450+ test/totality007/expected

447

451

448 test/tutorial001/run

452 test/tutorial001/run

449 test/tutorial001/*.idr

453 test/tutorial001/*.idr

src/Idris/REPL.hs+7−2

@@ -1218,13 +1218,18 @@ replSettings hFile = setComplete replCompletion $ defaultSettings {

1218 historyFile = hFile

1219 }

1220

1221−-- invoke as if from command line

1221+-- | Invoke as if from command line. It is an error if there are unresolved totality problems.

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

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

1223+idris opts = do res <- runErrorT $ execStateT totalMain idrisInit

1224 case res of

1225 Left err -> do putStrLn $ pshow idrisInit err

1226 return Nothing

1227 Right ist -> return (Just ist)

1228+ where totalMain = do idrisMain opts

1229+ ist <- getIState

1230+ case idris_totcheckfail ist of

1231+ ((fc, msg):_) -> ierror . At fc . Msg $ "Could not build: "++ msg

1232+ [] -> return ()

1228

1233

1229

1234

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

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

test/totality007/expectednew file+3

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

1+Type checking ./Totality.idr

2+Totality.idr:4:1:Totality.foo is not total as there are missing cases

3+Totality.idr:4:1:Could not build: Totality.foo is not total as there are missing cases

test/totality007/runnew file+3

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

1+#!/usr/bin/env bash

2+idris $@ --build totality.ipkg

3+rm -f src/*.ibc

test/totality007/src/Totality.idrnew file+4

@@ -0,0 +1,4 @@

1+module Totality

2+

3+total foo : Nat -> Nat

4+foo Z = Z

test/totality007/totality.ipkgnew file+7

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

1+package totality

2+

3+-- totality007

4+-- Test that the package builder doesn't allow totality errors in a build

5+opts = ""

6+sourcedir = src

7+modules = Totality