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