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