ff2ed8b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #3571 from jfdm/revert-verbosity

Reverted changes to verbosity reporting.

commitff2ed8b51b96aded389fe3decb6758fe917ea978 authorJan de Muijnck-Hughes <jfdm@users.noreply.github.com> dateMon 12 Dec 2016, 11:33 (10 years ago) parentb79bf7b cf61801

6 files changed+8−19

compare with master

unifiedsplit

CHANGELOG.md+1−1 src/IRTS/Compiler.hs+3−4 src/Idris/IBC.hs+2−2 src/Idris/Parser.hs+1−1 test/base001/expected−4 test/pkg008/expected+1−7

CHANGELOG.md+1−1

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

1212

1313## Tool Updates

1414

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

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

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

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

1818 Compiling; and Code Generation.

src/IRTS/Compiler.hs+3−4

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

5252

5353-- | Compile to simplified forms and return CodegenInfo

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

55−compile codegen f mtm

56− = do v <- verbose

57− when v $ iputStrLn "Compiling Output."

55+compile codegen f mtm = do

56+ logCodeGen 1 "Compiling Output."

5857 checkMVs -- check for undefined metavariables

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

6059 exports <- findExports

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

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

111110 triple <- Idris.AbsSyntax.targetTriple

112111 cpu <- Idris.AbsSyntax.targetCPU

113− when v $ iputStrLn "Generating Code."

112+ logCodeGen 1 "Generating Code."

114113 case checked of

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

116115 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

220220

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

222222writeIBC src f

223− = do v <- verbose

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

223+ = do

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

225225 i <- getIState

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

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

src/Idris/Parser.hs+1−1

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

18031803 setContext ctxt')

18041804 (map snd (idris_totcheck i))

18051805 -- build size change graph from simplified definitions

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

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

18071807 i <- getIState

18081808 mapM_ buildSCG (idris_totcheck i)

18091809 mapM_ checkDeclTotality (idris_totcheck i)

test/base001/expected−4

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

11Type checking ./base001.idr

2−Totality checking ./base001.idr

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

4−Compiling Output.

5−Generating Code.

62exit1: Executing cmd 'exit 1'

73exit1: raw exitStatus = 256

84exit1: WEXITSTATUS(exitStatus) = 1

test/pkg008/expected+1−7

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

11Entering directory `./src'

22Type checking ./NumOps.idr

3−Totality checking ./NumOps.idr

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

53Type checking ./Test.idr

6−Totality checking ./Test.idr

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

84Leaving directory `./src'

9−Entering directory `./src'

10−Compiling Output.

11−Generating Code.

125Test Passed

136Test Passed

7+Entering directory `./src'

148Leaving directory `./src'

159Entering directory `./src'

1610Removed: NumOps.ibc