From ee9989ba094078e15e602c8235fe57d0ebd39bfa Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Thu, 29 Apr 2021 23:56:46 +0100 Subject: [PATCH] Reduce logging overhead Checking the log categories isn't cheap because it involves parsing a string. So, record whether we've ever set a log level. If we haven't, there's no point in checking the string. This reduces overhead and saves a few seconds in typechecking the Idris code base - also means we don't have to worry so much about adding more logging if we feel we need it! --- src/Core/Context.idr | 6 ++++-- src/Core/Context/Log.idr | 12 ++++++------ src/Core/Normalise.idr | 36 ++++++++++++++++++++++-------------- src/Core/Options.idr | 4 +++- src/Core/Options/Log.idr | 14 ++++++++------ src/Core/UnifyState.idr | 8 +++++--- src/Idris/SetOptions.idr | 3 ++- src/TTImp/TTImp.idr | 4 ++-- 8 files changed, 52 insertions(+), 35 deletions(-) diff --git a/src/Core/Context.idr b/src/Core/Context.idr index ffbf89b91..15dc9d931 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -2479,8 +2479,10 @@ addLogLevel : {auto c : Ref Ctxt Defs} -> addLogLevel lvl = do defs <- get Ctxt case lvl of - Nothing => put Ctxt (record { options->session->logLevel = defaultLogLevel } defs) - Just l => put Ctxt (record { options->session->logLevel $= insertLogLevel l } defs) + Nothing => put Ctxt (record { options->session->logEnabled = True, + options->session->logLevel = defaultLogLevel } defs) + Just l => put Ctxt (record { options->session->logEnabled = True, + options->session->logLevel $= insertLogLevel l } defs) export withLogLevel : {auto c : Ref Ctxt Defs} -> diff --git a/src/Core/Context/Log.idr b/src/Core/Context/Log.idr index 7585179e3..7edf0b0ba 100644 --- a/src/Core/Context/Log.idr +++ b/src/Core/Context/Log.idr @@ -16,8 +16,8 @@ logTerm : {vars : _} -> String -> Nat -> Lazy String -> Term vars -> Core () logTerm str n msg tm = do opts <- getSession - let lvl = mkLogLevel str n - if keepLog lvl (logLevel opts) + let lvl = mkLogLevel (logEnabled opts) str n + if keepLog lvl (logEnabled opts) (logLevel opts) then do tm' <- toFullNames tm coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg ++ ": " ++ show tm' @@ -27,7 +27,7 @@ log' : {auto c : Ref Ctxt Defs} -> LogLevel -> Lazy String -> Core () log' lvl msg = do opts <- getSession - if keepLog lvl (logLevel opts) + if keepLog lvl (logEnabled opts) (logLevel opts) then coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg else pure () @@ -37,7 +37,7 @@ export log : {auto c : Ref Ctxt Defs} -> String -> Nat -> Lazy String -> Core () log str n msg - = do let lvl = mkLogLevel str n + = do let lvl = mkLogLevel (logEnabled !getSession) str n log' lvl msg export @@ -45,8 +45,8 @@ logC : {auto c : Ref Ctxt Defs} -> String -> Nat -> Core String -> Core () logC str n cmsg = do opts <- getSession - let lvl = mkLogLevel str n - if keepLog lvl (logLevel opts) + let lvl = mkLogLevel (logEnabled opts) str n + if keepLog lvl (logEnabled opts) (logLevel opts) then do msg <- cmsg coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg else pure () diff --git a/src/Core/Normalise.idr b/src/Core/Normalise.idr index 3faf8bb25..53d9252da 100644 --- a/src/Core/Normalise.idr +++ b/src/Core/Normalise.idr @@ -219,6 +219,9 @@ parameters (defs : Defs, topopts : EvalOpts) = evalRef env True fc Func (Resolved i) (map (EmptyFC,) args ++ stk) (NApp fc (NMeta nm i args) stk) + -- The commented out logging here might still be useful one day, but + -- evalRef is used a lot and even these tiny checks turn out to be + -- worth skipping if we can evalRef : {auto c : Ref Ctxt Defs} -> {free : _} -> Env Term free -> @@ -243,12 +246,16 @@ parameters (defs : Defs, topopts : EvalOpts) Just res <- lookupCtxtExact n (gamma defs) | Nothing => pure def let redok1 = evalAll topopts - let redok2 = reducibleInAny (currentNS defs :: nestedNS defs) +-- let redok2 = reducibleInAny (currentNS defs :: nestedNS defs) +-- (fullname res) +-- (visibility res) + -- want to shortcut that second check, if we're evaluating + -- everything, so don't let bind unless we need that log! + let redok = redok1 || reducibleInAny (currentNS defs :: nestedNS defs) (fullname res) (visibility res) - let redok = redok1 || redok2 - unless redok2 $ logC "eval.stuck" 5 $ do n' <- toFullNames n - pure $ "Stuck function: " ++ show n' +-- unless redok2 $ logC "eval.stuck" 5 $ do n' <- toFullNames n +-- pure $ "Stuck function: " ++ show n' if redok then do Just opts' <- useMeta (noCycles res) fc n defs topopts @@ -1171,8 +1178,8 @@ logNF : {vars : _} -> String -> Nat -> Lazy String -> Env Term vars -> NF vars -> Core () logNF str n msg env tmnf = do opts <- getSession - let lvl = mkLogLevel str n - when (keepLog lvl (logLevel opts)) $ + let lvl = mkLogLevel (logEnabled opts) str n + when (keepLog lvl (logEnabled opts) (logLevel opts)) $ do defs <- get Ctxt tm <- quote defs env tmnf tm' <- toFullNames tm @@ -1187,7 +1194,7 @@ logTermNF' : {vars : _} -> LogLevel -> Lazy String -> Env Term vars -> Term vars -> Core () logTermNF' lvl msg env tm = do opts <- getSession - when (keepLog lvl (logLevel opts)) $ + when (keepLog lvl (logEnabled opts) (logLevel opts)) $ do defs <- get Ctxt tmnf <- normaliseHoles defs env tm tm' <- toFullNames tmnf @@ -1199,7 +1206,7 @@ logTermNF : {vars : _} -> {auto c : Ref Ctxt Defs} -> String -> Nat -> Lazy String -> Env Term vars -> Term vars -> Core () logTermNF str n msg env tm - = do let lvl = mkLogLevel str n + = do let lvl = mkLogLevel (logEnabled !getSession) str n logTermNF' lvl msg env tm export @@ -1208,8 +1215,8 @@ logGlue : {vars : _} -> String -> Nat -> Lazy String -> Env Term vars -> Glued vars -> Core () logGlue str n msg env gtm = do opts <- getSession - let lvl = mkLogLevel str n - when (keepLog lvl (logLevel opts)) $ + let lvl = mkLogLevel (logEnabled opts) str n + when (keepLog lvl (logEnabled opts) (logLevel opts)) $ do defs <- get Ctxt tm <- getTerm gtm tm' <- toFullNames tm @@ -1222,8 +1229,8 @@ logGlueNF : {vars : _} -> String -> Nat -> Lazy String -> Env Term vars -> Glued vars -> Core () logGlueNF str n msg env gtm = do opts <- getSession - let lvl = mkLogLevel str n - when (keepLog lvl (logLevel opts)) $ + let lvl = mkLogLevel (logEnabled opts) str n + when (keepLog lvl (logEnabled opts) (logLevel opts)) $ do defs <- get Ctxt tm <- getTerm gtm tmnf <- normaliseHoles defs env tm @@ -1237,13 +1244,14 @@ logEnv : {vars : _} -> String -> Nat -> String -> Env Term vars -> Core () logEnv str n msg env = do opts <- getSession - when (keepLog lvl (logLevel opts)) $ do + when (logEnabled opts && + keepLog lvl (logEnabled opts) (logLevel opts)) $ do coreLift (putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg) dumpEnv env where lvl : LogLevel - lvl = mkLogLevel str n + lvl = mkLogLevel True str n dumpEnv : {vs : List Name} -> Env Term vs -> Core () dumpEnv [] = pure () diff --git a/src/Core/Options.idr b/src/Core/Options.idr index 65e3f3582..f6d9d01d7 100644 --- a/src/Core/Options.idr +++ b/src/Core/Options.idr @@ -141,6 +141,8 @@ record Session where findipkg : Bool codegen : CG directives : List String + logEnabled : Bool -- do we check logging flags at all? This is 'False' until + -- any logging is enabled. logLevel : LogLevels logTimings : Bool ignoreMissingPkg : Bool -- fail silently on missing packages. This is because @@ -197,7 +199,7 @@ defaultPPrint = MkPPOpts False True False export defaultSession : Session -defaultSession = MkSessionOpts False False False Chez [] defaultLogLevel +defaultSession = MkSessionOpts False False False Chez [] False defaultLogLevel False False False Nothing Nothing Nothing Nothing False diff --git a/src/Core/Options/Log.idr b/src/Core/Options/Log.idr index 2094303e1..23f9018bb 100644 --- a/src/Core/Options/Log.idr +++ b/src/Core/Options/Log.idr @@ -50,9 +50,10 @@ mkLogLevel' ps n = MkLogLevel (maybe [] forget ps) n ||| list. This bypasses the fact that the function `split` returns a non-empty ||| list no matter what. export -mkLogLevel : String -> Nat -> LogLevel -mkLogLevel "" = mkLogLevel' Nothing -mkLogLevel ps = mkLogLevel' (Just (split (== '.') ps)) +mkLogLevel : Bool -> String -> Nat -> LogLevel +mkLogLevel False _ = mkLogLevel' Nothing +mkLogLevel _ "" = mkLogLevel' Nothing +mkLogLevel _ ps = mkLogLevel' (Just (split (== '.') ps)) ||| The unsafe constructor should only be used in places where the topic has already ||| been appropriately processed. @@ -98,7 +99,7 @@ parseLogLevel str = do ns = tail nns in case ns of [] => pure (MkLogLevel [], n) - [ns] => pure (mkLogLevel n, ns) + [ns] => pure (mkLogLevel True n, ns) _ => Nothing lvl <- parsePositive n pure $ c (fromInteger lvl) @@ -127,8 +128,9 @@ insertLogLevel (MkLogLevel ps n) = insert ps n ||| We keep a log if there is a prefix of its path associated to a larger number ||| in the LogLevels. export -keepLog : LogLevel -> LogLevels -> Bool -keepLog (MkLogLevel path n) levels = go path levels where +keepLog : LogLevel -> Bool -> LogLevels -> Bool +keepLog (MkLogLevel _ Z) _ _ = True +keepLog (MkLogLevel path n) enabled levels = enabled && go path levels where go : List String -> StringTrie Nat -> Bool go path (MkStringTrie current) = here || there where diff --git a/src/Core/UnifyState.idr b/src/Core/UnifyState.idr index 6ccf9204f..3e95525ec 100644 --- a/src/Core/UnifyState.idr +++ b/src/Core/UnifyState.idr @@ -663,7 +663,8 @@ dumpHole' : {auto u : Ref UST UState} -> dumpHole' lvl hole = do ust <- get UST defs <- get Ctxt - when (keepLog lvl (logLevel $ session $ options defs)) $ do + sopts <- getSession + when (keepLog lvl (logEnabled sopts) (logLevel sopts)) $ do defs <- get Ctxt case !(lookupCtxtExact (Resolved hole) (gamma defs)) of Nothing => pure () @@ -723,8 +724,9 @@ dumpConstraints : {auto u : Ref UST UState} -> dumpConstraints str n all = do ust <- get UST defs <- get Ctxt - let lvl = mkLogLevel str n - when (keepLog lvl (logLevel $ session $ options defs)) $ + sopts <- getSession + let lvl = mkLogLevel (logEnabled sopts) str n + when (keepLog lvl (logEnabled sopts) (logLevel sopts)) $ do let hs = toList (guesses ust) ++ toList (if all then holes ust else currentHoles ust) case hs of diff --git a/src/Idris/SetOptions.idr b/src/Idris/SetOptions.idr index 924003966..7bd4294a5 100644 --- a/src/Idris/SetOptions.idr +++ b/src/Idris/SetOptions.idr @@ -202,7 +202,8 @@ preOptions (DumpVMCode f :: opts) = do setSession (record { dumpvmcode = Just f } !getSession) preOptions opts preOptions (Logging n :: opts) - = do setSession (record { logLevel $= insertLogLevel n } !getSession) + = do setSession (record { logEnabled = True, + logLevel $= insertLogLevel n } !getSession) preOptions opts preOptions (ConsoleWidth n :: opts) = do setConsoleWidth n diff --git a/src/TTImp/TTImp.idr b/src/TTImp/TTImp.idr index 11855d49e..129c64333 100644 --- a/src/TTImp/TTImp.idr +++ b/src/TTImp/TTImp.idr @@ -1165,8 +1165,8 @@ logRaw : {auto c : Ref Ctxt Defs} -> String -> Nat -> Lazy String -> RawImp -> Core () logRaw str n msg tm = do opts <- getSession - let lvl = mkLogLevel str n - if keepLog lvl (logLevel opts) + let lvl = mkLogLevel (logEnabled opts) str n + if keepLog lvl (logEnabled opts) (logLevel opts) then do coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg ++ ": " ++ show tm else pure ()