@@ -403,7 +403,7 @@ buildSCG (_, n) = do
403403 case lookupCtxt Nothing n (idris_callgraph ist) of
404404 [cg] -> case lookupDef Nothing n (tt_ctxt ist) of
405405 [CaseOp _ _ _ _ _ args sc _ _] ->
406− do logLvl 5 $ "Building SCG for " ++ show n ++ " from\n"
406+ do logLvl 3 $ "Building SCG for " ++ show n ++ " from\n"
407407 ++ show sc
408408 let newscg = buildSCG' ist sc args
409409 logLvl 5 $ show newscg
@@ -498,8 +498,9 @@ checkSizeChange n = do
498498 ist <- get
499499 case lookupCtxt Nothing n (idris_callgraph ist) of
500500 [cg] -> do let ms = mkMultiPaths ist [] (scg cg)
501− logLvl 6 ("Multipath for " ++ show n ++ ":\n" ++
501+ logLvl 5 ("Multipath for " ++ show n ++ ":\n" ++
502502 "from " ++ show (scg cg) ++ "\n" ++
503+ show (length ms) ++ "\n" ++
503504 showSep "\n" (map show ms))
504505 logLvl 6 (show cg)
505506 -- every multipath must have an infinitely descending
@@ -507,7 +508,8 @@ checkSizeChange n = do
507508 -- also need to checks functions called are all total
508509 -- (Unchecked is okay as we'll spot problems here)
509510 let tot = map (checkMP ist (length (argsdef cg))) ms
510− logLvl 3 $ "Paths for " ++ show n ++ " yield " ++ (show tot)
511+ logLvl 4 $ "Generated " ++ show (length tot) ++ " paths"
512+ logLvl 6 $ "Paths for " ++ show n ++ " yield " ++ (show tot)
511513 return (noPartial tot)
512514 [] -> do logLvl 5 $ "No paths for " ++ show n
513515 return Unchecked