From 6d37471cccf2e6d108a6454a0227fb18505f03a2 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Thu, 29 Apr 2021 15:18:59 +0100 Subject: [PATCH] Add --profile flag If set, when compiling this generates an executable which generates profiling data. Currently supported by Racket and Chez, other backends silently ignore it. --- CHANGELOG.md | 2 ++ docs/source/backends/index.rst | 6 ++++++ idris2.ipkg | 4 ++++ src/Compiler/Scheme/Chez.idr | 28 ++++++++++++++++++---------- src/Compiler/Scheme/Racket.idr | 15 ++++++++++----- src/Core/Options.idr | 3 ++- src/Idris/CommandLine.idr | 4 ++++ src/Idris/IDEMode/REPL.idr | 1 + src/Idris/Parser.idr | 2 ++ src/Idris/REPL.idr | 3 +++ src/Idris/SetOptions.idr | 3 +++ src/Idris/Syntax.idr | 3 +++ 12 files changed, 58 insertions(+), 16 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index b8f5b31bd..471e62489 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -24,6 +24,8 @@ Compiler changes: * Racket codegen now always uses `blodwen-sleep` instead of `idris2_sleep` in order to not block the Racket runtime when `sleep` is called. +* Added `--profile` flag, which generates profile data if supported by a back + end. Currently supported by the Chez and Racket back ends. Library changes: diff --git a/docs/source/backends/index.rst b/docs/source/backends/index.rst index 60f2aa8c3..52a899ae4 100644 --- a/docs/source/backends/index.rst +++ b/docs/source/backends/index.rst @@ -48,6 +48,12 @@ This will compile the expression ``Main.main``, generating an executable ``hello`` (with an extension depending on the code generator) in the ``build/exec`` directory. +If the backend supports it, you can generate profiling data by setting +the ``profile`` flag, either by starting Idris with ``--profile``, or +running ``:set profile`` at the REPL. The profile data generated will depend +on the back end you are using. Currently, the Chez and Racket back ends +support generating profile data. + There are five code generators provided in Idris 2, and (later) there will be a system for plugging in new code generators for a variety of targets. The default is to compile via Chez Scheme, with an alternative via Racket or Gambit. diff --git a/idris2.ipkg b/idris2.ipkg index 5014fc72e..82b1a75e5 100644 --- a/idris2.ipkg +++ b/idris2.ipkg @@ -4,5 +4,9 @@ depends = network sourcedir = "src" +-- Set if you want the executable to generate profiling data +-- (Currently supported by Racket and Chez back ends, others ignore it) +-- opts = "--profile" + main = Idris.Main executable = idris2 diff --git a/src/Compiler/Scheme/Chez.idr b/src/Compiler/Scheme/Chez.idr index 1fd82cdad..431ccf289 100644 --- a/src/Compiler/Scheme/Chez.idr +++ b/src/Compiler/Scheme/Chez.idr @@ -78,8 +78,12 @@ schHeader chez libs showSep "\n" (map (\x => "(load-shared-object \"" ++ escapeString x ++ "\")") libs) ++ "\n\n" ++ "(let ()\n" -schFooter : String -schFooter = "(collect 4)\n(blodwen-run-finalisers))\n" +schFooter : Bool -> String +schFooter prof + = "(collect 4)\n(blodwen-run-finalisers)\n" ++ + if prof + then "(profile-dump-html))\n" + else ")\n" showChezChar : Char -> String -> String showChezChar '\\' = ("\\\\" ++) @@ -379,8 +383,8 @@ startChezWinSh chez appdir target = unlines ||| Compile a TT expression to Chez Scheme compileToSS : Ref Ctxt Defs -> - String -> ClosedTerm -> (outfile : String) -> Core () -compileToSS c appdir tm outfile + Bool -> String -> ClosedTerm -> (outfile : String) -> Core () +compileToSS c prof appdir tm outfile = do ds <- getDirectives Chez libs <- findLibs ds traverse_ copyLib libs @@ -402,7 +406,7 @@ compileToSS c appdir tm outfile support ++ extraRuntime ++ code ++ concat (map fst fgndefs) ++ "(collect-request-handler (lambda () (collect) (blodwen-run-finalisers)))\n" ++ - main ++ schFooter + main ++ schFooter prof Right () <- coreLift $ writeFile outfile scm | Left err => throw (FileErr outfile err) coreLift_ $ chmodRaw outfile 0o755 @@ -410,10 +414,13 @@ compileToSS c appdir tm outfile ||| Compile a Chez Scheme source file to an executable, daringly with runtime checks off. compileToSO : {auto c : Ref Ctxt Defs} -> - String -> (appDirRel : String) -> (outSsAbs : String) -> Core () -compileToSO chez appDirRel outSsAbs + Bool -> String -> (appDirRel : String) -> (outSsAbs : String) -> Core () +compileToSO prof chez appDirRel outSsAbs = do let tmpFileAbs = appDirRel "compileChez" - let build = "(parameterize ([optimize-level 3] [compile-file-message #f]) (compile-program " ++ + let build = "(parameterize ([optimize-level 3] " + ++ (if prof then "[compile-profile #t] " + else "") ++ + "[compile-file-message #f]) (compile-program " ++ show outSsAbs ++ "))" Right () <- coreLift $ writeFile tmpFileAbs build | Left err => throw (FileErr tmpFileAbs err) @@ -451,8 +458,9 @@ compileExpr makeitso c tmpDir outputDir tm outfile let outSsAbs = cwd outputDir outSsFile let outSoAbs = cwd outputDir outSoFile chez <- coreLift $ findChez - compileToSS c appDirGen tm outSsAbs - logTime "++ Make SO" $ when makeitso $ compileToSO chez appDirGen outSsAbs + let prof = profile !getSession + compileToSS c (makeitso && prof) appDirGen tm outSsAbs + logTime "++ Make SO" $ when makeitso $ compileToSO prof chez appDirGen outSsAbs let outShRel = outputDir outfile if isWindows then makeShWindows chez outShRel appDirRel (if makeitso then outSoFile else outSsFile) diff --git a/src/Compiler/Scheme/Racket.idr b/src/Compiler/Scheme/Racket.idr index 4cbf62b6b..19d80f1c0 100644 --- a/src/Compiler/Scheme/Racket.idr +++ b/src/Compiler/Scheme/Racket.idr @@ -40,8 +40,8 @@ findRacoExe = do env <- idrisGetEnv "RACKET_RACO" pure $ (fromMaybe "/usr/bin/env raco" env) ++ " exe" -schHeader : String -> String -schHeader libs +schHeader : Bool -> String -> String +schHeader prof libs = "#lang racket/base\n" ++ "; @generated\n" ++ "(require racket/async-channel)\n" ++ -- for asynchronous channels @@ -52,6 +52,7 @@ schHeader libs "(require rnrs/io/ports-6)\n" ++ -- for files "(require srfi/19)\n" ++ -- for file handling and data "(require ffi/unsafe ffi/unsafe/define)\n" ++ -- for calling C + (if prof then "(require profile)\n" else "") ++ "(require racket/flonum)" ++ -- for float-typed transcendental functions libs ++ "(let ()\n" @@ -386,10 +387,14 @@ compileToRKT c appdir tm outfile support <- readDataFile "racket/support.rkt" ds <- getDirectives Racket extraRuntime <- getExtraRuntime ds - let scm = schHeader (concat (map fst fgndefs)) ++ + let prof = profile !getSession + let runmain + = if prof + then "(profile (void " ++ main ++ ") #:order 'self)\n" + else "(void " ++ main ++ ")\n" + let scm = schHeader prof (concat (map fst fgndefs)) ++ support ++ extraRuntime ++ code ++ - "(void " ++ main ++ ")\n" ++ - schFooter + runmain ++ schFooter Right () <- coreLift $ writeFile outfile scm | Left err => throw (FileErr outfile err) coreLift_ $ chmodRaw outfile 0o755 diff --git a/src/Core/Options.idr b/src/Core/Options.idr index 09156e434..65e3f3582 100644 --- a/src/Core/Options.idr +++ b/src/Core/Options.idr @@ -151,6 +151,7 @@ record Session where dumplifted : Maybe String -- file to output lambda lifted definitions dumpanf : Maybe String -- file to output ANF definitions dumpvmcode : Maybe String -- file to output VM code definitions + profile : Bool -- generate profiling information, if supported public export record PPrinter where @@ -198,7 +199,7 @@ export defaultSession : Session defaultSession = MkSessionOpts False False False Chez [] defaultLogLevel False False False Nothing Nothing - Nothing Nothing + Nothing Nothing False export defaultElab : ElabDirectives diff --git a/src/Idris/CommandLine.idr b/src/Idris/CommandLine.idr index 0bcac2089..789e9741d 100644 --- a/src/Idris/CommandLine.idr +++ b/src/Idris/CommandLine.idr @@ -66,6 +66,8 @@ data CLOpt BuildDir String | ||| Set output directory OutputDir String | + ||| Generate profile data when compiling (backend dependent) + Profile | ||| Show the installation prefix ShowPrefix | ||| Display Idris version @@ -191,6 +193,8 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly] (Just $ "Set build directory"), MkOpt ["--output-dir"] [Required "dir"] (\d => [OutputDir d]) (Just $ "Set output directory"), + MkOpt ["--profile"] [] [Profile] + (Just "Generate profile data when compiling, if supported"), optSeparator, MkOpt ["--prefix"] [] [ShowPrefix] diff --git a/src/Idris/IDEMode/REPL.idr b/src/Idris/IDEMode/REPL.idr index 10821263e..170af5ad2 100644 --- a/src/Idris/IDEMode/REPL.idr +++ b/src/Idris/IDEMode/REPL.idr @@ -292,6 +292,7 @@ SExpable REPLOpt where toSExp (EvalMode mod) = SExpList [ SymbolAtom "eval", toSExp mod ] toSExp (Editor editor) = SExpList [ SymbolAtom "editor", toSExp editor ] toSExp (CG str) = SExpList [ SymbolAtom "cg", toSExp str ] + toSExp (Profile p) = SExpList [ SymbolAtom "profile", toSExp p ] displayIDEResult : {auto c : Ref Ctxt Defs} -> diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 71fddd57b..1c41a7d9c 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -1565,6 +1565,8 @@ setOption set pure (ShowNamespace set) <|> do exactIdent "showtypes" pure (ShowTypes set) + <|> do exactIdent "profile" + pure (Profile set) <|> if set then setVarOption else fatalError "Unrecognised option" replCmd : List String -> Rule () diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index 016eca3e3..7b138db27 100644 --- a/src/Idris/REPL.idr +++ b/src/Idris/REPL.idr @@ -185,6 +185,9 @@ setOpt (CG e) case getCG (options defs) e of Just cg => setCG cg Nothing => iputStrLn (reflow "No such code generator available") +setOpt (Profile t) + = do pp <- getSession + setSession (record { profile = t } pp) getOptions : {auto c : Ref Ctxt Defs} -> {auto o : Ref ROpts REPLOpts} -> diff --git a/src/Idris/SetOptions.idr b/src/Idris/SetOptions.idr index 44df641ad..924003966 100644 --- a/src/Idris/SetOptions.idr +++ b/src/Idris/SetOptions.idr @@ -135,6 +135,9 @@ preOptions (IdeModeSocket _ :: opts) preOptions (CheckOnly :: opts) = do setSession (record { nobanner = True } !getSession) preOptions opts +preOptions (Profile :: opts) + = do setSession (record { profile = True } !getSession) + preOptions opts preOptions (Quiet :: opts) = do setOutput (REPL True) preOptions opts diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index d900f5389..58d8a734d 100644 --- a/src/Idris/Syntax.idr +++ b/src/Idris/Syntax.idr @@ -409,6 +409,7 @@ data REPLOpt : Type where EvalMode : REPLEval -> REPLOpt Editor : String -> REPLOpt CG : String -> REPLOpt + Profile : Bool -> REPLOpt export Show REPLOpt where @@ -418,6 +419,7 @@ Show REPLOpt where show (EvalMode mod) = "eval = " ++ show mod show (Editor editor) = "editor = " ++ show editor show (CG str) = "cg = " ++ str + show (Profile p) = "profile = " ++ show p export Pretty REPLOpt where @@ -427,6 +429,7 @@ Pretty REPLOpt where pretty (EvalMode mod) = pretty "eval" <++> equals <++> pretty mod pretty (Editor editor) = pretty "editor" <++> equals <++> pretty editor pretty (CG str) = pretty "cg" <++> equals <++> pretty str + pretty (Profile p) = pretty "profile" <++> equals <++> pretty p public export data EditCmd : Type where