280810b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #3551 from jfdm/improv-compiler-progress-reporting

Improve progress reporting.

commit280810b516dd0704e7c3d727aac6b070c9651597 authorJan de Muijnck-Hughes <jfdm@users.noreply.github.com> dateThu 8 Dec 2016, 12:04 (10 years ago) parent4eee260 53c8ca7

7 files changed+29−8

compare with master

unifiedsplit

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

CHANGELOG.md+8

@@ -10,6 +10,14 @@

1010 + `FirstClassReflection`, which must be enabled to define a `%reflection`

1111 function

1212

13+## Tool Updates

14+

15++ Output from verbose Idris 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.

19+

20+

1321## Library Updates

1422

1523+ Terminating programs has been improved with more appropriate

src/IRTS/Compiler.hs+4−2

@@ -53,7 +53,9 @@ import System.Process

5353-- | Compile to simplified forms and return CodegenInfo

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

5555compile codegen f mtm

56− = do checkMVs -- check for undefined metavariables

56+ = do v <- verbose

57+ when v $ iputStrLn "Compiling Output."

58+ checkMVs -- check for undefined metavariables

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

5860 exports <- findExports

5961 let rootNames = case mtm of

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

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

109111 triple <- Idris.AbsSyntax.targetTriple

110112 cpu <- Idris.AbsSyntax.targetCPU

111− logCodeGen 1 "Building output"

113+ when v $ iputStrLn "Generating Code."

112114 case checked of

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

114116 hdrs impdirs objs libs flags

src/Idris/AbsSyntaxTree.hs+1−1

@@ -120,7 +120,7 @@ defaultOpts = IOption { opt_logLevel = 0

120120 , opt_showimp = False

121121 , opt_errContext = False

122122 , opt_repl = True

123− , opt_verbose = True

123+ , opt_verbose = False

124124 , opt_nobanner = False

125125 , opt_quiet = False

126126 , opt_codegen = Via IBCFormat "c"

src/Idris/IBC.hs+3−2

@@ -220,7 +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 logIBC 1 $ "Writing ibc " ++ show f

223+ = do v <- verbose

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

224225 i <- getIState

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

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

@@ -313,7 +314,7 @@ ibc i (IBCCG n) f = case lookupCtxtExact n (idris_callgraph i) of

313314 _ -> ifail "IBC write failed"

314315ibc i (IBCCoercion n) f = return f { ibc_coercions = n : ibc_coercions f }

315316ibc i (IBCAccess n a) f = return f { ibc_access = (n,a) : ibc_access f }

316−ibc i (IBCFlags n) f

317+ibc i (IBCFlags n) f

317318 = case lookupCtxtExact n (idris_flags i) of

318319 Just a -> return f { ibc_flags = (n,a): ibc_flags f }

319320 _ -> ifail "IBC write failed"

src/Idris/Parser.hs+2−2

@@ -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− logLvl 1 "Totality checking"

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

18071807 i <- getIState

18081808 mapM_ buildSCG (idris_totcheck i)

18091809 mapM_ checkDeclTotality (idris_totcheck i)

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

18261826

18271827 logLvl 1 ("Finished " ++ f)

18281828 ibcsd <- valIBCSubDir i

1829− logLvl 1 "Universe checking"

1829+ logLvl 1 $ "Universe checking " ++ f

18301830 iucheck

18311831 let ibc = ibcPathNoFallback ibcsd f

18321832 i <- getIState

test/base001/expected+4

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

11Type checking ./base001.idr

2+Totality checking ./base001.idr

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

4+Compiling Output.

5+Generating Code.

26exit1: Executing cmd 'exit 1'

37exit1: raw exitStatus = 256

48exit1: WEXITSTATUS(exitStatus) = 1

test/pkg008/expected+7−1

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

11Entering directory `./src'

22Type checking ./NumOps.idr

3+Totality checking ./NumOps.idr

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

35Type checking ./Test.idr

6+Totality checking ./Test.idr

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

48Leaving directory `./src'

9+Entering directory `./src'

10+Compiling Output.

11+Generating Code.

512Test Passed

613Test Passed

7−Entering directory `./src'

814Leaving directory `./src'

915Entering directory `./src'

1016Removed: NumOps.ibc