cf61801 · Idris-dev · git.iko.soy

CHANGELOG.md+1−1

compare with master

unifiedsplit

@@ -12,7 +12,7 @@

12

13## Tool Updates

14

15−+ Output from verbose Idris has been updated to more accurately reflect

15++ Idris' logging output has been updated to more accurately reflect

16 its progress through the compiler. Idris, when verbose, will report

17 explicitly: Type Checking; Totality Checking; IBC Generation;

18 Compiling; and Code Generation.

src/IRTS/Compiler.hs+3−4

@@ -52,9 +52,8 @@ import System.Process

52

53-- | Compile to simplified forms and return CodegenInfo

54compile :: Codegen -> FilePath -> Maybe Term -> Idris CodegenInfo

55−compile codegen f mtm

55+compile codegen f mtm = do

56− = do v <- verbose

57− when v $ iputStrLn "Compiling Output."

56+ logCodeGen 1 "Compiling Output."

58 checkMVs -- check for undefined metavariables

57 checkMVs -- check for undefined metavariables

59 checkTotality -- refuse to compile if there are totality problems

58 checkTotality -- refuse to compile if there are totality problems

60 exports <- findExports

59 exports <- findExports

@@ -110,7 +109,7 @@ compile codegen f mtm

110 Just f -> runIO $ writeFile f (dumpDefuns defuns)

109 Just f -> runIO $ writeFile f (dumpDefuns defuns)

111 triple <- Idris.AbsSyntax.targetTriple

110 triple <- Idris.AbsSyntax.targetTriple

112 cpu <- Idris.AbsSyntax.targetCPU

111 cpu <- Idris.AbsSyntax.targetCPU

113− when v $ iputStrLn "Generating Code."

112+ logCodeGen 1 "Generating Code."

114 case checked of

113 case checked of

115 OK c -> do return $ CodegenInfo f outty triple cpu

114 OK c -> do return $ CodegenInfo f outty triple cpu

116 hdrs impdirs objs libs flags

115 hdrs impdirs objs libs flags

src/Idris/IBC.hs+2−2

@@ -220,8 +220,8 @@ writeArchive fp i = do let a = L.foldl (\x y -> addEntryToArchive y x) emptyArch

220

221writeIBC :: FilePath -> FilePath -> Idris ()

222writeIBC src f

223− = do v <- verbose

223+ = do

224− when v $ iputStrLn $ "Writing IBC for: " ++ show f

224+ logIBC 1 $ "Writing IBC for: " ++ show f

225 i <- getIState

226-- case (Data.List.map fst (idris_metavars i)) \\ primDefs of

227-- (_:_) -> ifail "Can't write ibc when there are unsolved metavariables"

src/Idris/Parser.hs+1−1

@@ -1803,7 +1803,7 @@ loadSource lidr f toline

1803 setContext ctxt')

1804 (map snd (idris_totcheck i))

1805 -- build size change graph from simplified definitions

1806− when v $ iputStrLn $ "Totality checking " ++ f

1806+ logLvl 1 $ "Totality checking " ++ f

1807 i <- getIState

1808 mapM_ buildSCG (idris_totcheck i)

1809 mapM_ checkDeclTotality (idris_totcheck i)

test/base001/expected−4

@@ -1,8 +1,4 @@

1Type checking ./base001.idr

2−Totality checking ./base001.idr

3−Writing IBC for: "./base001.ibc"

4−Compiling Output.

5−Generating Code.

6exit1: Executing cmd 'exit 1'

2exit1: Executing cmd 'exit 1'

7exit1: raw exitStatus = 256

3exit1: raw exitStatus = 256

8exit1: WEXITSTATUS(exitStatus) = 1

4exit1: WEXITSTATUS(exitStatus) = 1

test/pkg008/expected+1−7

@@ -1,16 +1,10 @@

1Entering directory `./src'

2Type checking ./NumOps.idr

3−Totality checking ./NumOps.idr

4−Writing IBC for: "./NumOps.ibc"

5Type checking ./Test.idr

3Type checking ./Test.idr

6−Totality checking ./Test.idr

7−Writing IBC for: "./Test.ibc"

8Leaving directory `./src'

4Leaving directory `./src'

9−Entering directory `./src'

10−Compiling Output.

11−Generating Code.

12Test Passed

5Test Passed

13Test Passed

6Test Passed

7+Entering directory `./src'

14Leaving directory `./src'

8Leaving directory `./src'

15Entering directory `./src'

9Entering directory `./src'

16Removed: NumOps.ibc

10Removed: NumOps.ibc