idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-07-07 09:46:22 +03:00
Code Issues Projects Releases Wiki Activity

[ cleanup ] --timing levels

Browse Source
This commit is contained in:
Guillaume Allais 2022-04-13 10:17:47 +01:00 committed by G. Allais
parent f5400537bd
commit 43c5b5263c
20 changed files with 62 additions and 56 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
idris2.ipkg
View File

@ -4,6 +4,9 @@ depends = network
sourcedir = "src"
-- Set if you want the build to output timing data
-- opts = "--timing 1"
-- Set if you want the executable to generate profiling data
-- (Currently supported by Racket and Chez back ends, others ignore it)
-- opts = "--profile"

24
src/Compiler/Common.idr
View File

@ -103,7 +103,7 @@ compile {c} cg tm out
let outputDir = outputDirWithDefault d
ensureDirectoryExists tmpDir
ensureDirectoryExists outputDir
logTime "+ Code generation overall" $
logTime 1 "Code generation overall" $
compileExpr cg c tmpDir outputDir tm out
||| execute
@ -279,7 +279,7 @@ getCompileData doLazyAnnots phase_in tm_in
arr <- coreLift $ newArray asize
defs <- get Ctxt
logTime "++ Get names" $ getAllDesc (natHackNames' ++ noMangleNames ++ keys ns) arr defs
logTime 2 "Get names" $ getAllDesc (natHackNames' ++ noMangleNames ++ keys ns) arr defs
let entries = catMaybes !(coreLift (toList arr))
let allNs = map (Resolved . fst) entries
@ -294,20 +294,20 @@ getCompileData doLazyAnnots phase_in tm_in
log "compile.execute" 40 $
"Kept: " ++ concat (intersperse ", " $ map show rcns)
logTime "++ Merge lambda" $ traverse_ mergeLamDef rcns
logTime "++ Fix arity" $ traverse_ fixArityDef rcns
logTime 2 "Merge lambda" $ traverse_ mergeLamDef rcns
logTime 2 "Fix arity" $ traverse_ fixArityDef rcns
compiledtm <- fixArityExp !(compileExp tm)
(cseDefs, csetm) <- logTime "++ CSE" $ cse rcns compiledtm
(cseDefs, csetm) <- logTime 2 "CSE" $ cse rcns compiledtm
namedDefs <- logTime "++ Forget names" $
namedDefs <- logTime 2 "Forget names" $
traverse getNamedDef cseDefs
let mainname = MN "__mainExpression" 0
(liftedtm, ldefs) <- liftBody {doLazyAnnots} mainname csetm
lifted_in <- if phase >= Lifted
then logTime "++ Lambda lift" $
then logTime 2 "Lambda lift" $
traverse (lambdaLift doLazyAnnots) cseDefs
else pure []
@ -315,10 +315,10 @@ getCompileData doLazyAnnots phase_in tm_in
ldefs ++ concat lifted_in
anf <- if phase >= ANF
then logTime "++ Get ANF" $ traverse (\ (n, d) => pure (n, !(toANF d))) lifted
then logTime 2 "Get ANF" $ traverse (\ (n, d) => pure (n, !(toANF d))) lifted
else pure []
vmcode <- if phase >= VMCode
then logTime "++ Get VM Code" $ pure (allDefs anf)
then logTime 2 "Get VM Code" $ pure (allDefs anf)
else pure []
defs <- get Ctxt
@ -373,15 +373,15 @@ getIncCompileData doLazyAnnots phase
namedDefs <- traverse getNamedDef cseDefs
lifted_in <- if phase >= Lifted
then logTime "++ Lambda lift" $
then logTime 2 "Lambda lift" $
traverse (lambdaLift doLazyAnnots) cseDefs
else pure []
let lifted = concat lifted_in
anf <- if phase >= ANF
then logTime "++ Get ANF" $ traverse (\ (n, d) => pure (n, !(toANF d))) lifted
then logTime 2 "Get ANF" $ traverse (\ (n, d) => pure (n, !(toANF d))) lifted
else pure []
vmcode <- if phase >= VMCode
then logTime "++ Get VM Code" $ pure (allDefs anf)
then logTime 2 "Get VM Code" $ pure (allDefs anf)
else pure []
pure (MkCompileData (CErased emptyFC) namedDefs lifted anf vmcode)

2
src/Compiler/Scheme/Chez.idr
View File

@ -549,7 +549,7 @@ compileExprWhole makeitso c tmpDir outputDir tm outfile
chez <- coreLift $ findChez
let prof = profile !getSession
compileToSS c (makeitso && prof) appDirGen tm outSsAbs
logTime "++ Make SO" $ when makeitso $
logTime 2 "Make SO" $ when makeitso $
compileToSO prof chez appDirGen outSsAbs
let outShRel = outputDir </> outfile
if isWindows

2
src/Compiler/Scheme/ChezSep.idr
View File

@ -276,7 +276,7 @@ compileExpr makeitso c tmpDir outputDir tm outfile = do
(supportChanged, chezLibs) <- compileToSS c chez appDirRel tm
-- compile the code
logTime "++ Make SO" $ when makeitso $ do
logTime 2 "Make SO" $ when makeitso $ do
-- compile the support code
when supportChanged $ do
log "compiler.scheme.chez" 3 $ "Compiling support"

2
src/Compiler/Scheme/Racket.idr
View File

@ -442,7 +442,7 @@ compileExpr mkexec c tmpDir outputDir tm outfile
racket <- coreLift findRacket
ok <- the (Core Int) $ if mkexec
then logTime "+ Build racket" $
then logTime 1 "Build racket" $
coreLift $
system (raco ++ " -o " ++ outBinAbs ++ " " ++ outRktAbs)
else pure 0

4
src/Core/Context.idr
View File

@ -2378,8 +2378,8 @@ withLogLevel l comp = do
pure r
export
setLogTimings : {auto c : Ref Ctxt Defs} -> Bool -> Core ()
setLogTimings b = update Ctxt { options->session->logTimings := b }
setLogTimings : {auto c : Ref Ctxt Defs} -> Nat -> Core ()
setLogTimings n = update Ctxt { options->session->logTimings := Just n }
export
setDebugElabCheck : {auto c : Ref Ctxt Defs} -> Bool -> Core ()

15
src/Core/Context/Log.idr
View File

@ -3,6 +3,7 @@ module Core.Context.Log
import Core.Context
import Core.Options
import Data.String
import Libraries.Data.StringMap
import System.Clock
@ -126,8 +127,8 @@ logTimeOver nsecs str act
export
logTimeWhen : {auto c : Ref Ctxt Defs} ->
Bool -> Lazy String -> Core a -> Core a
logTimeWhen p str act
Bool -> Nat -> Lazy String -> Core a -> Core a
logTimeWhen p lvl str act
= if p
then do clock <- coreLift (clockTime Process)
let t = seconds clock * nano + nanoseconds clock
@ -136,7 +137,9 @@ logTimeWhen p str act
let t' = seconds clock * nano + nanoseconds clock
let time = t' - t
assert_total $ -- We're not dividing by 0
coreLift $ putStrLn $ "TIMING " ++ str ++ ": " ++
coreLift $ do
let header = "TIMING " ++ replicate lvl '+' ++ ifThenElse (0 < lvl) " " ""
putStrLn $ header ++ str ++ ": " ++
show (time `div` nano) ++ "." ++
addZeros (unpack (show ((time `mod` nano) `div` micro))) ++
"s"
@ -204,7 +207,7 @@ showTimeRecord
export
logTime : {auto c : Ref Ctxt Defs} ->
Lazy String -> Core a -> Core a
logTime str act
Nat -> Lazy String -> Core a -> Core a
logTime lvl str act
= do opts <- getSession
logTimeWhen (logTimings opts) str act
logTimeWhen (maybe False (lvl <=) (logTimings opts)) lvl str act

4
src/Core/Options.idr
View File

@ -157,7 +157,7 @@ record Session where
logEnabled : Bool -- do we check logging flags at all? This is 'False' until
-- any logging is enabled.
logLevel : LogLevels
logTimings : Bool
logTimings : Maybe Nat -- log level, higher means more details
debugElabCheck : Bool -- do conversion check to verify results of elaborator
dumpcases : Maybe String -- file to output compiled case trees
dumplifted : Maybe String -- file to output lambda lifted definitions
@ -227,7 +227,7 @@ defaultPPrint = MkPPOpts False True False
export
defaultSession : Session
defaultSession = MkSessionOpts False CoveringOnly False False Chez [] 1000 False False
defaultLogLevel False False Nothing Nothing
defaultLogLevel Nothing False Nothing Nothing
Nothing Nothing False 1 False True
False [] False False

2
src/Core/SchemeEval/Evaluate.idr
View File

@ -64,7 +64,7 @@ seval : {auto c : Ref Ctxt Defs} ->
seval mode env tm
= do -- Check the evaluator is initialised. This will fail if the backend
-- doesn't support scheme evaluation.
True <- logTimeWhen False "Scheme eval" initialiseSchemeEval
True <- logTimeWhen False 0 "Scheme eval" initialiseSchemeEval
| False => throw (InternalError "Loading scheme support failed")
-- make sure all the names in the term are compiled

4
src/Idris/CommandLine.idr
View File

@ -132,7 +132,7 @@ data CLOpt
RunREPL String |
IgnoreMissingIPKG |
FindIPKG |
Timing |
Timing (Maybe Nat) |
DebugElabCheck |
AltErrorCount Nat |
||| Treat warnings as errors
@ -303,7 +303,7 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly]
optSeparator,
MkOpt ["--client"] [Required "REPL command"] (\f => [RunREPL f])
(Just "Run a REPL command then quit immediately"),
MkOpt ["--timing"] [] [Timing]
MkOpt ["--timing"] [AutoNat "level"] (\ n => [Timing n])
(Just "Display timing logs"),
optSeparator,

4
src/Idris/Driver.idr
View File

@ -183,11 +183,11 @@ stMain cgs opts
else pure fname
setMainFile fname
result <- case fname of
Nothing => logTime "+ Loading prelude" $ do
Nothing => logTime 1 "Loading prelude" $ do
when (not $ noprelude session) $
readPrelude True
pure Done
Just f => logTime "+ Loading main file" $ do
Just f => logTime 1 "Loading main file" $ do
res <- loadMainFile f
displayErrors res
pure res

2
src/Idris/Package.idr
View File

@ -757,7 +757,7 @@ partitionOpts opts = foldr pOptUpdate (MkPFR [] [] False) opts
optType (Package cmd f) = PPackage cmd f
optType Quiet = POpt
optType Verbose = POpt
optType Timing = POpt
optType (Timing l) = POpt
optType (Logging l) = POpt
optType CaseTreeHeuristics = POpt
optType (DumpCases f) = POpt

12
src/Idris/ProcessIdr.idr
View File

@ -80,7 +80,7 @@ processDecls decls
= do xs <- concat <$> traverse processDecl decls
Nothing <- checkDelayedHoles
| Just err => pure (if null xs then [err] else xs)
errs <- logTime ("+++ Totality check overall") getTotalityErrors
errs <- logTime 3 ("Totality check overall") getTotalityErrors
pure (xs ++ errs)
readModule : {auto c : Ref Ctxt Defs} ->
@ -332,7 +332,7 @@ processMod sourceFileName ttcFileName msg sourcecode origin
else -- needs rebuilding
do iputStrLn msg
Right (ws, MkState decor hnames, mod) <-
logTime ("++ Parsing " ++ sourceFileName) $
logTime 2 ("Parsing " ++ sourceFileName) $
pure $ runParser (PhysicalIdrSrc origin)
(isLitFile sourceFileName)
sourcecode
@ -364,7 +364,7 @@ processMod sourceFileName ttcFileName msg sourcecode origin
-- a phase before this which builds the dependency graph
-- (also that we only build child dependencies if rebuilding
-- changes the interface - will need to store a hash in .ttc!)
logTime "++ Reading imports" $
logTime 2 "Reading imports" $
traverse_ (readImport False) imports
-- Before we process the source, make sure the "hide_everywhere"
@ -372,12 +372,12 @@ processMod sourceFileName ttcFileName msg sourcecode origin
-- defs <- get Ctxt
-- traverse (\x => setVisibility emptyFC x Private) (hiddenNames defs)
setNS (miAsNamespace ns)
errs <- logTime "++ Processing decls" $
errs <- logTime 2 "Processing decls" $
processDecls (decls mod)
-- coreLift $ gc
when (isNil errs) $
logTime "++ Compile defs" $ compileAndInlineAll
logTime 2 "Compile defs" $ compileAndInlineAll
-- Save the import hashes for the imports we just read.
-- If they haven't changed next time, and the source
@ -403,7 +403,7 @@ process msgPrefix buildMsg sourceFileName ident
= do Right res <- coreLift (readFile sourceFileName)
| Left err => pure [FileErr sourceFileName err]
catch (do ttcFileName <- getTTCFileName sourceFileName "ttc"
Just errs <- logTime ("+ Elaborating " ++ sourceFileName) $
Just errs <- logTime 1 ("Elaborating " ++ sourceFileName) $
processMod sourceFileName ttcFileName
(msgPrefix <++> pretty "Building" <++> buildMsg)
res ident

10
src/Idris/REPL.idr
View File

@ -609,7 +609,7 @@ execExp ctm
do iputStrLn (reflow "No such code generator available")
pure CompilationFailed
tm_erased <- prepareExp ctm
logTimeWhen !getEvalTiming "Execution" $
logTimeWhen !getEvalTiming 0 "Execution" $
execute cg tm_erased
pure $ Executed ctm
@ -663,7 +663,7 @@ loadMainFile f
Right res <- coreLift (readFile f)
| Left err => do setSource ""
pure (ErrorLoadingFile f err)
errs <- logTime "+ Build deps" $ buildDeps f
errs <- logTime 1 "Build deps" $ buildDeps f
updateErrorLine errs
setSource res
resetProofState
@ -752,13 +752,13 @@ process (Eval itm)
Execute => do ignore (execExp itm); pure (Executed itm)
Scheme =>
do (tm `WithType` ty) <- inferAndElab InExpr itm
qtm <- logTimeWhen !getEvalTiming "Evaluation" $
qtm <- logTimeWhen !getEvalTiming 0 "Evaluation" $
(do nf <- snfAll [] tm
quote [] nf)
itm <- logTimeWhen False "resugar" $ resugar [] qtm
itm <- logTimeWhen False 0 "Resugar" $ resugar [] qtm
pure (Evaluated itm Nothing)
_ =>
do (ntm `WithType` ty) <- logTimeWhen !getEvalTiming "Evaluation" $
do (ntm `WithType` ty) <- logTimeWhen !getEvalTiming 0 "Evaluation" $
inferAndNormalize emode itm
itm <- resugar [] ntm
defs <- get Ctxt

4
src/Idris/SetOptions.idr
View File

@ -347,8 +347,8 @@ preOptions (Directory d :: opts)
preOptions (ListPackages :: opts)
= do listPackages
pure False
preOptions (Timing :: opts)
= do setLogTimings True
preOptions (Timing tm :: opts)
= do setLogTimings (fromMaybe 10 tm)
preOptions opts
preOptions (DebugElabCheck :: opts)
= do setDebugElabCheck True

4
src/TTImp/ProcessDecls.idr
View File

@ -192,7 +192,7 @@ processTTImpFile : {auto c : Ref Ctxt Defs} ->
String -> Core Bool
processTTImpFile fname
= do modIdent <- ctxtPathToNS fname
Right (ws, decor, tti) <- logTime "Parsing" $
Right (ws, decor, tti) <- logTime 0 "Parsing" $
coreLift $ parseFile fname (PhysicalIdrSrc modIdent)
(do decls <- prog (PhysicalIdrSrc modIdent)
eoi
@ -200,7 +200,7 @@ processTTImpFile fname
| Left err => do coreLift (putStrLn (show err))
pure False
traverse_ recordWarning ws
logTime "Elaboration" $
logTime 0 "Elaboration" $
catch (do ignore $ processTTImpDecls (MkNested []) [] tti
Nothing <- checkDelayedHoles
| Just err => throw err

2
src/TTImp/ProcessDecls/Totality.idr
View File

@ -41,7 +41,7 @@ checkTotalityOK n
checkTotality : FC -> Core (Maybe Error)
checkTotality fc
= do ignore $ logTime ("+++ Checking Termination " ++ show n) (checkTotal fc n)
= do ignore $ logTime 3 ("Checking Termination " ++ show n) (checkTotal fc n)
-- ^ checked lazily, so better calculate here
t <- getTotality fc n
err <- checkCovering fc (isCovering t)

8
src/TTImp/ProcessDef.idr
View File

@ -491,7 +491,7 @@ checkClause {vars} mult vis totreq hashit n opts nest env (PatClause fc lhs_in r
log "declare.def.clause" 5 $ "Checking RHS " ++ show rhs
logEnv "declare.def.clause" 5 "In env" env'
rhstm <- logTime ("+++ Check RHS " ++ show fc) $
rhstm <- logTime 3 ("Check RHS " ++ show fc) $
wrapErrorC opts (InRHS fc !(getFullName (Resolved n))) $
checkTermSub n rhsMode opts nest' env' env sub' rhs (gnf env' lhsty')
clearHoleLHS
@ -997,7 +997,7 @@ processDef opts nest env fc n_in cs_in
let pats = map toPats (rights cs)
(cargs ** (tree_ct, unreachable)) <-
logTime ("+++ Building compile time case tree for " ++ show n) $
logTime 3 ("Building compile time case tree for " ++ show n) $
getPMDef fc (CompileTime mult) n ty (rights cs)
traverse_ warnUnreachable unreachable
@ -1031,7 +1031,7 @@ processDef opts nest env fc n_in cs_in
update Ctxt { toCompileCase $= (n ::) }
atotal <- toResolvedNames (NS builtinNS (UN $ Basic "assert_total"))
logTime ("+++ Building size change graphs " ++ show n) $
logTime 3 ("Building size change graphs " ++ show n) $
when (not (InCase `elem` opts)) $
do calcRefs False atotal (Resolved nidx)
sc <- calculateSizeChange fc n
@ -1040,7 +1040,7 @@ processDef opts nest env fc n_in cs_in
md <- get MD -- don't need the metadata collected on the coverage check
cov <- logTime ("+++ Checking Coverage " ++ show n) $ checkCoverage nidx ty mult cs
cov <- logTime 3 ("Checking Coverage " ++ show n) $ checkCoverage nidx ty mult cs
setCovering fc n cov
put MD md

8
src/Yaffle/Main.idr
View File

@ -24,9 +24,9 @@ import System
usage : String
usage = "Usage: yaffle <input file> [--timing]"
processArgs : List String -> Core Bool
processArgs [] = pure False
processArgs ["--timing"] = pure True
processArgs : List String -> Core (Maybe Nat)
processArgs [] = pure Nothing
processArgs ["--timing"] = pure (Just 10)
processArgs _
= coreLift $ do ignore $ putStrLn usage
exitWith (ExitFailure 1)
@ -46,7 +46,7 @@ yaffleMain sourceFileName args
u <- newRef UST initUState
s <- newRef Syn initSyntax
o <- newRef ROpts (defaultOpts (Just sourceFileName) (REPL ErrorLvl) [])
setLogTimings t
whenJust t $ setLogTimings
addPrimitives
case extension sourceFileName of
Just "ttc" => do coreLift_ $ putStrLn "Processing as TTC"

2
src/Yaffle/REPL.idr
View File

@ -90,7 +90,7 @@ process (GenerateDef line name)
case !(lookupDefExact n' (gamma defs)) of
Just None =>
catch
(do ((fc, cs) :: _) <- logTime "Generation" $
(do ((fc, cs) :: _) <- logTime 0 "Generation" $
makeDefN (\p, n => onLine line p) 1 n'
| _ => coreLift_ (putStrLn "Failed")
coreLift_ $ putStrLn (show cs))