1 /* Title: Pure/Tools/profiling_report.scala |
1 /* Title: Pure/Tools/profiling_report.scala |
2 Author: Makarius |
2 Author: Makarius |
3 |
3 |
4 Report Poly/ML profiling information from log files. |
4 Report Poly/ML profiling information from session build database. |
5 */ |
5 */ |
6 |
6 |
7 package isabelle |
7 package isabelle |
8 |
8 |
9 |
9 |
10 import java.util.Locale |
|
11 |
|
12 |
|
13 object Profiling_Report |
10 object Profiling_Report |
14 { |
11 { |
15 def profiling_report(log_file: Build_Log.Log_File): List[(Long, String)] = |
12 def profiling_report( |
|
13 options: Options, |
|
14 session_name: String, |
|
15 theories: List[String] = Nil, |
|
16 clean_name: Boolean = false, |
|
17 progress: Progress = new Progress): Unit = |
16 { |
18 { |
17 val Line = """^(?:### )?([ 0-9]{10}) (\S+|GARBAGE COLLECTION.*)$""".r |
19 val store = Sessions.store(options) |
18 val Count = """ *(\d+)""".r |
20 val resources = Resources.empty |
19 val clean = """-?\(\d+\).*$""".r |
21 val session = new Session(options, resources) |
20 |
22 |
21 var results = Map.empty[String, Long] |
23 using(store.open_database_context())(db_context => |
22 for (Line(Count(Value.Long(count)), raw_fun) <- log_file.lines) { |
24 { |
23 val fun = clean.replaceAllIn(raw_fun, "") |
25 val result = |
24 results += (fun -> (results.getOrElse(fun, 0L) + count)) |
26 db_context.input_database(session_name)((db, name) => Some(store.read_theories(db, name))) |
25 } |
27 result match { |
26 for ((fun, count) <- results.toList.sortBy(_._2)) yield (count, fun) |
28 case None => error("Missing build database for session " + quote(session_name)) |
|
29 case Some(used_theories) => |
|
30 theories.filterNot(used_theories.toSet) match { |
|
31 case Nil => |
|
32 case bad => error("Unknown theories " + commas_quote(bad)) |
|
33 } |
|
34 val reports = |
|
35 (for { |
|
36 thy <- used_theories.iterator |
|
37 if theories.isEmpty || theories.contains(thy) |
|
38 command <- Build_Job.read_theory(db_context, resources, session_name, thy).iterator |
|
39 snapshot = Document.State.init.snippet(command) |
|
40 rendering = new Rendering(snapshot, options, session) |
|
41 Text.Info(_, Protocol.ML_Profiling(report)) <- |
|
42 rendering.text_messages(Text.Range.full).iterator |
|
43 } yield if (clean_name) report.clean_name else report).toList |
|
44 |
|
45 for (report <- ML_Profiling.account(reports)) progress.echo(report.print) |
|
46 } |
|
47 }) |
27 } |
48 } |
28 |
49 |
29 |
50 |
30 /* Isabelle tool wrapper */ |
51 /* Isabelle tool wrapper */ |
31 |
52 |
32 val isabelle_tool = |
53 val isabelle_tool = |
33 Isabelle_Tool("profiling_report", "report Poly/ML profiling information from log files", |
54 Isabelle_Tool("profiling_report", "report Poly/ML profiling information from log files", |
34 Scala_Project.here, args => |
55 Scala_Project.here, args => |
35 { |
56 { |
|
57 var theories: List[String] = Nil |
|
58 var clean_name = false |
|
59 var options = Options.init() |
|
60 |
36 val getopts = |
61 val getopts = |
37 Getopts(""" |
62 Getopts(""" |
38 Usage: isabelle profiling_report [LOGS ...] |
63 Usage: isabelle profiling_report [OPTIONS] SESSION |
39 |
64 |
40 Report Poly/ML profiling output from log files (potentially compressed). |
65 Options are: |
41 """) |
66 -T NAME restrict to given theories (multiple options possible) |
42 val log_names = getopts(args) |
67 -c clean function names |
43 for (name <- log_names) { |
68 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
44 val log_file = Build_Log.Log_File(Path.explode(name)) |
69 |
45 val results = |
70 Report Poly/ML profiling from the build database of the given session |
46 for ((count, fun) <- profiling_report(log_file)) |
71 (without up-to-date check of sources). |
47 yield |
72 """, |
48 String.format(Locale.ROOT, "%14d %s", |
73 "T:" -> (arg => theories = theories ::: List(arg)), |
49 count.asInstanceOf[AnyRef], fun.asInstanceOf[AnyRef]) |
74 "c" -> (_ => clean_name = true), |
50 if (results.nonEmpty) |
75 "o:" -> (arg => options = options + arg)) |
51 Output.writeln(cat_lines((log_file.name + ":") :: results)) |
76 |
52 } |
77 val more_args = getopts(args) |
|
78 val session_name = |
|
79 more_args match { |
|
80 case List(session_name) => session_name |
|
81 case _ => getopts.usage() |
|
82 } |
|
83 |
|
84 val progress = new Console_Progress() |
|
85 |
|
86 profiling_report(options, session_name, theories = theories, |
|
87 clean_name = clean_name, progress = progress) |
53 }) |
88 }) |
54 } |
89 } |