diff --git a/dolmen_bin.opam b/dolmen_bin.opam index 3bef4a173..4e8338d8f 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 52b006a81..409d95b90 100644 --- a/dolmen_loop.opam +++ b/dolmen_loop.opam @@ -19,6 +19,9 @@ depends: [ "progress" "terminal" ] +pin-depends: [ + [ "progress" "git+https://github.com/Gbury/progress.git#custom" ] +] tags: [ "logic" "computation" "automated theorem prover" ] homepage: "https://github.com/Gbury/dolmen" dev-repo: "git+https://github.com/Gbury/dolmen.git" diff --git a/src/bin/errors.ml b/src/bin/errors.ml index aa06877fb..054c18ff4 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.Pipeline.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.Pipeline.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 84da8ced3..0a68ca24c 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 @@ -38,14 +37,14 @@ let finally st e = 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 = @@ -62,9 +61,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 70bfec79a..d002b6b5e 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; ] @@ -345,11 +345,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 ~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 @@ -360,12 +366,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 *) (* ************************************************************************* *) @@ -633,10 +633,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 bf84edbb8..beb785b11 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 - Tui Report + 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 400d87c82..84e38e646 100644 --- a/src/loop/state.ml +++ b/src/loop/state.ml @@ -178,118 +178,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 7214bf173..02e976408 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 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