Merge pull request #1355 from edwinb/profileflag

Add --profile flag

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:
 

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.

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

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)

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

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

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]

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} ->

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 ()

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} ->

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

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