From bdbf86d512581c004de8dff96a421fffb4e6ea96 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Wed, 16 Nov 2022 13:13:53 +0100 Subject: [PATCH 01/17] Add progress option --- src/bin/loop.ml | 6 +- src/bin/main.ml | 2 + src/bin/options.ml | 26 ++-- src/loop/dune | 6 +- src/loop/parser.ml | 121 ++++++++++++----- src/loop/parser.mli | 6 +- src/loop/parser_intf.ml | 3 +- src/loop/pipeline.ml | 2 + src/loop/pipeline.mli | 3 + src/loop/state.ml | 40 ++++-- src/loop/stats.ml | 293 ++++++++++++++++++++++++++++++++++++++++ src/loop/stats.mli | 12 ++ src/loop/stats_intf.ml | 37 +++++ src/loop/typer.ml | 198 ++++++++++++++------------- src/loop/typer.mli | 2 + src/lsp/loop.ml | 11 +- src/standard/loc.ml | 13 ++ src/standard/loc.mli | 14 +- 18 files changed, 635 insertions(+), 160 deletions(-) create mode 100644 src/loop/stats.ml create mode 100644 src/loop/stats.mli create mode 100644 src/loop/stats_intf.ml diff --git a/src/bin/loop.ml b/src/bin/loop.ml index 817eb4cbd..98c243dba 100644 --- a/src/bin/loop.ml +++ b/src/bin/loop.ml @@ -4,9 +4,9 @@ module State = Dolmen_loop.State module Pipeline = Dolmen_loop.Pipeline.Make(State) -module Parser = Dolmen_loop.Parser.Make(State) +module Stats = Dolmen_loop.Stats.Make(State) +module Parser = Dolmen_loop.Parser.Make(State)(Stats) module Header = Dolmen_loop.Headers.Make(State) module Typer = Dolmen_loop.Typer.Typer(State) -module Typer_Pipe = Dolmen_loop.Typer.Make(Dolmen.Std.Expr)(Dolmen.Std.Expr.Print)(State)(Typer) +module Typer_Pipe = Dolmen_loop.Typer.Make(Dolmen.Std.Expr)(Dolmen.Std.Expr.Print)(State)(Stats)(Typer) module Check = Dolmen_model.Loop.Make(State)(Parser)(Typer)(Typer_Pipe) - diff --git a/src/bin/main.ml b/src/bin/main.ml index ca557bdba..1618cf2bc 100644 --- a/src/bin/main.ml +++ b/src/bin/main.ml @@ -24,6 +24,7 @@ let debug_typed_pipe st stmt = (* ************************ *) let handle_exn st exn = + Loop.Stats.finalise st; let _st = Errors.exn st exn in exit 125 @@ -62,6 +63,7 @@ let run st = ) ) in + let () = Loop.Stats.finalise st in let st = Loop.Header.check st in let _st = Dolmen_loop.State.flush st () in () diff --git a/src/bin/options.ml b/src/bin/options.ml index 7b6f5d532..9d279c29e 100644 --- a/src/bin/options.ml +++ b/src/bin/options.ml @@ -324,6 +324,7 @@ let mk_run_state header_lang_version smtlib2_forced_logic type_check check_model debug report_style max_warn reports syntax_error_ref + progress_enabled = (* Side-effects *) let () = Option.iter Gc.set gc_opt in @@ -352,6 +353,10 @@ let mk_run_state ~header_check ~header_licenses ~header_lang_version + |> Loop.Stats.init + ~enabled:progress_enabled + ~typing:type_check + ~model:check_model (* Profiling *) (* ************************************************************************* *) @@ -571,19 +576,23 @@ let state = would be too long), and lastly $(b,minimal) prints each report on one line" in Arg.(value & opt report_style Contextual & info ["report-style"] ~doc ~docs:error_section) - in + in let max_warn = let doc = Format.asprintf "Maximum number of warnings to display (excess warnings will be counted and a count of silenced warnings reported at the end)." in Arg.(value & opt int max_int & info ["max-warn"] ~doc ~docs:error_section) + in + let syntax_error_ref = + let doc = Format.asprintf + "Print the syntax error reference number when a syntax error is raised." in - let syntax_error_ref = - let doc = Format.asprintf - "Print the syntax error reference number when a syntax error is raised." - in - Arg.(value & opt bool false & info ["syntax-error-ref"] ~doc ~docs:error_section) - in + Arg.(value & opt bool false & info ["syntax-error-ref"] ~doc ~docs:error_section) + in + let progress_enabled = + let doc = Format.asprintf "Print progress information." in + Arg.(value & opt bool false & info ["progress"] ~doc ~docs:profiling_section) + in Term.(const mk_run_state $ profiling_t $ gc $ gc_t $ bt $ colors $ abort_on_bug $ @@ -592,7 +601,8 @@ let state = header_check $ header_licenses $ header_lang_version $ force_smtlib2_logic $ typing $ check_model $ - debug $ report_style $ max_warn $ reports $ syntax_error_ref) + debug $ report_style $ max_warn $ reports $ syntax_error_ref $ + progress_enabled) (* List command term *) diff --git a/src/loop/dune b/src/loop/dune index 01a76ada8..6eb90ce93 100644 --- a/src/loop/dune +++ b/src/loop/dune @@ -4,7 +4,7 @@ (instrumentation (backend bisect_ppx)) (libraries ; External deps - gen unix fmt pp_loc + gen unix fmt pp_loc progress ; main dolmen deps , with versioned languages deps dolmen dolmen.intf dolmen.std dolmen.class @@ -16,9 +16,9 @@ ; Useful utilities Alarm Report ; Interfaces - Expr_intf Parser_intf Typer_intf Headers_intf + Expr_intf Parser_intf Typer_intf Headers_intf Stats_intf ; Implementations Logic Response Code State ; Pipeline & Pipes - Pipeline Parser Typer Headers) + Pipeline Parser Typer Headers Stats) ) diff --git a/src/loop/parser.ml b/src/loop/parser.ml index 289099490..292584758 100644 --- a/src/loop/parser.ml +++ b/src/loop/parser.ml @@ -65,10 +65,14 @@ let parsing_error = (* ************************************************************************ *) type 'a file = 'a State.file +let file_size = Stats.file_size module type S = Parser_intf.S -module Make(State : State.S) = struct +module Make + (State : State.S) + (Stats : Stats.S with type state := State.t) += struct (* Prologue *) (* ************************************************************************ *) @@ -105,14 +109,6 @@ module Make(State : State.S) = struct (* ************************************************************************ *) - let gen_of_llist l = - let l = ref l in - (fun () -> match Lazy.force !l with - | [] -> None - | x :: r -> - l := (lazy r); Some x - ) - let switch_to_full_mode ?loc lang st (old : _ file) (file: _ file) = let st = match old.mode with @@ -160,30 +156,68 @@ module Make(State : State.S) = struct in aux - let wrap_parser ~file g = fun st -> + let wrap_parser ?input ~loc_of_res ~file g = fun st -> begin match (State.get interactive_prompt st) st with | None -> () | Some prelude -> Format.printf "%s @?" prelude end; + let counter = Stats.start_counter st in match g () with - | ret -> st, ret + | None -> + let st = Stats.record_parsed st input counter Dolmen.Std.Loc.no_loc in + st, None + | Some res as ret -> + let st = Stats.record_parsed st input counter (loc_of_res res) in + st, ret | exception Dolmen.Std.Loc.Uncaught (loc, exn, bt) -> + let st = Stats.record_parsed st input counter loc in let st = State.error st ~file ~loc:{ file = file.loc; loc; } Report.Error.uncaught_exn (exn, bt) in st, None | exception Dolmen.Std.Loc.Lexing_error (loc, lex) -> + let st = Stats.record_parsed st input counter loc in let st = State.error st ~file ~loc:{ file = file.loc; loc; } lexing_error lex in st, None | exception Dolmen.Std.Loc.Syntax_error (loc, perr) -> + let st = Stats.record_parsed st input counter loc in let syntax_error_ref = State.get_or ~default:false syntax_error_ref st in let st = State.error st ~file ~loc:{ file = file.loc; loc; } parsing_error (syntax_error_ref, perr) in st, None + let wrap_lazy_list ?input ~loc_of_res ~file llist = + let first = ref true in + let l = ref [] in + let rec aux st = + if !first then begin + first := false; + let counter = Stats.start_counter st in + let list = Lazy.force llist in + l := list; + (* record the sizes of statements parsed *) + let st = + List.fold_left (fun st res -> + Stats.record_parsed st input None (loc_of_res res) + ) st list + in + (* record the time spent parsing *) + let st = Stats.record_parsed st input counter Dolmen.Std.Loc.no_loc in + aux st + end else begin + let elt = + match !l with + | [] -> None + | x :: r -> l := r; Some x + in + wrap_parser ~loc_of_res ~file (fun () -> elt) st + end + in + aux + let parse_logic prelude st (file : Logic.language file) = (* Parse the input *) - let st, file, g = + let st, file, input, g = try match file.source with | `Stdin -> @@ -191,7 +225,7 @@ module Make(State : State.S) = struct ?language:file.lang (`Stdin (Logic.Smtlib2 `Latest)) in let file = { file with loc = file_loc; lang = Some lang; } in - st, file, gen + st, file, None, gen | `Raw (filename, contents) -> let lang = match file.lang with @@ -206,13 +240,15 @@ module Make(State : State.S) = struct let lang, file_loc, gen, cl = Logic.parse_input ~language:lang (`Raw (filename, lang, contents)) in let file = { file with loc = file_loc; lang = Some lang; } in - st, file, gen_finally gen cl + let input, st = Stats.new_input st filename (String.length contents) in + st, file, Some input, gen_finally gen cl | Some `Full -> let lang, file_loc, l = Logic.parse_raw_lazy ~language:lang ~filename contents in let file = { file with loc = file_loc; lang = Some lang; } in - st, file, gen_of_llist l + let input, st = Stats.new_input st filename (String.length contents) in + st, file, Some input, gen_of_llist l end | `File f -> let s = Dolmen.Std.Statement.include_ f [] in @@ -237,18 +273,20 @@ module Make(State : State.S) = struct Dolmen.Std.Statement.pack [s; Dolmen.Std.Statement.prove ()] in let file = { file with lang = Some lang; } in - st, file, (Gen.singleton s') + st, file, None, (Gen.singleton s') with | Logic.Extension_not_found ext -> - State.error st extension_not_found ext, file, Gen.empty + State.error st extension_not_found ext, file, None, Gen.empty in let st = set_logic_file st file in (* Wrap the resulting parser *) - st, wrap_parser ~file (Gen.append (Gen.of_list prelude) g) + st, wrap_parser + ?input ~file ~loc_of_res:(fun (c : Dolmen.Std.Statement.t) -> c.loc) + (Gen.append (Gen.of_list prelude) g) let parse_response prelude st (file : Response.language file) = (* Parse the input *) - let st, file, g = + let st, file, input, g = try match file.source with | `Stdin -> @@ -256,7 +294,7 @@ module Make(State : State.S) = struct ?language:file.lang (`Stdin (Response.Smtlib2 `Latest)) in let file = { file with loc = file_loc; lang = Some lang; } in - st, file, gen + st, file, None, `Gen gen | `Raw (filename, contents) -> let lang = match file.lang with @@ -271,20 +309,24 @@ module Make(State : State.S) = struct let lang, file_loc, gen, cl = Response.parse_input ~language:lang (`Raw (filename, lang, contents)) in let file = { file with loc = file_loc; lang = Some lang; } in - st, file, gen_finally gen cl + let input, st = Stats.new_input st filename (String.length contents) in + st, file, Some input, gen_finally gen cl | Some `Full -> let lang, file_loc, l = Response.parse_raw_lazy ?language:file.lang ~filename contents in let file = { file with loc = file_loc; lang = Some lang; } in - st, file, gen_of_llist l + let input, st = Stats.new_input st filename (String.length contents) in + st, file, Some input, gen_of_llist l end | `File f -> begin match Response.find ?language:file.lang ~dir:file.dir f with | None -> let st = State.error st file_not_found (file.dir, f) in - st, file, Gen.empty + st, file, None, `Gen Gen.empty | Some filename -> + let file_size = file_size filename in + let input, st = Stats.new_input st f file_size in begin match file.mode with | None | Some `Incremental -> @@ -292,22 +334,31 @@ module Make(State : State.S) = struct Response.parse_input ?language:file.lang (`File filename) in let file = { file with loc = file_loc; lang = Some lang; } in - st, file, gen_finally gen cl + st, file, Some input, `Gen (gen_finally gen cl) | Some `Full -> let lang, file_loc, l = Response.parse_file_lazy ?language:file.lang filename in let file = { file with loc = file_loc; lang = Some lang; } in - st, file, gen_of_llist l + st, file, Some input, `Llist l end end with | Logic.Extension_not_found ext -> - State.error st extension_not_found ext, file, Gen.empty + State.error st extension_not_found ext, file, None, `Gen Gen.empty in let st = State.set State.response_file file st in (* Wrap the resulting parser *) - st, wrap_parser ~file (Gen.append (Gen.of_list prelude) g) + let loc_of_res (a : Dolmen.Std.Answer.t) = a.loc in + match g with + | `Gen g -> + st, wrap_parser + ?input ~file ~loc_of_res + (Gen.append (Gen.of_list prelude) g) + | `Llist l -> + st, wrap_lazy_list + ?input ~file ~loc_of_res + (lazy (prelude @ (Lazy.force l))) (* Expand dolmen statements *) (* ************************************************************************ *) @@ -315,10 +366,12 @@ module Make(State : State.S) = struct let merge _ st = st let expand st c = + let loc_of_res (c : Dolmen.Std.Statement.t) = c.loc in let ret = match c with | { S.descr = S.Pack l; _ } -> let file = State.get State.logic_file st in - st, `Gen (merge, wrap_parser ~file (Gen.of_list l)) + (* we do not try and record stats for the wrapping list -> parser done here *) + st, `Gen (merge, wrap_parser ~loc_of_res ~file (Gen.of_list l)) (* TODO: filter the statements by passing some options *) | { S.descr = S.Include file; _ } -> let logic_file = State.get State.logic_file st in @@ -329,19 +382,21 @@ module Make(State : State.S) = struct match Logic.find ?language ~dir file with | None -> State.error ~loc st file_not_found (dir, file), `Ok - | Some file -> + | Some filename -> + let file_size = file_size filename in + let input, st = Stats.new_input st (Filename.basename filename) file_size in begin match logic_file.mode with | None | Some `Incremental -> - let lang, file_loc, gen, cl = Logic.parse_input ?language (`File file) in + let lang, file_loc, gen, cl = Logic.parse_input ?language (`File filename) in let new_logic_file = { logic_file with loc = file_loc; lang = Some lang; } in let st = set_logic_file st new_logic_file in - st, `Gen (merge, wrap_parser ~file:new_logic_file (gen_finally gen cl)) + st, `Gen (merge, wrap_parser ~input ~loc_of_res ~file:new_logic_file (gen_finally gen cl)) | Some `Full -> - let lang, file_loc, l = Logic.parse_file_lazy ?language file in + let lang, file_loc, l = Logic.parse_file_lazy ?language filename in let new_logic_file = { logic_file with loc = file_loc; lang = Some lang; } in let st = set_logic_file st new_logic_file in - st, `Gen (merge, wrap_parser ~file:new_logic_file (gen_of_llist l)) + st, `Gen (merge, wrap_lazy_list ~input ~loc_of_res ~file:new_logic_file l) end end | _ -> (st, `Ok) diff --git a/src/loop/parser.mli b/src/loop/parser.mli index ae11e2bf2..f584b51fc 100644 --- a/src/loop/parser.mli +++ b/src/loop/parser.mli @@ -21,8 +21,12 @@ val parsing_error : (bool * ]) Report.error (** Parsing errors *) +(** Interface *) module type S = Parser_intf.S (** This module provides convenient pipes for parsing and dealing with includes. *) -module Make(State : State.S) : S with type state := State.t and type 'a key := 'a State.key +module Make + (State : State.S) + (Stats : Stats.S with type state := State.t) + : S with type state := State.t and type 'a key := 'a State.key diff --git a/src/loop/parser_intf.ml b/src/loop/parser_intf.ml index 964da76c4..7093d03ee 100644 --- a/src/loop/parser_intf.ml +++ b/src/loop/parser_intf.ml @@ -46,7 +46,8 @@ module type S = sig returns a tuple of the new state (including the detected input language), together with a statement generator. *) - val expand : state -> Dolmen.Std.Statement.t -> + val expand : + state -> Dolmen.Std.Statement.t -> state * [ `Ok | `Gen of (state -> state -> state) * (state -> state * Dolmen.Std.Statement.t option) ] (** Expand statements (such as includes). Returns the new state, and either: diff --git a/src/loop/pipeline.ml b/src/loop/pipeline.ml index b90a60004..998980d63 100644 --- a/src/loop/pipeline.ml +++ b/src/loop/pipeline.ml @@ -64,6 +64,8 @@ module Make(State : State.S) = struct let iter_ ?name f = op ?name (fun st x -> f x; st, x) + let peek ?name f = op ?name (fun st x -> let st' = f st x in st', x) + let f_map ?name ?(test=(fun _ _ -> true)) f = op ?name (fun st x -> if test st x then begin diff --git a/src/loop/pipeline.mli b/src/loop/pipeline.mli index ec46b083f..be3cdcd55 100644 --- a/src/loop/pipeline.mli +++ b/src/loop/pipeline.mli @@ -58,6 +58,9 @@ module Make(State : State.S) : sig val iter_ : ?name:string -> ('a -> unit) -> (_, 'a, 'a) op (** Perform the function's side-effect and return the same input. *) + val peek : ?name:string -> ('st -> 'a -> 'st) -> ('st, 'a, 'a) op + (** Peek at the current payload of the pipeline, and modify the state. *) + val f_map : ?name:string -> ?test:('st -> 'a -> bool) -> diff --git a/src/loop/state.ml b/src/loop/state.ml index 7c72c2f1a..d58ad3ff1 100644 --- a/src/loop/state.ml +++ b/src/loop/state.ml @@ -120,6 +120,7 @@ module type S = sig val size_limit : float key val logic_file : Logic.language file key val response_file : Response.language file key + val progress_display : (unit, unit) Progress.Display.t key (* common keys *) end @@ -169,6 +170,9 @@ let size_limit : float key = create_key ~pipe "size_limit" let logic_file : Logic.language file key = create_key ~pipe "logic_file" let response_file : Response.language file key = create_key ~pipe "response_file" +let progress_display : (unit, unit) Progress.Display.t key = + create_key ~pipe "progress_display" + let init ?bt:(bt_value=(Printexc.backtrace_status ())) ~debug:debug_value @@ -253,6 +257,11 @@ let flush st () = (cur - max) (if max = 0 then "" else "additional ") let error ?file ?loc st error payload = + let () = + match get progress_display st with + | d -> Progress.Display.finalise d + | exception Key_not_found _ -> () + in let st = flush st () in let loc = Dolmen.Std.Misc.opt_map loc Dolmen.Std.Loc.full_loc in let aux _ = Code.exit (Report.Error.code error) in @@ -277,19 +286,26 @@ let warn ?file ?loc st warn payload = if get cur_warn st >= get max_warn st then aux st else - begin match get report_style st with - | Minimal -> - Format.kfprintf aux Format.err_formatter - "W:%s@." (Report.Warning.mnemonic warn) - | Regular | Contextual -> - Format.kfprintf aux Format.err_formatter - ("@[%a%a @[%a@]%a@]@.") - (pp_loc ?file st) loc - Fmt.(styled `Bold @@ styled (`Fg (`Hi `Magenta)) string) "Warning" - Report.Warning.print (warn, payload) - Report.Warning.print_hints (warn, payload) - end + Progress.interject_with (fun () -> + match get report_style st with + | Minimal -> + Format.kfprintf aux Format.err_formatter + "W:%s@." (Report.Warning.mnemonic warn) + | Regular | Contextual -> + Format.kfprintf aux Format.err_formatter + ("@[%a%a @[%a@]%a@]@.") + (pp_loc ?file st) loc + Fmt.(styled `Bold @@ styled (`Fg (`Hi `Magenta)) string) "Warning" + Report.Warning.print (warn, payload) + Report.Warning.print_hints (warn, payload) + ) | Fatal -> + let () = + match get progress_display st with + | d -> Progress.Display.finalise d + | exception Key_not_found _ -> () + in + let st = flush st () in let aux _ = Code.exit (Report.Warning.code warn) in begin match get report_style st with | Minimal -> diff --git a/src/loop/stats.ml b/src/loop/stats.ml new file mode 100644 index 000000000..eb92ad4b9 --- /dev/null +++ b/src/loop/stats.ml @@ -0,0 +1,293 @@ + +(* This file is free software, part of dolmen. See file "LICENSE" for more information *) + +(* Some helpers *) +(* ************************************************************************* *) + +let file_size file_path = + let st = Unix.stat file_path in + st.st_size + +(* Custom progress bar *) +(* ************************************************************************* *) + +let percentage_printer = + Progress.Printer.create () + ~string_len:4 + ~to_string:(fun p -> Format.asprintf "%3d%%" p) + +module Bytes_stats = struct + + type t = { + total_bytes : int; + processed_bytes : int; + elapsed_time : Mtime.span; + } + + let zero = { + total_bytes = 0; + processed_bytes = 0; + elapsed_time = Mtime.Span.zero; + } + + let input total_bytes = { zero with total_bytes } + + let total_bytes { total_bytes; _ } = total_bytes + let elapsed_time { elapsed_time; _ } = elapsed_time + let processed_bytes { processed_bytes; _ } = processed_bytes + let percentage { processed_bytes; total_bytes; _ } = + int_of_float (100. *. (float processed_bytes) /. (float total_bytes)) + let perthousand { processed_bytes; total_bytes; _ } = + int_of_float (1000. *. (float processed_bytes) /. (float total_bytes)) + + let line phase : t Progress.Line.t = + let open Progress.Line in + list [ + using (fun _ -> phase) (of_printer ~init:phase (Progress.Printer.string ~width:50)); + using elapsed_time (of_printer ~init:Mtime.Span.zero Progress.Units.Duration.mm_ss); + using processed_bytes (of_printer ~init:0 Progress.Units.Bytes.of_int); + using total_bytes (of_printer ~init:0 Progress.Units.Bytes.of_int); + (* TODO: add bytes/seconds *) + using perthousand (bar ~data:`Latest 1000); + using percentage (of_printer ~init:0 percentage_printer); + ] + +end + +(* Stats & progress bars *) +(* ************************************************************************* *) + +module type S = Stats_intf.S + +module Make(State : State.S) = struct + + (* type *) + + type config = { + enabled : bool; + typing : bool; + model : bool; + } + + type input = int + type counter = Mtime_clock.counter + type parsing = { + stats : Bytes_stats.t array; + reporters : Bytes_stats.t Progress.Reporter.t array; + } + + type typing = { + stats : Bytes_stats.t; + reporter : Bytes_stats.t Progress.Reporter.t; + } + + type model = { + stats : Bytes_stats.t; + reporter : Bytes_stats.t Progress.Reporter.t; + } + + + (* state keys *) + + let pipe = "stats" + + let config_key : config State.key = + State.create_key ~pipe "stats_config" + + let parsing_key : parsing State.key = + State.create_key ~pipe "stats_parsing" + + let typing_key : typing State.key = + State.create_key ~pipe "stats_typing" + + let model_key : model State.key = + State.create_key ~pipe "stats_model" + + + (* state init *) + + let init ~enabled ~typing ~model st = + let config = { enabled; typing; model; } in + let st = State.set config_key config st in + if not enabled then st + else begin + (* create progress display *) + let config = Progress.Config.v () in + let multi = Progress.Multi.blank in + let display = Progress.Display.start ~config multi in + let st = State.set State.progress_display display st in + (* create bars *) + let st = + let parsing : parsing = + let stats = [| |] in + let reporters = [| |] in + { stats; reporters; } + in + State.set parsing_key parsing st + in + let st = + if not typing then st + else begin + let typing : typing = + let stats = Bytes_stats.zero in + let line = Bytes_stats.line "typing" in + let reporter = Progress.Display.add_line display line in + { stats; reporter; } + in + State.set typing_key typing st + end + in + let st = + if not model then st + else begin + let model : model = + let stats = Bytes_stats.zero in + let line = Bytes_stats.line "model" in + let reporter = Progress.Display.add_line display line in + { stats; reporter; } + in + State.set model_key model st + end + in + st + end + + (* common *) + + let config st = State.get config_key st + + let start_counter st = + if (config st).enabled then Some (Mtime_clock.counter ()) else None + + (* parsing and inputs *) + + let new_input st input_name input_size = + let config = config st in + if config.enabled then begin + let parsing = State.get parsing_key st in + let display = State.get State.progress_display st in + let n = Array.length parsing.stats in + assert (n = Array.length parsing.reporters); + let z = Bytes_stats.input input_size in + let line_name = Format.asprintf "parsing (%s)" input_name in + let line = Bytes_stats.line line_name in + let above = + (if config.model then 1 else 0 (* model *)) + + (if config.typing then 1 else 0 (* typing *)) + + n (* already existing parsing lines *) + in + let reporter = Progress.Display.add_line ~above display line in + let stats = Array.append parsing.stats [| z |] in + let reporters = Array.append parsing.reporters [| reporter |] in + let parsing : parsing = { stats; reporters; } in + let st' = State.set parsing_key parsing st in + n, st' + end else + 0, st + + let record_parsed st input counter loc = + match input with + | None -> st + | Some input -> + let span = + match counter with + | None -> Mtime.Span.zero + | Some counter -> Mtime_clock.count counter + in + let config = config st in + if config.enabled then begin + (* record the loc as parsed *) + let st = + let parsing = State.get parsing_key st in + let input_stats = parsing.stats.(input) in + let input_reporter = parsing.reporters.(input) in + let elapsed_time = Mtime.Span.add span input_stats.elapsed_time in + let processed_bytes = max input_stats.processed_bytes (Dolmen.Std.Loc.last_byte loc) in + let input_stats = { input_stats with elapsed_time; processed_bytes; } in + let () = Progress.Reporter.report input_reporter input_stats in + let stats = Array.copy parsing.stats in + let () = Array.set stats input input_stats in + let parsing = { parsing with stats } in + State.set parsing_key parsing st + in + (* add the loc to be typed *) + let st = + if not config.typing then st + else begin + let bytes_to_type = Dolmen.Std.Loc.length_in_bytes loc in + let typing = State.get typing_key st in + let total_bytes = typing.stats.total_bytes + bytes_to_type in + let stats = { typing.stats with total_bytes } in + let typing = { typing with stats } in + let () = Progress.Reporter.report typing.reporter stats in + State.set typing_key typing st + end + in + st + end else + st + + let record_typed st counter loc = + match counter with + | None -> st + | Some counter -> + let span = Mtime_clock.count counter in + let config = config st in + (* record the loc as typed *) + let st = + if not config.typing then st + else begin + let processed = Dolmen.Std.Loc.length_in_bytes loc in + let typing = State.get typing_key st in + let elapsed_time = Mtime.Span.add span typing.stats.elapsed_time in + let processed_bytes = typing.stats.processed_bytes + processed in + let stats = { typing.stats with elapsed_time; processed_bytes; } in + let typing = { typing with stats } in + let () = Progress.Reporter.report typing.reporter stats in + State.set typing_key typing st + end + in + (* add the loc to be checked for model *) + let st = + if not config.model then st + else begin + let bytes_to_type = Dolmen.Std.Loc.length_in_bytes loc in + let model = State.get model_key st in + let total_bytes = model.stats.total_bytes + bytes_to_type in + let stats = { model.stats with total_bytes } in + let model = { model with stats } in + let () = Progress.Reporter.report model.reporter stats in + State.set model_key model st + end + in + st + + (* finalisation *) + + let finalise st = + let config = config st in + if config.typing then begin + let typing = State.get typing_key st in + let () = Unix.sleepf (1. /. 60.) in + Progress.Reporter.report typing.reporter typing.stats + end; + if config.model then begin + let model = State.get model_key st in + let () = Unix.sleepf (1. /. 60.) in + Progress.Reporter.report model.reporter model.stats + end; + if config.enabled then begin + let parsing = State.get parsing_key st in + Array.iter2 (fun stats reporter -> + let () = Unix.sleepf (1. /. 60.) in + Progress.Reporter.report reporter stats + ) parsing.stats parsing.reporters; + let display = State.get State.progress_display st in + let () = Unix.sleepf (1. /. 60.) in + Progress.Display.finalise display + end; + () + +end + + diff --git a/src/loop/stats.mli b/src/loop/stats.mli new file mode 100644 index 000000000..940fccdab --- /dev/null +++ b/src/loop/stats.mli @@ -0,0 +1,12 @@ + +(* This file is free software, part of Dolmen. See file "LICENSE" for more details. *) + +val file_size : string -> int +(** File size in bytes. *) + +(** Interface *) +module type S = Stats_intf.S + +(** This module provides convenient pipes for parsing and dealing with includes. *) +module Make(State : State.S) : S with type state := State.t + diff --git a/src/loop/stats_intf.ml b/src/loop/stats_intf.ml new file mode 100644 index 000000000..fdd81a2d5 --- /dev/null +++ b/src/loop/stats_intf.ml @@ -0,0 +1,37 @@ + +(* This file is free software, part of Dolmen. See file "LICENSE" for more details. *) + +module type S = sig + + type state + (** The type of state for a whole pipeline *) + + type input + (** A type to track input files *) + + type counter + (** Time counter *) + + val init : + enabled:bool -> + typing:bool -> + model:bool -> + state -> state + (** Initialisation for the state. *) + + val start_counter : state -> counter option + (** Start a counter. *) + + val new_input : state -> string -> int -> input * state + (** Record a new input source, with the given name and size (in bytes). *) + + val record_parsed : state -> input option -> counter option -> Dolmen.Std.Loc.t -> state + (** *) + + val record_typed : state -> counter option -> Dolmen.Std.Loc.t -> state + (** *) + + val finalise : state -> unit + (** Finalise the stats. *) + +end diff --git a/src/loop/typer.ml b/src/loop/typer.ml index f6a058524..8a5f2ef86 100644 --- a/src/loop/typer.ml +++ b/src/loop/typer.ml @@ -1736,6 +1736,8 @@ module Make and type term_cst := Expr.term_cst and type formula := Expr.formula) (State : State.S) + (Stats : Stats.S + with type state := State.t) (Typer : Typer with type state := State.t and type ty := Expr.ty @@ -1939,103 +1941,107 @@ module Make if not (State.get type_check st) then st, `Done () else + let counter = Stats.start_counter st in let input = `Logic (State.get State.logic_file st) in - match normalize st c with - - (* Pack and includes. - These should have been filtered out before this point. - TODO: emit some kind of warning ? *) - | { S.descr = S.Pack _; _ } -> st, `Done () - | { S.descr = S.Include _; _ } -> st, `Done () - - (* State&Assertion stack management *) - | { S.descr = S.Reset; _ } -> - let st = Typer.reset st ~loc:c.S.loc () in - st, `Continue (simple (other_id c) c.S.loc `Reset) - | { S.descr = S.Pop i; _ } -> - let st = Typer.pop st ~input ~loc:c.S.loc i in - st, `Continue (simple (other_id c) c.S.loc (`Pop i)) - | { S.descr = S.Push i; _ } -> - let st = Typer.push st ~input ~loc:c.S.loc i in - st, `Continue (simple (other_id c) c.S.loc (`Push i)) - | { S.descr = S.Reset_assertions; _ } -> - let st = Typer.reset_assertions st ~loc:c.S.loc () in - st, `Continue (simple (other_id c) c.S.loc `Reset_assertions) - - (* Plain statements - TODO: allow the `plain` function to return a meaningful value *) - | { S.descr = S.Plain t; _ } -> - st, `Continue (simple (other_id c) c.S.loc (`Plain t)) - - (* Hypotheses and goal statements *) - | { S.descr = S.Prove l; _ } -> - let st, l = Typer.formulas st ~input ~loc:c.S.loc ~attrs:c.S.attrs l in - st, `Continue (simple (prove_id c) c.S.loc (`Solve l)) - - (* Hypotheses & Goals *) - | { S.descr = S.Clause l; _ } -> - let st, res = Typer.formulas st ~input ~loc:c.S.loc ~attrs:c.S.attrs l in - let stmt : typechecked stmt = simple (hyp_id c) c.S.loc (`Clause res) in - st, `Continue stmt - | { S.descr = S.Antecedent t; _ } -> - let st, ret = Typer.formula st ~input ~loc:c.S.loc ~attrs:c.S.attrs ~goal:false t in - let stmt : typechecked stmt = simple (hyp_id c) c.S.loc (`Hyp ret) in - st, `Continue stmt - | { S.descr = S.Consequent t; _ } -> - let st, ret = Typer.formula st ~input ~loc:c.S.loc ~attrs:c.S.attrs ~goal:true t in - let stmt : typechecked stmt = simple (goal_id c) c.S.loc (`Goal ret) in - st, `Continue stmt - - (* Other set_logics should check whether corresponding plugins are activated ? *) - | { S.descr = S.Set_logic s; _ } -> - let st = Typer.set_logic st ~input ~loc:c.S.loc s in - st, `Continue (simple (other_id c) c.S.loc (`Set_logic s)) - - (* Set/Get info *) - | { S.descr = S.Get_info s; _ } -> - st, `Continue (simple (other_id c) c.S.loc (`Get_info s)) - | { S.descr = S.Set_info t; _ } -> - st, `Continue (simple (other_id c) c.S.loc (`Set_info t)) - - (* Set/Get options *) - | { S.descr = S.Get_option s; _ } -> - st, `Continue (simple (other_id c) c.S.loc (`Get_option s)) - | { S.descr = S.Set_option t; _ } -> - st, `Continue (simple (other_id c) c.S.loc (`Set_option t)) - - (* Declarations and definitions *) - | { S.descr = S.Defs d; _ } -> - let st, l = Typer.defs ~mode:`Create_id st ~input ~loc:c.S.loc ~attrs:c.S.attrs d in - let res : typechecked stmt = simple (def_id c) c.S.loc (`Defs l) in - st, `Continue (res) - | { S.descr = S.Decls l; _ } -> - let st, l = Typer.decls st ~input ~loc:c.S.loc ~attrs:c.S.attrs l in - let res : typechecked stmt = simple (decl_id c) c.S.loc (`Decls l) in - st, `Continue (res) - - (* Smtlib's proof/model instructions *) - | { S.descr = S.Get_proof; _ } -> - st, `Continue (simple (other_id c) c.S.loc `Get_proof) - | { S.descr = S.Get_unsat_core; _ } -> - st, `Continue (simple (other_id c) c.S.loc `Get_unsat_core) - | { S.descr = S.Get_unsat_assumptions; _ } -> - st, `Continue (simple (other_id c) c.S.loc `Get_unsat_assumptions) - | { S.descr = S.Get_model; _ } -> - st, `Continue (simple (other_id c) c.S.loc `Get_model) - | { S.descr = S.Get_value l; _ } -> - let st, l = Typer.terms st ~input ~loc:c.S.loc ~attrs:c.S.attrs l in - st, `Continue (simple (other_id c) c.S.loc (`Get_value l)) - | { S.descr = S.Get_assignment; _ } -> - st, `Continue (simple (other_id c) c.S.loc `Get_assignment) - (* Assertions *) - | { S.descr = S.Get_assertions; _ } -> - st, `Continue (simple (other_id c) c.S.loc `Get_assertions) - (* Misc *) - | { S.descr = S.Echo s; _ } -> - st, `Continue (simple (other_id c) c.S.loc (`Echo s)) - | { S.descr = S.Exit; _ } -> - st, `Continue (simple (other_id c) c.S.loc `Exit) - + let st, res = + match normalize st c with + + (* Pack and includes. + These should have been filtered out before this point. + TODO: emit some kind of warning ? *) + | { S.descr = S.Pack _; _ } -> st, `Done () + | { S.descr = S.Include _; _ } -> st, `Done () + + (* State&Assertion stack management *) + | { S.descr = S.Reset; _ } -> + let st = Typer.reset st ~loc:c.S.loc () in + st, `Continue (simple (other_id c) c.S.loc `Reset) + | { S.descr = S.Pop i; _ } -> + let st = Typer.pop st ~input ~loc:c.S.loc i in + st, `Continue (simple (other_id c) c.S.loc (`Pop i)) + | { S.descr = S.Push i; _ } -> + let st = Typer.push st ~input ~loc:c.S.loc i in + st, `Continue (simple (other_id c) c.S.loc (`Push i)) + | { S.descr = S.Reset_assertions; _ } -> + let st = Typer.reset_assertions st ~loc:c.S.loc () in + st, `Continue (simple (other_id c) c.S.loc `Reset_assertions) + + (* Plain statements + TODO: allow the `plain` function to return a meaningful value *) + | { S.descr = S.Plain t; _ } -> + st, `Continue (simple (other_id c) c.S.loc (`Plain t)) + + (* Hypotheses and goal statements *) + | { S.descr = S.Prove l; _ } -> + let st, l = Typer.formulas st ~input ~loc:c.S.loc ~attrs:c.S.attrs l in + st, `Continue (simple (prove_id c) c.S.loc (`Solve l)) + + (* Hypotheses & Goals *) + | { S.descr = S.Clause l; _ } -> + let st, res = Typer.formulas st ~input ~loc:c.S.loc ~attrs:c.S.attrs l in + let stmt : typechecked stmt = simple (hyp_id c) c.S.loc (`Clause res) in + st, `Continue stmt + | { S.descr = S.Antecedent t; _ } -> + let st, ret = Typer.formula st ~input ~loc:c.S.loc ~attrs:c.S.attrs ~goal:false t in + let stmt : typechecked stmt = simple (hyp_id c) c.S.loc (`Hyp ret) in + st, `Continue stmt + | { S.descr = S.Consequent t; _ } -> + let st, ret = Typer.formula st ~input ~loc:c.S.loc ~attrs:c.S.attrs ~goal:true t in + let stmt : typechecked stmt = simple (goal_id c) c.S.loc (`Goal ret) in + st, `Continue stmt + + (* Other set_logics should check whether corresponding plugins are activated ? *) + | { S.descr = S.Set_logic s; _ } -> + let st = Typer.set_logic st ~input ~loc:c.S.loc s in + st, `Continue (simple (other_id c) c.S.loc (`Set_logic s)) + + (* Set/Get info *) + | { S.descr = S.Get_info s; _ } -> + st, `Continue (simple (other_id c) c.S.loc (`Get_info s)) + | { S.descr = S.Set_info t; _ } -> + st, `Continue (simple (other_id c) c.S.loc (`Set_info t)) + + (* Set/Get options *) + | { S.descr = S.Get_option s; _ } -> + st, `Continue (simple (other_id c) c.S.loc (`Get_option s)) + | { S.descr = S.Set_option t; _ } -> + st, `Continue (simple (other_id c) c.S.loc (`Set_option t)) + + (* Declarations and definitions *) + | { S.descr = S.Defs d; _ } -> + let st, l = Typer.defs ~mode:`Create_id st ~input ~loc:c.S.loc ~attrs:c.S.attrs d in + let res : typechecked stmt = simple (def_id c) c.S.loc (`Defs l) in + st, `Continue (res) + | { S.descr = S.Decls l; _ } -> + let st, l = Typer.decls st ~input ~loc:c.S.loc ~attrs:c.S.attrs l in + let res : typechecked stmt = simple (decl_id c) c.S.loc (`Decls l) in + st, `Continue (res) + + (* Smtlib's proof/model instructions *) + | { S.descr = S.Get_proof; _ } -> + st, `Continue (simple (other_id c) c.S.loc `Get_proof) + | { S.descr = S.Get_unsat_core; _ } -> + st, `Continue (simple (other_id c) c.S.loc `Get_unsat_core) + | { S.descr = S.Get_unsat_assumptions; _ } -> + st, `Continue (simple (other_id c) c.S.loc `Get_unsat_assumptions) + | { S.descr = S.Get_model; _ } -> + st, `Continue (simple (other_id c) c.S.loc `Get_model) + | { S.descr = S.Get_value l; _ } -> + let st, l = Typer.terms st ~input ~loc:c.S.loc ~attrs:c.S.attrs l in + st, `Continue (simple (other_id c) c.S.loc (`Get_value l)) + | { S.descr = S.Get_assignment; _ } -> + st, `Continue (simple (other_id c) c.S.loc `Get_assignment) + (* Assertions *) + | { S.descr = S.Get_assertions; _ } -> + st, `Continue (simple (other_id c) c.S.loc `Get_assertions) + (* Misc *) + | { S.descr = S.Echo s; _ } -> + st, `Continue (simple (other_id c) c.S.loc (`Echo s)) + | { S.descr = S.Exit; _ } -> + st, `Continue (simple (other_id c) c.S.loc `Exit) + in + let st = Stats.record_typed st counter c.S.loc in + st, res in res diff --git a/src/loop/typer.mli b/src/loop/typer.mli index 26f467ef6..538749221 100644 --- a/src/loop/typer.mli +++ b/src/loop/typer.mli @@ -63,6 +63,8 @@ module Make and type term_cst := Expr.term_cst and type formula := Expr.formula) (State : State.S) + (Stats : Stats.S + with type state := State.t) (Typer : Typer with type state := State.t and type ty := Expr.ty diff --git a/src/lsp/loop.ml b/src/lsp/loop.ml index 67a6f88cd..a42d2c8ef 100644 --- a/src/lsp/loop.ml +++ b/src/lsp/loop.ml @@ -3,10 +3,13 @@ module Pipeline = Dolmen_loop.Pipeline.Make(State) -module Parser = Dolmen_loop.Parser.Make(State) +module Stats = Dolmen_loop.Stats.Make(State) +module Parser = Dolmen_loop.Parser.Make(State)(Stats) module Header = Dolmen_loop.Headers.Make(State) module Typer = Dolmen_loop.Typer.Typer(State) -module Typer_Pipe = Dolmen_loop.Typer.Make(Dolmen.Std.Expr)(Dolmen.Std.Expr.Print)(State)(Typer) +module Typer_Pipe = + Dolmen_loop.Typer.Make + (Dolmen.Std.Expr)(Dolmen.Std.Expr.Print)(State)(Stats)(Typer) exception Finished of (State.t, string) result @@ -64,6 +67,10 @@ let process prelude path opt_contents = ~header_check:false ~header_licenses:[] ~header_lang_version:None + |> Stats.init + ~enabled:false + ~typing:false + ~model:false in try let st, g = Parser.parse_logic prelude st l_file in diff --git a/src/standard/loc.ml b/src/standard/loc.ml index 181f0a131..791c95b78 100644 --- a/src/standard/loc.ml +++ b/src/standard/loc.ml @@ -105,6 +105,19 @@ let mk_compact offset length = (Obj.magic e : t) end +let first_byte c = + let start, _ = split_compact c in + start + +let last_byte c = + let start, offset = split_compact c in + start + offset (* +1 ? *) + +let length_in_bytes c = + let _, offset = split_compact c in + offset + 1 + + (* File table *) (* ************************************************************************* *) diff --git a/src/standard/loc.mli b/src/standard/loc.mli index 0383f6240..dfe567d62 100644 --- a/src/standard/loc.mli +++ b/src/standard/loc.mli @@ -58,6 +58,18 @@ val is_dummy : loc -> bool (** Is the location an actual location, or a dummy one ? *) +(** {2 Compact location info} *) + +val first_byte : t -> int +(** The offset of the first byte that makes up the location. *) + +val last_byte : t -> int +(** The offset of the last byte that makes up the location. *) + +val length_in_bytes : t -> int +(** The number of bytes covered by a location. *) + + (** {2 Compact location handling} *) val mk_file : string -> file @@ -77,7 +89,7 @@ val compact : loc -> file * t (** Compactify a full location into a compact representation. *) val lexing_positions : loc -> Lexing.position * Lexing.position -(** Reutnr the pari of lexing positions corresponding to a location. *) +(** Return the pair of lexing positions corresponding to a location. *) (** {2 Printing locations} *) From d46b179f564759effabdae91b5c3f336c4f3a5be Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Wed, 16 Nov 2022 13:14:19 +0100 Subject: [PATCH 02/17] opam file --- dolmen_loop.opam | 1 + 1 file changed, 1 insertion(+) diff --git a/dolmen_loop.opam b/dolmen_loop.opam index 0301ec254..5647a86ed 100644 --- a/dolmen_loop.opam +++ b/dolmen_loop.opam @@ -16,6 +16,7 @@ depends: [ "gen" "odoc" { with-doc } "pp_loc" { >= "2.0.0" } + "progress" ] tags: [ "logic" "computation" "automated theorem prover" ] homepage: "https://github.com/Gbury/dolmen" From ce95b442beed72e479ea5d58f44f29ded6c820d5 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Wed, 16 Nov 2022 13:27:19 +0100 Subject: [PATCH 03/17] Fix errors --- src/loop/parser.ml | 62 ++++++++++++++++++++++++++-------------------- src/loop/stats.ml | 20 +++++++-------- 2 files changed, 45 insertions(+), 37 deletions(-) diff --git a/src/loop/parser.ml b/src/loop/parser.ml index 292584758..9bec34329 100644 --- a/src/loop/parser.ml +++ b/src/loop/parser.ml @@ -156,35 +156,40 @@ module Make in aux - let wrap_parser ?input ~loc_of_res ~file g = fun st -> - begin match (State.get interactive_prompt st) st with - | None -> () - | Some prelude -> Format.printf "%s @?" prelude - end; - let counter = Stats.start_counter st in - match g () with - | None -> - let st = Stats.record_parsed st input counter Dolmen.Std.Loc.no_loc in - st, None - | Some res as ret -> - let st = Stats.record_parsed st input counter (loc_of_res res) in - st, ret - | exception Dolmen.Std.Loc.Uncaught (loc, exn, bt) -> + let wrap_exn st file input counter = function + | Dolmen.Std.Loc.Uncaught (loc, exn, bt) -> let st = Stats.record_parsed st input counter loc in let st = State.error st ~file ~loc:{ file = file.loc; loc; } Report.Error.uncaught_exn (exn, bt) in st, None - | exception Dolmen.Std.Loc.Lexing_error (loc, lex) -> + | Dolmen.Std.Loc.Lexing_error (loc, lex) -> let st = Stats.record_parsed st input counter loc in let st = State.error st ~file ~loc:{ file = file.loc; loc; } lexing_error lex in st, None - | exception Dolmen.Std.Loc.Syntax_error (loc, perr) -> + | Dolmen.Std.Loc.Syntax_error (loc, perr) -> let st = Stats.record_parsed st input counter loc in let syntax_error_ref = State.get_or ~default:false syntax_error_ref st in let st = State.error st ~file ~loc:{ file = file.loc; loc; } parsing_error (syntax_error_ref, perr) in st, None + | exn -> raise exn + + let wrap_parser ?input ~loc_of_res ~file g = fun st -> + begin match (State.get interactive_prompt st) st with + | None -> () + | Some prelude -> Format.printf "%s @?" prelude + end; + let counter = Stats.start_counter st in + match g () with + | None -> + let st = Stats.record_parsed st input counter Dolmen.Std.Loc.no_loc in + st, None + | Some res as ret -> + let st = Stats.record_parsed st input counter (loc_of_res res) in + st, ret + | exception exn -> + wrap_exn st file input counter exn let wrap_lazy_list ?input ~loc_of_res ~file llist = let first = ref true in @@ -193,17 +198,20 @@ module Make if !first then begin first := false; let counter = Stats.start_counter st in - let list = Lazy.force llist in - l := list; - (* record the sizes of statements parsed *) - let st = - List.fold_left (fun st res -> - Stats.record_parsed st input None (loc_of_res res) - ) st list - in - (* record the time spent parsing *) - let st = Stats.record_parsed st input counter Dolmen.Std.Loc.no_loc in - aux st + try + let list = Lazy.force llist in + l := list; + (* record the sizes of statements parsed *) + let st = + List.fold_left (fun st res -> + Stats.record_parsed st input None (loc_of_res res) + ) st list + in + (* record the time spent parsing *) + let st = Stats.record_parsed st input counter Dolmen.Std.Loc.no_loc in + aux st + with exn -> + wrap_exn st file input None exn end else begin let elt = match !l with diff --git a/src/loop/stats.ml b/src/loop/stats.ml index eb92ad4b9..86f5bc6b4 100644 --- a/src/loop/stats.ml +++ b/src/loop/stats.ml @@ -266,17 +266,17 @@ module Make(State : State.S) = struct let finalise st = let config = config st in - if config.typing then begin - let typing = State.get typing_key st in - let () = Unix.sleepf (1. /. 60.) in - Progress.Reporter.report typing.reporter typing.stats - end; - if config.model then begin - let model = State.get model_key st in - let () = Unix.sleepf (1. /. 60.) in - Progress.Reporter.report model.reporter model.stats - end; if config.enabled then begin + if config.typing then begin + let typing = State.get typing_key st in + let () = Unix.sleepf (1. /. 60.) in + Progress.Reporter.report typing.reporter typing.stats + end; + if config.model then begin + let model = State.get model_key st in + let () = Unix.sleepf (1. /. 60.) in + Progress.Reporter.report model.reporter model.stats + end; let parsing = State.get parsing_key st in Array.iter2 (fun stats reporter -> let () = Unix.sleepf (1. /. 60.) in From cc6510ea3d70cb3c6c628bc3a064a716c23355bc Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Fri, 18 Nov 2022 13:39:48 +0100 Subject: [PATCH 04/17] Progress bars are working well --- dolmen_loop.opam | 1 + src/bin/loop.ml | 2 +- src/bin/main.ml | 1 - src/bin/options.ml | 14 ++- src/loop/dune | 2 +- src/loop/stats.ml | 197 +++++++++++++++++++++++++++-------------- src/loop/stats_intf.ml | 7 +- src/loop/typer.ml | 5 +- src/loop/typer.mli | 2 + src/loop/typer_intf.ml | 41 ++++----- src/lsp/loop.ml | 3 + src/model/loop.ml | 81 +++++++++++------ 12 files changed, 226 insertions(+), 130 deletions(-) diff --git a/dolmen_loop.opam b/dolmen_loop.opam index 5647a86ed..19190ebec 100644 --- a/dolmen_loop.opam +++ b/dolmen_loop.opam @@ -17,6 +17,7 @@ depends: [ "odoc" { with-doc } "pp_loc" { >= "2.0.0" } "progress" + "terminal" ] tags: [ "logic" "computation" "automated theorem prover" ] homepage: "https://github.com/Gbury/dolmen" diff --git a/src/bin/loop.ml b/src/bin/loop.ml index 98c243dba..565fae0e1 100644 --- a/src/bin/loop.ml +++ b/src/bin/loop.ml @@ -9,4 +9,4 @@ module Parser = Dolmen_loop.Parser.Make(State)(Stats) module Header = Dolmen_loop.Headers.Make(State) module Typer = Dolmen_loop.Typer.Typer(State) module Typer_Pipe = Dolmen_loop.Typer.Make(Dolmen.Std.Expr)(Dolmen.Std.Expr.Print)(State)(Stats)(Typer) -module Check = Dolmen_model.Loop.Make(State)(Parser)(Typer)(Typer_Pipe) +module Check = Dolmen_model.Loop.Make(State)(Stats)(Parser)(Typer)(Typer_Pipe) diff --git a/src/bin/main.ml b/src/bin/main.ml index 1618cf2bc..0c62ae00c 100644 --- a/src/bin/main.ml +++ b/src/bin/main.ml @@ -24,7 +24,6 @@ let debug_typed_pipe st stmt = (* ************************ *) let handle_exn st exn = - Loop.Stats.finalise st; let _st = Errors.exn st exn in exit 125 diff --git a/src/bin/options.ml b/src/bin/options.ml index 9d279c29e..029445a17 100644 --- a/src/bin/options.ml +++ b/src/bin/options.ml @@ -324,7 +324,7 @@ let mk_run_state header_lang_version smtlib2_forced_logic type_check check_model debug report_style max_warn reports syntax_error_ref - progress_enabled + progress_enabled progress_mem = (* Side-effects *) let () = Option.iter Gc.set gc_opt in @@ -354,6 +354,8 @@ let mk_run_state ~header_licenses ~header_lang_version |> Loop.Stats.init + ~mem:progress_mem + ~max_mem:(int_of_float size_limit) ~enabled:progress_enabled ~typing:type_check ~model:check_model @@ -522,7 +524,7 @@ let state = let size = let doc = "Stop the program if it tries and use more the $(docv) memory space. " ^ "Accepts usual suffixes for sizes : k,M,G,T. " ^ - "Without suffix, default to a size in octet." in + "Without suffix, default to a size in bytes/octet." in Arg.(value & opt c_size 1_000_000_000. & info ["s"; "size"] ~docv:"SIZE" ~doc ~docs) in @@ -593,6 +595,12 @@ let state = let doc = Format.asprintf "Print progress information." in Arg.(value & opt bool false & info ["progress"] ~doc ~docs:profiling_section) in + let progress_mem = + let doc = Format.asprintf + "Compute memory usage in progress info. Note that this may slow \ + down dolmen significantly (experiments suggest around 3x)." in + Arg.(value & opt bool false & info ["progress-mem"] ~doc ~docs:profiling_section) + in Term.(const mk_run_state $ profiling_t $ gc $ gc_t $ bt $ colors $ abort_on_bug $ @@ -602,7 +610,7 @@ let state = header_lang_version $ force_smtlib2_logic $ typing $ check_model $ debug $ report_style $ max_warn $ reports $ syntax_error_ref $ - progress_enabled) + progress_enabled $ progress_mem) (* List command term *) diff --git a/src/loop/dune b/src/loop/dune index 6eb90ce93..fe9c874e8 100644 --- a/src/loop/dune +++ b/src/loop/dune @@ -4,7 +4,7 @@ (instrumentation (backend bisect_ppx)) (libraries ; External deps - gen unix fmt pp_loc progress + gen unix fmt pp_loc terminal progress ; main dolmen deps , with versioned languages deps dolmen dolmen.intf dolmen.std dolmen.class diff --git a/src/loop/stats.ml b/src/loop/stats.ml index 86f5bc6b4..dbfb59b01 100644 --- a/src/loop/stats.ml +++ b/src/loop/stats.ml @@ -8,6 +8,11 @@ let file_size file_path = let st = Unix.stat file_path in st.st_size +let obj_size obj = + let in_words = Obj.reachable_words (Obj.repr obj) in + let in_bytes = in_words * (Sys.word_size / 8) in + in_bytes + (* Custom progress bar *) (* ************************************************************************* *) @@ -16,21 +21,27 @@ let percentage_printer = ~string_len:4 ~to_string:(fun p -> Format.asprintf "%3d%%" p) -module Bytes_stats = struct +module Aux = struct type t = { - total_bytes : int; - processed_bytes : int; - elapsed_time : Mtime.span; + total_bytes : int; (* total bytes to process *) + processed_bytes : int; (* processed bytes *) + elapsed_time : Mtime.span; (* time spent processing *) + max_mem : int; (* memory limit *) + cur_mem : int; (* memory currently used *) + last_mem : Mtime.span; (* last span that cur memory was computed *) } - let zero = { + let zero max_mem = { total_bytes = 0; processed_bytes = 0; elapsed_time = Mtime.Span.zero; + max_mem; + cur_mem = 0; + last_mem = Mtime.Span.zero; } - let input total_bytes = { zero with total_bytes } + let input max_mem total_bytes = { (zero max_mem) with total_bytes } let total_bytes { total_bytes; _ } = total_bytes let elapsed_time { elapsed_time; _ } = elapsed_time @@ -39,17 +50,29 @@ module Bytes_stats = struct int_of_float (100. *. (float processed_bytes) /. (float total_bytes)) let perthousand { processed_bytes; total_bytes; _ } = int_of_float (1000. *. (float processed_bytes) /. (float total_bytes)) - - let line phase : t Progress.Line.t = + let cur_mem { cur_mem; _ } = cur_mem + let ratio_mem { cur_mem; max_mem; _ } = + int_of_float (1000. *. (float cur_mem) /. (float max_mem)) + + let line ~mem phase : t Progress.Line.t = + let process_width, mem_width = + match Terminal.Size.get_columns () with + | None -> `Expand, `Fixed 20 + | Some w -> `Expand, `Fixed (w - 170) + in let open Progress.Line in list [ - using (fun _ -> phase) (of_printer ~init:phase (Progress.Printer.string ~width:50)); + using (fun _ -> phase) (of_printer ~init:phase (Progress.Printer.string ~width:20)); using elapsed_time (of_printer ~init:Mtime.Span.zero Progress.Units.Duration.mm_ss); using processed_bytes (of_printer ~init:0 Progress.Units.Bytes.of_int); + const "/"; using total_bytes (of_printer ~init:0 Progress.Units.Bytes.of_int); (* TODO: add bytes/seconds *) - using perthousand (bar ~data:`Latest 1000); + using perthousand (bar ~width:process_width ~data:`Latest 1000); using percentage (of_printer ~init:0 percentage_printer); + if mem then const "|" else noop (); + if mem then using cur_mem (of_printer ~init:0 Progress.Units.Bytes.of_int) else noop (); + if mem then using ratio_mem (bar ~width:mem_width ~data:`Latest 1000) else noop (); ] end @@ -64,6 +87,8 @@ module Make(State : State.S) = struct (* type *) type config = { + mem : bool; + max_mem : int; enabled : bool; typing : bool; model : bool; @@ -72,18 +97,18 @@ module Make(State : State.S) = struct type input = int type counter = Mtime_clock.counter type parsing = { - stats : Bytes_stats.t array; - reporters : Bytes_stats.t Progress.Reporter.t array; + stats : Aux.t array; + reporters : Aux.t Progress.Reporter.t array; } type typing = { - stats : Bytes_stats.t; - reporter : Bytes_stats.t Progress.Reporter.t; + stats : Aux.t; + reporter : Aux.t Progress.Reporter.t; } type model = { - stats : Bytes_stats.t; - reporter : Bytes_stats.t Progress.Reporter.t; + stats : Aux.t; + reporter : Aux.t Progress.Reporter.t; } @@ -106,15 +131,17 @@ module Make(State : State.S) = struct (* state init *) - let init ~enabled ~typing ~model st = - let config = { enabled; typing; model; } in + let init ~mem ~max_mem ~enabled ~typing ~model st = + let config = { mem; max_mem; enabled; typing; model; } in let st = State.set config_key config st in if not enabled then st else begin (* create progress display *) - let config = Progress.Config.v () in - let multi = Progress.Multi.blank in - let display = Progress.Display.start ~config multi in + let display = + let config = Progress.Config.v () in + let multi = Progress.Multi.blank in + Progress.Display.start ~config multi + in let st = State.set State.progress_display display st in (* create bars *) let st = @@ -129,8 +156,8 @@ module Make(State : State.S) = struct if not typing then st else begin let typing : typing = - let stats = Bytes_stats.zero in - let line = Bytes_stats.line "typing" in + let stats = Aux.zero max_mem in + let line = Aux.line ~mem:config.mem "typing" in let reporter = Progress.Display.add_line display line in { stats; reporter; } in @@ -141,8 +168,8 @@ module Make(State : State.S) = struct if not model then st else begin let model : model = - let stats = Bytes_stats.zero in - let line = Bytes_stats.line "model" in + let stats = Aux.zero max_mem in + let line = Aux.line ~mem:config.mem "model" in let reporter = Progress.Display.add_line display line in { stats; reporter; } in @@ -168,9 +195,9 @@ module Make(State : State.S) = struct let display = State.get State.progress_display st in let n = Array.length parsing.stats in assert (n = Array.length parsing.reporters); - let z = Bytes_stats.input input_size in - let line_name = Format.asprintf "parsing (%s)" input_name in - let line = Bytes_stats.line line_name in + let z = Aux.input config.max_mem input_size in + let line_name = Format.asprintf "%s" input_name in + let line = Aux.line ~mem:false line_name in let above = (if config.model then 1 else 0 (* model *)) + (if config.typing then 1 else 0 (* typing *)) + @@ -189,59 +216,64 @@ module Make(State : State.S) = struct match input with | None -> st | Some input -> - let span = - match counter with - | None -> Mtime.Span.zero - | Some counter -> Mtime_clock.count counter - in - let config = config st in - if config.enabled then begin - (* record the loc as parsed *) - let st = - let parsing = State.get parsing_key st in - let input_stats = parsing.stats.(input) in - let input_reporter = parsing.reporters.(input) in - let elapsed_time = Mtime.Span.add span input_stats.elapsed_time in - let processed_bytes = max input_stats.processed_bytes (Dolmen.Std.Loc.last_byte loc) in - let input_stats = { input_stats with elapsed_time; processed_bytes; } in - let () = Progress.Reporter.report input_reporter input_stats in - let stats = Array.copy parsing.stats in - let () = Array.set stats input input_stats in - let parsing = { parsing with stats } in - State.set parsing_key parsing st - in - (* add the loc to be typed *) - let st = - if not config.typing then st - else begin - let bytes_to_type = Dolmen.Std.Loc.length_in_bytes loc in - let typing = State.get typing_key st in - let total_bytes = typing.stats.total_bytes + bytes_to_type in - let stats = { typing.stats with total_bytes } in - let typing = { typing with stats } in - let () = Progress.Reporter.report typing.reporter stats in - State.set typing_key typing st - end - in - st - end else - st + begin match counter with + | None -> st + | Some counter -> + let span = Mtime_clock.count counter in + let config = config st in + assert config.enabled; + (* record the loc as parsed *) + let st = + let parsing = State.get parsing_key st in + let input_stats = parsing.stats.(input) in + let input_reporter = parsing.reporters.(input) in + let elapsed_time = Mtime.Span.add span input_stats.elapsed_time in + let processed_bytes = max input_stats.processed_bytes (Dolmen.Std.Loc.last_byte loc) in + let input_stats = { input_stats with elapsed_time; processed_bytes; } in + let () = Progress.Reporter.report input_reporter input_stats in + let stats = Array.copy parsing.stats in + let () = Array.set stats input input_stats in + let parsing = { parsing with stats } in + State.set parsing_key parsing st + in + (* add the loc to be typed *) + let st = + if not config.typing then st + else begin + let bytes_to_type = Dolmen.Std.Loc.length_in_bytes loc in + let typing = State.get typing_key st in + let total_bytes = typing.stats.total_bytes + bytes_to_type in + let stats = { typing.stats with total_bytes } in + let typing = { typing with stats } in + let () = Progress.Reporter.report typing.reporter stats in + State.set typing_key typing st + end + in + st + end - let record_typed st counter loc = + let record_typed st counter loc persistent_data = match counter with | None -> st | Some counter -> let span = Mtime_clock.count counter in let config = config st in + assert (config.enabled); (* record the loc as typed *) let st = if not config.typing then st else begin - let processed = Dolmen.Std.Loc.length_in_bytes loc in let typing = State.get typing_key st in + let processed = Dolmen.Std.Loc.length_in_bytes loc in let elapsed_time = Mtime.Span.add span typing.stats.elapsed_time in + let cur_mem = + if config.mem && Mtime.Span.to_s + (Mtime.Span.abs_diff elapsed_time typing.stats.last_mem) >= 0.5 + then obj_size persistent_data + else typing.stats.cur_mem + in let processed_bytes = typing.stats.processed_bytes + processed in - let stats = { typing.stats with elapsed_time; processed_bytes; } in + let stats = { typing.stats with elapsed_time; processed_bytes; cur_mem; } in let typing = { typing with stats } in let () = Progress.Reporter.report typing.reporter stats in State.set typing_key typing st @@ -262,6 +294,35 @@ module Make(State : State.S) = struct in st + let record_checked st counter loc persistent_data = + match counter with + | None -> st + | Some counter -> + let span = Mtime_clock.count counter in + let config = config st in + assert (config.enabled); + (* record the loc as typed *) + let st = + if not config.model then st + else begin + let model = State.get model_key st in + let cur_mem = + if not config.mem then model.stats.cur_mem + else match persistent_data with + | `Set obj -> obj_size obj + | `Add obj -> model.stats.cur_mem + obj_size obj + in + let processed = Dolmen.Std.Loc.length_in_bytes loc in + let elapsed_time = Mtime.Span.add span model.stats.elapsed_time in + let processed_bytes = model.stats.processed_bytes + processed in + let stats = { model.stats with elapsed_time; processed_bytes; cur_mem; } in + let model = { model with stats } in + let () = Progress.Reporter.report model.reporter stats in + State.set model_key model st + end + in + st + (* finalisation *) let finalise st = diff --git a/src/loop/stats_intf.ml b/src/loop/stats_intf.ml index fdd81a2d5..4dba58fa5 100644 --- a/src/loop/stats_intf.ml +++ b/src/loop/stats_intf.ml @@ -13,6 +13,8 @@ module type S = sig (** Time counter *) val init : + mem: bool -> + max_mem:int -> enabled:bool -> typing:bool -> model:bool -> @@ -28,7 +30,10 @@ module type S = sig val record_parsed : state -> input option -> counter option -> Dolmen.Std.Loc.t -> state (** *) - val record_typed : state -> counter option -> Dolmen.Std.Loc.t -> state + val record_typed : state -> counter option -> Dolmen.Std.Loc.t -> 'a -> state + (** *) + + val record_checked : state -> counter option -> Dolmen.Std.Loc.t -> [ `Add of 'a | `Set of 'a] -> state (** *) val finalise : state -> unit diff --git a/src/loop/typer.ml b/src/loop/typer.ml index 8a5f2ef86..aed03f947 100644 --- a/src/loop/typer.ml +++ b/src/loop/typer.ml @@ -1740,6 +1740,7 @@ module Make with type state := State.t) (Typer : Typer with type state := State.t + and type 'a key := 'a State.key and type ty := Expr.ty and type ty_var := Expr.ty_var and type ty_cst := Expr.ty_cst @@ -1763,6 +1764,8 @@ module Make (* Types used in Pipes *) (* ************************************************************************ *) + type ty_state = Typer.ty_state + (* Used for representing typed statements *) type +'a stmt = { id : Dolmen.Std.Id.t; @@ -2040,7 +2043,7 @@ module Make | { S.descr = S.Exit; _ } -> st, `Continue (simple (other_id c) c.S.loc `Exit) in - let st = Stats.record_typed st counter c.S.loc in + let st = Stats.record_typed st counter c.S.loc (State.get Typer.ty_state st) in st, res in res diff --git a/src/loop/typer.mli b/src/loop/typer.mli index 538749221..9a3f2a202 100644 --- a/src/loop/typer.mli +++ b/src/loop/typer.mli @@ -67,6 +67,7 @@ module Make with type state := State.t) (Typer : Typer with type state := State.t + and type 'a key := 'a State.key and type ty := Expr.ty and type ty_var := Expr.ty_var and type ty_cst := Expr.ty_cst @@ -76,6 +77,7 @@ module Make and type formula := Expr.formula) : S with type state := State.t and type 'a key := 'a State.key + and type ty_state = Typer.ty_state and type ty := Expr.ty and type ty_var := Expr.ty_var and type ty_cst := Expr.ty_cst diff --git a/src/loop/typer_intf.ml b/src/loop/typer_intf.ml index 4d80a449f..c81e06932 100644 --- a/src/loop/typer_intf.ml +++ b/src/loop/typer_intf.ml @@ -4,6 +4,9 @@ module type Types = sig type state + type 'a key + type ty_state + type ty type ty_var type ty_cst @@ -23,6 +26,9 @@ module type Typer = sig include Types + val ty_state : ty_state key + (** Key to store the local typechecking state in the global pipeline state. *) + type input = [ | `Logic of Logic.language State.file | `Response of Response.language State.file @@ -80,14 +86,16 @@ end (** Extended signature for typer. *) module type Typer_Full = sig - type state - (** Global state for the while pipeline. *) - - type 'a key - (** Type of keys for the state. *) - - type ty_state - (** The type for the state of the typer. *) + include Typer + with type ty := Dolmen.Std.Expr.ty + and type ty_var := Dolmen.Std.Expr.ty_var + and type ty_cst := Dolmen.Std.Expr.ty_cst + and type term := Dolmen.Std.Expr.term + and type term_var := Dolmen.Std.Expr.term_var + and type term_cst := Dolmen.Std.Expr.term_cst + and type formula := Dolmen.Std.Expr.formula + (** This signature includes the requirements to instantiate the {Pipes.Make: + functor*) type env (** The type of the typechecker environment. *) @@ -104,9 +112,6 @@ module type Typer_Full = sig type builtin_symbols (** The type of builin symbols for the type-checker. *) - val ty_state : ty_state key - (** Key to store the local typechecking state in the global pipeline state. *) - val check_model : bool key (** The typechecker needs to know whether we are checking models or not. *) @@ -118,18 +123,6 @@ module type Typer_Full = sig ?smtlib2_forced_logic:string option -> state -> state - include Typer - with type state := state - and type ty := Dolmen.Std.Expr.ty - and type ty_var := Dolmen.Std.Expr.ty_var - and type ty_cst := Dolmen.Std.Expr.ty_cst - and type term := Dolmen.Std.Expr.term - and type term_var := Dolmen.Std.Expr.term_var - and type term_cst := Dolmen.Std.Expr.term_cst - and type formula := Dolmen.Std.Expr.formula - (** This signature includes the requirements to instantiate the {Pipes.Make: - functor*) - val report_error : input:input -> state -> error -> state (** Report a typing error by calling the appropriate state function. *) @@ -151,8 +144,6 @@ module type S = sig include Types - type 'a key - val type_check : bool key val init : diff --git a/src/lsp/loop.ml b/src/lsp/loop.ml index a42d2c8ef..cb69aa052 100644 --- a/src/lsp/loop.ml +++ b/src/lsp/loop.ml @@ -68,9 +68,12 @@ let process prelude path opt_contents = ~header_licenses:[] ~header_lang_version:None |> Stats.init + ~mem:false + ~max_mem:0 ~enabled:false ~typing:false ~model:false + |> (fun (st : State.t) -> st) in try let st, g = Parser.parse_logic prelude st l_file in diff --git a/src/model/loop.ml b/src/model/loop.ml index 3be73c5a1..f75091a4c 100644 --- a/src/model/loop.ml +++ b/src/model/loop.ml @@ -151,6 +151,8 @@ type 'a file = 'a Dolmen_loop.State.file module Make (State : Dolmen_loop.State.S) + (Stats : Dolmen_loop.Stats.S + with type state := State.t) (Parse : Dolmen_loop.Parser.S with type state := State.t and type 'a key := 'a State.key) @@ -331,23 +333,34 @@ module Make Value.extract_exn ~ops:Bool.ops value let eval_def { file; loc; contents = defs; } st = - List.fold_left (fun st (cst, func) -> + let counter = Stats.start_counter st in + let st = + List.fold_left (fun st (cst, func) -> let value = eval st ~file ~loc func in define_value st cst value - ) st defs + ) st defs + in + let st = Stats.record_checked st counter loc.loc (`Add 0) in + st let eval_hyp st { file; loc; contents = hyp; } = + let counter = Stats.start_counter st in let res = eval_term st ~file ~loc hyp in + let st = Stats.record_checked st counter loc.loc (`Add 0) in if res then st else State.error ~file ~loc st bad_model `Hyp let eval_goal st { file; loc; contents = goal; } = + let counter = Stats.start_counter st in let res = eval_term st ~file ~loc goal in + let st = Stats.record_checked st counter loc.loc (`Add 0) in if not res then st else State.error ~file ~loc st bad_model `Goal let eval_clause st { file; loc; contents = clause; } = + let counter = Stats.start_counter st in let l = List.map (eval_term st ~file ~loc) clause in + let st = Stats.record_checked st counter loc.loc (`Add 0) in if List.exists (fun x -> x) l then st else State.error ~file ~loc st bad_model `Clause @@ -368,38 +381,48 @@ module Make let check st (c : Typer_Pipe.typechecked Typer_Pipe.stmt) = let st = if State.get check_model st then + let counter = Stats.start_counter st in let t = State.get check_state st in let file = State.get State.logic_file st in let loc = Dolmen.Std.Loc.{ file = file.loc; loc = c.loc; } in match c.contents with | #Typer_Pipe.exit - | #Typer_Pipe.decls - | #Typer_Pipe.get_info - | #Typer_Pipe.set_info -> st - | #Typer_Pipe.stack_control -> - State.error ~file ~loc st assertion_stack_not_supported () - | `Defs defs -> - let new_defs = pack_abstract_defs ~file ~loc defs in - State.set check_state { t with defs = new_defs :: t.defs; } st - | `Hyp contents -> - let assertion = { file; loc; contents; } in - State.set check_state { t with hyps = assertion :: t.hyps; } st - | `Goal contents -> - let assertion = { file; loc; contents; } in - State.set check_state { t with goals = assertion :: t.goals; } st - | `Clause contents -> - let assertion = { file; loc; contents; } in - State.set check_state { t with clauses = assertion :: t.clauses; } st - | `Solve l -> - begin match get_answer st with - | _, None -> - State.error ~file ~loc st missing_answer () - | st, Some answer -> - let local_hyps = List.map (fun contents -> { file; loc; contents; }) l in - let t = { t with hyps = local_hyps @ t.hyps; } in - let st = check_aux st t answer in - State.set check_state { t with hyps = []; goals = []; clauses = []; } st - end + | #Typer_Pipe.decls + | #Typer_Pipe.get_info + | #Typer_Pipe.set_info -> + let st = Stats.record_checked st counter c.loc (`Add 0) in + st + | #Typer_Pipe.stack_control -> + State.error ~file ~loc st assertion_stack_not_supported () + | `Defs defs -> + let new_defs = pack_abstract_defs ~file ~loc defs in + let st = Stats.record_checked st counter Dolmen.Std.Loc.no_loc (`Add new_defs) in + State.set check_state { t with defs = new_defs :: t.defs; } st + | `Hyp contents -> + let assertion = { file; loc; contents; } in + let st = Stats.record_checked st counter Dolmen.Std.Loc.no_loc (`Add assertion) in + State.set check_state { t with hyps = assertion :: t.hyps; } st + | `Goal contents -> + let assertion = { file; loc; contents; } in + let st = Stats.record_checked st counter Dolmen.Std.Loc.no_loc (`Add assertion) in + State.set check_state { t with goals = assertion :: t.goals; } st + | `Clause contents -> + let assertion = { file; loc; contents; } in + let st = Stats.record_checked st counter Dolmen.Std.Loc.no_loc (`Add assertion) in + State.set check_state { t with clauses = assertion :: t.clauses; } st + | `Solve l -> + begin match get_answer st with + | _, None -> + State.error ~file ~loc st missing_answer () + | st, Some answer -> + let local_hyps = List.map (fun contents -> { file; loc; contents; }) l in + let t = { t with hyps = local_hyps @ t.hyps; } in + let st = Stats.record_checked st counter Dolmen.Std.Loc.no_loc (`Add local_hyps) in + let st = check_aux st t answer in + let t = { t with defs = []; hyps = []; goals = []; clauses = []; } in + let st = Stats.record_checked st None c.loc (`Set t) in + State.set check_state t st + end else st in From 153893e6dc9b68c364851ef6464c8cf87b3894a2 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Fri, 18 Nov 2022 15:27:13 +0100 Subject: [PATCH 05/17] WIP --- src/loop/stats.ml | 20 +++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) diff --git a/src/loop/stats.ml b/src/loop/stats.ml index dbfb59b01..182f4c58b 100644 --- a/src/loop/stats.ml +++ b/src/loop/stats.ml @@ -58,7 +58,7 @@ module Aux = struct let process_width, mem_width = match Terminal.Size.get_columns () with | None -> `Expand, `Fixed 20 - | Some w -> `Expand, `Fixed (w - 170) + | Some w -> `Expand, `Fixed ((w - 100) / 2) in let open Progress.Line in list [ @@ -68,11 +68,11 @@ module Aux = struct const "/"; using total_bytes (of_printer ~init:0 Progress.Units.Bytes.of_int); (* TODO: add bytes/seconds *) - using perthousand (bar ~width:process_width ~data:`Latest 1000); - using percentage (of_printer ~init:0 percentage_printer); if mem then const "|" else noop (); if mem then using cur_mem (of_printer ~init:0 Progress.Units.Bytes.of_int) else noop (); if mem then using ratio_mem (bar ~width:mem_width ~data:`Latest 1000) else noop (); + using perthousand (bar ~width:process_width ~data:`Latest 1000); + using percentage (of_printer ~init:0 percentage_printer); ] end @@ -266,14 +266,16 @@ module Make(State : State.S) = struct let typing = State.get typing_key st in let processed = Dolmen.Std.Loc.length_in_bytes loc in let elapsed_time = Mtime.Span.add span typing.stats.elapsed_time in - let cur_mem = - if config.mem && Mtime.Span.to_s - (Mtime.Span.abs_diff elapsed_time typing.stats.last_mem) >= 0.5 - then obj_size persistent_data - else typing.stats.cur_mem + let cur_mem, last_mem = + if config.mem && ( + Mtime.Span.equal Mtime.Span.zero typing.stats.elapsed_time + || (Mtime.Span.to_s + (Mtime.Span.abs_diff elapsed_time typing.stats.last_mem) >= 0.3)) + then obj_size persistent_data, elapsed_time + else typing.stats.cur_mem, typing.stats.last_mem in let processed_bytes = typing.stats.processed_bytes + processed in - let stats = { typing.stats with elapsed_time; processed_bytes; cur_mem; } in + let stats = { typing.stats with elapsed_time; processed_bytes; cur_mem; last_mem; } in let typing = { typing with stats } in let () = Progress.Reporter.report typing.reporter stats in State.set typing_key typing st From 3ba363cd3293877dcb5cb7a1bcf576b1ed502dd0 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Mon, 21 Nov 2022 15:16:14 +0100 Subject: [PATCH 06/17] Proper interface for terminal interaction --- src/bin/main.ml | 5 +- src/loop/dune | 2 +- src/loop/parser.ml | 21 +++ src/loop/state.ml | 41 ++---- src/loop/stats.ml | 295 ++++++++--------------------------------- src/loop/stats_intf.ml | 3 - src/loop/tui.ml | 174 ++++++++++++++++++++++++ src/loop/tui.mli | 48 +++++++ 8 files changed, 319 insertions(+), 270 deletions(-) create mode 100644 src/loop/tui.ml create mode 100644 src/loop/tui.mli diff --git a/src/bin/main.ml b/src/bin/main.ml index 0c62ae00c..3c61d4a66 100644 --- a/src/bin/main.ml +++ b/src/bin/main.ml @@ -24,6 +24,7 @@ let debug_typed_pipe st stmt = (* ************************ *) let handle_exn st exn = + let () = Dolmen_loop.Tui.finalise_display () in let _st = Errors.exn st exn in exit 125 @@ -33,7 +34,7 @@ let finally st e = | Some (bt,exn) -> (* Print the backtrace if requested *) if Loop.State.(get bt) st then ( - Format.eprintf "foo ?!@."; + (* TODO: use Tui *) Printexc.print_raw_backtrace stdout bt); handle_exn st exn @@ -62,7 +63,7 @@ let run st = ) ) in - let () = Loop.Stats.finalise st in + let () = Dolmen_loop.Tui.finalise_display () in let st = Loop.Header.check st in let _st = Dolmen_loop.State.flush st () in () diff --git a/src/loop/dune b/src/loop/dune index fe9c874e8..86663e99d 100644 --- a/src/loop/dune +++ b/src/loop/dune @@ -14,7 +14,7 @@ ) (modules ; Useful utilities - Alarm Report + Alarm Tui Report ; Interfaces Expr_intf Parser_intf Typer_intf Headers_intf Stats_intf ; Implementations diff --git a/src/loop/parser.ml b/src/loop/parser.ml index 9bec34329..8b80fda2e 100644 --- a/src/loop/parser.ml +++ b/src/loop/parser.ml @@ -157,6 +157,27 @@ module Make aux let wrap_exn st file input counter = function + | Dolmen.Std.Loc.Uncaught (loc, Pipeline.Sigint, _) -> + let st = Stats.record_parsed st input counter loc in + let st = + State.error st ~file ~loc:{ file = file.loc; loc; } + Report.Error.user_interrupt () + in + st, None + | Dolmen.Std.Loc.Uncaught (loc, Pipeline.Out_of_time, _) -> + let st = Stats.record_parsed st input counter loc in + let st = + State.error st ~file ~loc:{ file = file.loc; loc; } + Report.Error.timeout () + in + st, None + | Dolmen.Std.Loc.Uncaught (loc, Pipeline.Out_of_space, _) -> + let st = Stats.record_parsed st input counter loc in + let st = + State.error st ~file ~loc:{ file = file.loc; loc; } + Report.Error.spaceout () + in + st, None | Dolmen.Std.Loc.Uncaught (loc, exn, bt) -> let st = Stats.record_parsed st input counter loc in let st = diff --git a/src/loop/state.ml b/src/loop/state.ml index d58ad3ff1..fca87574a 100644 --- a/src/loop/state.ml +++ b/src/loop/state.ml @@ -120,7 +120,6 @@ module type S = sig val size_limit : float key val logic_file : Logic.language file key val response_file : Response.language file key - val progress_display : (unit, unit) Progress.Display.t key (* common keys *) end @@ -170,9 +169,6 @@ let size_limit : float key = create_key ~pipe "size_limit" let logic_file : Logic.language file key = create_key ~pipe "logic_file" let response_file : Response.language file key = create_key ~pipe "response_file" -let progress_display : (unit, unit) Progress.Display.t key = - create_key ~pipe "progress_display" - let init ?bt:(bt_value=(Printexc.backtrace_status ())) ~debug:debug_value @@ -257,11 +253,7 @@ let flush st () = (cur - max) (if max = 0 then "" else "additional ") let error ?file ?loc st error payload = - let () = - match get progress_display st with - | d -> Progress.Display.finalise d - | exception Key_not_found _ -> () - in + let () = Tui.finalise_display () in let st = flush st () in let loc = Dolmen.Std.Misc.opt_map loc Dolmen.Std.Loc.full_loc in let aux _ = Code.exit (Report.Error.code error) in @@ -286,25 +278,20 @@ let warn ?file ?loc st warn payload = if get cur_warn st >= get max_warn st then aux st else - Progress.interject_with (fun () -> - match get report_style st with - | Minimal -> - Format.kfprintf aux Format.err_formatter - "W:%s@." (Report.Warning.mnemonic warn) - | Regular | Contextual -> - Format.kfprintf aux Format.err_formatter - ("@[%a%a @[%a@]%a@]@.") - (pp_loc ?file st) loc - Fmt.(styled `Bold @@ styled (`Fg (`Hi `Magenta)) string) "Warning" - Report.Warning.print (warn, payload) - Report.Warning.print_hints (warn, payload) - ) + begin match get report_style st with + | Minimal -> + Tui.kfprintf aux Format.err_formatter + "W:%s@." (Report.Warning.mnemonic warn) + | Regular | Contextual -> + Tui.kfprintf aux Format.err_formatter + ("@[%a%a @[%a@]%a@]@.") + (pp_loc ?file st) loc + Fmt.(styled `Bold @@ styled (`Fg (`Hi `Magenta)) string) "Warning" + Report.Warning.print (warn, payload) + Report.Warning.print_hints (warn, payload) + end | Fatal -> - let () = - match get progress_display st with - | d -> Progress.Display.finalise d - | exception Key_not_found _ -> () - in + let () = Tui.finalise_display () in let st = flush st () in let aux _ = Code.exit (Report.Warning.code warn) in begin match get report_style st with diff --git a/src/loop/stats.ml b/src/loop/stats.ml index 182f4c58b..37945048a 100644 --- a/src/loop/stats.ml +++ b/src/loop/stats.ml @@ -8,75 +8,6 @@ let file_size file_path = let st = Unix.stat file_path in st.st_size -let obj_size obj = - let in_words = Obj.reachable_words (Obj.repr obj) in - let in_bytes = in_words * (Sys.word_size / 8) in - in_bytes - -(* Custom progress bar *) -(* ************************************************************************* *) - -let percentage_printer = - Progress.Printer.create () - ~string_len:4 - ~to_string:(fun p -> Format.asprintf "%3d%%" p) - -module Aux = struct - - type t = { - total_bytes : int; (* total bytes to process *) - processed_bytes : int; (* processed bytes *) - elapsed_time : Mtime.span; (* time spent processing *) - max_mem : int; (* memory limit *) - cur_mem : int; (* memory currently used *) - last_mem : Mtime.span; (* last span that cur memory was computed *) - } - - let zero max_mem = { - total_bytes = 0; - processed_bytes = 0; - elapsed_time = Mtime.Span.zero; - max_mem; - cur_mem = 0; - last_mem = Mtime.Span.zero; - } - - let input max_mem total_bytes = { (zero max_mem) with total_bytes } - - let total_bytes { total_bytes; _ } = total_bytes - let elapsed_time { elapsed_time; _ } = elapsed_time - let processed_bytes { processed_bytes; _ } = processed_bytes - let percentage { processed_bytes; total_bytes; _ } = - int_of_float (100. *. (float processed_bytes) /. (float total_bytes)) - let perthousand { processed_bytes; total_bytes; _ } = - int_of_float (1000. *. (float processed_bytes) /. (float total_bytes)) - let cur_mem { cur_mem; _ } = cur_mem - let ratio_mem { cur_mem; max_mem; _ } = - int_of_float (1000. *. (float cur_mem) /. (float max_mem)) - - let line ~mem phase : t Progress.Line.t = - let process_width, mem_width = - match Terminal.Size.get_columns () with - | None -> `Expand, `Fixed 20 - | Some w -> `Expand, `Fixed ((w - 100) / 2) - in - let open Progress.Line in - list [ - using (fun _ -> phase) (of_printer ~init:phase (Progress.Printer.string ~width:20)); - using elapsed_time (of_printer ~init:Mtime.Span.zero Progress.Units.Duration.mm_ss); - using processed_bytes (of_printer ~init:0 Progress.Units.Bytes.of_int); - const "/"; - using total_bytes (of_printer ~init:0 Progress.Units.Bytes.of_int); - (* TODO: add bytes/seconds *) - if mem then const "|" else noop (); - if mem then using cur_mem (of_printer ~init:0 Progress.Units.Bytes.of_int) else noop (); - if mem then using ratio_mem (bar ~width:mem_width ~data:`Latest 1000) else noop (); - using perthousand (bar ~width:process_width ~data:`Latest 1000); - using percentage (of_printer ~init:0 percentage_printer); - ] - -end - (* Stats & progress bars *) (* ************************************************************************* *) @@ -94,23 +25,8 @@ module Make(State : State.S) = struct model : bool; } - type input = int + type input = Tui.Bar.t State.key type counter = Mtime_clock.counter - type parsing = { - stats : Aux.t array; - reporters : Aux.t Progress.Reporter.t array; - } - - type typing = { - stats : Aux.t; - reporter : Aux.t Progress.Reporter.t; - } - - type model = { - stats : Aux.t; - reporter : Aux.t Progress.Reporter.t; - } - (* state keys *) @@ -119,16 +35,15 @@ module Make(State : State.S) = struct let config_key : config State.key = State.create_key ~pipe "stats_config" - let parsing_key : parsing State.key = - State.create_key ~pipe "stats_parsing" + let parsing_lines : int State.key = + State.create_key ~pipe "parsing_lines" - let typing_key : typing State.key = + let typing_key : Tui.Bar.t State.key = State.create_key ~pipe "stats_typing" - let model_key : model State.key = + let model_key : Tui.Bar.t State.key = State.create_key ~pipe "stats_model" - (* state init *) let init ~mem ~max_mem ~enabled ~typing ~model st = @@ -137,41 +52,29 @@ module Make(State : State.S) = struct if not enabled then st else begin (* create progress display *) - let display = - let config = Progress.Config.v () in - let multi = Progress.Multi.blank in - Progress.Display.start ~config multi - in - let st = State.set State.progress_display display st in - (* create bars *) - let st = - let parsing : parsing = - let stats = [| |] in - let reporters = [| |] in - { stats; reporters; } - in - State.set parsing_key parsing st - in + let () = Tui.init_display () in + (* init the number of parsing lines *) + let st = State.set parsing_lines 0 st in + (* create typing bar *) let st = if not typing then st else begin - let typing : typing = - let stats = Aux.zero max_mem in - let line = Aux.line ~mem:config.mem "typing" in - let reporter = Progress.Display.add_line display line in - { stats; reporter; } + let typing = + Tui.Bar.create () + ~config:{ mem_bar = config.mem } + ~name:"typing" ~max_mem ~total_bytes:0 in State.set typing_key typing st end in + (* create parsing bar *) let st = if not model then st else begin - let model : model = - let stats = Aux.zero max_mem in - let line = Aux.line ~mem:config.mem "model" in - let reporter = Progress.Display.add_line display line in - { stats; reporter; } + let model = + Tui.Bar.create () + ~config:{ mem_bar = config.mem } + ~name:"model" ~max_mem ~total_bytes:0 in State.set model_key model st end @@ -190,27 +93,28 @@ module Make(State : State.S) = struct let new_input st input_name input_size = let config = config st in - if config.enabled then begin - let parsing = State.get parsing_key st in - let display = State.get State.progress_display st in - let n = Array.length parsing.stats in - assert (n = Array.length parsing.reporters); - let z = Aux.input config.max_mem input_size in - let line_name = Format.asprintf "%s" input_name in - let line = Aux.line ~mem:false line_name in - let above = - (if config.model then 1 else 0 (* model *)) + - (if config.typing then 1 else 0 (* typing *)) + - n (* already existing parsing lines *) - in - let reporter = Progress.Display.add_line ~above display line in - let stats = Array.append parsing.stats [| z |] in - let reporters = Array.append parsing.reporters [| reporter |] in - let parsing : parsing = { stats; reporters; } in - let st' = State.set parsing_key parsing st in - n, st' - end else - 0, st + let key = + State.create_key ~pipe + (Format.asprintf "parsing:%s" input_name) + in + let st = + if config.enabled then begin + let n = State.get parsing_lines st in + let above = + (if config.model then 1 else 0 (* model *)) + + (if config.typing then 1 else 0 (* typing *)) + + n (* already existing parsing lines *) + in + let name = Format.asprintf "%s" input_name in + let parsing = + Tui.Bar.create ~config:{ mem_bar = false } () + ~name ~above ~max_mem:config.max_mem ~total_bytes:input_size + in + State.set key parsing st + end else + st + in + key, st let record_parsed st input counter loc = match input with @@ -223,32 +127,14 @@ module Make(State : State.S) = struct let config = config st in assert config.enabled; (* record the loc as parsed *) - let st = - let parsing = State.get parsing_key st in - let input_stats = parsing.stats.(input) in - let input_reporter = parsing.reporters.(input) in - let elapsed_time = Mtime.Span.add span input_stats.elapsed_time in - let processed_bytes = max input_stats.processed_bytes (Dolmen.Std.Loc.last_byte loc) in - let input_stats = { input_stats with elapsed_time; processed_bytes; } in - let () = Progress.Reporter.report input_reporter input_stats in - let stats = Array.copy parsing.stats in - let () = Array.set stats input input_stats in - let parsing = { parsing with stats } in - State.set parsing_key parsing st - in + let parsing = State.get input st in + Tui.Bar.add_processed parsing ~span + ~processed:(`Last loc) ~mem:`None; (* add the loc to be typed *) - let st = - if not config.typing then st - else begin - let bytes_to_type = Dolmen.Std.Loc.length_in_bytes loc in - let typing = State.get typing_key st in - let total_bytes = typing.stats.total_bytes + bytes_to_type in - let stats = { typing.stats with total_bytes } in - let typing = { typing with stats } in - let () = Progress.Reporter.report typing.reporter stats in - State.set typing_key typing st - end - in + if config.typing then begin + let typing = State.get typing_key st in + Tui.Bar.add_to_process typing ~loc + end; st end @@ -260,40 +146,16 @@ module Make(State : State.S) = struct let config = config st in assert (config.enabled); (* record the loc as typed *) - let st = - if not config.typing then st - else begin - let typing = State.get typing_key st in - let processed = Dolmen.Std.Loc.length_in_bytes loc in - let elapsed_time = Mtime.Span.add span typing.stats.elapsed_time in - let cur_mem, last_mem = - if config.mem && ( - Mtime.Span.equal Mtime.Span.zero typing.stats.elapsed_time - || (Mtime.Span.to_s - (Mtime.Span.abs_diff elapsed_time typing.stats.last_mem) >= 0.3)) - then obj_size persistent_data, elapsed_time - else typing.stats.cur_mem, typing.stats.last_mem - in - let processed_bytes = typing.stats.processed_bytes + processed in - let stats = { typing.stats with elapsed_time; processed_bytes; cur_mem; last_mem; } in - let typing = { typing with stats } in - let () = Progress.Reporter.report typing.reporter stats in - State.set typing_key typing st - end - in + if config.typing then begin + let typing = State.get typing_key st in + Tui.Bar.add_processed typing ~span + ~processed:(`Sum loc) ~mem:(`Set persistent_data); + end; (* add the loc to be checked for model *) - let st = - if not config.model then st - else begin - let bytes_to_type = Dolmen.Std.Loc.length_in_bytes loc in - let model = State.get model_key st in - let total_bytes = model.stats.total_bytes + bytes_to_type in - let stats = { model.stats with total_bytes } in - let model = { model with stats } in - let () = Progress.Reporter.report model.reporter stats in - State.set model_key model st - end - in + if config.model then begin + let model = State.get model_key st in + Tui.Bar.add_to_process model ~loc + end; st let record_checked st counter loc persistent_data = @@ -304,52 +166,11 @@ module Make(State : State.S) = struct let config = config st in assert (config.enabled); (* record the loc as typed *) - let st = - if not config.model then st - else begin - let model = State.get model_key st in - let cur_mem = - if not config.mem then model.stats.cur_mem - else match persistent_data with - | `Set obj -> obj_size obj - | `Add obj -> model.stats.cur_mem + obj_size obj - in - let processed = Dolmen.Std.Loc.length_in_bytes loc in - let elapsed_time = Mtime.Span.add span model.stats.elapsed_time in - let processed_bytes = model.stats.processed_bytes + processed in - let stats = { model.stats with elapsed_time; processed_bytes; cur_mem; } in - let model = { model with stats } in - let () = Progress.Reporter.report model.reporter stats in - State.set model_key model st - end - in - st - - (* finalisation *) - - let finalise st = - let config = config st in - if config.enabled then begin - if config.typing then begin - let typing = State.get typing_key st in - let () = Unix.sleepf (1. /. 60.) in - Progress.Reporter.report typing.reporter typing.stats - end; if config.model then begin let model = State.get model_key st in - let () = Unix.sleepf (1. /. 60.) in - Progress.Reporter.report model.reporter model.stats + Tui.Bar.add_processed model ~span ~processed:(`Sum loc) ~mem:persistent_data; end; - let parsing = State.get parsing_key st in - Array.iter2 (fun stats reporter -> - let () = Unix.sleepf (1. /. 60.) in - Progress.Reporter.report reporter stats - ) parsing.stats parsing.reporters; - let display = State.get State.progress_display st in - let () = Unix.sleepf (1. /. 60.) in - Progress.Display.finalise display - end; - () + st end diff --git a/src/loop/stats_intf.ml b/src/loop/stats_intf.ml index 4dba58fa5..0d98b4056 100644 --- a/src/loop/stats_intf.ml +++ b/src/loop/stats_intf.ml @@ -36,7 +36,4 @@ module type S = sig val record_checked : state -> counter option -> Dolmen.Std.Loc.t -> [ `Add of 'a | `Set of 'a] -> state (** *) - val finalise : state -> unit - (** Finalise the stats. *) - end diff --git a/src/loop/tui.ml b/src/loop/tui.ml new file mode 100644 index 000000000..870677b0a --- /dev/null +++ b/src/loop/tui.ml @@ -0,0 +1,174 @@ + +(* This file is free software, part of dolmen. See file "LICENSE" for more information *) + +(* Global state and terminal interaction *) +(* ************************************************************************* *) + +let display : (unit, unit) Progress.Display.t option ref = ref None + +let init_display () = + match !display with + | Some _ -> + assert false + | None -> + let config = Progress.Config.v () in + let multi = Progress.Multi.blank in + let d = Progress.Display.start ~config multi in + display := Some d + +let finalise_display () = + match !display with + | None -> () + | Some d -> + let () = Progress.Display.finalise d in + display := None + +(* Regular printing *) +(* ************************************************************************* *) + +let kfprintf aux fmt format = + match !display with + | None -> Format.kfprintf aux fmt format + | Some d -> + Progress.Display.pause d; + Format.kfprintf + (fun fmt -> Progress.Display.resume d; aux fmt) + fmt format + +let fprintf fmt format = kfprintf (fun _ -> ()) fmt format +let printf format = fprintf Format.std_formatter format +let eprintf format = fprintf Format.err_formatter format + + +(* Progress bars *) +(* ************************************************************************* *) + +module Bar = struct + + module Data = struct + + type t = { + total_bytes : int; (* total bytes to process *) + processed_bytes : int; (* processed bytes *) + elapsed_time : Mtime.span; (* time spent processing *) + max_mem : int; (* memory limit *) + cur_mem : int; (* memory currently used *) + last_mem : Mtime.span; (* last span that cur memory was computed *) + } + + let zero max_mem = { + total_bytes = 0; + processed_bytes = 0; + elapsed_time = Mtime.Span.zero; + max_mem; + cur_mem = 0; + last_mem = Mtime.Span.zero; + } + + let input max_mem total_bytes = { (zero max_mem) with total_bytes } + + let total_bytes { total_bytes; _ } = total_bytes + let elapsed_time { elapsed_time; _ } = elapsed_time + let processed_bytes { processed_bytes; _ } = processed_bytes + let percentage { processed_bytes; total_bytes; _ } = + int_of_float (100. *. (float processed_bytes) /. (float total_bytes)) + let perthousand { processed_bytes; total_bytes; _ } = + int_of_float (1000. *. (float processed_bytes) /. (float total_bytes)) + let cur_mem { cur_mem; _ } = cur_mem + let ratio_mem { cur_mem; max_mem; _ } = + int_of_float (1000. *. (float cur_mem) /. (float max_mem)) + + end + + type config = { + mem_bar : bool; + } + + type t = { + mutable data : Data.t; + config : config; + reporter : Data.t Progress.Reporter.t; + } + + let percentage_printer = + Progress.Printer.create () + ~string_len:4 + ~to_string:(fun p -> Format.asprintf "%3d%%" p) + + let line ~config ~name = + let process_width, mem_width = + match Terminal.Size.get_columns () with + | None -> `Expand, `Fixed 20 + | Some w -> `Expand, `Fixed ((w - 100) / 2) + in + let open Progress.Line in + list [ + using (fun _ -> name) (of_printer ~init:name (Progress.Printer.string ~width:20)); + using Data.elapsed_time (of_printer ~init:Mtime.Span.zero Progress.Units.Duration.mm_ss); + using Data.processed_bytes (of_printer ~init:0 Progress.Units.Bytes.of_int); + const "/"; + using Data.total_bytes (of_printer ~init:0 Progress.Units.Bytes.of_int); + (* TODO: add bytes/seconds *) + if config.mem_bar then + const "|" + else + noop (); + if config.mem_bar then + using Data.cur_mem (of_printer ~init:0 Progress.Units.Bytes.of_int) + else + noop (); + if config.mem_bar then + using Data.ratio_mem (bar ~width:mem_width ~data:`Latest 1000) + else + noop (); + using Data.perthousand (bar ~width:process_width ~data:`Latest 1000); + using Data.percentage (of_printer ~init:0 percentage_printer); + ] + + let create ?above ~config ~name ~max_mem ~total_bytes () = + let data = Data.input max_mem total_bytes in + let line = line ~config ~name in + match !display with + | None -> failwith "Display not intialised" + | Some d -> + let reporter = Progress.Display.add_line ?above d line in + { data; config; reporter; } + + let obj_size obj = + let in_words = Obj.reachable_words (Obj.repr obj) in + let in_bytes = in_words * (Sys.word_size / 8) in + in_bytes + + let[@inline] add_to_process ({ data; reporter; _ } as t) ~loc = + let total_bytes = data.total_bytes + (Dolmen.Std.Loc.length_in_bytes loc) in + let new_data = { data with total_bytes; } in + let () = Progress.Reporter.report reporter new_data in + t.data <- new_data + + let[@inline] add_processed ({ data; config; reporter; } as t) ~span ~processed ~mem = + let elapsed_time = Mtime.Span.add data.elapsed_time span in + let cur_mem, last_mem = + if not config.mem_bar then + data.cur_mem, data.last_mem + else begin + match mem with + | `None -> data.cur_mem, data.last_mem + | `Add obj -> obj_size obj + data.cur_mem, data.last_mem + | `Set obj -> + if Mtime.Span.equal Mtime.Span.zero data.elapsed_time + || (Mtime.Span.to_s (Mtime.Span.abs_diff elapsed_time data.last_mem) >= 0.3) + then obj_size obj, elapsed_time + else data.cur_mem, data.last_mem + end + in + let processed_bytes = + match processed with + | `Last loc -> max data.processed_bytes (Dolmen.Std.Loc.last_byte loc) + | `Sum loc -> data.processed_bytes + (Dolmen.Std.Loc.length_in_bytes loc) + in + let new_data = { data with elapsed_time; cur_mem; last_mem; processed_bytes; } in + let () = Progress.Reporter.report reporter new_data in + t.data <- new_data + +end + diff --git a/src/loop/tui.mli b/src/loop/tui.mli new file mode 100644 index 000000000..5f2193fb8 --- /dev/null +++ b/src/loop/tui.mli @@ -0,0 +1,48 @@ + +(* This file is free software, part of Dolmen. See file "LICENSE" for more details. *) + +(** {2 Global display} *) + +val init_display : unit -> unit + +val finalise_display : unit -> unit + + +(** {2 Printing} *) + +val printf : ('a, Format.formatter, unit) format -> 'a + +val eprintf : ('a, Format.formatter, unit) format -> 'a + +val fprintf : + Format.formatter -> ('a, Format.formatter, unit) format -> 'a + +val kfprintf : + (Format.formatter -> 'a) -> Format.formatter -> + ('b, Format.formatter, unit, 'a) format4 -> 'b + + +(** {2 Progress Bar} *) + +module Bar : sig + + type t + + type config = { + mem_bar : bool; + } + + val create : + ?above:int -> config:config -> name:string -> + max_mem:int -> total_bytes:int -> unit -> t + + val add_to_process : + t -> loc:Dolmen.Std.Loc.t -> unit + + val add_processed : + t -> span:Mtime.Span.t -> + processed:[< `Last of Dolmen.Std.Loc.t | `Sum of Dolmen.Std.Loc.t ] -> + mem:[< `None | `Add of _ | `Set of _ ] -> + unit + +end From 3cd035445872ac89e8054f1a15e6ad3c0ff3d34d Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Mon, 21 Nov 2022 15:30:46 +0100 Subject: [PATCH 07/17] Proper doc --- src/loop/tui.mli | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/src/loop/tui.mli b/src/loop/tui.mli index 5f2193fb8..01385a3c9 100644 --- a/src/loop/tui.mli +++ b/src/loop/tui.mli @@ -4,22 +4,28 @@ (** {2 Global display} *) val init_display : unit -> unit +(* Create and initialise the display *) val finalise_display : unit -> unit +(* Finalise the display. Can be called multiple times. *) (** {2 Printing} *) val printf : ('a, Format.formatter, unit) format -> 'a +(* Analogue to {Format.printf} but properly wraps the display. *) val eprintf : ('a, Format.formatter, unit) format -> 'a +(* Analogue to {Format.eprintf} but properly wraps the display. *) val fprintf : Format.formatter -> ('a, Format.formatter, unit) format -> 'a +(* Analogue to {Format.fprintf} but properly wraps the display. *) val kfprintf : (Format.formatter -> 'a) -> Format.formatter -> ('b, Format.formatter, unit, 'a) format4 -> 'b +(* Analogue to {Format.kfprintf} but properly wraps the display. *) (** {2 Progress Bar} *) @@ -27,22 +33,27 @@ val kfprintf : module Bar : sig type t + (** The type of a progress bar. This type includes some mutable data. *) type config = { mem_bar : bool; } + (** Configuration for progress bars. *) val create : ?above:int -> config:config -> name:string -> max_mem:int -> total_bytes:int -> unit -> t + (** Create a new progress bar. *) val add_to_process : t -> loc:Dolmen.Std.Loc.t -> unit + (** Add some location as needing to be processed in the progress bar. *) val add_processed : t -> span:Mtime.Span.t -> processed:[< `Last of Dolmen.Std.Loc.t | `Sum of Dolmen.Std.Loc.t ] -> mem:[< `None | `Add of _ | `Set of _ ] -> unit + (** Record the given loc as processed for the given bar. *) end From 248d5468aed42e765721c60d73c99c148cc86e07 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Mon, 28 Nov 2022 16:41:55 +0100 Subject: [PATCH 08/17] Better option for progress --- src/bin/options.ml | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/src/bin/options.ml b/src/bin/options.ml index 029445a17..b59f5dd36 100644 --- a/src/bin/options.ml +++ b/src/bin/options.ml @@ -592,14 +592,22 @@ let state = Arg.(value & opt bool false & info ["syntax-error-ref"] ~doc ~docs:error_section) in let progress_enabled = - let doc = Format.asprintf "Print progress information." in - Arg.(value & opt bool false & info ["progress"] ~doc ~docs:profiling_section) + let default = false in + let pos_flag = + let doc = Format.asprintf "Enable printing of progress bars." in + Arg.info ["p"; "progress"] ~doc ~docs:profiling_section + in + let neg_flag = + let doc = Format.asprintf "Disable printing of progress bars." in + Arg.info ["no-progress"] ~doc ~docs:profiling_section + in + Arg.(value & vflag default [true, pos_flag; false, neg_flag]) in let progress_mem = let doc = Format.asprintf "Compute memory usage in progress info. Note that this may slow \ down dolmen significantly (experiments suggest around 3x)." in - Arg.(value & opt bool false & info ["progress-mem"] ~doc ~docs:profiling_section) + Arg.(value & opt bool true & info ["progress-mem"] ~doc ~docs:profiling_section) in Term.(const mk_run_state $ profiling_t $ gc $ gc_t $ bt $ colors $ From 5960176f6f6776489131296310f42cdad490ab71 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Tue, 29 Nov 2022 18:14:06 +0100 Subject: [PATCH 09/17] Make only dolmen_bin depend on progress --- dolmen_bin.opam | 5 ++ dolmen_loop.opam | 2 - src/bin/errors.ml | 14 ++-- src/bin/loop.ml | 3 - src/bin/main.ml | 17 ++-- src/bin/options.ml | 28 +++---- src/bin/state.ml | 120 +++++++++++++++++++++++++++ src/bin/stats.ml | 170 +++++++++++++++++++++++++++++++++++++++ src/{loop => bin}/tui.ml | 0 src/bin/tui.mli | 59 ++++++++++++++ src/loop/dune | 4 +- src/loop/state.ml | 115 -------------------------- src/loop/stats.ml | 161 ++---------------------------------- src/loop/stats.mli | 2 +- src/loop/stats_intf.ml | 9 --- src/lsp/loop.ml | 8 +- 16 files changed, 395 insertions(+), 322 deletions(-) create mode 100644 src/bin/state.ml create mode 100644 src/bin/stats.ml rename src/{loop => bin}/tui.ml (100%) create mode 100644 src/bin/tui.mli diff --git a/dolmen_bin.opam b/dolmen_bin.opam index a4ad3f664..1f34a6219 100644 --- a/dolmen_bin.opam +++ b/dolmen_bin.opam @@ -18,6 +18,11 @@ depends: [ "fmt" "cmdliner" { >= "1.1.0" } "odoc" { with-doc } + "progress" + "terminal" +] +pin-depends: [ + [ "progress" "git+https://github.com/Gbury/progress.git#custom" ] ] depopts: [ "memtrace" diff --git a/dolmen_loop.opam b/dolmen_loop.opam index 19190ebec..0301ec254 100644 --- a/dolmen_loop.opam +++ b/dolmen_loop.opam @@ -16,8 +16,6 @@ depends: [ "gen" "odoc" { with-doc } "pp_loc" { >= "2.0.0" } - "progress" - "terminal" ] tags: [ "logic" "computation" "automated theorem prover" ] homepage: "https://github.com/Gbury/dolmen" diff --git a/src/bin/errors.ml b/src/bin/errors.ml index a5c7e4078..d6575d145 100644 --- a/src/bin/errors.ml +++ b/src/bin/errors.ml @@ -14,35 +14,35 @@ let exn st = function | Dolmen_loop.Pipeline.Sigint -> Format.pp_print_flush Format.std_formatter (); Format.pp_print_flush Format.err_formatter (); - Loop.State.error st Dolmen_loop.Report.Error.user_interrupt () + State.error st Dolmen_loop.Report.Error.user_interrupt () (* Timeout, potentially wrapped by the typechecker *) | Dolmen_loop.Alarm.Out_of_time -> Format.pp_print_flush Format.std_formatter (); - Loop.State.error st Dolmen_loop.Report.Error.timeout () + State.error st Dolmen_loop.Report.Error.timeout () | Dolmen_loop.Alarm.Out_of_space -> Format.pp_print_flush Format.std_formatter (); Format.pp_print_flush Format.err_formatter (); - Loop.State.error st Dolmen_loop.Report.Error.spaceout () + State.error st Dolmen_loop.Report.Error.spaceout () (* Internal Dolmen Expr errors *) | Dolmen.Std.Expr.Ty.Bad_arity (c, l) -> let pp_sep fmt () = Format.fprintf fmt ";@ " in - Loop.State.error st Dolmen_loop.Report.Error.internal_error + State.error st Dolmen_loop.Report.Error.internal_error (Format.dprintf "@[Internal error: Bad arity for type constant '%a',\ @ which was provided arguments:@ [@[%a@]]@]" Dolmen.Std.Expr.Print.ty_cst c (Format.pp_print_list ~pp_sep Dolmen.Std.Expr.Ty.print) l) | Dolmen.Std.Expr.Type_already_defined c -> - Loop.State.error st Dolmen_loop.Report.Error.internal_error + State.error st Dolmen_loop.Report.Error.internal_error (Format.dprintf "@[Internal error: Type constant '%a' was already defined earlier,\ @ cannot re-define it.@]" Dolmen.Std.Expr.Print.id c) | Dolmen.Std.Expr.Term.Wrong_type (t, ty) -> - Loop.State.error st Dolmen_loop.Report.Error.internal_error + State.error st Dolmen_loop.Report.Error.internal_error (Format.dprintf "@[Internal error: A term of type@ %a@ was expected \ but instead got a term of type@ %a@]" @@ -52,5 +52,5 @@ let exn st = function (* Generic catch-all *) | exn -> let bt = Printexc.get_raw_backtrace () in - Loop.State.error st Dolmen_loop.Report.Error.uncaught_exn (exn, bt) + State.error st Dolmen_loop.Report.Error.uncaught_exn (exn, bt) diff --git a/src/bin/loop.ml b/src/bin/loop.ml index 565fae0e1..e037e7f5b 100644 --- a/src/bin/loop.ml +++ b/src/bin/loop.ml @@ -1,10 +1,7 @@ (* This file is free software, part of dolmen. See file "LICENSE" for more information *) -module State = Dolmen_loop.State module Pipeline = Dolmen_loop.Pipeline.Make(State) - -module Stats = Dolmen_loop.Stats.Make(State) module Parser = Dolmen_loop.Parser.Make(State)(Stats) module Header = Dolmen_loop.Headers.Make(State) module Typer = Dolmen_loop.Typer.Typer(State) diff --git a/src/bin/main.ml b/src/bin/main.ml index 3c61d4a66..f1d75f1db 100644 --- a/src/bin/main.ml +++ b/src/bin/main.ml @@ -1,19 +1,18 @@ (* This file is free software, part of dolmen. See file "LICENSE" for more information *) - (* Debug printing *) (* ************** *) let debug_parsed_pipe st c = - if Loop.State.get Loop.State.debug st then + if State.get State.debug st then Format.eprintf "[logic][parsed][%a] @[%a@]@." Dolmen.Std.Loc.print_compact c.Dolmen.Std.Statement.loc Dolmen.Std.Statement.print c; st, c let debug_typed_pipe st stmt = - if Loop.State.get Loop.State.debug st then + if State.get State.debug st then Format.eprintf "[logic][typed][%a] @[%a@]@\n@." Dolmen.Std.Loc.print_compact stmt.Loop.Typer_Pipe.loc Loop.Typer_Pipe.print stmt; @@ -24,7 +23,7 @@ let debug_typed_pipe st stmt = (* ************************ *) let handle_exn st exn = - let () = Dolmen_loop.Tui.finalise_display () in + let () = Tui.finalise_display () in let _st = Errors.exn st exn in exit 125 @@ -33,20 +32,20 @@ let finally st e = | None -> st | Some (bt,exn) -> (* Print the backtrace if requested *) - if Loop.State.(get bt) st then ( + if State.(get bt) st then ( (* TODO: use Tui *) Printexc.print_raw_backtrace stdout bt); handle_exn st exn let run st = - if Loop.State.get Loop.State.debug st then begin + if State.get State.debug st then begin Dolmen.Std.Expr.Print.print_index := true; () end; let st, g = try Loop.Parser.parse_logic [] st - (Loop.State.get Loop.State.logic_file st) + (State.get State.logic_file st) with exn -> handle_exn st exn in let st = @@ -63,9 +62,9 @@ let run st = ) ) in - let () = Dolmen_loop.Tui.finalise_display () in + let () = Tui.finalise_display () in let st = Loop.Header.check st in - let _st = Dolmen_loop.State.flush st () in + let _st = State.flush st () in () (* Warning/Error list *) diff --git a/src/bin/options.ml b/src/bin/options.ml index b59f5dd36..f23981f87 100644 --- a/src/bin/options.ml +++ b/src/bin/options.ml @@ -18,7 +18,7 @@ let profiling_section = "PROFILING" type cmd = | Run of { - state : Loop.State.t; + state : State.t; } | List_reports of { conf : Dolmen_loop.Report.Conf.t; @@ -244,9 +244,9 @@ let c_size = parse_size, print_size let report_style = Arg.enum [ - "minimal", Loop.State.Minimal; - "regular", Loop.State.Regular; - "contextual", Loop.State.Contextual; + "minimal", State.Minimal; + "regular", State.Regular; + "contextual", State.Contextual; ] @@ -338,11 +338,17 @@ let mk_run_state let () = if gc then at_exit (fun () -> Gc.print_stat stdout;) in let () = if abort_on_bug then Dolmen_loop.Code.abort Dolmen_loop.Code.bug in (* State creation *) - Loop.State.empty - |> Loop.State.init + State.empty + |> State.init ~bt ~debug ~report_style ~reports ~max_warn ~time_limit ~size_limit ~logic_file ~response_file + |> Stats.init + ~mem:progress_mem + ~max_mem:(int_of_float size_limit) + ~enabled:progress_enabled + ~typing:type_check + ~model:check_model |> Loop.Parser.init ~syntax_error_ref ~interactive_prompt:Loop.Parser.interactive_prompt_lang @@ -353,12 +359,6 @@ let mk_run_state ~header_check ~header_licenses ~header_lang_version - |> Loop.Stats.init - ~mem:progress_mem - ~max_mem:(int_of_float size_limit) - ~enabled:progress_enabled - ~typing:type_check - ~model:check_model (* Profiling *) (* ************************************************************************* *) @@ -630,10 +630,10 @@ let cli = | false, None -> `Ok (Run { state; }) | false, Some report -> - let conf = Loop.State.get Loop.State.reports state in + let conf = State.get State.reports state in `Ok (Doc { report; conf; }) | true, None -> - let conf = Loop.State.get Loop.State.reports state in + let conf = State.get State.reports state in `Ok (List_reports { conf; }) | true, Some _ -> `Error (false, diff --git a/src/bin/state.ml b/src/bin/state.ml new file mode 100644 index 000000000..8d17e40e9 --- /dev/null +++ b/src/bin/state.ml @@ -0,0 +1,120 @@ + +(* This file is free software, part of dolmen. See file "LICENSE" for more information *) + +include Dolmen_loop.State + +(* Erros, Warnings & locations *) +(* ************************************************************************* *) + +let loc_input ?file st (loc : Dolmen.Std.Loc.loc) = + (* sanity check to avoid pp_loc trying to read and/or print + too much when printing the source code snippet) *) + if loc.max_line_length >= 150 || + loc.stop_line - loc.start_line >= 100 then + None + else begin + match get report_style st, (file : _ file option) with + | _, None -> None + | _, Some { source = `Stdin; _ } -> None + | (Minimal | Regular), _ -> None + | Contextual, Some { source = `File filename; dir; _ } -> + let full_filename = Filename.concat dir filename in + let input = Pp_loc.Input.file full_filename in + Some input + | Contextual, Some { source = `Raw (_, contents); _ } -> + let input = Pp_loc.Input.string contents in + Some input + end + +let pp_loc ?file st fmt o = + match o with + | None -> () + | Some loc -> + if Dolmen.Std.Loc.is_dummy loc then () + else begin + match loc_input ?file st loc with + | None -> + Format.fprintf fmt "%a:@ " + Fmt.(styled `Bold @@ styled (`Fg (`Hi `White)) Dolmen.Std.Loc.fmt) loc + | Some input -> + let loc_start, loc_end = Dolmen.Std.Loc.lexing_positions loc in + let locs = Pp_loc.Position.of_lexing loc_start, Pp_loc.Position.of_lexing loc_end in + Format.fprintf fmt "%a:@ %a" + Fmt.(styled `Bold @@ styled (`Fg (`Hi `White)) Dolmen.Std.Loc.fmt) loc + (Pp_loc.pp ~max_lines:5 ~input) [locs] + end + +let flush st () = + let aux _ = set cur_warn 0 st in + let cur = get cur_warn st in + let max = get max_warn st in + if cur <= max then + aux () + else + match get report_style st with + | Minimal -> + Format.kfprintf aux Format.err_formatter + "W:%d@." (cur - max) + | Regular | Contextual -> + Format.kfprintf aux Format.err_formatter + ("@[%a @[%s@ %d@ %swarnings@]@]@.") + Fmt.(styled `Bold @@ styled (`Fg (`Hi `Magenta)) string) "Warning" + (if max = 0 then "Counted" else "Plus") + (cur - max) (if max = 0 then "" else "additional ") + +let error ?file ?loc st error payload = + let () = Tui.finalise_display () in + let st = flush st () in + let loc = Dolmen.Std.Misc.opt_map loc Dolmen.Std.Loc.full_loc in + let aux _ = Dolmen_loop.Code.exit (Dolmen_loop.Report.Error.code error) in + match get report_style st with + | Minimal -> + Format.kfprintf aux Format.err_formatter + "E:%s@." (Dolmen_loop.Report.Error.mnemonic error) + | Regular | Contextual -> + Format.kfprintf aux Format.err_formatter + ("@[%a%a @[%a@]%a@]@.") + (pp_loc ?file st) loc + Fmt.(styled `Bold @@ styled (`Fg (`Hi `Red)) string) "Error" + Dolmen_loop.Report.Error.print (error, payload) + Dolmen_loop.Report.Error.print_hints (error, payload) + +let warn ?file ?loc st warn payload = + let loc = Dolmen.Std.Misc.opt_map loc Dolmen.Std.Loc.full_loc in + match Dolmen_loop.Report.Conf.status (get reports st) warn with + | Disabled -> st + | Enabled -> + let aux _ = update cur_warn ((+) 1) st in + if get cur_warn st >= get max_warn st then + aux st + else + begin match get report_style st with + | Minimal -> + Tui.kfprintf aux Format.err_formatter + "W:%s@." (Dolmen_loop.Report.Warning.mnemonic warn) + | Regular | Contextual -> + Tui.kfprintf aux Format.err_formatter + ("@[%a%a @[%a@]%a@]@.") + (pp_loc ?file st) loc + Fmt.(styled `Bold @@ styled (`Fg (`Hi `Magenta)) string) "Warning" + Dolmen_loop.Report.Warning.print (warn, payload) + Dolmen_loop.Report.Warning.print_hints (warn, payload) + end + | Fatal -> + let () = Tui.finalise_display () in + let st = flush st () in + let aux _ = Dolmen_loop.Code.exit (Dolmen_loop.Report.Warning.code warn) in + begin match get report_style st with + | Minimal -> + Format.kfprintf aux Format.err_formatter + "F:%s@." (Dolmen_loop.Report.Warning.mnemonic warn) + | Regular | Contextual -> + Format.kfprintf aux Format.err_formatter + ("@[%a%a @[%a@]%a@]@.") + (pp_loc ?file st) loc + Fmt.(styled `Bold @@ styled (`Fg (`Hi `Red)) string) "Fatal Warning" + Dolmen_loop.Report.Warning.print (warn, payload) + Dolmen_loop.Report.Warning.print_hints (warn, payload) + end + + diff --git a/src/bin/stats.ml b/src/bin/stats.ml new file mode 100644 index 000000000..13795a746 --- /dev/null +++ b/src/bin/stats.ml @@ -0,0 +1,170 @@ + +(* This file is free software, part of dolmen. See file "LICENSE" for more information *) + +(* Some helpers *) +(* ************************************************************************* *) + +let file_size file_path = + let st = Unix.stat file_path in + st.st_size + +(* Stats & progress bars *) +(* ************************************************************************* *) + +(* type *) + +type config = { + mem : bool; + max_mem : int; + enabled : bool; + typing : bool; + model : bool; +} + +type input = Tui.Bar.t State.key +type counter = Mtime_clock.counter + +(* state keys *) + +let pipe = "stats" + +let config_key : config State.key = + State.create_key ~pipe "stats_config" + +let parsing_lines : int State.key = + State.create_key ~pipe "parsing_lines" + +let typing_key : Tui.Bar.t State.key = + State.create_key ~pipe "stats_typing" + +let model_key : Tui.Bar.t State.key = + State.create_key ~pipe "stats_model" + +(* state init *) + +let init ~mem ~max_mem ~enabled ~typing ~model st = + let config = { mem; max_mem; enabled; typing; model; } in + let st = State.set config_key config st in + if not enabled then st + else begin + (* create progress display *) + let () = Tui.init_display () in + (* init the number of parsing lines *) + let st = State.set parsing_lines 0 st in + (* create typing bar *) + let st = + if not typing then st + else begin + let typing = + Tui.Bar.create () + ~config:{ mem_bar = config.mem } + ~name:"typing" ~max_mem ~total_bytes:0 + in + State.set typing_key typing st + end + in + (* create parsing bar *) + let st = + if not model then st + else begin + let model = + Tui.Bar.create () + ~config:{ mem_bar = config.mem } + ~name:"model" ~max_mem ~total_bytes:0 + in + State.set model_key model st + end + in + st + end + +(* common *) + +let config st = State.get config_key st + +let start_counter st = + if (config st).enabled then Some (Mtime_clock.counter ()) else None + +(* parsing and inputs *) + +let new_input st input_name input_size = + let config = config st in + let key = + State.create_key ~pipe + (Format.asprintf "parsing:%s" input_name) + in + let st = + if config.enabled then begin + let n = State.get parsing_lines st in + let above = + (if config.model then 1 else 0 (* model *)) + + (if config.typing then 1 else 0 (* typing *)) + + n (* already existing parsing lines *) + in + let name = Format.asprintf "%s" input_name in + let parsing = + Tui.Bar.create ~config:{ mem_bar = false } () + ~name ~above ~max_mem:config.max_mem ~total_bytes:input_size + in + State.set key parsing st + end else + st + in + key, st + +let record_parsed st input counter loc = + match input with + | None -> st + | Some input -> + begin match counter with + | None -> st + | Some counter -> + let span = Mtime_clock.count counter in + let config = config st in + assert config.enabled; + (* record the loc as parsed *) + let parsing = State.get input st in + Tui.Bar.add_processed parsing ~span + ~processed:(`Last loc) ~mem:`None; + (* add the loc to be typed *) + if config.typing then begin + let typing = State.get typing_key st in + Tui.Bar.add_to_process typing ~loc + end; + st + end + +let record_typed st counter loc persistent_data = + match counter with + | None -> st + | Some counter -> + let span = Mtime_clock.count counter in + let config = config st in + assert (config.enabled); + (* record the loc as typed *) + if config.typing then begin + let typing = State.get typing_key st in + Tui.Bar.add_processed typing ~span + ~processed:(`Sum loc) ~mem:(`Set persistent_data); + end; + (* add the loc to be checked for model *) + if config.model then begin + let model = State.get model_key st in + Tui.Bar.add_to_process model ~loc + end; + st + +let record_checked st counter loc persistent_data = + match counter with + | None -> st + | Some counter -> + let span = Mtime_clock.count counter in + let config = config st in + assert (config.enabled); + (* record the loc as typed *) + if config.model then begin + let model = State.get model_key st in + Tui.Bar.add_processed model ~span ~processed:(`Sum loc) ~mem:persistent_data; + end; + st + diff --git a/src/loop/tui.ml b/src/bin/tui.ml similarity index 100% rename from src/loop/tui.ml rename to src/bin/tui.ml diff --git a/src/bin/tui.mli b/src/bin/tui.mli new file mode 100644 index 000000000..01385a3c9 --- /dev/null +++ b/src/bin/tui.mli @@ -0,0 +1,59 @@ + +(* This file is free software, part of Dolmen. See file "LICENSE" for more details. *) + +(** {2 Global display} *) + +val init_display : unit -> unit +(* Create and initialise the display *) + +val finalise_display : unit -> unit +(* Finalise the display. Can be called multiple times. *) + + +(** {2 Printing} *) + +val printf : ('a, Format.formatter, unit) format -> 'a +(* Analogue to {Format.printf} but properly wraps the display. *) + +val eprintf : ('a, Format.formatter, unit) format -> 'a +(* Analogue to {Format.eprintf} but properly wraps the display. *) + +val fprintf : + Format.formatter -> ('a, Format.formatter, unit) format -> 'a +(* Analogue to {Format.fprintf} but properly wraps the display. *) + +val kfprintf : + (Format.formatter -> 'a) -> Format.formatter -> + ('b, Format.formatter, unit, 'a) format4 -> 'b +(* Analogue to {Format.kfprintf} but properly wraps the display. *) + + +(** {2 Progress Bar} *) + +module Bar : sig + + type t + (** The type of a progress bar. This type includes some mutable data. *) + + type config = { + mem_bar : bool; + } + (** Configuration for progress bars. *) + + val create : + ?above:int -> config:config -> name:string -> + max_mem:int -> total_bytes:int -> unit -> t + (** Create a new progress bar. *) + + val add_to_process : + t -> loc:Dolmen.Std.Loc.t -> unit + (** Add some location as needing to be processed in the progress bar. *) + + val add_processed : + t -> span:Mtime.Span.t -> + processed:[< `Last of Dolmen.Std.Loc.t | `Sum of Dolmen.Std.Loc.t ] -> + mem:[< `None | `Add of _ | `Set of _ ] -> + unit + (** Record the given loc as processed for the given bar. *) + +end diff --git a/src/loop/dune b/src/loop/dune index 86663e99d..cc3081fcf 100644 --- a/src/loop/dune +++ b/src/loop/dune @@ -5,7 +5,7 @@ (libraries ; External deps gen unix fmt pp_loc terminal progress - ; main dolmen deps , with versioned languages deps + ; main dolmen deps, with versioned languages deps dolmen dolmen.intf dolmen.std dolmen.class dolmen.smtlib2 dolmen.tptp @@ -14,7 +14,7 @@ ) (modules ; Useful utilities - Alarm Tui Report + Alarm Report ; Interfaces Expr_intf Parser_intf Typer_intf Headers_intf Stats_intf ; Implementations diff --git a/src/loop/state.ml b/src/loop/state.ml index fca87574a..ba1d8c870 100644 --- a/src/loop/state.ml +++ b/src/loop/state.ml @@ -193,118 +193,3 @@ let init |> set logic_file logic_file_value |> set response_file response_file_value -(* State and locations *) -(* ************************************************************************* *) - -let loc_input ?file st (loc : Dolmen.Std.Loc.loc) = - (* sanity check to avoid pp_loc trying to read and/or print - too much when printing the source code snippet) *) - if loc.max_line_length >= 150 || - loc.stop_line - loc.start_line >= 100 then - None - else begin - match get report_style st, (file : _ file option) with - | _, None -> None - | _, Some { source = `Stdin; _ } -> None - | (Minimal | Regular), _ -> None - | Contextual, Some { source = `File filename; dir; _ } -> - let full_filename = Filename.concat dir filename in - let input = Pp_loc.Input.file full_filename in - Some input - | Contextual, Some { source = `Raw (_, contents); _ } -> - let input = Pp_loc.Input.string contents in - Some input - end - -let pp_loc ?file st fmt o = - match o with - | None -> () - | Some loc -> - if Dolmen.Std.Loc.is_dummy loc then () - else begin - match loc_input ?file st loc with - | None -> - Format.fprintf fmt "%a:@ " - Fmt.(styled `Bold @@ styled (`Fg (`Hi `White)) Dolmen.Std.Loc.fmt) loc - | Some input -> - let loc_start, loc_end = Dolmen.Std.Loc.lexing_positions loc in - let locs = Pp_loc.Position.of_lexing loc_start, Pp_loc.Position.of_lexing loc_end in - Format.fprintf fmt "%a:@ %a" - Fmt.(styled `Bold @@ styled (`Fg (`Hi `White)) Dolmen.Std.Loc.fmt) loc - (Pp_loc.pp ~max_lines:5 ~input) [locs] - end - -let flush st () = - let aux _ = set cur_warn 0 st in - let cur = get cur_warn st in - let max = get max_warn st in - if cur <= max then - aux () - else - match get report_style st with - | Minimal -> - Format.kfprintf aux Format.err_formatter - "W:%d@." (cur - max) - | Regular | Contextual -> - Format.kfprintf aux Format.err_formatter - ("@[%a @[%s@ %d@ %swarnings@]@]@.") - Fmt.(styled `Bold @@ styled (`Fg (`Hi `Magenta)) string) "Warning" - (if max = 0 then "Counted" else "Plus") - (cur - max) (if max = 0 then "" else "additional ") - -let error ?file ?loc st error payload = - let () = Tui.finalise_display () in - let st = flush st () in - let loc = Dolmen.Std.Misc.opt_map loc Dolmen.Std.Loc.full_loc in - let aux _ = Code.exit (Report.Error.code error) in - match get report_style st with - | Minimal -> - Format.kfprintf aux Format.err_formatter - "E:%s@." (Report.Error.mnemonic error) - | Regular | Contextual -> - Format.kfprintf aux Format.err_formatter - ("@[%a%a @[%a@]%a@]@.") - (pp_loc ?file st) loc - Fmt.(styled `Bold @@ styled (`Fg (`Hi `Red)) string) "Error" - Report.Error.print (error, payload) - Report.Error.print_hints (error, payload) - -let warn ?file ?loc st warn payload = - let loc = Dolmen.Std.Misc.opt_map loc Dolmen.Std.Loc.full_loc in - match Report.Conf.status (get reports st) warn with - | Disabled -> st - | Enabled -> - let aux _ = update cur_warn ((+) 1) st in - if get cur_warn st >= get max_warn st then - aux st - else - begin match get report_style st with - | Minimal -> - Tui.kfprintf aux Format.err_formatter - "W:%s@." (Report.Warning.mnemonic warn) - | Regular | Contextual -> - Tui.kfprintf aux Format.err_formatter - ("@[%a%a @[%a@]%a@]@.") - (pp_loc ?file st) loc - Fmt.(styled `Bold @@ styled (`Fg (`Hi `Magenta)) string) "Warning" - Report.Warning.print (warn, payload) - Report.Warning.print_hints (warn, payload) - end - | Fatal -> - let () = Tui.finalise_display () in - let st = flush st () in - let aux _ = Code.exit (Report.Warning.code warn) in - begin match get report_style st with - | Minimal -> - Format.kfprintf aux Format.err_formatter - "F:%s@." (Report.Warning.mnemonic warn) - | Regular | Contextual -> - Format.kfprintf aux Format.err_formatter - ("@[%a%a @[%a@]%a@]@.") - (pp_loc ?file st) loc - Fmt.(styled `Bold @@ styled (`Fg (`Hi `Red)) string) "Fatal Warning" - Report.Warning.print (warn, payload) - Report.Warning.print_hints (warn, payload) - end - - diff --git a/src/loop/stats.ml b/src/loop/stats.ml index 37945048a..5cbe64108 100644 --- a/src/loop/stats.ml +++ b/src/loop/stats.ml @@ -13,165 +13,20 @@ let file_size file_path = module type S = Stats_intf.S -module Make(State : State.S) = struct +module Noop(State : State.S) = struct - (* type *) + type input = unit + type counter = unit - type config = { - mem : bool; - max_mem : int; - enabled : bool; - typing : bool; - model : bool; - } + let start_counter _ = None - type input = Tui.Bar.t State.key - type counter = Mtime_clock.counter + let new_input st _ _ = (), st - (* state keys *) + let record_parsed st _ _ _ = st - let pipe = "stats" + let record_typed st _ _ _ = st - let config_key : config State.key = - State.create_key ~pipe "stats_config" - - let parsing_lines : int State.key = - State.create_key ~pipe "parsing_lines" - - let typing_key : Tui.Bar.t State.key = - State.create_key ~pipe "stats_typing" - - let model_key : Tui.Bar.t State.key = - State.create_key ~pipe "stats_model" - - (* state init *) - - let init ~mem ~max_mem ~enabled ~typing ~model st = - let config = { mem; max_mem; enabled; typing; model; } in - let st = State.set config_key config st in - if not enabled then st - else begin - (* create progress display *) - let () = Tui.init_display () in - (* init the number of parsing lines *) - let st = State.set parsing_lines 0 st in - (* create typing bar *) - let st = - if not typing then st - else begin - let typing = - Tui.Bar.create () - ~config:{ mem_bar = config.mem } - ~name:"typing" ~max_mem ~total_bytes:0 - in - State.set typing_key typing st - end - in - (* create parsing bar *) - let st = - if not model then st - else begin - let model = - Tui.Bar.create () - ~config:{ mem_bar = config.mem } - ~name:"model" ~max_mem ~total_bytes:0 - in - State.set model_key model st - end - in - st - end - - (* common *) - - let config st = State.get config_key st - - let start_counter st = - if (config st).enabled then Some (Mtime_clock.counter ()) else None - - (* parsing and inputs *) - - let new_input st input_name input_size = - let config = config st in - let key = - State.create_key ~pipe - (Format.asprintf "parsing:%s" input_name) - in - let st = - if config.enabled then begin - let n = State.get parsing_lines st in - let above = - (if config.model then 1 else 0 (* model *)) + - (if config.typing then 1 else 0 (* typing *)) + - n (* already existing parsing lines *) - in - let name = Format.asprintf "%s" input_name in - let parsing = - Tui.Bar.create ~config:{ mem_bar = false } () - ~name ~above ~max_mem:config.max_mem ~total_bytes:input_size - in - State.set key parsing st - end else - st - in - key, st - - let record_parsed st input counter loc = - match input with - | None -> st - | Some input -> - begin match counter with - | None -> st - | Some counter -> - let span = Mtime_clock.count counter in - let config = config st in - assert config.enabled; - (* record the loc as parsed *) - let parsing = State.get input st in - Tui.Bar.add_processed parsing ~span - ~processed:(`Last loc) ~mem:`None; - (* add the loc to be typed *) - if config.typing then begin - let typing = State.get typing_key st in - Tui.Bar.add_to_process typing ~loc - end; - st - end - - let record_typed st counter loc persistent_data = - match counter with - | None -> st - | Some counter -> - let span = Mtime_clock.count counter in - let config = config st in - assert (config.enabled); - (* record the loc as typed *) - if config.typing then begin - let typing = State.get typing_key st in - Tui.Bar.add_processed typing ~span - ~processed:(`Sum loc) ~mem:(`Set persistent_data); - end; - (* add the loc to be checked for model *) - if config.model then begin - let model = State.get model_key st in - Tui.Bar.add_to_process model ~loc - end; - st - - let record_checked st counter loc persistent_data = - match counter with - | None -> st - | Some counter -> - let span = Mtime_clock.count counter in - let config = config st in - assert (config.enabled); - (* record the loc as typed *) - if config.model then begin - let model = State.get model_key st in - Tui.Bar.add_processed model ~span ~processed:(`Sum loc) ~mem:persistent_data; - end; - st + let record_checked st _ _ _ = st end - diff --git a/src/loop/stats.mli b/src/loop/stats.mli index 940fccdab..64a549901 100644 --- a/src/loop/stats.mli +++ b/src/loop/stats.mli @@ -8,5 +8,5 @@ val file_size : string -> int module type S = Stats_intf.S (** This module provides convenient pipes for parsing and dealing with includes. *) -module Make(State : State.S) : S with type state := State.t +module Noop(State : State.S) : S with type state := State.t diff --git a/src/loop/stats_intf.ml b/src/loop/stats_intf.ml index 0d98b4056..2a9b35017 100644 --- a/src/loop/stats_intf.ml +++ b/src/loop/stats_intf.ml @@ -12,15 +12,6 @@ module type S = sig type counter (** Time counter *) - val init : - mem: bool -> - max_mem:int -> - enabled:bool -> - typing:bool -> - model:bool -> - state -> state - (** Initialisation for the state. *) - val start_counter : state -> counter option (** Start a counter. *) diff --git a/src/lsp/loop.ml b/src/lsp/loop.ml index cb69aa052..4c84399b8 100644 --- a/src/lsp/loop.ml +++ b/src/lsp/loop.ml @@ -3,7 +3,7 @@ module Pipeline = Dolmen_loop.Pipeline.Make(State) -module Stats = Dolmen_loop.Stats.Make(State) +module Stats = Dolmen_loop.Stats.Noop(State) module Parser = Dolmen_loop.Parser.Make(State)(Stats) module Header = Dolmen_loop.Headers.Make(State) module Typer = Dolmen_loop.Typer.Typer(State) @@ -67,12 +67,6 @@ let process prelude path opt_contents = ~header_check:false ~header_licenses:[] ~header_lang_version:None - |> Stats.init - ~mem:false - ~max_mem:0 - ~enabled:false - ~typing:false - ~model:false |> (fun (st : State.t) -> st) in try From 41c30ca420fdd5acadd88e2886dcff3c8072f94e Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Sun, 25 Dec 2022 12:47:56 +0100 Subject: [PATCH 10/17] Vendor progress lib --- .gitmodules | 3 +++ dolmen_bin.opam | 11 +++++------ dolmen_loop.opam | 1 - dune | 3 +++ src/bin/dune | 2 ++ src/bin/main.ml | 7 ++++--- src/loop/dune | 2 +- vendor/progress | 1 + 8 files changed, 19 insertions(+), 11 deletions(-) create mode 100644 .gitmodules create mode 160000 vendor/progress diff --git a/.gitmodules b/.gitmodules new file mode 100644 index 000000000..cb9cd24ad --- /dev/null +++ b/.gitmodules @@ -0,0 +1,3 @@ +[submodule "vendor/progress"] + path = vendor/progress + url = https://github.com/Gbury/progress.git diff --git a/dolmen_bin.opam b/dolmen_bin.opam index 1f34a6219..be14a15ae 100644 --- a/dolmen_bin.opam +++ b/dolmen_bin.opam @@ -14,15 +14,14 @@ depends: [ "dolmen_type" {= version } "dolmen_loop" {= version } "dolmen_model" {= version } + "odoc" { with-doc } "dune" { >= "3.0" } "fmt" "cmdliner" { >= "1.1.0" } - "odoc" { with-doc } - "progress" - "terminal" -] -pin-depends: [ - [ "progress" "git+https://github.com/Gbury/progress.git#custom" ] + "pp_loc" { >= "2.0.0" } +# These two are currently vendored +# "progress" +# "terminal" ] depopts: [ "memtrace" diff --git a/dolmen_loop.opam b/dolmen_loop.opam index 0301ec254..8e48652ba 100644 --- a/dolmen_loop.opam +++ b/dolmen_loop.opam @@ -15,7 +15,6 @@ depends: [ "dune" { >= "3.0" } "gen" "odoc" { with-doc } - "pp_loc" { >= "2.0.0" } ] tags: [ "logic" "computation" "automated theorem prover" ] homepage: "https://github.com/Gbury/dolmen" diff --git a/dune b/dune index 1bcb14139..3b7203e6c 100644 --- a/dune +++ b/dune @@ -1,3 +1,6 @@ +; directory for vendored libs +(vendored_dirs vendor) + (env ; Ensure no inlinging takes place in dev mode to have more accurate backtraces (dev (ocamlopt_flags :standard -inline 0)) diff --git a/src/bin/dune b/src/bin/dune index 3a5f51545..ff1843e95 100644 --- a/src/bin/dune +++ b/src/bin/dune @@ -6,6 +6,8 @@ (libraries ; external deps cmdliner fmt gen + pp_loc progress terminal + mtime mtime.clock.os ; dolmen deps dolmen dolmen.intf dolmen.std dolmen_type dolmen_loop dolmen_model diff --git a/src/bin/main.ml b/src/bin/main.ml index f1d75f1db..b82c08b3e 100644 --- a/src/bin/main.ml +++ b/src/bin/main.ml @@ -32,9 +32,10 @@ let finally st e = | None -> st | Some (bt,exn) -> (* Print the backtrace if requested *) - if State.(get bt) st then ( - (* TODO: use Tui *) - Printexc.print_raw_backtrace stdout bt); + if State.(get bt) st then begin + Tui.eprintf "%s@." + (Printexc.raw_backtrace_to_string bt) + end; handle_exn st exn let run st = diff --git a/src/loop/dune b/src/loop/dune index cc3081fcf..0ed4ff9ce 100644 --- a/src/loop/dune +++ b/src/loop/dune @@ -4,7 +4,7 @@ (instrumentation (backend bisect_ppx)) (libraries ; External deps - gen unix fmt pp_loc terminal progress + gen unix fmt ; main dolmen deps, with versioned languages deps dolmen dolmen.intf dolmen.std dolmen.class diff --git a/vendor/progress b/vendor/progress new file mode 160000 index 000000000..019cc6ae1 --- /dev/null +++ b/vendor/progress @@ -0,0 +1 @@ +Subproject commit 019cc6ae1622535ce260694f19eaaec3a360ad27 From ff9036c742631eaafed541cfb8ae56224481ae7f Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Mon, 26 Dec 2022 00:54:40 +0100 Subject: [PATCH 11/17] Update opam file --- dolmen_bin.opam | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/dolmen_bin.opam b/dolmen_bin.opam index be14a15ae..7840068e4 100644 --- a/dolmen_bin.opam +++ b/dolmen_bin.opam @@ -19,9 +19,18 @@ depends: [ "fmt" "cmdliner" { >= "1.1.0" } "pp_loc" { >= "2.0.0" } + "mtime" {>= "1.1.0"} # These two are currently vendored # "progress" # "terminal" +# thus we need their deps + "stdlib-shims" + "fmt" {>= "0.8.5"} + "logs" {>= "0.7.0"} + "uucp" {>= "2.0.0"} + "uutf" {>= "1.0.0"} + "vector" + "optint" {>= "0.1.0"} ] depopts: [ "memtrace" From 70ff5fba21308dcc62ce78d42c54e48945b064a9 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Tue, 3 Jan 2023 15:11:09 +0100 Subject: [PATCH 12/17] Try and fix CI --- .github/workflows/build.yml | 4 +++- .github/workflows/install.yml | 2 ++ .github/workflows/release.yml | 2 ++ .github/workflows/test.yml | 4 +++- 4 files changed, 10 insertions(+), 2 deletions(-) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 3854c5c7e..ed11ff037 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -56,9 +56,11 @@ jobs: # Build/test steps # ---------------- steps: - # checkout the repo (full clone, necessary for push later) + # checkout the repo - name: Checkout the repo uses: actions/checkout@v3 + with: + submodules: recursive # Setup ocaml/opam - name: Setup ocaml/opam uses: avsm/setup-ocaml@v2 diff --git a/.github/workflows/install.yml b/.github/workflows/install.yml index 747f2f09d..d0ebb9a95 100644 --- a/.github/workflows/install.yml +++ b/.github/workflows/install.yml @@ -70,6 +70,8 @@ jobs: # checkout the repo (full clone, necessary for push later) - name: Checkout the repo uses: actions/checkout@v3 + with: + submodules: recursive # Setup ocaml/opam - name: Setup ocaml/opam uses: avsm/setup-ocaml@v2 diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index d345d1906..f72025bf1 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -58,6 +58,8 @@ jobs: # checkout the repo - name: Checkout the repo uses: actions/checkout@v3 + with: + submodules: recursive # Setup ocaml/opam - name: Setup ocaml/opam uses: avsm/setup-ocaml@v2 diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 6b2d19f5f..98a5d8ddc 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -49,9 +49,11 @@ jobs: # Build/test steps # ---------------- steps: - # checkout the repo (full clone, necessary for push later) + # checkout the repo - name: Checkout the repo uses: actions/checkout@v3 + with: + submodules: recursive # Setup ocaml/opam - name: Setup ocaml/opam uses: avsm/setup-ocaml@v2 From 670dbe2e2110eaae43fe9950886635a82329e1f1 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Tue, 3 Jan 2023 15:47:14 +0100 Subject: [PATCH 13/17] Update for mtime 2.0 --- dolmen_bin.opam | 2 +- src/bin/tui.ml | 5 +++-- vendor/progress | 2 +- 3 files changed, 5 insertions(+), 4 deletions(-) diff --git a/dolmen_bin.opam b/dolmen_bin.opam index 7840068e4..f76ce4ea7 100644 --- a/dolmen_bin.opam +++ b/dolmen_bin.opam @@ -19,7 +19,7 @@ depends: [ "fmt" "cmdliner" { >= "1.1.0" } "pp_loc" { >= "2.0.0" } - "mtime" {>= "1.1.0"} + "mtime" {>= "2.0.0"} # These two are currently vendored # "progress" # "terminal" diff --git a/src/bin/tui.ml b/src/bin/tui.ml index 870677b0a..8e244bfc3 100644 --- a/src/bin/tui.ml +++ b/src/bin/tui.ml @@ -155,8 +155,9 @@ module Bar = struct | `None -> data.cur_mem, data.last_mem | `Add obj -> obj_size obj + data.cur_mem, data.last_mem | `Set obj -> - if Mtime.Span.equal Mtime.Span.zero data.elapsed_time - || (Mtime.Span.to_s (Mtime.Span.abs_diff elapsed_time data.last_mem) >= 0.3) + if Mtime.Span.( + equal zero data.elapsed_time + || (compare (abs_diff elapsed_time data.last_mem) (300 * ms) >= 0)) then obj_size obj, elapsed_time else data.cur_mem, data.last_mem end diff --git a/vendor/progress b/vendor/progress index 019cc6ae1..728e0d8f7 160000 --- a/vendor/progress +++ b/vendor/progress @@ -1 +1 @@ -Subproject commit 019cc6ae1622535ce260694f19eaaec3a360ad27 +Subproject commit 728e0d8f7505d7dd1bf7904982c59d47de9cca66 From 601e256e05e0beec7f5818b34d3d6864d263623e Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Tue, 3 Jan 2023 16:05:25 +0100 Subject: [PATCH 14/17] Revert "Update for mtime 2.0" This reverts commit b6ede8b5b592af87f7fa07a226172f160ea52bad. --- dolmen_bin.opam | 2 +- src/bin/tui.ml | 5 ++--- vendor/progress | 2 +- 3 files changed, 4 insertions(+), 5 deletions(-) diff --git a/dolmen_bin.opam b/dolmen_bin.opam index f76ce4ea7..7840068e4 100644 --- a/dolmen_bin.opam +++ b/dolmen_bin.opam @@ -19,7 +19,7 @@ depends: [ "fmt" "cmdliner" { >= "1.1.0" } "pp_loc" { >= "2.0.0" } - "mtime" {>= "2.0.0"} + "mtime" {>= "1.1.0"} # These two are currently vendored # "progress" # "terminal" diff --git a/src/bin/tui.ml b/src/bin/tui.ml index 8e244bfc3..870677b0a 100644 --- a/src/bin/tui.ml +++ b/src/bin/tui.ml @@ -155,9 +155,8 @@ module Bar = struct | `None -> data.cur_mem, data.last_mem | `Add obj -> obj_size obj + data.cur_mem, data.last_mem | `Set obj -> - if Mtime.Span.( - equal zero data.elapsed_time - || (compare (abs_diff elapsed_time data.last_mem) (300 * ms) >= 0)) + if Mtime.Span.equal Mtime.Span.zero data.elapsed_time + || (Mtime.Span.to_s (Mtime.Span.abs_diff elapsed_time data.last_mem) >= 0.3) then obj_size obj, elapsed_time else data.cur_mem, data.last_mem end diff --git a/vendor/progress b/vendor/progress index 728e0d8f7..019cc6ae1 160000 --- a/vendor/progress +++ b/vendor/progress @@ -1 +1 @@ -Subproject commit 728e0d8f7505d7dd1bf7904982c59d47de9cca66 +Subproject commit 019cc6ae1622535ce260694f19eaaec3a360ad27 From 87300461a92838e75916572542fe266fd90913f6 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Tue, 3 Jan 2023 16:06:24 +0100 Subject: [PATCH 15/17] Add upper bound on mtime Mtime 2.0.0 is not yet available on the windows repo (and thus neither on the windows CI), so limiting the compatibility for now. --- dolmen_bin.opam | 2 +- vendor/progress | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/dolmen_bin.opam b/dolmen_bin.opam index 7840068e4..e42451741 100644 --- a/dolmen_bin.opam +++ b/dolmen_bin.opam @@ -19,7 +19,7 @@ depends: [ "fmt" "cmdliner" { >= "1.1.0" } "pp_loc" { >= "2.0.0" } - "mtime" {>= "1.1.0"} + "mtime" {>= "1.1.0" & < "2.0.0" } # These two are currently vendored # "progress" # "terminal" diff --git a/vendor/progress b/vendor/progress index 019cc6ae1..0be9e0478 160000 --- a/vendor/progress +++ b/vendor/progress @@ -1 +1 @@ -Subproject commit 019cc6ae1622535ce260694f19eaaec3a360ad27 +Subproject commit 0be9e047845b700a59262b77a1725d49591a010e From a480c8f186e8604f650006d7b3e4bf40de7b7de6 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Mon, 16 Jan 2023 18:07:34 +0100 Subject: [PATCH 16/17] Fix build --- src/bin/options.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/bin/options.ml b/src/bin/options.ml index f23981f87..0839160aa 100644 --- a/src/bin/options.ml +++ b/src/bin/options.ml @@ -439,8 +439,8 @@ let reports = (* ************************************************************************* *) let mk_file lang mode input = - let dir,source = Loop.State.split_input input in - Loop.State.mk_file ?lang ?mode dir source + let dir,source = State.split_input input in + State.mk_file ?lang ?mode dir source let logic_file = let docs = common_section in From e635c925b31ef8a32a8b31066a8d72cb3be83af4 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Wed, 25 Jan 2023 14:49:22 +0100 Subject: [PATCH 17/17] Fix rebase --- src/loop/parser.ml | 47 +++++++++++++++++++++++++++------------------- 1 file changed, 28 insertions(+), 19 deletions(-) diff --git a/src/loop/parser.ml b/src/loop/parser.ml index 8b80fda2e..6be81cbd4 100644 --- a/src/loop/parser.ml +++ b/src/loop/parser.ml @@ -196,7 +196,7 @@ module Make st, None | exn -> raise exn - let wrap_parser ?input ~loc_of_res ~file g = fun st -> + let wrap_parser ?(cleanup=(fun () -> ())) ?input ~loc_of_res ~file g = fun st -> begin match (State.get interactive_prompt st) st with | None -> () | Some prelude -> Format.printf "%s @?" prelude @@ -204,12 +204,14 @@ module Make let counter = Stats.start_counter st in match g () with | None -> + let () = cleanup () in let st = Stats.record_parsed st input counter Dolmen.Std.Loc.no_loc in st, None | Some res as ret -> let st = Stats.record_parsed st input counter (loc_of_res res) in st, ret | exception exn -> + let () = cleanup () in wrap_exn st file input counter exn let wrap_lazy_list ?input ~loc_of_res ~file llist = @@ -250,11 +252,11 @@ module Make try match file.source with | `Stdin -> - let lang, file_loc, gen, _ = Logic.parse_input + let lang, file_loc, gen, cl = Logic.parse_input ?language:file.lang (`Stdin (Logic.Smtlib2 `Latest)) in let file = { file with loc = file_loc; lang = Some lang; } in - st, file, None, gen + st, file, None, `Gen (gen, Some cl) | `Raw (filename, contents) -> let lang = match file.lang with @@ -270,14 +272,14 @@ module Make ~language:lang (`Raw (filename, lang, contents)) in let file = { file with loc = file_loc; lang = Some lang; } in let input, st = Stats.new_input st filename (String.length contents) in - st, file, Some input, gen_finally gen cl + st, file, Some input, `Gen (gen, Some cl) | Some `Full -> let lang, file_loc, l = Logic.parse_raw_lazy ~language:lang ~filename contents in let file = { file with loc = file_loc; lang = Some lang; } in let input, st = Stats.new_input st filename (String.length contents) in - st, file, Some input, gen_of_llist l + st, file, Some input, `Llist l end | `File f -> let s = Dolmen.Std.Statement.include_ f [] in @@ -302,16 +304,23 @@ module Make Dolmen.Std.Statement.pack [s; Dolmen.Std.Statement.prove ()] in let file = { file with lang = Some lang; } in - st, file, None, (Gen.singleton s') + st, file, None, `Gen (Gen.singleton s', None) with | Logic.Extension_not_found ext -> - State.error st extension_not_found ext, file, None, Gen.empty + State.error st extension_not_found ext, file, None, `Gen (Gen.empty, None) in let st = set_logic_file st file in (* Wrap the resulting parser *) - st, wrap_parser - ?input ~file ~loc_of_res:(fun (c : Dolmen.Std.Statement.t) -> c.loc) - (Gen.append (Gen.of_list prelude) g) + let loc_of_res (c : Dolmen.Std.Statement.t) = c.loc in + match g with + | `Gen (gen, cleanup) -> + st, wrap_parser + ?cleanup ?input ~file ~loc_of_res + (Gen.append (Gen.of_list prelude) gen) + | `Llist l -> + st, wrap_lazy_list + ?input ~file ~loc_of_res + (lazy (prelude @ (Lazy.force l))) let parse_response prelude st (file : Response.language file) = (* Parse the input *) @@ -319,11 +328,11 @@ module Make try match file.source with | `Stdin -> - let lang, file_loc, gen, _ = Response.parse_input + let lang, file_loc, gen, cl = Response.parse_input ?language:file.lang (`Stdin (Response.Smtlib2 `Latest)) in let file = { file with loc = file_loc; lang = Some lang; } in - st, file, None, `Gen gen + st, file, None, `Gen (gen, Some cl) | `Raw (filename, contents) -> let lang = match file.lang with @@ -339,20 +348,20 @@ module Make ~language:lang (`Raw (filename, lang, contents)) in let file = { file with loc = file_loc; lang = Some lang; } in let input, st = Stats.new_input st filename (String.length contents) in - st, file, Some input, gen_finally gen cl + st, file, Some input, `Gen (gen, Some cl) | Some `Full -> let lang, file_loc, l = Response.parse_raw_lazy ?language:file.lang ~filename contents in let file = { file with loc = file_loc; lang = Some lang; } in let input, st = Stats.new_input st filename (String.length contents) in - st, file, Some input, gen_of_llist l + st, file, Some input, `Llist l end | `File f -> begin match Response.find ?language:file.lang ~dir:file.dir f with | None -> let st = State.error st file_not_found (file.dir, f) in - st, file, None, `Gen Gen.empty + st, file, None, `Gen (Gen.empty, None) | Some filename -> let file_size = file_size filename in let input, st = Stats.new_input st f file_size in @@ -363,7 +372,7 @@ module Make Response.parse_input ?language:file.lang (`File filename) in let file = { file with loc = file_loc; lang = Some lang; } in - st, file, Some input, `Gen (gen_finally gen cl) + st, file, Some input, `Gen (gen, Some cl) | Some `Full -> let lang, file_loc, l = Response.parse_file_lazy ?language:file.lang filename @@ -374,15 +383,15 @@ module Make end with | Logic.Extension_not_found ext -> - State.error st extension_not_found ext, file, None, `Gen Gen.empty + State.error st extension_not_found ext, file, None, `Gen (Gen.empty, None) in let st = State.set State.response_file file st in (* Wrap the resulting parser *) let loc_of_res (a : Dolmen.Std.Answer.t) = a.loc in match g with - | `Gen g -> + | `Gen (g, cleanup) -> st, wrap_parser - ?input ~file ~loc_of_res + ?cleanup ?input ~file ~loc_of_res (Gen.append (Gen.of_list prelude) g) | `Llist l -> st, wrap_lazy_list