Makes timing output more intuative to read.

The timings flag (`--timing`) displays various timing information during the entire compilation process.
This is useful when performing adhoc profiling of the compiler.
However, the information is a mixture of timestamps and relative progress.
The information is inherently nested, and such nesting is not immediatly clear in the output.
This can be confusing.

This minor changes nests the timing information on output so that when aligned one can see the timestamps at the highest level, and progress during the elaboration stage.
This commit is contained in:
Jan de Muijnck-Hughes 2020-08-07 13:26:44 +01:00
parent 3d53c2874b
commit 5b5a6b9a38
3 changed files with 8 additions and 8 deletions

View File

@ -175,11 +175,11 @@ stMain cgs opts
else pure fname
setMainFile fname
result <- case fname of
Nothing => logTime "Loading prelude" $ do
Nothing => logTime "+ Loading prelude" $ do
when (not $ noprelude session) $
readPrelude True
pure Done
Just f => logTime "Loading main file" $ do
Just f => logTime "+ Loading main file" $ do
res <- loadMainFile f
displayErrors res
pure res

View File

@ -267,7 +267,7 @@ processMod srcf ttcf msg sourcecode
pure Nothing
else -- needs rebuilding
do iputStrLn msg
Right mod <- logTime ("Parsing " ++ srcf) $
Right mod <- logTime ("++ Parsing " ++ srcf) $
pure (runParser (isLitFile srcf) sourcecode (do p <- prog srcf; eoi; pure p))
| Left err => pure (Just [ParseFail (getParseErrorLoc srcf err) err])
initHash
@ -287,7 +287,7 @@ processMod srcf ttcf msg sourcecode
-- a phase before this which builds the dependency graph
-- (also that we only build child dependencies if rebuilding
-- changes the interface - will need to store a hash in .ttc!)
logTime "Reading imports" $
logTime "++ Reading imports" $
traverse_ (readImport False) imps
-- Before we process the source, make sure the "hide_everywhere"
@ -295,11 +295,11 @@ processMod srcf ttcf msg sourcecode
-- defs <- get Ctxt
-- traverse (\x => setVisibility emptyFC x Private) (hiddenNames defs)
setNS ns
errs <- logTime "Processing decls" $
errs <- logTime "++ Processing decls" $
processDecls (decls mod)
-- coreLift $ gc
logTime "Compile defs" $ compileAndInlineAll
logTime "++ Compile defs" $ compileAndInlineAll
-- Save the import hashes for the imports we just read.
-- If they haven't changed next time, and the source
@ -323,7 +323,7 @@ process buildmsg file
= do Right res <- coreLift (readFile file)
| Left err => pure [FileErr file err]
catch (do ttcf <- getTTCFileName file "ttc"
Just errs <- logTime ("Elaborating " ++ file) $
Just errs <- logTime ("+ Elaborating " ++ file) $
processMod file ttcf buildmsg res
| Nothing => pure [] -- skipped it
if isNil errs

View File

@ -597,7 +597,7 @@ loadMainFile f
Right res <- coreLift (readFile f)
| Left err => do setSource ""
pure (ErrorLoadingFile f err)
errs <- logTime "Build deps" $ buildDeps f
errs <- logTime "+ Build deps" $ buildDeps f
updateErrorLine errs
setSource res
resetProofState