From 7f7b11ed54b7fc0bf8d12a10807d8b1986cd67a0 Mon Sep 17 00:00:00 2001
From: Edwin Brady <ecb10@st-andrews.ac.uk>
Date: Thu, 29 Apr 2021 23:11:38 +0100
Subject: [PATCH 1/3] Use transforms for fastPack/fastUnpack

We've had these for a while, used for interface specialisation, but
they're not yet used anywhere else or properly documented. We should
document them soon, but for now, it's a useful performance boost to
always use the fast versions of pack/unpack/concat at runtime.

Also moves a couple to the prelude, to ensure that the fast versions are
defined in the same place as the 'normal' version so that the
transformation will always fire (that is, no need to import Data.String
for the transformation to work).
---
 libs/base/Data/String.idr         | 21 ++-------------------
 libs/prelude/Prelude/Types.idr    | 27 +++++++++++++++++++++++++++
 src/Core/Normalise.idr            | 15 ++++++++++-----
 tests/idris2/coverage015/expected |  6 +++---
 4 files changed, 42 insertions(+), 27 deletions(-)

diff --git a/libs/base/Data/String.idr b/libs/base/Data/String.idr
index aad51da11..0e35332c4 100644
--- a/libs/base/Data/String.idr
+++ b/libs/base/Data/String.idr
@@ -18,25 +18,6 @@ partial
 foldl1 : (a -> a -> a) -> List a -> a
 foldl1 f (x::xs) = foldl f x xs
 
--- This function runs fast when compiled but won't compute at compile time.
--- If you need to unpack strings at compile time, use Prelude.unpack.
-%foreign
-  "scheme:string-unpack"
-  "javascript:lambda:(str)=>__prim_js2idris_array(Array.from(str))"
-export
-fastUnpack : String -> List Char
-
--- This works quickly because when string-concat builds the result, it allocates
--- enough room in advance so there's only one allocation, rather than lots!
---
--- Like fastUnpack, this function won't reduce at compile time.
--- If you need to concatenate strings at compile time, use Prelude.concat.
-%foreign
-  "scheme:string-concat"
-  "javascript:lambda:(xs)=>''.concat(...__prim_idris2js_array(xs))"
-export
-fastConcat : List String -> String
-
 -- This uses fastConcat internally so it won't compute at compile time.
 export
 fastUnlines : List String -> String
@@ -132,6 +113,8 @@ export
 unlines : List String -> String
 unlines = pack . unlines' . map unpack
 
+%transform "fastUnlines" unlines = fastUnlines
+
 ||| A view checking whether a string is empty
 ||| and, if not, returning its head and tail
 public export
diff --git a/libs/prelude/Prelude/Types.idr b/libs/prelude/Prelude/Types.idr
index 56823219e..2b22acfa7 100644
--- a/libs/prelude/Prelude/Types.idr
+++ b/libs/prelude/Prelude/Types.idr
@@ -412,6 +412,19 @@ Traversable List where
   traverse f [] = pure []
   traverse f (x::xs) = pure (::) <*> (f x) <*> (traverse f xs)
 
+-- This works quickly because when string-concat builds the result, it allocates
+-- enough room in advance so there's only one allocation, rather than lots!
+--
+-- Like fastUnpack, this function won't reduce at compile time.
+-- If you need to concatenate strings at compile time, use Prelude.concat.
+%foreign
+  "scheme:string-concat"
+  "javascript:lambda:(xs)=>''.concat(...__prim_idris2js_array(xs))"
+export
+fastConcat : List String -> String
+
+%transform "fastConcat" concat {t = List} {a = String} = fastConcat
+
 ||| Check if something is a member of a list using the default Boolean equality.
 public export
 elem : Eq a => a -> List a -> Bool
@@ -537,6 +550,9 @@ pack (x :: xs) = strCons x (pack xs)
 export
 fastPack : List Char -> String
 
+-- always use 'fastPack' at run time
+%transform "fastPack" pack = fastPack
+
 ||| Turns a string into a list of characters.
 |||
 ||| ```idris example
@@ -552,6 +568,17 @@ unpack str = unpack' (prim__cast_IntegerInt (natToInteger (length str)) - 1) str
              then acc
              else assert_total $ unpack' (pos - 1) str (assert_total (prim__strIndex str pos)::acc)
 
+-- This function runs fast when compiled but won't compute at compile time.
+-- If you need to unpack strings at compile time, use Prelude.unpack.
+%foreign
+  "scheme:string-unpack"
+  "javascript:lambda:(str)=>__prim_js2idris_array(Array.from(str))"
+export
+fastUnpack : String -> List Char
+
+-- always use 'fastPack' at run time
+%transform "fastUnpack" unpack = fastUnpack
+
 public export
 Semigroup String where
   (<+>) = (++)
diff --git a/src/Core/Normalise.idr b/src/Core/Normalise.idr
index 6c5c89b9e..3faf8bb25 100644
--- a/src/Core/Normalise.idr
+++ b/src/Core/Normalise.idr
@@ -226,16 +226,20 @@ parameters (defs : Defs, topopts : EvalOpts)
               FC -> NameType -> Name -> Stack free -> (def : Lazy (NF free)) ->
               Core (NF free)
     evalRef env meta fc (DataCon tag arity) fn stk def
-        = do logC "eval.ref.data" 50 $ pure $ "Found data constructor: " ++ show !(toFullNames fn)
+        = do -- logC "eval.ref.data" 50 $ do fn' <- toFullNames fn -- Can't use ! here, it gets lifted too far
+             --                             pure $ "Found data constructor: " ++ show fn'
              pure $ NDCon fc fn tag arity stk
     evalRef env meta fc (TyCon tag arity) fn stk def
-        = do logC "eval.ref.type" 50 $ pure $ "Found type constructor: " ++ show !(toFullNames fn)
+        = do -- logC "eval.ref.type" 50 $ do fn' <- toFullNames fn
+             --                             pure $ "Found type constructor: " ++ show fn'
              pure $ ntCon fc fn tag arity stk
     evalRef env meta fc Bound fn stk def
-        = do logC "eval.ref.bound" 50 $ pure $ "Found bound variable: " ++ show !(toFullNames fn)
+        = do -- logC "eval.ref.bound" 50 $ do fn' <- toFullNames fn
+             --                              pure $ "Found bound variable: " ++ show fn'
              pure def
     evalRef env meta fc nt@Func n stk def
-        = do logC "eval.ref.func" 50 $ pure $ "Found function: " ++ show !(toFullNames n)
+        = do -- logC "eval.ref.func" 50 $ do n' <- toFullNames n
+             --                             pure $ "Found function: " ++ show n'
              Just res <- lookupCtxtExact n (gamma defs)
                   | Nothing => pure def
              let redok1 = evalAll topopts
@@ -243,7 +247,8 @@ parameters (defs : Defs, topopts : EvalOpts)
                                          (fullname res)
                                          (visibility res)
              let redok = redok1 || redok2
-             unless redok2 $ logC "eval.stuck" 5 $ pure $ "Stuck function: " ++ show !(toFullNames 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
diff --git a/tests/idris2/coverage015/expected b/tests/idris2/coverage015/expected
index 744935e3b..76d4b644e 100644
--- a/tests/idris2/coverage015/expected
+++ b/tests/idris2/coverage015/expected
@@ -1,11 +1,11 @@
 1/1: Building Issue1169 (Issue1169.idr)
-LOG coverage.missing:50: Getting constructors for: $resolved1926 [2 closures]
+LOG coverage.missing:50: Getting constructors for: $resolved1928 [2 closures]
 LOG coverage.missing:20: Getting constructors for: (Builtin.Pair String Builtin.Unit)
 LOG coverage.missing:50: Looking for missing alts at type String
-LOG coverage.missing:50: Getting constructors for: $resolved1923 [0 closures]
+LOG coverage.missing:50: Getting constructors for: $resolved1925 [0 closures]
 LOG coverage.missing:20: Getting constructors for: Builtin.Unit
 LOG coverage.missing:20: (Builtin.MkPair {e:0} {e:1} {e:2} {e:3})
-LOG coverage.empty:10: Checking type: TyCon 100 0 params: [] constructors: [$resolved1927] mutual with: [] detaggable by: Just []
+LOG coverage.empty:10: Checking type: TyCon 100 0 params: [] constructors: [$resolved1929] mutual with: [] detaggable by: Just []
 LOG coverage:5: Checking coverage for: (Main.test (Builtin.MkPair String Builtin.Unit {_:368} {_:369}))
 LOG coverage:10: (raw term: (Main.test (Builtin.MkPair String Builtin.Unit {_:368} {_:369})))
 LOG coverage:5: Erased to: (Main.test (Builtin.MkPair [__] [__] {_:368} {_:369}))

From ee9989ba094078e15e602c8235fe57d0ebd39bfa Mon Sep 17 00:00:00 2001
From: Edwin Brady <ecb10@st-andrews.ac.uk>
Date: Thu, 29 Apr 2021 23:56:46 +0100
Subject: [PATCH 2/3] 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 ()

From 3bd1ad222eb7d448a46f4b6d1a102c5e64ca4f23 Mon Sep 17 00:00:00 2001
From: Edwin Brady <ecb10@st-andrews.ac.uk>
Date: Fri, 30 Apr 2021 16:49:23 +0100
Subject: [PATCH 3/3] Replace an old log

This comes up in a test, and I don't think it affects evaluation
performance while typechecking, since we compute 'redok2' there.
---
 src/Core/Normalise.idr | 14 ++++++--------
 1 file changed, 6 insertions(+), 8 deletions(-)

diff --git a/src/Core/Normalise.idr b/src/Core/Normalise.idr
index 53d9252da..80bae451d 100644
--- a/src/Core/Normalise.idr
+++ b/src/Core/Normalise.idr
@@ -246,16 +246,14 @@ 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)
---                                          (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)
+             let redok2 = reducibleInAny (currentNS defs :: nestedNS defs)
                                          (fullname res)
                                          (visibility res)
---              unless redok2 $ logC "eval.stuck" 5 $ do n' <- toFullNames n
---                                                       pure $ "Stuck function: " ++ show n'
+             -- want to shortcut that second check, if we're evaluating
+             -- everything, so don't let bind unless we need that log!
+             let redok = redok1 || redok2
+             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