1(*
2 * Copyright 2014, NICTA
3 *
4 * This software may be distributed and modified according to the terms of
5 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
6 * See "LICENSE_BSD2.txt" for details.
7 *
8 * @TAG(NICTA_BSD)
9 *)
10
11theory AutoLevity_Hooks
12imports
13  AutoLevity_Base
14  AutoLevity_Theory_Report
15begin
16
17(*
18 * This file installs the dependency tracing hooks so that they
19 * will be active in the current Isabelle session. These are the
20 * toplevel command hooks for tracing dependencies, and a shutdown
21 * hook for writing out the dependencies when the session finishes.
22 *)
23
24(* Install toplevel command hooks. *)
25setup \<open>
26case getenv "AUTOLEVITY" of
27  "1" => (tracing ("Setting up AUTOLEVITY=1");
28          AutoLevity_Base.setup_command_hook {trace_apply = false})
29| "2" => (tracing ("Setting up AUTOLEVITY=2");
30          AutoLevity_Base.setup_command_hook {trace_apply = true})
31| _ => I
32\<close>
33
34(* Collect all the traces and write them to a combined file. *)
35ML \<open>
36structure AutoLevity_Combined_Report = struct
37
38(* Session-qualified theory name -> JSON ouput lines *)
39fun levity_report_for thy_name: string list option =
40let
41  val thy = Thy_Info.get_theory thy_name;
42  val thy_short_name = Context.theory_name thy;
43
44  val trans = AutoLevity_Base.get_transactions ();
45in if Symtab.defined trans thy_short_name then
46     AutoLevity_Theory_Report.get_reports_for_thy thy
47     |> AutoLevity_Theory_Report.string_reports_of
48     |> SOME
49   else
50     NONE
51end;
52
53(* This has the usual race condition, but should be very unlikely in practice *)
54fun local_temp_file path = let
55  val dir = Path.dir path;
56  val file = Path.base_name path;
57  fun try_path () = let
58    (* avoid colliding with other processes *)
59    val pid = Posix.ProcEnv.getpid () |> Posix.Process.pidToWord |> SysWord.toInt;
60    (* timestamp *)
61    val now = Time.now () |> Time.toMilliseconds;
62    (* serialized pseudorandom state within this process *)
63    val rand = Random.random_range 100000 999999;
64    val temp_id = Library.space_implode "-" (map string_of_int [pid, now, rand]);
65    val temp_path = Path.append dir (Path.basic (file ^ ".tmp" ^ temp_id));
66    in if File.exists temp_path
67       then
68         ((* again, this should be very unlikely in practice *)
69          warning ("local_temp_file: (unlikely) failed attempt: " ^
70                   Path.implode temp_path);
71          try_path ())
72       else
73         (File.append temp_path ""; (* create empty file *)
74          temp_path)
75    end;
76  in try_path () end;
77
78(* Output all traces in this session to given path.
79   Wraps each theory in the session in a JSON dictionary as follows:
80
81   {
82     "session": <escaped session name>,
83     "content": [
84       <theory "foo" content>,
85       <theory "bar" content>,
86       ...
87     ]
88   }
89*)
90fun levity_report_all output_path: unit =
91let
92  val this_session = Session.get_name ();
93  (* Use a temp file for atomic output. Note that we don't use
94     File.tmp_path or similar because the standard /tmp/isabelle-*
95     tmpdir might not be on the same file system as output_path,
96     whereas we can only rename atomically on the same file system *)
97  val temp_path = local_temp_file output_path;
98
99  (* Wrap individual theory reports in a JSON dictionary as follows:
100
101     {
102       "theory": <escaped theory name>,
103       "content": <theory content as JSON dictionary>
104     }
105
106     Note that this closes and re-opens the output file
107     over and over. But it's better than building the entire
108     combined output in memory. *)
109  fun dump_all _ [] = ()
110    | dump_all (first: bool) (thy_name::remaining) = let
111        val _ = @{print} ("Reporting on " ^ thy_name ^ "...")
112        val separator = if first then "" else ", "; (* from previous item *)
113        val json_start = [separator, "{", quote "theory", ":", JSON_string_encode thy_name, ",\n",
114                          quote "content", ":"];
115        val json_end = ["}\n"];
116        in case levity_report_for thy_name of
117              NONE => (
118                @{print} ("No transaction record for " ^ thy_name);
119                dump_all first remaining
120                )
121            | SOME thy_report => (
122                File.append_list temp_path (json_start @ thy_report @ json_end);
123                dump_all false remaining
124                )
125        end;
126
127  val thy_names = Thy_Info.get_names ();
128  val _ = File.write_list temp_path
129            ["{", quote "session", ":", JSON_string_encode this_session, ",\n",
130             quote "content", ":", "[\n"];
131  val _ = dump_all true thy_names;
132  val _ = File.append_list temp_path ["]\n", "}"];
133  val _ = OS.FileSys.rename {
134            old = Path.implode (Path.expand temp_path),
135            new = Path.implode (Path.expand output_path)
136          };
137in
138    @{print} ("Report written to: " ^ Path.implode output_path);
139    ()
140end;
141
142(* Wrapper that outputs to the Isabelle build log directory *)
143fun levity_session_log () =
144let
145  val this_session = Session.get_name ();
146  val fname = this_session ^ ".lev";
147  val output_path = Path.make ["log", fname]
148                    |> Path.append (Path.explode (getenv "ISABELLE_OUTPUT"));
149  val session_traces = AutoLevity_Base.get_transactions ();
150in
151  if Symtab.is_empty session_traces
152  (* AutoLevity does not collect traces for interactive PIDE sessions,
153   * so don't overwrite the levity log *)
154  then warning ("No traces for session: " ^ this_session)
155  else levity_report_all output_path
156end
157handle exn =>
158  (* from Pure/Tools/build.ML *)
159  (List.app (fn msg => writeln (encode_lines (YXML.content_of msg)))
160            (Runtime.exn_message_list exn);
161   Exn.reraise exn);
162
163end
164\<close>
165
166(* Do the output when the Isabelle session finishes.
167   The session shutdown hook requires a patch to Isabelle, so we wrap
168   this code to be a no-op on vanilla Isabelle installations. *)
169ML \<open>
170try (ML_Context.eval ML_Compiler.flags @{here})
171    (ML_Lex.read_pos @{here}
172      "Session.register_shutdown_hook AutoLevity_Combined_Report.levity_session_log")
173\<close>
174
175end
176