author | wenzelm |
Tue, 08 Jun 2021 23:34:06 +0200 | |
changeset 73838 | 0e6a5a6cc767 |
parent 73835 | 5dae03d50db1 |
child 74712 | bcca7e3bcd0d |
permissions | -rw-r--r-- |
64342 | 1 |
/* Title: Pure/Tools/profiling_report.scala |
64311 | 2 |
Author: Makarius |
3 |
||
73835 | 4 |
Report Poly/ML profiling information from session build database. |
64311 | 5 |
*/ |
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
10 |
object Profiling_Report |
|
11 |
{ |
|
73835 | 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 = |
|
64311 | 18 |
{ |
73835 | 19 |
val store = Sessions.store(options) |
20 |
val resources = Resources.empty |
|
21 |
val session = new Session(options, resources) |
|
64311 | 22 |
|
73835 | 23 |
using(store.open_database_context())(db_context => |
24 |
{ |
|
25 |
val result = |
|
26 |
db_context.input_database(session_name)((db, name) => Some(store.read_theories(db, name))) |
|
27 |
result match { |
|
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) |
|
73838 | 40 |
(Protocol.ML_Profiling(report), _) <- snapshot.messages.iterator |
73835 | 41 |
} yield if (clean_name) report.clean_name else report).toList |
42 |
||
43 |
for (report <- ML_Profiling.account(reports)) progress.echo(report.print) |
|
44 |
} |
|
45 |
}) |
|
64311 | 46 |
} |
47 |
||
48 |
||
49 |
/* Isabelle tool wrapper */ |
|
50 |
||
51 |
val isabelle_tool = |
|
72763 | 52 |
Isabelle_Tool("profiling_report", "report Poly/ML profiling information from log files", |
53 |
Scala_Project.here, args => |
|
64311 | 54 |
{ |
73835 | 55 |
var theories: List[String] = Nil |
56 |
var clean_name = false |
|
57 |
var options = Options.init() |
|
58 |
||
71686
eb44cf7ae926
tuned -- Command_Line.tool is already part of Isabelle_Tool;
wenzelm
parents:
71632
diff
changeset
|
59 |
val getopts = |
eb44cf7ae926
tuned -- Command_Line.tool is already part of Isabelle_Tool;
wenzelm
parents:
71632
diff
changeset
|
60 |
Getopts(""" |
73835 | 61 |
Usage: isabelle profiling_report [OPTIONS] SESSION |
62 |
||
63 |
Options are: |
|
64 |
-T NAME restrict to given theories (multiple options possible) |
|
65 |
-c clean function names |
|
66 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
|
64311 | 67 |
|
73835 | 68 |
Report Poly/ML profiling from the build database of the given session |
69 |
(without up-to-date check of sources). |
|
70 |
""", |
|
71 |
"T:" -> (arg => theories = theories ::: List(arg)), |
|
72 |
"c" -> (_ => clean_name = true), |
|
73 |
"o:" -> (arg => options = options + arg)) |
|
74 |
||
75 |
val more_args = getopts(args) |
|
76 |
val session_name = |
|
77 |
more_args match { |
|
78 |
case List(session_name) => session_name |
|
79 |
case _ => getopts.usage() |
|
80 |
} |
|
81 |
||
82 |
val progress = new Console_Progress() |
|
83 |
||
84 |
profiling_report(options, session_name, theories = theories, |
|
85 |
clean_name = clean_name, progress = progress) |
|
64311 | 86 |
}) |
87 |
} |