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

@@ -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} ->

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 ()

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 ()

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
 

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

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

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

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 ()