Some fixes in time logging code

src/Core/Context.idr

@@ -753,7 +753,7 @@ record Defs where
   userHoles : NameMap ()
      -- ^ Metavariables the user still has to fill in. In practice, that's
      -- everything with a user accessible name and a definition of Hole
-  timings : StringMap Integer
+  timings : StringMap (Bool, Integer)
      -- ^ record of timings from logTimeRecord
 
 -- Label for context references
@@ -1996,12 +1996,9 @@ logTimeWhen p str act
     addZeros [x,y] = "0" ++ cast x ++ cast y
     addZeros str = pack str
 
--- for ad-hoc profiling, record the time the action takes and add it
--- to the time for the given category
-export
-logTimeRecord : {auto c : Ref Ctxt Defs} ->
-                String -> Core a -> Core a
-logTimeRecord key act
+logTimeRecord' : {auto c : Ref Ctxt Defs} ->
+                 String -> Core a -> Core a
+logTimeRecord' key act
     = do clock <- coreLift clockTime
          let nano = 1000000000
          let t = seconds clock * nano + nanoseconds clock
@@ -2012,10 +2009,26 @@ logTimeRecord key act
          defs <- get Ctxt
          let tot = case lookup key (timings defs) of
                         Nothing => 0
-                        Just t => t
-         put Ctxt (record { timings $= insert key (tot + time) } defs)
+                        Just (_, t) => t
+         put Ctxt (record { timings $= insert key (False, tot + time) } defs)
          pure res
 
+-- for ad-hoc profiling, record the time the action takes and add it
+-- to the time for the given category
+export
+logTimeRecord : {auto c : Ref Ctxt Defs} ->
+                String -> Core a -> Core a
+logTimeRecord key act
+    = do defs <- get Ctxt
+         -- Only record if we're not currently recording that key
+         case lookup key (timings defs) of
+              Just (True, t) => act
+              Just (False, t)
+                => do put Ctxt (record { timings $= insert key (True, t) } defs)
+                      logTimeRecord' key act
+              Nothing
+                => logTimeRecord' key act
+
 export
 showTimeRecord : {auto c : Ref Ctxt Defs} ->
                  Core ()
@@ -2029,8 +2042,8 @@ showTimeRecord
     addZeros [x,y] = "0" ++ cast x ++ cast y
     addZeros str = pack str
 
-    showTimeLog : (String, Integer) -> Core ()
-    showTimeLog (key, time)
+    showTimeLog : (String, (Bool, Integer)) -> Core ()
+    showTimeLog (key, (_, time))
         = do coreLift $ putStr (key ++ ": ")
              let nano = 1000000000
              assert_total $ -- We're not dividing by 0

src/Core/UnifyState.idr

@@ -13,6 +13,7 @@ import Utils.Binary
 
 import Data.IntMap
 import Data.NameMap
+import Data.StringMap
 
 %default covering
 
@@ -469,7 +470,8 @@ tryErrorUnify elab
                    commit
                    pure (Right res))
                (\err => do put UST ust
-                           put Ctxt defs
+                           defs' <- get Ctxt
+                           put Ctxt (record { timings = timings defs' } defs)
                            pure (Left err))
 
 export

src/Idris/Main.idr

@@ -174,6 +174,7 @@ stMain opts
                       -- exit with an error code if there was an error, otherwise
                       -- just exit
                     do ropts <- get ROpts
+                       showTimeRecord
                        case errorLine ropts of
                          Nothing => pure ()
                          Just _ => coreLift $ exit 1

src/TTImp/Elab/Check.idr

@@ -17,6 +17,7 @@ import TTImp.TTImp
 
 import Data.IntMap
 import Data.NameMap
+import Data.StringMap
 
 public export
 data ElabMode = InType | InLHS RigCount | InExpr
@@ -370,7 +371,8 @@ tryError elab
                (\err => do put UST ust
                            put EST est
                            put MD md
-                           put Ctxt defs
+                           defs' <- get Ctxt
+                           put Ctxt (record { timings = timings defs' } defs)
                            pure (Left err))
 
 export

src/TTImp/ProcessType.idr

@@ -135,7 +135,7 @@ processType {vars} eopts nest env fc rig vis opts (MkImpTy tfc n_in ty_raw)
          -- level check so don't set the flag.
          when (not (InCase `elem` eopts)) $ setLinearCheck idx True
 
-         log 1 $ "Setting options for " ++ show n ++ ": " ++ show opts
+         log 2 $ "Setting options for " ++ show n ++ ": " ++ show opts
          traverse (processFnOpt fc (Resolved idx)) opts
 
          -- Add to the interactive editing metadata