Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101(************************************************************************)(* * The Rocq Prover / The Rocq Development Team *)(* v * Copyright INRIA, CNRS and contributors *)(* <O___,, * (see version control and CREDITS file for authors & dates) *)(* \VV/ **************************************************************)(* // * This file is distributed under the terms of the *)(* * GNU Lesser General Public License Version 2.1 *)(* * (see LICENSE file for the text of the license) *)(************************************************************************)
let die fmt = Printf.kfprintf (fun _ -> exit 1) stderr (fmt^^"\n%!")
let usage () = die "Usage: rocq timelog2html [options] VFILE DATAFILES\n\n%a\n%s" (fun fmt len -> Printf.fprintf fmt "1 to %d data files are supported." len) Htmloutput.max_data_count "Data files may be .json or .json.gz profile files (as produced by rocq c -profile),\ \nor timing files (as produced by rocq c -time-file).\ \n\ \nOptions:\ \n -o FILE: output to FILE (default is - meaning stdout)\ \n -raw-o FILE: output machine readable data to FILE (default off, - means stdout)\ \n (only supported with 2 data files)\ \n -min-diff DIFF: in -raw-o, only output lines with time diff greater than DIFF\ \n (DIFF in OCaml float format, default 1e-4)"
let parse_files = function | [] | [_] -> usage () | vfile :: data_files -> let data_files = Array.of_list data_files in let () = if Array.length data_files > Htmloutput.max_data_count then usage () in vfile, data_files
type output = Stdout | File of string
type opts = { output : output; raw_output : output option; min_diff : Q.t;}
let defaults = { output = Stdout; raw_output = None; min_diff = Q.(one / of_int 10_000);}
let with_output f out = match out with | Stdout -> f stdout | File fname -> let ch = open_out fname in Fun.protect ~finally:(fun () -> close_out ch) (fun () -> f ch)
let parse_output = function | "-" -> Stdout | f -> File f
let parse_min_diff d = try Q.of_float @@ float_of_string d with Failure _ -> usage ()
let rec parse_args opts = function | "-o" :: f :: args -> parse_args { opts with output = parse_output f } args | "-raw-o" :: f :: args -> parse_args { opts with raw_output = Some (parse_output f) } args | "-min-diff" :: d :: args -> parse_args { opts with min_diff = parse_min_diff d } args | ["-o"|"-raw-o"|"-min-diff"] -> usage() | args -> opts, parse_files args
let file_data data_file = if List.exists (fun suf -> CString.is_suffix suf data_file) [".json"; ".json.gz"] then let data = Profparser.parse ~file:data_file in data_file, CArray.of_list data else let data = Timelogparser.parse ~file:data_file in data_file, data |> CArray.map_of_list (fun (loc, time) -> loc, { BenchUtil.dummy_data with time; })
let main args = let opts, (vfile, data_files) = parse_args defaults args in
let source = BenchUtil.read_whole_file vfile in
let all_data = Array.map file_data data_files in
let all_data = BenchUtil.combine_related_data all_data in
let dummy = Array.make (Array.length data_files) BenchUtil.dummy_data in
let all_data = Array.of_list (Sourcehandler.join_to_source ~dummy ~source (Array.to_list all_data)) in
let vname = Filename.basename vfile in
let () = opts.raw_output |> Option.iter @@ with_output @@ fun ch -> Htmloutput.raw_output ch ~min_diff:opts.min_diff all_data in let () = opts.output |> with_output @@ fun ch -> Htmloutput.output ch ~vname ~data_files all_data in ()