From 5b5a6b9a38c2b89a1d4467d1549ca02405766ed8 Mon Sep 17 00:00:00 2001 From: Jan de Muijnck-Hughes Date: Fri, 7 Aug 2020 13:26:44 +0100 Subject: [PATCH] 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. --- src/Idris/Driver.idr | 4 ++-- src/Idris/ProcessIdr.idr | 10 +++++----- src/Idris/REPL.idr | 2 +- 3 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/Idris/Driver.idr b/src/Idris/Driver.idr index 2a9093794..420af50e8 100644 --- a/src/Idris/Driver.idr +++ b/src/Idris/Driver.idr @@ -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 diff --git a/src/Idris/ProcessIdr.idr b/src/Idris/ProcessIdr.idr index 0e38e007c..0e5878448 100644 --- a/src/Idris/ProcessIdr.idr +++ b/src/Idris/ProcessIdr.idr @@ -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 diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index db38ecead..4c975fd1a 100644 --- a/src/Idris/REPL.idr +++ b/src/Idris/REPL.idr @@ -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