git.iko.soy/Idris-dev
on master help sign in
Reduce logging at level 1
63cfb38Edwin Brady
src/Idris/Elab/Clause.hs+1−1
compare with master
unifiedsplit
@@ -836,7 +836,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
836
836
837 let rhs' = rhsElab
837 let rhs' = rhsElab
838
838
839− when (not (null defer)) $ logElab 1 $ "DEFERRED " ++
839+ when (not (null defer)) $ logElab 2 $ "DEFERRED " ++
840 show (map (\ (n, (_,_,t,_)) -> (n, t)) defer)
840 show (map (\ (n, (_,_,t,_)) -> (n, t)) defer)
841
841
842 -- If there's holes, set the metavariables as undefinable
842 -- If there's holes, set the metavariables as undefinable
src/Idris/IBC.hs+12−12
@@ -223,7 +223,7 @@ writeArchive fp i = do let a = L.foldl (\x y -> addEntryToArchive y x) emptyArch
223writeIBC :: FilePath -> FilePath -> Idris ()
223writeIBC :: FilePath -> FilePath -> Idris ()
224writeIBC src f
224writeIBC src f
225 = do
225 = do
226− logIBC 1 $ "Writing IBC for: " ++ show f
226+ logIBC 2 $ "Writing IBC for: " ++ show f
227 iReport 2 $ "Writing IBC for: " ++ show f
227 iReport 2 $ "Writing IBC for: " ++ show f
228 i <- getIState
228 i <- getIState
229-- case (Data.List.map fst (idris_metavars i)) \\ primDefs of
229-- case (Data.List.map fst (idris_metavars i)) \\ primDefs of
@@ -233,8 +233,8 @@ writeIBC src f
233 ibcf <- mkIBC (ibc_write i) (initIBC { sourcefile = src })
233 ibcf <- mkIBC (ibc_write i) (initIBC { sourcefile = src })
234 idrisCatch (do runIO $ createDirectoryIfMissing True (dropFileName f)
234 idrisCatch (do runIO $ createDirectoryIfMissing True (dropFileName f)
235 writeArchive f ibcf
235 writeArchive f ibcf
236− logIBC 1 "Written")
236+ logIBC 2 "Written")
237− (\c -> do logIBC 1 $ "Failed " ++ pshow i c)
237+ (\c -> do logIBC 2 $ "Failed " ++ pshow i c)
238 return ()
238 return ()
239
239
240-- | Write a package index containing all the imports in the current
240-- | Write a package index containing all the imports in the current
@@ -244,14 +244,14 @@ writePkgIndex :: FilePath -> Idris ()
244writePkgIndex f
244writePkgIndex f
245 = do i <- getIState
245 = do i <- getIState
246 let imps = map (\ (x, y) -> (True, x)) $ idris_imported i
246 let imps = map (\ (x, y) -> (True, x)) $ idris_imported i
247− logIBC 1 $ "Writing package index " ++ show f ++ " including\n" ++
247+ logIBC 2 $ "Writing package index " ++ show f ++ " including\n" ++
248 show (map snd imps)
248 show (map snd imps)
249 resetNameIdx
249 resetNameIdx
250 let ibcf = initIBC { ibc_imports = imps }
250 let ibcf = initIBC { ibc_imports = imps }
251 idrisCatch (do runIO $ createDirectoryIfMissing True (dropFileName f)
251 idrisCatch (do runIO $ createDirectoryIfMissing True (dropFileName f)
252 writeArchive f ibcf
252 writeArchive f ibcf
253− logIBC 1 "Written")
253+ logIBC 2 "Written")
254− (\c -> do logIBC 1 $ "Failed " ++ pshow i c)
254+ (\c -> do logIBC 2 $ "Failed " ++ pshow i c)
255 return ()
255 return ()
256
256
257mkIBC :: [IBCWrite] -> IBCFile -> Idris IBCFile
257mkIBC :: [IBCWrite] -> IBCFile -> Idris IBCFile
@@ -369,7 +369,7 @@ process :: Bool -- ^ Reexporting
369process reexp phase archive fn = do
369process reexp phase archive fn = do
370 ver <- getEntry 0 "ver" archive
370 ver <- getEntry 0 "ver" archive
371 when (ver /= ibcVersion) $ do
371 when (ver /= ibcVersion) $ do
372− logIBC 1 "ibc out of date"
372+ logIBC 2 "ibc out of date"
373 let e = if ver < ibcVersion
373 let e = if ver < ibcVersion
374 then "an earlier" else "a later"
374 then "an earlier" else "a later"
375 ldir <- runIO $ getIdrisLibDir
375 ldir <- runIO $ getIdrisLibDir
@@ -524,10 +524,10 @@ processImports reexp phase ar = do
524 p -> p
524 p -> p
525 case fp of
525 case fp of
526 LIDR fn -> do
526 LIDR fn -> do
527− logIBC 1 $ "Failed at " ++ fn
527+ logIBC 2 $ "Failed at " ++ fn
528 ifail "Must be an ibc"
528 ifail "Must be an ibc"
529 IDR fn -> do
529 IDR fn -> do
530− logIBC 1 $ "Failed at " ++ fn
530+ logIBC 2 $ "Failed at " ++ fn
531 ifail "Must be an ibc"
531 ifail "Must be an ibc"
532 IBC fn src -> loadIBC (reexp && re) phase' fn) fs
532 IBC fn src -> loadIBC (reexp && re) phase' fn) fs
533
533
@@ -650,7 +650,7 @@ processDefs ar = do
650 case d' of
650 case d' of
651 TyDecl _ _ -> return ()
651 TyDecl _ _ -> return ()
652 _ -> do
652 _ -> do
653− logIBC 1 $ "SOLVING " ++ show n
653+ logIBC 2 $ "SOLVING " ++ show n
654 solveDeferred emptyFC n
654 solveDeferred emptyFC n
655 updateIState (\i -> i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })) ds
655 updateIState (\i -> i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })) ds
656 where
656 where
@@ -749,9 +749,9 @@ processAccess reexp phase ar = do
749
749
750 if (not reexp)
750 if (not reexp)
751 then do
751 then do
752− logIBC 1 $ "Not exporting " ++ show n
752+ logIBC 2 $ "Not exporting " ++ show n
753 setAccessibility n Hidden
753 setAccessibility n Hidden
754− else logIBC 1 $ "Exporting " ++ show n
754+ else logIBC 2 $ "Exporting " ++ show n
755 -- Everything should be available at the REPL from
755 -- Everything should be available at the REPL from
756 -- things imported publicly
756 -- things imported publicly
757 when (phase == IBC_REPL True) $ setAccessibility n Public) ds
757 when (phase == IBC_REPL True) $ setAccessibility n Public) ds