author | wenzelm |
Fri, 01 Apr 2022 17:06:10 +0200 | |
changeset 75393 | 87ebf5a50283 |
parent 74755 | 510296c0d8d1 |
child 75394 | 42267c650205 |
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 |
||
75393 | 10 |
object Profiling_Report { |
73835 | 11 |
def profiling_report( |
12 |
options: Options, |
|
74712 | 13 |
session: String, |
73835 | 14 |
theories: List[String] = Nil, |
15 |
clean_name: Boolean = false, |
|
75393 | 16 |
progress: Progress = new Progress |
17 |
): Unit = { |
|
73835 | 18 |
val store = Sessions.store(options) |
64311 | 19 |
|
75393 | 20 |
using(store.open_database_context())(db_context => { |
73835 | 21 |
val result = |
74712 | 22 |
db_context.input_database(session)((db, name) => Some(store.read_theories(db, name))) |
73835 | 23 |
result match { |
74712 | 24 |
case None => error("Missing build database for session " + quote(session)) |
73835 | 25 |
case Some(used_theories) => |
26 |
theories.filterNot(used_theories.toSet) match { |
|
27 |
case Nil => |
|
28 |
case bad => error("Unknown theories " + commas_quote(bad)) |
|
29 |
} |
|
30 |
val reports = |
|
31 |
(for { |
|
32 |
thy <- used_theories.iterator |
|
33 |
if theories.isEmpty || theories.contains(thy) |
|
74755
510296c0d8d1
clarified signature: avoid potential misunderstanding of Resources.empty as proper Resources;
wenzelm
parents:
74712
diff
changeset
|
34 |
command <- Build_Job.read_theory(db_context, List(session), thy).iterator |
73835 | 35 |
snapshot = Document.State.init.snippet(command) |
73838 | 36 |
(Protocol.ML_Profiling(report), _) <- snapshot.messages.iterator |
73835 | 37 |
} yield if (clean_name) report.clean_name else report).toList |
38 |
||
39 |
for (report <- ML_Profiling.account(reports)) progress.echo(report.print) |
|
40 |
} |
|
41 |
}) |
|
64311 | 42 |
} |
43 |
||
44 |
||
45 |
/* Isabelle tool wrapper */ |
|
46 |
||
47 |
val isabelle_tool = |
|
72763 | 48 |
Isabelle_Tool("profiling_report", "report Poly/ML profiling information from log files", |
75393 | 49 |
Scala_Project.here, |
50 |
args => { |
|
73835 | 51 |
var theories: List[String] = Nil |
52 |
var clean_name = false |
|
53 |
var options = Options.init() |
|
54 |
||
71686
eb44cf7ae926
tuned -- Command_Line.tool is already part of Isabelle_Tool;
wenzelm
parents:
71632
diff
changeset
|
55 |
val getopts = |
eb44cf7ae926
tuned -- Command_Line.tool is already part of Isabelle_Tool;
wenzelm
parents:
71632
diff
changeset
|
56 |
Getopts(""" |
73835 | 57 |
Usage: isabelle profiling_report [OPTIONS] SESSION |
58 |
||
59 |
Options are: |
|
60 |
-T NAME restrict to given theories (multiple options possible) |
|
61 |
-c clean function names |
|
62 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
|
64311 | 63 |
|
73835 | 64 |
Report Poly/ML profiling from the build database of the given session |
65 |
(without up-to-date check of sources). |
|
66 |
""", |
|
67 |
"T:" -> (arg => theories = theories ::: List(arg)), |
|
68 |
"c" -> (_ => clean_name = true), |
|
69 |
"o:" -> (arg => options = options + arg)) |
|
70 |
||
71 |
val more_args = getopts(args) |
|
72 |
val session_name = |
|
73 |
more_args match { |
|
74 |
case List(session_name) => session_name |
|
75 |
case _ => getopts.usage() |
|
76 |
} |
|
77 |
||
78 |
val progress = new Console_Progress() |
|
79 |
||
80 |
profiling_report(options, session_name, theories = theories, |
|
81 |
clean_name = clean_name, progress = progress) |
|
64311 | 82 |
}) |
83 |
} |