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