Merge PR coq#19428: Add -profile support for coqchk

Reviewed-by: ppedrot Ack-by: JasonGross Ack-by: silene Co-authored-by: ppedrot <[email protected]>
Alizter · Sep 9, 2024 · 418501a · 418501a
2 parents 1b98a2f + c7f6485
commit 418501a
Show file tree

Hide file tree

Showing 9 changed files with 95 additions and 11 deletions.
diff --git a/checker/analyze.ml b/checker/analyze.ml
@@ -436,6 +436,11 @@ let parse chan =
   let () = fill ans 0 [] in
   (ans.(0), memory)
 
+let parse chan : _ * _ =
+  NewProfile.profile "analyze"
+    (fun () -> parse chan)
+    ()
+
 end
 
 module IChannel =
@@ -504,3 +509,6 @@ let instantiate (p, mem) =
     | String _ -> ()
   done;
   get_data p
+
+let instantiate pmem : Obj.t =
+  NewProfile.profile "instantiate" (fun () -> instantiate pmem) ()
diff --git a/checker/check.ml b/checker/check.ml
@@ -257,6 +257,16 @@ let try_locate_qualified_library lib = match lib with
     | LibUnmappedDir -> error_unmapped_dir qid
     | LibNotFound -> error_lib_not_found qid
 
+let lib_to_string = function
+  | PhysicalFile f -> f
+  | LogicalFile qid -> String.concat "." (List.rev (qid.basename :: qid.dirpath))
+
+let try_locate_qualified_library lib : _ * _ =
+  NewProfile.profile "try_locate_qualified_library"
+    ~args:(fun () -> [("name", `String (lib_to_string lib))])
+    (fun () -> try_locate_qualified_library lib)
+    ()
+
 (************************************************************************)
 (*s Low-level interning of libraries from files *)
 
@@ -304,6 +314,7 @@ type intern_mode = Rec | Root | Dep (* Rec = standard, Root = -norec, Dep = depe
 let depgraph = ref LibraryMap.empty
 
 let marshal_in_segment (type a) ~validate ~value ~(segment : a ObjFile.segment) f ch : a =
+  NewProfile.profile "marshal_in_segment" (fun () ->
   let () = LargeFile.seek_in ch segment.ObjFile.pos in
   if validate then
     let v =
@@ -319,7 +330,8 @@ let marshal_in_segment (type a) ~validate ~value ~(segment : a ObjFile.segment)
     let v = Analyze.instantiate v in
     Obj.obj v
   else
-    System.marshal_in f ch
+    System.marshal_in f ch)
+    ()
 
 let summary_seg : summary_disk ObjFile.id = ObjFile.make_id "summary"
 let library_seg : library_disk ObjFile.id = ObjFile.make_id "library"
@@ -363,6 +375,12 @@ let intern_from_file ~intern_mode ~enable_VM (dir, f) =
   opaque_tables := LibraryMap.add sd.md_name table !opaque_tables;
   mk_library sd md f table digest (Vmlibrary.inject vmlib)
 
+let intern_from_file ~intern_mode ~enable_VM dirf : library_t =
+  NewProfile.profile "intern_from_file"
+    ~args:(fun () -> [("name", `String (DirPath.to_string (fst dirf)))])
+    (fun () -> intern_from_file ~intern_mode ~enable_VM dirf)
+    ()
+
 (* Read a compiled library and all dependencies, in reverse order.
    Do not include files that are already in the context. *)
 let rec intern_library ~intern_mode ~enable_VM seen (dir, f) needed =

diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml
@@ -218,3 +218,9 @@ let check_inductive env mind mb =
   (* TODO non oracle flags *)
 
   add_mind mind mb env
+
+let check_inductive env mind mb : Environ.env =
+  NewProfile.profile "check_inductive"
+    ~args:(fun () -> [("name", `String (MutInd.to_string mind))])
+    (fun () -> check_inductive env mind mb)
+    ()
diff --git a/checker/checker.ml b/checker/checker.ml
@@ -127,6 +127,11 @@ let init_load_path () =
   (* then current directory *)
   add_path ~unix_path:"." ~coq_root:Check.default_root_prefix
 
+let init_load_path () : unit =
+  NewProfile.profile "init_load_path"
+    init_load_path
+    ()
+
 let impredicative_set = ref false
 let set_impredicative_set () = impredicative_set := true
 
@@ -188,6 +193,7 @@ let print_usage_channel co command =
 \n\
 \n  -d (d1,..,dn)               enable specified debug messages\
 \n  -debug                      enable all debug messages\
+\n  -profile file               output profiling info to file\
 \n  -where                      print coqchk's standard library location and exit\
 \n  -v, --version               print coqchk version and exit\
 \n  -o, --output-context        print the list of assumptions\
@@ -323,6 +329,8 @@ let explain_exn = function
                report ())
   | e -> CErrors.print e (* for anomalies and other uncaught exceptions *)
 
+let profile = ref None
+
 let parse_args argv =
   let rec parse = function
     | [] -> ()
@@ -355,6 +363,12 @@ let parse_args argv =
       parse rem
     | "-debug" :: rem -> CDebug.set_debug_all true; parse rem
 
+    | "-profile" :: s :: rem ->
+      profile := Some s;
+      parse rem
+
+    | "-profile" :: [] -> usage 1
+
     | "-where" :: _ ->
       let env = Boot.Env.init () in
       let coqlib = Boot.Env.coqlib env |> Boot.Path.to_string in
@@ -383,20 +397,30 @@ let parse_args argv =
   in
   parse (List.tl (Array.to_list argv))
 
+let init_profile ~file =
+  let ch = open_out file in
+  let fname = Filename.basename file in
+  NewProfile.init { output = Format.formatter_of_out_channel ch; fname; };
+  at_exit (fun () ->
+      NewProfile.finish ();
+      close_out ch)
 
 (* XXX: At some point we need to either port the checker to use the
    feedback system or to remove its use completely. *)
 let init_with_argv argv =
   let _fhandle = Feedback.(add_feeder (console_feedback_listener Format.err_formatter)) in
   try
     parse_args argv;
+    Option.iter (fun file -> init_profile ~file) !profile;
     if CDebug.(get_flag misc) then Printexc.record_backtrace true;
     Flags.if_verbose print_header ();
     if not !boot then init_load_path ();
     (* additional loadpath, given with -R/-Q options *)
-    List.iter
-      (fun (unix_path, coq_root) -> add_rec_path ~unix_path ~coq_root)
-      (List.rev !includes);
+    NewProfile.profile "add_load_paths" (fun () ->
+        List.iter
+          (fun (unix_path, coq_root) -> add_rec_path ~unix_path ~coq_root)
+          (List.rev !includes))
+      ();
     includes := [];
     make_senv ()
   with e ->

diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
@@ -79,7 +79,11 @@ let check_constant_declaration env opac kn cb opacify =
   | Some _ | None -> opac
 
 let check_constant_declaration env opac kn cb opacify =
-  let opac = check_constant_declaration env opac kn cb opacify in
+  let opac = NewProfile.profile "check_constant" ~args:(fun () ->
+      [("name", `String (Constant.to_string kn))])
+      (fun () -> check_constant_declaration env opac kn cb opacify)
+      ()
+  in
   Environ.add_constant kn cb env, opac
 
 let check_quality_mask env qmask lincheck =
@@ -297,4 +301,8 @@ and check_signature env opac sign mp_mse res opacify = match sign with
       in
       opac
 
-let check_module env opac mp mb = check_module env opac mp mb Cset.empty
+let check_module env opac mp mb =
+  NewProfile.profile "check_module"
+    ~args:(fun () -> [("name", `String (ModPath.to_string mp))])
+    (fun () -> check_module env opac mp mb Cset.empty)
+    ()
diff --git a/checker/safe_checking.ml b/checker/safe_checking.ml
@@ -21,5 +21,16 @@ let import senv opac clib vmtab digest =
   let opac = Mod_checking.check_module env opac mb.mod_mp mb in
   let (_,senv) = Safe_typing.import clib vmtab digest senv in senv, opac
 
+let import senv opac clib vmtab digest : _ * _ =
+  NewProfile.profile "import"
+    ~args:(fun () ->
+        let dp = match (Safe_typing.module_of_library clib).mod_mp with
+          | MPfile dp -> dp
+          | _ -> assert false
+        in
+        [("name", `String (Names.DirPath.to_string dp))])
+    (fun () ->import senv opac clib vmtab digest)
+    ()
+
 let unsafe_import senv clib vmtab digest =
   let (_,senv) = Safe_typing.import clib vmtab digest senv in senv
diff --git a/checker/validate.ml b/checker/validate.ml
@@ -233,8 +233,8 @@ let print_frame = function
 | CtxField i -> Printf.sprintf "fld=%i" i
 | CtxTag i -> Printf.sprintf "tag=%i" i
 
-let validate v (o, mem) =
-  try val_gen v mem mt_ec o
+let validate v (o, mem) : unit =
+  try NewProfile.profile "validate" (fun () -> val_gen v mem mt_ec o) ()
   with ValidObjError(msg,ctx,obj) ->
     let rctx = List.rev_map print_frame ctx in
     print_endline ("Context: "^String.concat"/"rctx);

diff --git a/doc/changelog/12-infrastructure-and-dependencies/19428-coqchk-profile.rst b/doc/changelog/12-infrastructure-and-dependencies/19428-coqchk-profile.rst
@@ -0,0 +1,8 @@
+- **Changed:**
+  `coq_makefile` generates profiling info for `coqc` in `foo.vo.prof.json.gz` instead of `foo.v.prof.json.gz`
+  (`#19428 <https://github.com/coq/coq/pull/19428>`_,
+  by Gaëtan Gilbert).
+- **Added:**
+  `coq_makefile` generates profiling info for `coqchk` in `validate.prof.json.gz`
+  (`#19428 <https://github.com/coq/coq/pull/19428>`_,
+  by Gaëtan Gilbert).
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
@@ -308,8 +308,8 @@ else
 endif
 
 ifneq (,$(PROFILING))
-  PROFILE_ARG=-profile $<.prof.json
-  PROFILE_ZIP=gzip -f $<.prof.json
+  PROFILE_ARG=-profile $@.prof.json
+  PROFILE_ZIP=gzip -f $@.prof.json
 else
   PROFILE_ARG=
   PROFILE_ZIP=true
@@ -510,7 +510,8 @@ vok: $(VOFILES:%.vo=%.vok)
 .PHONY: vok
 
 validate: $(VOFILES)
-	$(TIMER) $(COQCHK) $(COQCHKFLAGS) $(COQLIBS_NOML) $^
+	$(TIMER) $(COQCHK) $(COQCHKFLAGS) $(COQLIBS_NOML) $(PROFILE_ARG) $^
+	$(HIDE)$(PROFILE_ZIP)
 .PHONY: validate
 
 only: $(TGTS)