diff --git a/idris2.ipkg b/idris2.ipkg index ae45fd512..a6f86b44b 100644 --- a/idris2.ipkg +++ b/idris2.ipkg @@ -4,6 +4,9 @@ depends = network sourcedir = "src" +-- Set if you want the build to output timing data +-- opts = "--timing 1" + -- Set if you want the executable to generate profiling data -- (Currently supported by Racket and Chez back ends, others ignore it) -- opts = "--profile" diff --git a/src/Compiler/Common.idr b/src/Compiler/Common.idr index a3b85501d..a38007480 100644 --- a/src/Compiler/Common.idr +++ b/src/Compiler/Common.idr @@ -103,7 +103,7 @@ compile {c} cg tm out let outputDir = outputDirWithDefault d ensureDirectoryExists tmpDir ensureDirectoryExists outputDir - logTime "+ Code generation overall" $ + logTime 1 "Code generation overall" $ compileExpr cg c tmpDir outputDir tm out ||| execute @@ -279,7 +279,7 @@ getCompileData doLazyAnnots phase_in tm_in arr <- coreLift $ newArray asize defs <- get Ctxt - logTime "++ Get names" $ getAllDesc (natHackNames' ++ noMangleNames ++ keys ns) arr defs + logTime 2 "Get names" $ getAllDesc (natHackNames' ++ noMangleNames ++ keys ns) arr defs let entries = catMaybes !(coreLift (toList arr)) let allNs = map (Resolved . fst) entries @@ -294,20 +294,20 @@ getCompileData doLazyAnnots phase_in tm_in log "compile.execute" 40 $ "Kept: " ++ concat (intersperse ", " $ map show rcns) - logTime "++ Merge lambda" $ traverse_ mergeLamDef rcns - logTime "++ Fix arity" $ traverse_ fixArityDef rcns + logTime 2 "Merge lambda" $ traverse_ mergeLamDef rcns + logTime 2 "Fix arity" $ traverse_ fixArityDef rcns compiledtm <- fixArityExp !(compileExp tm) - (cseDefs, csetm) <- logTime "++ CSE" $ cse rcns compiledtm + (cseDefs, csetm) <- logTime 2 "CSE" $ cse rcns compiledtm - namedDefs <- logTime "++ Forget names" $ + namedDefs <- logTime 2 "Forget names" $ traverse getNamedDef cseDefs let mainname = MN "__mainExpression" 0 (liftedtm, ldefs) <- liftBody {doLazyAnnots} mainname csetm lifted_in <- if phase >= Lifted - then logTime "++ Lambda lift" $ + then logTime 2 "Lambda lift" $ traverse (lambdaLift doLazyAnnots) cseDefs else pure [] @@ -315,10 +315,10 @@ getCompileData doLazyAnnots phase_in tm_in ldefs ++ concat lifted_in anf <- if phase >= ANF - then logTime "++ Get ANF" $ traverse (\ (n, d) => pure (n, !(toANF d))) lifted + then logTime 2 "Get ANF" $ traverse (\ (n, d) => pure (n, !(toANF d))) lifted else pure [] vmcode <- if phase >= VMCode - then logTime "++ Get VM Code" $ pure (allDefs anf) + then logTime 2 "Get VM Code" $ pure (allDefs anf) else pure [] defs <- get Ctxt @@ -373,15 +373,15 @@ getIncCompileData doLazyAnnots phase namedDefs <- traverse getNamedDef cseDefs lifted_in <- if phase >= Lifted - then logTime "++ Lambda lift" $ + then logTime 2 "Lambda lift" $ traverse (lambdaLift doLazyAnnots) cseDefs else pure [] let lifted = concat lifted_in anf <- if phase >= ANF - then logTime "++ Get ANF" $ traverse (\ (n, d) => pure (n, !(toANF d))) lifted + then logTime 2 "Get ANF" $ traverse (\ (n, d) => pure (n, !(toANF d))) lifted else pure [] vmcode <- if phase >= VMCode - then logTime "++ Get VM Code" $ pure (allDefs anf) + then logTime 2 "Get VM Code" $ pure (allDefs anf) else pure [] pure (MkCompileData (CErased emptyFC) namedDefs lifted anf vmcode) diff --git a/src/Compiler/Scheme/Chez.idr b/src/Compiler/Scheme/Chez.idr index 45a14fb4f..7fa5a6831 100644 --- a/src/Compiler/Scheme/Chez.idr +++ b/src/Compiler/Scheme/Chez.idr @@ -549,7 +549,7 @@ compileExprWhole makeitso c tmpDir outputDir tm outfile chez <- coreLift $ findChez let prof = profile !getSession compileToSS c (makeitso && prof) appDirGen tm outSsAbs - logTime "++ Make SO" $ when makeitso $ + logTime 2 "Make SO" $ when makeitso $ compileToSO prof chez appDirGen outSsAbs let outShRel = outputDir outfile if isWindows diff --git a/src/Compiler/Scheme/ChezSep.idr b/src/Compiler/Scheme/ChezSep.idr index d251dc887..5f77d342f 100644 --- a/src/Compiler/Scheme/ChezSep.idr +++ b/src/Compiler/Scheme/ChezSep.idr @@ -276,7 +276,7 @@ compileExpr makeitso c tmpDir outputDir tm outfile = do (supportChanged, chezLibs) <- compileToSS c chez appDirRel tm -- compile the code - logTime "++ Make SO" $ when makeitso $ do + logTime 2 "Make SO" $ when makeitso $ do -- compile the support code when supportChanged $ do log "compiler.scheme.chez" 3 $ "Compiling support" diff --git a/src/Compiler/Scheme/Racket.idr b/src/Compiler/Scheme/Racket.idr index e4737340e..f2d9d62c7 100644 --- a/src/Compiler/Scheme/Racket.idr +++ b/src/Compiler/Scheme/Racket.idr @@ -442,7 +442,7 @@ compileExpr mkexec c tmpDir outputDir tm outfile racket <- coreLift findRacket ok <- the (Core Int) $ if mkexec - then logTime "+ Build racket" $ + then logTime 1 "Build racket" $ coreLift $ system (raco ++ " -o " ++ outBinAbs ++ " " ++ outRktAbs) else pure 0 diff --git a/src/Core/Context.idr b/src/Core/Context.idr index bd36aa00a..8599a4410 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -2378,8 +2378,8 @@ withLogLevel l comp = do pure r export -setLogTimings : {auto c : Ref Ctxt Defs} -> Bool -> Core () -setLogTimings b = update Ctxt { options->session->logTimings := b } +setLogTimings : {auto c : Ref Ctxt Defs} -> Nat -> Core () +setLogTimings n = update Ctxt { options->session->logTimings := Just n } export setDebugElabCheck : {auto c : Ref Ctxt Defs} -> Bool -> Core () diff --git a/src/Core/Context/Log.idr b/src/Core/Context/Log.idr index 513275728..d8ddd6747 100644 --- a/src/Core/Context/Log.idr +++ b/src/Core/Context/Log.idr @@ -3,6 +3,7 @@ module Core.Context.Log import Core.Context import Core.Options +import Data.String import Libraries.Data.StringMap import System.Clock @@ -126,8 +127,8 @@ logTimeOver nsecs str act export logTimeWhen : {auto c : Ref Ctxt Defs} -> - Bool -> Lazy String -> Core a -> Core a -logTimeWhen p str act + Bool -> Nat -> Lazy String -> Core a -> Core a +logTimeWhen p lvl str act = if p then do clock <- coreLift (clockTime Process) let t = seconds clock * nano + nanoseconds clock @@ -136,7 +137,9 @@ logTimeWhen p str act let t' = seconds clock * nano + nanoseconds clock let time = t' - t assert_total $ -- We're not dividing by 0 - coreLift $ putStrLn $ "TIMING " ++ str ++ ": " ++ + coreLift $ do + let header = "TIMING " ++ replicate lvl '+' ++ ifThenElse (0 < lvl) " " "" + putStrLn $ header ++ str ++ ": " ++ show (time `div` nano) ++ "." ++ addZeros (unpack (show ((time `mod` nano) `div` micro))) ++ "s" @@ -204,7 +207,7 @@ showTimeRecord export logTime : {auto c : Ref Ctxt Defs} -> - Lazy String -> Core a -> Core a -logTime str act + Nat -> Lazy String -> Core a -> Core a +logTime lvl str act = do opts <- getSession - logTimeWhen (logTimings opts) str act + logTimeWhen (maybe False (lvl <=) (logTimings opts)) lvl str act diff --git a/src/Core/Options.idr b/src/Core/Options.idr index 17981c0e5..e8809670c 100644 --- a/src/Core/Options.idr +++ b/src/Core/Options.idr @@ -157,7 +157,7 @@ record Session where logEnabled : Bool -- do we check logging flags at all? This is 'False' until -- any logging is enabled. logLevel : LogLevels - logTimings : Bool + logTimings : Maybe Nat -- log level, higher means more details debugElabCheck : Bool -- do conversion check to verify results of elaborator dumpcases : Maybe String -- file to output compiled case trees dumplifted : Maybe String -- file to output lambda lifted definitions @@ -227,7 +227,7 @@ defaultPPrint = MkPPOpts False True False export defaultSession : Session defaultSession = MkSessionOpts False CoveringOnly False False Chez [] 1000 False False - defaultLogLevel False False Nothing Nothing + defaultLogLevel Nothing False Nothing Nothing Nothing Nothing False 1 False True False [] False False diff --git a/src/Core/SchemeEval/Evaluate.idr b/src/Core/SchemeEval/Evaluate.idr index 05a39a53b..d940b3740 100644 --- a/src/Core/SchemeEval/Evaluate.idr +++ b/src/Core/SchemeEval/Evaluate.idr @@ -64,7 +64,7 @@ seval : {auto c : Ref Ctxt Defs} -> seval mode env tm = do -- Check the evaluator is initialised. This will fail if the backend -- doesn't support scheme evaluation. - True <- logTimeWhen False "Scheme eval" initialiseSchemeEval + True <- logTimeWhen False 0 "Scheme eval" initialiseSchemeEval | False => throw (InternalError "Loading scheme support failed") -- make sure all the names in the term are compiled diff --git a/src/Idris/CommandLine.idr b/src/Idris/CommandLine.idr index 1f9d12a72..739c6516f 100644 --- a/src/Idris/CommandLine.idr +++ b/src/Idris/CommandLine.idr @@ -132,7 +132,7 @@ data CLOpt RunREPL String | IgnoreMissingIPKG | FindIPKG | - Timing | + Timing (Maybe Nat) | DebugElabCheck | AltErrorCount Nat | ||| Treat warnings as errors @@ -303,7 +303,7 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly] optSeparator, MkOpt ["--client"] [Required "REPL command"] (\f => [RunREPL f]) (Just "Run a REPL command then quit immediately"), - MkOpt ["--timing"] [] [Timing] + MkOpt ["--timing"] [AutoNat "level"] (\ n => [Timing n]) (Just "Display timing logs"), optSeparator, diff --git a/src/Idris/Driver.idr b/src/Idris/Driver.idr index 31bf6cd9f..cf18c8719 100644 --- a/src/Idris/Driver.idr +++ b/src/Idris/Driver.idr @@ -183,11 +183,11 @@ stMain cgs opts else pure fname setMainFile fname result <- case fname of - Nothing => logTime "+ Loading prelude" $ do + Nothing => logTime 1 "Loading prelude" $ do when (not $ noprelude session) $ readPrelude True pure Done - Just f => logTime "+ Loading main file" $ do + Just f => logTime 1 "Loading main file" $ do res <- loadMainFile f displayErrors res pure res diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr index 2a37da050..cecfb7a18 100644 --- a/src/Idris/Package.idr +++ b/src/Idris/Package.idr @@ -757,7 +757,7 @@ partitionOpts opts = foldr pOptUpdate (MkPFR [] [] False) opts optType (Package cmd f) = PPackage cmd f optType Quiet = POpt optType Verbose = POpt - optType Timing = POpt + optType (Timing l) = POpt optType (Logging l) = POpt optType CaseTreeHeuristics = POpt optType (DumpCases f) = POpt diff --git a/src/Idris/ProcessIdr.idr b/src/Idris/ProcessIdr.idr index 99012bba4..342381295 100644 --- a/src/Idris/ProcessIdr.idr +++ b/src/Idris/ProcessIdr.idr @@ -80,7 +80,7 @@ processDecls decls = do xs <- concat <$> traverse processDecl decls Nothing <- checkDelayedHoles | Just err => pure (if null xs then [err] else xs) - errs <- logTime ("+++ Totality check overall") getTotalityErrors + errs <- logTime 3 ("Totality check overall") getTotalityErrors pure (xs ++ errs) readModule : {auto c : Ref Ctxt Defs} -> @@ -332,7 +332,7 @@ processMod sourceFileName ttcFileName msg sourcecode origin else -- needs rebuilding do iputStrLn msg Right (ws, MkState decor hnames, mod) <- - logTime ("++ Parsing " ++ sourceFileName) $ + logTime 2 ("Parsing " ++ sourceFileName) $ pure $ runParser (PhysicalIdrSrc origin) (isLitFile sourceFileName) sourcecode @@ -364,7 +364,7 @@ processMod sourceFileName ttcFileName msg sourcecode origin -- 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 2 "Reading imports" $ traverse_ (readImport False) imports -- Before we process the source, make sure the "hide_everywhere" @@ -372,12 +372,12 @@ processMod sourceFileName ttcFileName msg sourcecode origin -- defs <- get Ctxt -- traverse (\x => setVisibility emptyFC x Private) (hiddenNames defs) setNS (miAsNamespace ns) - errs <- logTime "++ Processing decls" $ + errs <- logTime 2 "Processing decls" $ processDecls (decls mod) -- coreLift $ gc when (isNil errs) $ - logTime "++ Compile defs" $ compileAndInlineAll + logTime 2 "Compile defs" $ compileAndInlineAll -- Save the import hashes for the imports we just read. -- If they haven't changed next time, and the source @@ -403,7 +403,7 @@ process msgPrefix buildMsg sourceFileName ident = do Right res <- coreLift (readFile sourceFileName) | Left err => pure [FileErr sourceFileName err] catch (do ttcFileName <- getTTCFileName sourceFileName "ttc" - Just errs <- logTime ("+ Elaborating " ++ sourceFileName) $ + Just errs <- logTime 1 ("Elaborating " ++ sourceFileName) $ processMod sourceFileName ttcFileName (msgPrefix <++> pretty "Building" <++> buildMsg) res ident diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index 7b620027d..9e0a336c1 100644 --- a/src/Idris/REPL.idr +++ b/src/Idris/REPL.idr @@ -609,7 +609,7 @@ execExp ctm do iputStrLn (reflow "No such code generator available") pure CompilationFailed tm_erased <- prepareExp ctm - logTimeWhen !getEvalTiming "Execution" $ + logTimeWhen !getEvalTiming 0 "Execution" $ execute cg tm_erased pure $ Executed ctm @@ -663,7 +663,7 @@ loadMainFile f Right res <- coreLift (readFile f) | Left err => do setSource "" pure (ErrorLoadingFile f err) - errs <- logTime "+ Build deps" $ buildDeps f + errs <- logTime 1 "Build deps" $ buildDeps f updateErrorLine errs setSource res resetProofState @@ -752,13 +752,13 @@ process (Eval itm) Execute => do ignore (execExp itm); pure (Executed itm) Scheme => do (tm `WithType` ty) <- inferAndElab InExpr itm - qtm <- logTimeWhen !getEvalTiming "Evaluation" $ + qtm <- logTimeWhen !getEvalTiming 0 "Evaluation" $ (do nf <- snfAll [] tm quote [] nf) - itm <- logTimeWhen False "resugar" $ resugar [] qtm + itm <- logTimeWhen False 0 "Resugar" $ resugar [] qtm pure (Evaluated itm Nothing) _ => - do (ntm `WithType` ty) <- logTimeWhen !getEvalTiming "Evaluation" $ + do (ntm `WithType` ty) <- logTimeWhen !getEvalTiming 0 "Evaluation" $ inferAndNormalize emode itm itm <- resugar [] ntm defs <- get Ctxt diff --git a/src/Idris/SetOptions.idr b/src/Idris/SetOptions.idr index d37500ac2..0f26fe480 100644 --- a/src/Idris/SetOptions.idr +++ b/src/Idris/SetOptions.idr @@ -347,8 +347,8 @@ preOptions (Directory d :: opts) preOptions (ListPackages :: opts) = do listPackages pure False -preOptions (Timing :: opts) - = do setLogTimings True +preOptions (Timing tm :: opts) + = do setLogTimings (fromMaybe 10 tm) preOptions opts preOptions (DebugElabCheck :: opts) = do setDebugElabCheck True diff --git a/src/TTImp/ProcessDecls.idr b/src/TTImp/ProcessDecls.idr index 986e84839..da7df11a3 100644 --- a/src/TTImp/ProcessDecls.idr +++ b/src/TTImp/ProcessDecls.idr @@ -192,7 +192,7 @@ processTTImpFile : {auto c : Ref Ctxt Defs} -> String -> Core Bool processTTImpFile fname = do modIdent <- ctxtPathToNS fname - Right (ws, decor, tti) <- logTime "Parsing" $ + Right (ws, decor, tti) <- logTime 0 "Parsing" $ coreLift $ parseFile fname (PhysicalIdrSrc modIdent) (do decls <- prog (PhysicalIdrSrc modIdent) eoi @@ -200,7 +200,7 @@ processTTImpFile fname | Left err => do coreLift (putStrLn (show err)) pure False traverse_ recordWarning ws - logTime "Elaboration" $ + logTime 0 "Elaboration" $ catch (do ignore $ processTTImpDecls (MkNested []) [] tti Nothing <- checkDelayedHoles | Just err => throw err diff --git a/src/TTImp/ProcessDecls/Totality.idr b/src/TTImp/ProcessDecls/Totality.idr index c92763858..6a5c1979b 100644 --- a/src/TTImp/ProcessDecls/Totality.idr +++ b/src/TTImp/ProcessDecls/Totality.idr @@ -41,7 +41,7 @@ checkTotalityOK n checkTotality : FC -> Core (Maybe Error) checkTotality fc - = do ignore $ logTime ("+++ Checking Termination " ++ show n) (checkTotal fc n) + = do ignore $ logTime 3 ("Checking Termination " ++ show n) (checkTotal fc n) -- ^ checked lazily, so better calculate here t <- getTotality fc n err <- checkCovering fc (isCovering t) diff --git a/src/TTImp/ProcessDef.idr b/src/TTImp/ProcessDef.idr index c96959ac8..fb951158d 100644 --- a/src/TTImp/ProcessDef.idr +++ b/src/TTImp/ProcessDef.idr @@ -491,7 +491,7 @@ checkClause {vars} mult vis totreq hashit n opts nest env (PatClause fc lhs_in r log "declare.def.clause" 5 $ "Checking RHS " ++ show rhs logEnv "declare.def.clause" 5 "In env" env' - rhstm <- logTime ("+++ Check RHS " ++ show fc) $ + rhstm <- logTime 3 ("Check RHS " ++ show fc) $ wrapErrorC opts (InRHS fc !(getFullName (Resolved n))) $ checkTermSub n rhsMode opts nest' env' env sub' rhs (gnf env' lhsty') clearHoleLHS @@ -997,7 +997,7 @@ processDef opts nest env fc n_in cs_in let pats = map toPats (rights cs) (cargs ** (tree_ct, unreachable)) <- - logTime ("+++ Building compile time case tree for " ++ show n) $ + logTime 3 ("Building compile time case tree for " ++ show n) $ getPMDef fc (CompileTime mult) n ty (rights cs) traverse_ warnUnreachable unreachable @@ -1031,7 +1031,7 @@ processDef opts nest env fc n_in cs_in update Ctxt { toCompileCase $= (n ::) } atotal <- toResolvedNames (NS builtinNS (UN $ Basic "assert_total")) - logTime ("+++ Building size change graphs " ++ show n) $ + logTime 3 ("Building size change graphs " ++ show n) $ when (not (InCase `elem` opts)) $ do calcRefs False atotal (Resolved nidx) sc <- calculateSizeChange fc n @@ -1040,7 +1040,7 @@ processDef opts nest env fc n_in cs_in md <- get MD -- don't need the metadata collected on the coverage check - cov <- logTime ("+++ Checking Coverage " ++ show n) $ checkCoverage nidx ty mult cs + cov <- logTime 3 ("Checking Coverage " ++ show n) $ checkCoverage nidx ty mult cs setCovering fc n cov put MD md diff --git a/src/Yaffle/Main.idr b/src/Yaffle/Main.idr index 3eec0378e..60800bb22 100644 --- a/src/Yaffle/Main.idr +++ b/src/Yaffle/Main.idr @@ -24,9 +24,9 @@ import System usage : String usage = "Usage: yaffle [--timing]" -processArgs : List String -> Core Bool -processArgs [] = pure False -processArgs ["--timing"] = pure True +processArgs : List String -> Core (Maybe Nat) +processArgs [] = pure Nothing +processArgs ["--timing"] = pure (Just 10) processArgs _ = coreLift $ do ignore $ putStrLn usage exitWith (ExitFailure 1) @@ -46,7 +46,7 @@ yaffleMain sourceFileName args u <- newRef UST initUState s <- newRef Syn initSyntax o <- newRef ROpts (defaultOpts (Just sourceFileName) (REPL ErrorLvl) []) - setLogTimings t + whenJust t $ setLogTimings addPrimitives case extension sourceFileName of Just "ttc" => do coreLift_ $ putStrLn "Processing as TTC" diff --git a/src/Yaffle/REPL.idr b/src/Yaffle/REPL.idr index 82b5a5dba..e6f06415d 100644 --- a/src/Yaffle/REPL.idr +++ b/src/Yaffle/REPL.idr @@ -90,7 +90,7 @@ process (GenerateDef line name) case !(lookupDefExact n' (gamma defs)) of Just None => catch - (do ((fc, cs) :: _) <- logTime "Generation" $ + (do ((fc, cs) :: _) <- logTime 0 "Generation" $ makeDefN (\p, n => onLine line p) 1 n' | _ => coreLift_ (putStrLn "Failed") coreLift_ $ putStrLn (show cs))