Merge pull request #1076 from ejgallego/flame_fcc

[fcc] New option --trace-file for flamegraph generation.

Author: ejgallego

CHANGES.md

@@ -78,6 +78,9 @@
    (@ejgallego, #590)
  - [plugins] New plugin to dump document data (@ejgallego, Stefania
    Dumbrava, #1075)
+ - [fcc] New option `--trace-file` that will generate trace data for
+   visualizing with perfetto.dev (@ejgallego, AlexJ, Gaëtan Gilbert,
+   #1076)
 
 # coq-lsp 0.2.4: (W)Activation
 ------------------------------

compiler/args.ml

@@ -1,3 +1,13 @@
+(************************************************************************)
+(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1+ / GPL3+     *)
+(* Copyright 2019-2024 Inria      -- Dual License LGPL 2.1+ / GPL3+     *)
+(* Copyright 2024-2025 Emilio J. Gallego Arias -- LGPL 2.1+ / GPL3+     *)
+(* Copyright 2025      CNRS                    -- LGPL 2.1+ / GPL3+     *)
+(* Written by: Emilio J. Gallego Arias & coq-lsp contributors           *)
+(************************************************************************)
+(* Flèche => command-line compiler                                      *)
+(************************************************************************)
+
 module Display = struct
   type t =
     | Verbose
@@ -12,6 +22,7 @@ type t =
   ; debug : bool  (** run in debug mode *)
   ; display : Display.t  (** display level *)
   ; plugins : string list  (** Flèche plugins to load *)
+  ; trace_file : string option  (** Save flame profile to file *)
   ; max_errors : int option
         (** Maximum erros before aborting the compilation *)
   ; coq_diags_level : int

compiler/compile.ml

@@ -1,3 +1,13 @@
+(************************************************************************)
+(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1+ / GPL3+     *)
+(* Copyright 2019-2024 Inria      -- Dual License LGPL 2.1+ / GPL3+     *)
+(* Copyright 2024-2025 Emilio J. Gallego Arias -- LGPL 2.1+ / GPL3+     *)
+(* Copyright 2025      CNRS                    -- LGPL 2.1+ / GPL3+     *)
+(* Written by: Emilio J. Gallego Arias & coq-lsp contributors           *)
+(************************************************************************)
+(* Flèche => command-line compiler                                      *)
+(************************************************************************)
+
 open Fleche
 
 let is_in_dir ~dir ~file = CString.is_prefix dir file
@@ -59,7 +69,35 @@ let compile_file ~cc file : int =
       Theory.close ~uri;
       status_of_doc doc)
 
-let compile ~cc =
-  List.fold_left
-    (fun status file -> if status = 0 then compile_file ~cc file else status)
-    0
+let compile_file ~cc file : int =
+  let args () = [ ("file", `String file) ] in
+  NewProfile.profile "compile" ~args (fun () -> compile_file ~cc file) ()
+
+let oprofile = ref None
+
+let init_profile trace_file =
+  match trace_file with
+  | None -> ()
+  | Some file ->
+    let oc = Stdlib.open_out file in
+    let fmt = Format.formatter_of_out_channel oc in
+    oprofile := Some (oc, fmt);
+    NewProfile.init { output = fmt; fname = "fcc" }
+
+let finish_profile () =
+  match !oprofile with
+  | None -> ()
+  | Some (oc, fmt) ->
+    NewProfile.finish ();
+    Format.pp_print_flush fmt ();
+    Stdlib.close_out oc
+
+let compile ~cc ~trace_file files =
+  init_profile trace_file;
+  let finally = finish_profile in
+  let compile () =
+    List.fold_left
+      (fun status file -> if status = 0 then compile_file ~cc file else status)
+      0 files
+  in
+  Fun.protect ~finally compile

compiler/driver.ml

@@ -43,6 +43,7 @@ let go ~int_backend args =
       ; debug
       ; files
       ; plugins
+      ; trace_file
       ; max_errors
       ; coq_diags_level
       ; record_comments
@@ -67,4 +68,4 @@ let go ~int_backend args =
   let cc = Cc.{ root_state; workspaces; default; io; token } in
   (* Initialize plugins *)
   plugin_init plugins;
-  Compile.compile ~cc files
+  Compile.compile ~cc ~trace_file files

compiler/fcc.ml

@@ -2,9 +2,9 @@
 open Cmdliner
 open Fcc_lib
 
-let fcc_main int_backend roots display debug plugins files coqlib findlib_config
-    ocamlpath rload_path load_path require_libraries no_vo max_errors
-    coq_diags_level record_comments =
+let fcc_main int_backend roots display debug plugins trace_file files coqlib
+    findlib_config ocamlpath rload_path load_path require_libraries no_vo
+    max_errors coq_diags_level record_comments =
   let vo_load_path = rload_path @ load_path in
   let args = [] in
   let cmdline =
@@ -25,6 +25,7 @@ let fcc_main int_backend roots display debug plugins files coqlib findlib_config
       ; files
       ; debug
       ; plugins
+      ; trace_file
       ; max_errors
       ; coq_diags_level
       ; record_comments
@@ -52,6 +53,10 @@ let plugins : string list Term.t =
   let doc = "Compiler plugins to load" in
   Arg.(value & opt_all string [] & info [ "plugin" ] ~docv:"PLUGINS" ~doc)
 
+let trace_file : string option Term.t =
+  let doc = "Activate profiling and output a Rocq flame graph in FILE" in
+  Arg.(value & opt (some string) None & info [ "trace_file" ] ~docv:"FILE" ~doc)
+
 let no_vo : bool Term.t =
   let doc = "Don't generate .vo files at the end of compilation" in
   Arg.(value & flag & info [ "no_vo" ] ~doc)
@@ -98,9 +103,10 @@ let fcc_cmd : int Cmd.t =
   let fcc_term =
     let open Coq.Args in
     Term.(
-      const fcc_main $ int_backend $ roots $ display $ debug $ plugins $ file
-      $ coqlib $ findlib_config $ ocamlpath $ rload_paths $ qload_paths
-      $ ri_from $ no_vo $ max_errors $ coq_diags_level $ record_comments)
+      const fcc_main $ int_backend $ roots $ display $ debug $ plugins
+      $ trace_file $ file $ coqlib $ findlib_config $ ocamlpath $ rload_paths
+      $ qload_paths $ ri_from $ no_vo $ max_errors $ coq_diags_level
+      $ record_comments)
   in
   let exits = Exit_codes.[ fatal; stopped; scheduled; uri_failed ] in
   Cmd.(v (Cmd.info "fcc" ~exits ~version ~doc ~man) fcc_term)

coq/parsing.ml

@@ -30,6 +30,9 @@ let parse ~token ~st ps =
   (* This runs already inside Coq.protect *)
   State.in_state ~token ~st ~f:(parse ~st) ps
 
+let parse ~token ~st ps =
+  NewProfile.profile "Coq.parse" (fun () -> parse ~token ~st ps) ()
+
 (* Read the input stream until a dot or a "end of proof" token is encountered *)
 let parse_to_terminator : unit Pcoq.Entry.t =
   (* type 'a parser_fun = { parser_fun : te LStream.t -> 'a } *)

fleche/doc.ml

@@ -479,6 +479,11 @@ let create ~token ~env ~uri ~languageId ~version ~raw =
   handle_contents_creation ~env ~uri ~version ~languageId ~raw
     (handle_doc_creation_exec ~token)
 
+let create ~token ~env ~uri ~languageId ~version ~raw =
+  NewProfile.profile "Doc.create"
+    (fun () -> create ~token ~env ~uri ~languageId ~version ~raw)
+    ()
+
 (* Used in bump, we should consolidate with create *)
 let recreate ~token ~doc ~version ~contents =
   let env, uri, languageId = (doc.env, doc.uri, doc.languageId) in
@@ -563,6 +568,11 @@ let bump_version ~token ~version ~raw doc =
     conv_error_doc ~raw ~uri ~languageId ~version ~env:doc.env ~root:doc.root e
   | Contents.R.Ok contents -> bump_version ~token ~version ~contents doc
 
+let bump_version ~token ~version ~raw doc =
+  NewProfile.profile "Doc.bump_version"
+    (fun () -> bump_version ~token ~version ~raw doc)
+    ()
+
 let update_env ~doc ~env =
   let range = Completion.range doc.completed in
   { doc with completed = WorkspaceUpdated range; env }
@@ -866,6 +876,11 @@ let parse_action ~token ~lines ~st last_tok doc_handle =
       in
       (Skip (span_range, last_tok_range), parse_diags, feedback, time))
 
+let parse_action ~token ~lines ~st last_tok doc_handle =
+  NewProfile.profile "Doc.parse_action"
+    (fun () -> parse_action ~token ~lines ~st last_tok doc_handle)
+    ()
+
 (* Result of node-building action *)
 type document_action =
   | Stop of Completion.t * Node.t
@@ -983,6 +998,14 @@ let document_action ~token ~io ~st ~parsing_diags ~parsing_feedback
       node_of_coq_result ~token ~doc ~range:ast_range ~prev ~ast ~st
         ~parsing_diags ~parsing_feedback ~feedback ~info last_tok_new res)
 
+let document_action ~token ~io ~st ~parsing_diags ~parsing_feedback
+    ~parsing_time ~prev ~doc last_tok doc_handle action =
+  NewProfile.profile "Doc.document_action"
+    (fun () ->
+      document_action ~token ~io ~st ~parsing_diags ~parsing_feedback
+        ~parsing_time ~prev ~doc last_tok doc_handle action)
+    ()
+
 module Target = struct
   type t =
     | End
@@ -1091,6 +1114,12 @@ let process_and_parse ~io ~token ~target ~uri ~version doc last_tok doc_handle =
   let doc = { doc with nodes = List.rev doc.nodes } in
   doc
 
+let process_and_parse ~io ~token ~target ~uri ~version doc last_tok doc_handle =
+  NewProfile.profile "Doc.process_and_parse"
+    (fun () ->
+      process_and_parse ~io ~token ~target ~uri ~version doc last_tok doc_handle)
+    ()
+
 let log_doc_completion (completed : Completion.t) =
   let timestamp = Unix.gettimeofday () in
   let range = Completion.range completed in
@@ -1164,6 +1193,9 @@ let check ~io ~token ~target ~doc () =
     Util.print_stats ();
     doc
 
+let check ~io ~token ~target ~doc () =
+  NewProfile.profile "Doc.check" (fun () -> check ~io ~token ~target ~doc ()) ()
+
 let save ~token ~doc =
   match doc.completed with
   | Yes _ ->

fleche/memo.ml

@@ -213,6 +213,8 @@ module type EvalType = sig
 
   type output
 
+  val name : string
+
   val eval :
     token:Coq.Limits.Token.t -> t -> (output, Coq.Loc_t.t) Coq.Protect.E.t
 
@@ -279,6 +281,10 @@ module SEval (E : EvalType) :
       let () = HC.add_execution cache i (res, stats) in
       (res, Stats.make ~stats ~cache_hit:false ~time_hash ())
 
+  let evalS ~token i =
+    let name = "Memo." ^ E.name in
+    NewProfile.profile name (fun () -> evalS ~token i) ()
+
   let eval ~token i = evalS ~token i |> fst
 end
 
@@ -330,10 +336,16 @@ module CEval (E : LocEvalType) = struct
       let () = HC.add_execution_loc cache i (stm_loc, res, stats) in
       (res, Stats.make ~stats ~cache_hit:false ~time_hash ())
 
+  let evalS ~token i =
+    let name = "Memo." ^ E.name in
+    NewProfile.profile name (fun () -> evalS ~token i) ()
+
   let eval ~token i = evalS ~token i |> fst
 end
 
 module VernacEval = struct
+  let name = "Interp"
+
   type t = Coq.State.t * Coq.Ast.t
 
   (* This crutially relies on our ppx to ignore the CAst location *)
@@ -356,6 +368,8 @@ end
 module Interp = CEval (VernacEval)
 
 module RequireEval = struct
+  let name = "Require"
+
   type t = Coq.State.t * Coq.Files.t * Coq.Ast.Require.t
 
   (* This crutially relies on our ppx to ignore the CAst location *)
@@ -387,13 +401,17 @@ module Require = CEval (RequireEval)
 module Admit = SEval (struct
   include Coq.State
 
+  let name = "Admit"
+
   type output = Coq.State.t
 
   let input_info st = Format.asprintf "st %d" (Hashtbl.hash st)
   let eval ~token st = Coq.State.admit ~token ~st
 end)
 
 module InitEval = struct
+  let name = "Init"
+
   type t = Coq.State.t * Coq.Workspace.t * Coq.Files.t * Lang.LUri.File.t
 
   let equal (s1, w1, f1, u1) (s2, w2, f2, u2) : bool =