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