From d0f89f8c59cda2e7e74fec693e511e910fbc0434 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 5 Dec 2017 12:34:36 +0100 Subject: [lib] Rename Profile to CProfile New module introduced in OCaml 4.05 I think, can create problems when linking with the OCaml toplevel for `Drop`. --- checker/inductive.ml | 4 +- dev/doc/debugging.md | 4 +- engine/uState.ml | 4 +- engine/universes.ml | 4 +- kernel/cooking.ml | 4 +- kernel/inductive.ml | 4 +- kernel/reduction.ml | 16 +- kernel/typeops.ml | 4 +- kernel/uGraph.ml | 16 +- kernel/vars.ml | 12 +- lib/cProfile.ml | 714 ++++++++++++++++++++++++++++++++++++++++++++++ lib/cProfile.mli | 119 ++++++++ lib/lib.mllib | 2 +- lib/profile.ml | 714 ---------------------------------------------- lib/profile.mli | 119 -------- plugins/ltac/rewrite.ml | 8 +- pretyping/evarconv.ml | 4 +- pretyping/reductionops.ml | 8 +- pretyping/retyping.ml | 4 +- pretyping/tacred.ml | 4 +- pretyping/typeclasses.ml | 4 +- pretyping/unification.ml | 4 +- proofs/refiner.ml | 4 +- tactics/auto.ml | 4 +- tactics/eauto.ml | 4 +- tactics/tactics.ml | 8 +- toplevel/coqtop.ml | 4 +- 27 files changed, 900 insertions(+), 900 deletions(-) create mode 100644 lib/cProfile.ml create mode 100644 lib/cProfile.mli delete mode 100644 lib/profile.ml delete mode 100644 lib/profile.mli diff --git a/checker/inductive.ml b/checker/inductive.ml index 1271a02b0..22353ec16 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -1070,8 +1070,8 @@ let check_fix env ((nvect,_),(names,_,bodies as _recdef) as fix) = done (* -let cfkey = Profile.declare_profile "check_fix";; -let check_fix env fix = Profile.profile3 cfkey check_fix env fix;; +let cfkey = CProfile.declare_profile "check_fix";; +let check_fix env fix = CProfile.profile3 cfkey check_fix env fix;; *) (************************************************************************) diff --git a/dev/doc/debugging.md b/dev/doc/debugging.md index 7d3d811cc..fa145d498 100644 --- a/dev/doc/debugging.md +++ b/dev/doc/debugging.md @@ -73,8 +73,8 @@ Per function profiling To profile function foo in file bar.ml, add the following lines, just after the definition of the function: - let fookey = Profile.declare_profile "foo";; - let foo a b c = Profile.profile3 fookey foo a b c;; + let fookey = CProfile.declare_profile "foo";; + let foo a b c = CProfile.profile3 fookey foo a b c;; where foo is assumed to have three arguments (adapt using Profile.profile1, Profile. profile2, etc). diff --git a/engine/uState.ml b/engine/uState.ml index c28e78f7d..9510371be 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -236,8 +236,8 @@ let add_constraints ctx cstrs = uctx_univ_variables = vars; uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes } -(* let addconstrkey = Profile.declare_profile "add_constraints_context";; *) -(* let add_constraints_context = Profile.profile2 addconstrkey add_constraints_context;; *) +(* let addconstrkey = CProfile.declare_profile "add_constraints_context";; *) +(* let add_constraints_context = CProfile.profile2 addconstrkey add_constraints_context;; *) let add_universe_constraints ctx cstrs = let univs, local = ctx.uctx_local in diff --git a/engine/universes.ml b/engine/universes.ml index 0250295fd..30490ec56 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -946,8 +946,8 @@ let normalize_context_set ctx us algs = let us = normalize_opt_subst us in (us, algs), (ctx', Constraint.union noneqs eqs) -(* let normalize_conkey = Profile.declare_profile "normalize_context_set" *) -(* let normalize_context_set a b c = Profile.profile3 normalize_conkey normalize_context_set a b c *) +(* let normalize_conkey = CProfile.declare_profile "normalize_context_set" *) +(* let normalize_context_set a b c = CProfile.profile3 normalize_conkey normalize_context_set a b c *) let is_trivial_leq (l,d,r) = Univ.Level.is_prop l && (d == Univ.Le || (d == Univ.Lt && Univ.Level.is_set r)) diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 2579ac045..7b921d35b 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -250,7 +250,7 @@ let cook_constant ~hcons env { from = cb; info } = cook_context = Some const_hyps; } -(* let cook_constant_key = Profile.declare_profile "cook_constant" *) -(* let cook_constant = Profile.profile2 cook_constant_key cook_constant *) +(* let cook_constant_key = CProfile.declare_profile "cook_constant" *) +(* let cook_constant = CProfile.profile2 cook_constant_key cook_constant *) let expmod_constr modlist c = expmod_constr (RefTable.create 13) modlist c diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 62aa9a2d7..2a629f00a 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -1098,8 +1098,8 @@ let check_fix env ((nvect,_),(names,_,bodies as recdef) as fix) = () (* -let cfkey = Profile.declare_profile "check_fix";; -let check_fix env fix = Profile.profile3 cfkey check_fix env fix;; +let cfkey = CProfile.declare_profile "check_fix";; +let check_fix env fix = CProfile.profile3 cfkey check_fix env fix;; *) (************************************************************************) diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 41d6c05eb..ca67c5f13 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -833,8 +833,8 @@ let gen_conv cv_pb l2r reds env evars univs t1 t2 = let gen_conv cv_pb ?(l2r=false) ?(reds=full_transparent_state) env ?(evars=(fun _->None), universes env) = let evars, univs = evars in if Flags.profile then - let fconv_universes_key = Profile.declare_profile "trans_fconv_universes" in - Profile.profile8 fconv_universes_key gen_conv cv_pb l2r reds env evars univs + let fconv_universes_key = CProfile.declare_profile "trans_fconv_universes" in + CProfile.profile8 fconv_universes_key gen_conv cv_pb l2r reds env evars univs else gen_conv cv_pb l2r reds env evars univs let conv = gen_conv CONV @@ -860,8 +860,8 @@ let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 = (* Profiling *) let infer_conv_universes = if Flags.profile then - let infer_conv_universes_key = Profile.declare_profile "infer_conv_universes" in - Profile.profile8 infer_conv_universes_key infer_conv_universes + let infer_conv_universes_key = CProfile.declare_profile "infer_conv_universes" in + CProfile.profile8 infer_conv_universes_key infer_conv_universes else infer_conv_universes let infer_conv ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_state) @@ -895,13 +895,13 @@ let default_conv cv_pb ?(l2r=false) env t1 t2 = let default_conv_leq = default_conv CUMUL (* -let convleqkey = Profile.declare_profile "Kernel_reduction.conv_leq";; +let convleqkey = CProfile.declare_profile "Kernel_reduction.conv_leq";; let conv_leq env t1 t2 = - Profile.profile4 convleqkey conv_leq env t1 t2;; + CProfile.profile4 convleqkey conv_leq env t1 t2;; -let convkey = Profile.declare_profile "Kernel_reduction.conv";; +let convkey = CProfile.declare_profile "Kernel_reduction.conv";; let conv env t1 t2 = - Profile.profile4 convleqkey conv env t1 t2;; + CProfile.profile4 convleqkey conv env t1 t2;; *) (* Application with on-the-fly reduction *) diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 4ccef5c38..4a935f581 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -435,8 +435,8 @@ let infer env constr = let infer = if Flags.profile then - let infer_key = Profile.declare_profile "Fast_infer" in - Profile.profile2 infer_key (fun b c -> infer b c) + let infer_key = CProfile.declare_profile "Fast_infer" in + CProfile.profile2 infer_key (fun b c -> infer b c) else (fun b c -> infer b c) let assumption_of_judgment env {uj_val=c; uj_type=t} = diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 00c0ea70d..f1e8d1031 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -890,24 +890,24 @@ let dump_universes output g = let merge_constraints = if Flags.profile then - let key = Profile.declare_profile "merge_constraints" in - Profile.profile2 key merge_constraints + let key = CProfile.declare_profile "merge_constraints" in + CProfile.profile2 key merge_constraints else merge_constraints let check_constraints = if Flags.profile then - let key = Profile.declare_profile "check_constraints" in - Profile.profile2 key check_constraints + let key = CProfile.declare_profile "check_constraints" in + CProfile.profile2 key check_constraints else check_constraints let check_eq = if Flags.profile then - let check_eq_key = Profile.declare_profile "check_eq" in - Profile.profile3 check_eq_key check_eq + let check_eq_key = CProfile.declare_profile "check_eq" in + CProfile.profile3 check_eq_key check_eq else check_eq let check_leq = if Flags.profile then - let check_leq_key = Profile.declare_profile "check_leq" in - Profile.profile3 check_leq_key check_leq + let check_leq_key = CProfile.declare_profile "check_leq" in + CProfile.profile3 check_leq_key check_leq else check_leq diff --git a/kernel/vars.ml b/kernel/vars.ml index f52d734ef..eae917b5a 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -133,8 +133,8 @@ let substn_many lamv n c = substrec n c (* -let substkey = Profile.declare_profile "substn_many";; -let substn_many lamv n c = Profile.profile3 substkey substn_many lamv n c;; +let substkey = CProfile.declare_profile "substn_many";; +let substn_many lamv n c = CProfile.profile3 substkey substn_many lamv n c;; *) let make_subst = function @@ -274,8 +274,8 @@ let subst_univs_constr subst c = let subst_univs_constr = if Flags.profile then - let subst_univs_constr_key = Profile.declare_profile "subst_univs_constr" in - Profile.profile2 subst_univs_constr_key subst_univs_constr + let subst_univs_constr_key = CProfile.declare_profile "subst_univs_constr" in + CProfile.profile2 subst_univs_constr_key subst_univs_constr else subst_univs_constr let subst_univs_level_constr subst c = @@ -347,8 +347,8 @@ let subst_instance_constr subst c = in aux c -(* let substkey = Profile.declare_profile "subst_instance_constr";; *) -(* let subst_instance_constr inst c = Profile.profile2 substkey subst_instance_constr inst c;; *) +(* let substkey = CProfile.declare_profile "subst_instance_constr";; *) +(* let subst_instance_constr inst c = CProfile.profile2 substkey subst_instance_constr inst c;; *) let subst_instance_context s ctx = if Univ.Instance.is_empty s then ctx diff --git a/lib/cProfile.ml b/lib/cProfile.ml new file mode 100644 index 000000000..0bc226a45 --- /dev/null +++ b/lib/cProfile.ml @@ -0,0 +1,714 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* [] || Flags.profile then begin + let outside = create_record () in + stack := [outside]; + last_alloc := get_alloc (); + init_alloc := !last_alloc; + init_time := get_time (); + outside.tottime <- - !init_time; + outside.owntime <- - !init_time + end + +let ajoute n o = + o.owntime <- o.owntime + n.owntime; + o.tottime <- o.tottime + n.tottime; + ajoute_ownalloc o n.ownalloc; + ajoute_totalloc o n.totalloc; + o.owncount <- o.owncount + n.owncount; + o.intcount <- o.intcount + n.intcount; + o.immcount <- o.immcount + n.immcount + +let ajoute_to_list ((name,n) as e) l = + try ajoute n (List.assoc name l); l + with Not_found -> e::l + +let magic = 1249 + +let merge_profile filename (curr_table, curr_outside, curr_total as new_data) = + let (old_table, old_outside, old_total) = + try + let c = open_in filename in + if input_binary_int c <> magic + then Printf.printf "Incompatible recording file: %s\n" filename; + let old_data = input_value c in + close_in c; + old_data + with Sys_error msg -> + (Printf.printf "Unable to open %s: %s\n" filename msg; + new_data) in + let updated_data = + let updated_table = List.fold_right ajoute_to_list curr_table old_table in + ajoute curr_outside old_outside; + ajoute curr_total old_total; + (updated_table, old_outside, old_total) in + begin + (try + let c = + open_out_gen + [Open_creat;Open_wronly;Open_trunc;Open_binary] 0o644 filename in + output_binary_int c magic; + output_value c updated_data; + close_out c + with Sys_error _ -> Printf.printf "Unable to create recording file"); + updated_data + end + +(************************************************) +(* Compute a rough estimation of time overheads *) + +(* Time and space are not measured in the same way *) + +(* Byte allocation is an exact number and for long runs, the total + number of allocated bytes may exceed the maximum integer capacity + (2^31 on 32-bits architectures); therefore, allocation is measured + by small steps, total allocations are computed by adding elementary + measures and carries are controlled from step to step *) + +(* Unix measure of time is approximate and short delays are often + unperceivable; therefore, total times are measured in one (big) + step to avoid rounding errors and to get the best possible + approximation. + Note: Sys.time is the same as: + Unix.(let x = times () in x.tms_utime +. x.tms_stime) + *) + +(* +---------- start profile for f1 +overheadA| ... + ---------- [1w1] 1st call to get_time for f1 + overheadB| ... + ---------- start f1 + real 1 | ... + ---------- start profile for 1st call to f2 inside f1 + overheadA| ... + ---------- [2w1] 1st call to get_time for 1st f2 + overheadB| ... + ---------- start 1st f2 + real 2 | ... + ---------- end 1st f2 + overheadC| ... + ---------- [2w1] 2nd call to get_time for 1st f2 + overheadD| ... + ---------- end profile for 1st f2 + real 1 | ... + ---------- start profile for 2nd call to f2 inside f1 + overheadA| ... + ---------- [2'w1] 1st call to get_time for 2nd f2 + overheadB| ... + ---------- start 2nd f2 + real 2' | ... + ---------- end 2nd f2 + overheadC| ... + ---------- [2'w2] 2nd call to get_time for 2nd f2 + overheadD| ... + ---------- end profile for f2 + real 1 | ... + ---------- end f1 + overheadC| ... +---------- [1w1'] 2nd call to get_time for f1 +overheadD| ... +---------- end profile for f1 + +When profiling f2, overheadB + overheadC should be subtracted from measure +and overheadA + overheadB + overheadC + overheadD should be subtracted from +the amount for f1 + +Then the relevant overheads are : + + "overheadB + overheadC" to be subtracted to the measure of f as many time as f is called and + + "overheadA + overheadB + overheadC + overheadD" to be subtracted to + the measure of f as many time as f calls a profiled function (itself + included) +*) + +let dummy_last_alloc = ref 0.0 +let dummy_spent_alloc () = + let now = get_alloc () in + let before = !last_alloc in + last_alloc := now; + now -. before +let dummy_f x = x +let dummy_stack = ref [create_record ()] +let dummy_ov = 0 + +let loops = 10000 + +let time_overhead_A_D () = + let e = create_record () in + let before = get_time () in + for _i = 1 to loops do + (* This is a copy of profile1 for overhead estimation *) + let dw = dummy_spent_alloc () in + match !dummy_stack with [] -> assert false | p::_ -> + ajoute_ownalloc p dw; + ajoute_totalloc p dw; + e.owncount <- e.owncount + 1; + if not (p==e) then stack := e::!stack; + let totalloc0 = e.totalloc in + let intcount0 = e.intcount in + let dt = get_time () - 1 in + e.tottime <- dt + dummy_ov; e.owntime <- e.owntime + e.tottime; + ajoute_ownalloc p dw; + ajoute_totalloc p dw; + p.owntime <- p.owntime - e.tottime; + ajoute_totalloc p (e.totalloc-.totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !dummy_stack with [] -> assert false | _::s -> stack := s); + dummy_last_alloc := get_alloc () + done; + let after = get_time () in + let beforeloop = get_time () in + for _i = 1 to loops do () done; + let afterloop = get_time () in + float_of_int ((after - before) - (afterloop - beforeloop)) + /. float_of_int loops + +let time_overhead_B_C () = + let dummy_x = 0 in + let before = get_time () in + for _i = 1 to loops do + try + dummy_last_alloc := get_alloc (); + let _r = dummy_f dummy_x in + let _dw = dummy_spent_alloc () in + let _dt = get_time () in + () + with e when CErrors.noncritical e -> assert false + done; + let after = get_time () in + let beforeloop = get_time () in + for _i = 1 to loops do () done; + let afterloop = get_time () in + float_of_int ((after - before) - (afterloop - beforeloop)) + /. float_of_int loops + +let compute_alloc lo = lo /. (float_of_int word_length) + +(************************************************) +(* End a profiling session and print the result *) + +let format_profile (table, outside, total) = + print_newline (); + Printf.printf + "%-23s %9s %9s %10s %10s %10s\n" + "Function name" "Own time" "Tot. time" "Own alloc" "Tot. alloc" "Calls "; + let l = List.sort (fun (_,{tottime=p}) (_,{tottime=p'}) -> p' - p) table in + List.iter (fun (name,e) -> + Printf.printf + "%-23s %9.2f %9.2f %10.0f %10.0f %6d %6d\n" + name + (float_of_time e.owntime) (float_of_time e.tottime) + (compute_alloc e.ownalloc) + (compute_alloc e.totalloc) + e.owncount e.intcount) + l; + Printf.printf "%-23s %9.2f %9.2f %10.0f %10.0f %6d\n" + "others" + (float_of_time outside.owntime) (float_of_time outside.tottime) + (compute_alloc outside.ownalloc) + (compute_alloc outside.totalloc) + outside.intcount; + (* Here, own contains overhead time/alloc *) + Printf.printf "%-23s %9.2f %9.2f %10.0f %10.0f\n" + "Est. overhead/total" + (float_of_time total.owntime) (float_of_time total.tottime) + (compute_alloc total.ownalloc) + (compute_alloc total.totalloc); + Printf.printf + "Time in seconds and allocation in words (1 word = %d bytes)\n" + word_length + +let recording_file = ref "" +let set_recording s = recording_file := s + +let adjust_time ov_bc ov_ad e = + let bc_imm = float_of_int e.owncount *. ov_bc in + let ad_imm = float_of_int e.immcount *. ov_ad in + let abcd_all = float_of_int e.intcount *. (ov_ad +. ov_bc) in + {e with + tottime = e.tottime - int_of_float (abcd_all +. bc_imm); + owntime = e.owntime - int_of_float (ad_imm +. bc_imm) } + +let close_profile print = + if !prof_table <> [] then begin + let dw = spent_alloc () in + let t = get_time () in + match !stack with + | [outside] -> + outside.tottime <- outside.tottime + t; + outside.owntime <- outside.owntime + t; + ajoute_ownalloc outside dw; + ajoute_totalloc outside dw; + let ov_bc = time_overhead_B_C () (* B+C overhead *) in + let ov_ad = time_overhead_A_D () (* A+D overhead *) in + let adjust (n,e) = (n, adjust_time ov_bc ov_ad e) in + let adjtable = List.map adjust !prof_table in + let adjoutside = adjust_time ov_bc ov_ad outside in + let totalloc = !last_alloc -. !init_alloc in + let total = create_record () in + total.tottime <- outside.tottime; + total.totalloc <- totalloc; + (* We compute estimations of overhead, put into "own" fields *) + total.owntime <- outside.tottime - adjoutside.tottime; + total.ownalloc <- totalloc -. outside.totalloc; + let current_data = (adjtable, adjoutside, total) in + let updated_data = + match !recording_file with + | "" -> current_data + | name -> merge_profile !recording_file current_data + in + if print then format_profile updated_data; + init_profile () + | _ -> failwith "Inconsistency" + end + +let print_profile () = close_profile true + +let declare_profile name = + if name = "___outside___" || name = "___total___" then + failwith ("Error: "^name^" is a reserved keyword"); + let e = create_record () in + prof_table := (name,e)::!prof_table; + e + +(******************************) +(* Entry points for profiling *) +let profile1 e f a = + let dw = spent_alloc () in + match !stack with [] -> assert false | p::_ -> + (* We add spent alloc since last measure to current caller own/total alloc *) + ajoute_ownalloc p dw; + ajoute_totalloc p dw; + e.owncount <- e.owncount + 1; + if not (p==e) then stack := e::!stack; + let totalloc0 = e.totalloc in + let intcount0 = e.intcount in + let t = get_time () in + try + last_alloc := get_alloc (); + let r = f a in + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + r + with reraise -> + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + raise reraise + +let profile2 e f a b = + let dw = spent_alloc () in + match !stack with [] -> assert false | p::_ -> + (* We add spent alloc since last measure to current caller own/total alloc *) + ajoute_ownalloc p dw; + ajoute_totalloc p dw; + e.owncount <- e.owncount + 1; + if not (p==e) then stack := e::!stack; + let totalloc0 = e.totalloc in + let intcount0 = e.intcount in + let t = get_time () in + try + last_alloc := get_alloc (); + let r = f a b in + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + r + with reraise -> + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + raise reraise + +let profile3 e f a b c = + let dw = spent_alloc () in + match !stack with [] -> assert false | p::_ -> + (* We add spent alloc since last measure to current caller own/total alloc *) + ajoute_ownalloc p dw; + ajoute_totalloc p dw; + e.owncount <- e.owncount + 1; + if not (p==e) then stack := e::!stack; + let totalloc0 = e.totalloc in + let intcount0 = e.intcount in + let t = get_time () in + try + last_alloc := get_alloc (); + let r = f a b c in + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + r + with reraise -> + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + raise reraise + +let profile4 e f a b c d = + let dw = spent_alloc () in + match !stack with [] -> assert false | p::_ -> + (* We add spent alloc since last measure to current caller own/total alloc *) + ajoute_ownalloc p dw; + ajoute_totalloc p dw; + e.owncount <- e.owncount + 1; + if not (p==e) then stack := e::!stack; + let totalloc0 = e.totalloc in + let intcount0 = e.intcount in + let t = get_time () in + try + last_alloc := get_alloc (); + let r = f a b c d in + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + r + with reraise -> + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + raise reraise + +let profile5 e f a b c d g = + let dw = spent_alloc () in + match !stack with [] -> assert false | p::_ -> + (* We add spent alloc since last measure to current caller own/total alloc *) + ajoute_ownalloc p dw; + ajoute_totalloc p dw; + e.owncount <- e.owncount + 1; + if not (p==e) then stack := e::!stack; + let totalloc0 = e.totalloc in + let intcount0 = e.intcount in + let t = get_time () in + try + last_alloc := get_alloc (); + let r = f a b c d g in + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + r + with reraise -> + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + raise reraise + +let profile6 e f a b c d g h = + let dw = spent_alloc () in + match !stack with [] -> assert false | p::_ -> + (* We add spent alloc since last measure to current caller own/total alloc *) + ajoute_ownalloc p dw; + ajoute_totalloc p dw; + e.owncount <- e.owncount + 1; + if not (p==e) then stack := e::!stack; + let totalloc0 = e.totalloc in + let intcount0 = e.intcount in + let t = get_time () in + try + last_alloc := get_alloc (); + let r = f a b c d g h in + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + r + with reraise -> + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + raise reraise + +let profile7 e f a b c d g h i = + let dw = spent_alloc () in + match !stack with [] -> assert false | p::_ -> + (* We add spent alloc since last measure to current caller own/total alloc *) + ajoute_ownalloc p dw; + ajoute_totalloc p dw; + e.owncount <- e.owncount + 1; + if not (p==e) then stack := e::!stack; + let totalloc0 = e.totalloc in + let intcount0 = e.intcount in + let t = get_time () in + try + last_alloc := get_alloc (); + let r = f a b c d g h i in + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + r + with reraise -> + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + raise reraise + +let profile8 e f a b c d g h i j = + let dw = spent_alloc () in + match !stack with [] -> assert false | p::_ -> + (* We add spent alloc since last measure to current caller own/total alloc *) + ajoute_ownalloc p dw; + ajoute_totalloc p dw; + e.owncount <- e.owncount + 1; + if not (p==e) then stack := e::!stack; + let totalloc0 = e.totalloc in + let intcount0 = e.intcount in + let t = get_time () in + try + last_alloc := get_alloc (); + let r = f a b c d g h i j in + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + r + with reraise -> + let dw = spent_alloc () in + let dt = get_time () - t in + e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; + ajoute_ownalloc e dw; + ajoute_totalloc e dw; + p.owntime <- p.owntime - dt; + ajoute_totalloc p (e.totalloc -. totalloc0); + p.intcount <- p.intcount + e.intcount - intcount0 + 1; + p.immcount <- p.immcount + 1; + if not (p==e) then + (match !stack with [] -> assert false | _::s -> stack := s); + last_alloc := get_alloc (); + raise reraise + +let print_logical_stats a = + let (c, s, d) = CObj.obj_stats a in + Printf.printf "Expanded size: %10d (str: %8d) Depth: %6d\n" (s+c) c d + +let print_stats a = + let (c1, s, d) = CObj.obj_stats a in + let c2 = CObj.size a in + Printf.printf "Size: %8d (exp: %10d) Depth: %6d\n" + c2 (s + c1) d +(* +let _ = Gc.set { (Gc.get()) with Gc.verbose = 13 } +*) diff --git a/lib/cProfile.mli b/lib/cProfile.mli new file mode 100644 index 000000000..cae4397a1 --- /dev/null +++ b/lib/cProfile.mli @@ -0,0 +1,119 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* unit + +val print_profile : unit -> unit +val reset_profile : unit -> unit +val init_profile : unit -> unit +val declare_profile : string -> profile_key + +val profile1 : profile_key -> ('a -> 'b) -> 'a -> 'b +val profile2 : profile_key -> ('a -> 'b -> 'c) -> 'a -> 'b -> 'c +val profile3 : + profile_key -> ('a -> 'b -> 'c -> 'd) -> 'a -> 'b -> 'c -> 'd +val profile4 : + profile_key -> ('a -> 'b -> 'c -> 'd -> 'e) -> 'a -> 'b -> 'c -> 'd -> 'e +val profile5 : + profile_key -> + ('a -> 'b -> 'c -> 'd -> 'e -> 'f) -> 'a -> 'b -> 'c -> 'd -> 'e -> 'f +val profile6 : + profile_key -> + ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g) + -> 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g +val profile7 : + profile_key -> + ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h) + -> 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h +val profile8 : + profile_key -> + ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i) + -> 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i + + +(** Some utilities to compute the logical and physical sizes and depth + of ML objects *) + +(** Print logical size (in words) and depth of its argument + This function does not disturb the heap *) +val print_logical_stats : 'a -> unit + +(** Print physical size, logical size (in words) and depth of its argument + This function allocates itself a lot (the same order of magnitude + as the physical size of its argument) *) +val print_stats : 'a -> unit diff --git a/lib/lib.mllib b/lib/lib.mllib index 8791f0741..66f939a91 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -9,7 +9,7 @@ System CThread Spawn Trie -Profile +CProfile Explore Predicate Rtree diff --git a/lib/profile.ml b/lib/profile.ml deleted file mode 100644 index 0bc226a45..000000000 --- a/lib/profile.ml +++ /dev/null @@ -1,714 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* [] || Flags.profile then begin - let outside = create_record () in - stack := [outside]; - last_alloc := get_alloc (); - init_alloc := !last_alloc; - init_time := get_time (); - outside.tottime <- - !init_time; - outside.owntime <- - !init_time - end - -let ajoute n o = - o.owntime <- o.owntime + n.owntime; - o.tottime <- o.tottime + n.tottime; - ajoute_ownalloc o n.ownalloc; - ajoute_totalloc o n.totalloc; - o.owncount <- o.owncount + n.owncount; - o.intcount <- o.intcount + n.intcount; - o.immcount <- o.immcount + n.immcount - -let ajoute_to_list ((name,n) as e) l = - try ajoute n (List.assoc name l); l - with Not_found -> e::l - -let magic = 1249 - -let merge_profile filename (curr_table, curr_outside, curr_total as new_data) = - let (old_table, old_outside, old_total) = - try - let c = open_in filename in - if input_binary_int c <> magic - then Printf.printf "Incompatible recording file: %s\n" filename; - let old_data = input_value c in - close_in c; - old_data - with Sys_error msg -> - (Printf.printf "Unable to open %s: %s\n" filename msg; - new_data) in - let updated_data = - let updated_table = List.fold_right ajoute_to_list curr_table old_table in - ajoute curr_outside old_outside; - ajoute curr_total old_total; - (updated_table, old_outside, old_total) in - begin - (try - let c = - open_out_gen - [Open_creat;Open_wronly;Open_trunc;Open_binary] 0o644 filename in - output_binary_int c magic; - output_value c updated_data; - close_out c - with Sys_error _ -> Printf.printf "Unable to create recording file"); - updated_data - end - -(************************************************) -(* Compute a rough estimation of time overheads *) - -(* Time and space are not measured in the same way *) - -(* Byte allocation is an exact number and for long runs, the total - number of allocated bytes may exceed the maximum integer capacity - (2^31 on 32-bits architectures); therefore, allocation is measured - by small steps, total allocations are computed by adding elementary - measures and carries are controlled from step to step *) - -(* Unix measure of time is approximate and short delays are often - unperceivable; therefore, total times are measured in one (big) - step to avoid rounding errors and to get the best possible - approximation. - Note: Sys.time is the same as: - Unix.(let x = times () in x.tms_utime +. x.tms_stime) - *) - -(* ----------- start profile for f1 -overheadA| ... - ---------- [1w1] 1st call to get_time for f1 - overheadB| ... - ---------- start f1 - real 1 | ... - ---------- start profile for 1st call to f2 inside f1 - overheadA| ... - ---------- [2w1] 1st call to get_time for 1st f2 - overheadB| ... - ---------- start 1st f2 - real 2 | ... - ---------- end 1st f2 - overheadC| ... - ---------- [2w1] 2nd call to get_time for 1st f2 - overheadD| ... - ---------- end profile for 1st f2 - real 1 | ... - ---------- start profile for 2nd call to f2 inside f1 - overheadA| ... - ---------- [2'w1] 1st call to get_time for 2nd f2 - overheadB| ... - ---------- start 2nd f2 - real 2' | ... - ---------- end 2nd f2 - overheadC| ... - ---------- [2'w2] 2nd call to get_time for 2nd f2 - overheadD| ... - ---------- end profile for f2 - real 1 | ... - ---------- end f1 - overheadC| ... ----------- [1w1'] 2nd call to get_time for f1 -overheadD| ... ----------- end profile for f1 - -When profiling f2, overheadB + overheadC should be subtracted from measure -and overheadA + overheadB + overheadC + overheadD should be subtracted from -the amount for f1 - -Then the relevant overheads are : - - "overheadB + overheadC" to be subtracted to the measure of f as many time as f is called and - - "overheadA + overheadB + overheadC + overheadD" to be subtracted to - the measure of f as many time as f calls a profiled function (itself - included) -*) - -let dummy_last_alloc = ref 0.0 -let dummy_spent_alloc () = - let now = get_alloc () in - let before = !last_alloc in - last_alloc := now; - now -. before -let dummy_f x = x -let dummy_stack = ref [create_record ()] -let dummy_ov = 0 - -let loops = 10000 - -let time_overhead_A_D () = - let e = create_record () in - let before = get_time () in - for _i = 1 to loops do - (* This is a copy of profile1 for overhead estimation *) - let dw = dummy_spent_alloc () in - match !dummy_stack with [] -> assert false | p::_ -> - ajoute_ownalloc p dw; - ajoute_totalloc p dw; - e.owncount <- e.owncount + 1; - if not (p==e) then stack := e::!stack; - let totalloc0 = e.totalloc in - let intcount0 = e.intcount in - let dt = get_time () - 1 in - e.tottime <- dt + dummy_ov; e.owntime <- e.owntime + e.tottime; - ajoute_ownalloc p dw; - ajoute_totalloc p dw; - p.owntime <- p.owntime - e.tottime; - ajoute_totalloc p (e.totalloc-.totalloc0); - p.intcount <- p.intcount + e.intcount - intcount0 + 1; - p.immcount <- p.immcount + 1; - if not (p==e) then - (match !dummy_stack with [] -> assert false | _::s -> stack := s); - dummy_last_alloc := get_alloc () - done; - let after = get_time () in - let beforeloop = get_time () in - for _i = 1 to loops do () done; - let afterloop = get_time () in - float_of_int ((after - before) - (afterloop - beforeloop)) - /. float_of_int loops - -let time_overhead_B_C () = - let dummy_x = 0 in - let before = get_time () in - for _i = 1 to loops do - try - dummy_last_alloc := get_alloc (); - let _r = dummy_f dummy_x in - let _dw = dummy_spent_alloc () in - let _dt = get_time () in - () - with e when CErrors.noncritical e -> assert false - done; - let after = get_time () in - let beforeloop = get_time () in - for _i = 1 to loops do () done; - let afterloop = get_time () in - float_of_int ((after - before) - (afterloop - beforeloop)) - /. float_of_int loops - -let compute_alloc lo = lo /. (float_of_int word_length) - -(************************************************) -(* End a profiling session and print the result *) - -let format_profile (table, outside, total) = - print_newline (); - Printf.printf - "%-23s %9s %9s %10s %10s %10s\n" - "Function name" "Own time" "Tot. time" "Own alloc" "Tot. alloc" "Calls "; - let l = List.sort (fun (_,{tottime=p}) (_,{tottime=p'}) -> p' - p) table in - List.iter (fun (name,e) -> - Printf.printf - "%-23s %9.2f %9.2f %10.0f %10.0f %6d %6d\n" - name - (float_of_time e.owntime) (float_of_time e.tottime) - (compute_alloc e.ownalloc) - (compute_alloc e.totalloc) - e.owncount e.intcount) - l; - Printf.printf "%-23s %9.2f %9.2f %10.0f %10.0f %6d\n" - "others" - (float_of_time outside.owntime) (float_of_time outside.tottime) - (compute_alloc outside.ownalloc) - (compute_alloc outside.totalloc) - outside.intcount; - (* Here, own contains overhead time/alloc *) - Printf.printf "%-23s %9.2f %9.2f %10.0f %10.0f\n" - "Est. overhead/total" - (float_of_time total.owntime) (float_of_time total.tottime) - (compute_alloc total.ownalloc) - (compute_alloc total.totalloc); - Printf.printf - "Time in seconds and allocation in words (1 word = %d bytes)\n" - word_length - -let recording_file = ref "" -let set_recording s = recording_file := s - -let adjust_time ov_bc ov_ad e = - let bc_imm = float_of_int e.owncount *. ov_bc in - let ad_imm = float_of_int e.immcount *. ov_ad in - let abcd_all = float_of_int e.intcount *. (ov_ad +. ov_bc) in - {e with - tottime = e.tottime - int_of_float (abcd_all +. bc_imm); - owntime = e.owntime - int_of_float (ad_imm +. bc_imm) } - -let close_profile print = - if !prof_table <> [] then begin - let dw = spent_alloc () in - let t = get_time () in - match !stack with - | [outside] -> - outside.tottime <- outside.tottime + t; - outside.owntime <- outside.owntime + t; - ajoute_ownalloc outside dw; - ajoute_totalloc outside dw; - let ov_bc = time_overhead_B_C () (* B+C overhead *) in - let ov_ad = time_overhead_A_D () (* A+D overhead *) in - let adjust (n,e) = (n, adjust_time ov_bc ov_ad e) in - let adjtable = List.map adjust !prof_table in - let adjoutside = adjust_time ov_bc ov_ad outside in - let totalloc = !last_alloc -. !init_alloc in - let total = create_record () in - total.tottime <- outside.tottime; - total.totalloc <- totalloc; - (* We compute estimations of overhead, put into "own" fields *) - total.owntime <- outside.tottime - adjoutside.tottime; - total.ownalloc <- totalloc -. outside.totalloc; - let current_data = (adjtable, adjoutside, total) in - let updated_data = - match !recording_file with - | "" -> current_data - | name -> merge_profile !recording_file current_data - in - if print then format_profile updated_data; - init_profile () - | _ -> failwith "Inconsistency" - end - -let print_profile () = close_profile true - -let declare_profile name = - if name = "___outside___" || name = "___total___" then - failwith ("Error: "^name^" is a reserved keyword"); - let e = create_record () in - prof_table := (name,e)::!prof_table; - e - -(******************************) -(* Entry points for profiling *) -let profile1 e f a = - let dw = spent_alloc () in - match !stack with [] -> assert false | p::_ -> - (* We add spent alloc since last measure to current caller own/total alloc *) - ajoute_ownalloc p dw; - ajoute_totalloc p dw; - e.owncount <- e.owncount + 1; - if not (p==e) then stack := e::!stack; - let totalloc0 = e.totalloc in - let intcount0 = e.intcount in - let t = get_time () in - try - last_alloc := get_alloc (); - let r = f a in - let dw = spent_alloc () in - let dt = get_time () - t in - e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; - ajoute_ownalloc e dw; - ajoute_totalloc e dw; - p.owntime <- p.owntime - dt; - ajoute_totalloc p (e.totalloc -. totalloc0); - p.intcount <- p.intcount + e.intcount - intcount0 + 1; - p.immcount <- p.immcount + 1; - if not (p==e) then - (match !stack with [] -> assert false | _::s -> stack := s); - last_alloc := get_alloc (); - r - with reraise -> - let dw = spent_alloc () in - let dt = get_time () - t in - e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; - ajoute_ownalloc e dw; - ajoute_totalloc e dw; - p.owntime <- p.owntime - dt; - ajoute_totalloc p (e.totalloc -. totalloc0); - p.intcount <- p.intcount + e.intcount - intcount0 + 1; - p.immcount <- p.immcount + 1; - if not (p==e) then - (match !stack with [] -> assert false | _::s -> stack := s); - last_alloc := get_alloc (); - raise reraise - -let profile2 e f a b = - let dw = spent_alloc () in - match !stack with [] -> assert false | p::_ -> - (* We add spent alloc since last measure to current caller own/total alloc *) - ajoute_ownalloc p dw; - ajoute_totalloc p dw; - e.owncount <- e.owncount + 1; - if not (p==e) then stack := e::!stack; - let totalloc0 = e.totalloc in - let intcount0 = e.intcount in - let t = get_time () in - try - last_alloc := get_alloc (); - let r = f a b in - let dw = spent_alloc () in - let dt = get_time () - t in - e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; - ajoute_ownalloc e dw; - ajoute_totalloc e dw; - p.owntime <- p.owntime - dt; - ajoute_totalloc p (e.totalloc -. totalloc0); - p.intcount <- p.intcount + e.intcount - intcount0 + 1; - p.immcount <- p.immcount + 1; - if not (p==e) then - (match !stack with [] -> assert false | _::s -> stack := s); - last_alloc := get_alloc (); - r - with reraise -> - let dw = spent_alloc () in - let dt = get_time () - t in - e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; - ajoute_ownalloc e dw; - ajoute_totalloc e dw; - p.owntime <- p.owntime - dt; - ajoute_totalloc p (e.totalloc -. totalloc0); - p.intcount <- p.intcount + e.intcount - intcount0 + 1; - p.immcount <- p.immcount + 1; - if not (p==e) then - (match !stack with [] -> assert false | _::s -> stack := s); - last_alloc := get_alloc (); - raise reraise - -let profile3 e f a b c = - let dw = spent_alloc () in - match !stack with [] -> assert false | p::_ -> - (* We add spent alloc since last measure to current caller own/total alloc *) - ajoute_ownalloc p dw; - ajoute_totalloc p dw; - e.owncount <- e.owncount + 1; - if not (p==e) then stack := e::!stack; - let totalloc0 = e.totalloc in - let intcount0 = e.intcount in - let t = get_time () in - try - last_alloc := get_alloc (); - let r = f a b c in - let dw = spent_alloc () in - let dt = get_time () - t in - e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; - ajoute_ownalloc e dw; - ajoute_totalloc e dw; - p.owntime <- p.owntime - dt; - ajoute_totalloc p (e.totalloc -. totalloc0); - p.intcount <- p.intcount + e.intcount - intcount0 + 1; - p.immcount <- p.immcount + 1; - if not (p==e) then - (match !stack with [] -> assert false | _::s -> stack := s); - last_alloc := get_alloc (); - r - with reraise -> - let dw = spent_alloc () in - let dt = get_time () - t in - e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; - ajoute_ownalloc e dw; - ajoute_totalloc e dw; - p.owntime <- p.owntime - dt; - ajoute_totalloc p (e.totalloc -. totalloc0); - p.intcount <- p.intcount + e.intcount - intcount0 + 1; - p.immcount <- p.immcount + 1; - if not (p==e) then - (match !stack with [] -> assert false | _::s -> stack := s); - last_alloc := get_alloc (); - raise reraise - -let profile4 e f a b c d = - let dw = spent_alloc () in - match !stack with [] -> assert false | p::_ -> - (* We add spent alloc since last measure to current caller own/total alloc *) - ajoute_ownalloc p dw; - ajoute_totalloc p dw; - e.owncount <- e.owncount + 1; - if not (p==e) then stack := e::!stack; - let totalloc0 = e.totalloc in - let intcount0 = e.intcount in - let t = get_time () in - try - last_alloc := get_alloc (); - let r = f a b c d in - let dw = spent_alloc () in - let dt = get_time () - t in - e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; - ajoute_ownalloc e dw; - ajoute_totalloc e dw; - p.owntime <- p.owntime - dt; - ajoute_totalloc p (e.totalloc -. totalloc0); - p.intcount <- p.intcount + e.intcount - intcount0 + 1; - p.immcount <- p.immcount + 1; - if not (p==e) then - (match !stack with [] -> assert false | _::s -> stack := s); - last_alloc := get_alloc (); - r - with reraise -> - let dw = spent_alloc () in - let dt = get_time () - t in - e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; - ajoute_ownalloc e dw; - ajoute_totalloc e dw; - p.owntime <- p.owntime - dt; - ajoute_totalloc p (e.totalloc -. totalloc0); - p.intcount <- p.intcount + e.intcount - intcount0 + 1; - p.immcount <- p.immcount + 1; - if not (p==e) then - (match !stack with [] -> assert false | _::s -> stack := s); - last_alloc := get_alloc (); - raise reraise - -let profile5 e f a b c d g = - let dw = spent_alloc () in - match !stack with [] -> assert false | p::_ -> - (* We add spent alloc since last measure to current caller own/total alloc *) - ajoute_ownalloc p dw; - ajoute_totalloc p dw; - e.owncount <- e.owncount + 1; - if not (p==e) then stack := e::!stack; - let totalloc0 = e.totalloc in - let intcount0 = e.intcount in - let t = get_time () in - try - last_alloc := get_alloc (); - let r = f a b c d g in - let dw = spent_alloc () in - let dt = get_time () - t in - e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; - ajoute_ownalloc e dw; - ajoute_totalloc e dw; - p.owntime <- p.owntime - dt; - ajoute_totalloc p (e.totalloc -. totalloc0); - p.intcount <- p.intcount + e.intcount - intcount0 + 1; - p.immcount <- p.immcount + 1; - if not (p==e) then - (match !stack with [] -> assert false | _::s -> stack := s); - last_alloc := get_alloc (); - r - with reraise -> - let dw = spent_alloc () in - let dt = get_time () - t in - e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; - ajoute_ownalloc e dw; - ajoute_totalloc e dw; - p.owntime <- p.owntime - dt; - ajoute_totalloc p (e.totalloc -. totalloc0); - p.intcount <- p.intcount + e.intcount - intcount0 + 1; - p.immcount <- p.immcount + 1; - if not (p==e) then - (match !stack with [] -> assert false | _::s -> stack := s); - last_alloc := get_alloc (); - raise reraise - -let profile6 e f a b c d g h = - let dw = spent_alloc () in - match !stack with [] -> assert false | p::_ -> - (* We add spent alloc since last measure to current caller own/total alloc *) - ajoute_ownalloc p dw; - ajoute_totalloc p dw; - e.owncount <- e.owncount + 1; - if not (p==e) then stack := e::!stack; - let totalloc0 = e.totalloc in - let intcount0 = e.intcount in - let t = get_time () in - try - last_alloc := get_alloc (); - let r = f a b c d g h in - let dw = spent_alloc () in - let dt = get_time () - t in - e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; - ajoute_ownalloc e dw; - ajoute_totalloc e dw; - p.owntime <- p.owntime - dt; - ajoute_totalloc p (e.totalloc -. totalloc0); - p.intcount <- p.intcount + e.intcount - intcount0 + 1; - p.immcount <- p.immcount + 1; - if not (p==e) then - (match !stack with [] -> assert false | _::s -> stack := s); - last_alloc := get_alloc (); - r - with reraise -> - let dw = spent_alloc () in - let dt = get_time () - t in - e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; - ajoute_ownalloc e dw; - ajoute_totalloc e dw; - p.owntime <- p.owntime - dt; - ajoute_totalloc p (e.totalloc -. totalloc0); - p.intcount <- p.intcount + e.intcount - intcount0 + 1; - p.immcount <- p.immcount + 1; - if not (p==e) then - (match !stack with [] -> assert false | _::s -> stack := s); - last_alloc := get_alloc (); - raise reraise - -let profile7 e f a b c d g h i = - let dw = spent_alloc () in - match !stack with [] -> assert false | p::_ -> - (* We add spent alloc since last measure to current caller own/total alloc *) - ajoute_ownalloc p dw; - ajoute_totalloc p dw; - e.owncount <- e.owncount + 1; - if not (p==e) then stack := e::!stack; - let totalloc0 = e.totalloc in - let intcount0 = e.intcount in - let t = get_time () in - try - last_alloc := get_alloc (); - let r = f a b c d g h i in - let dw = spent_alloc () in - let dt = get_time () - t in - e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; - ajoute_ownalloc e dw; - ajoute_totalloc e dw; - p.owntime <- p.owntime - dt; - ajoute_totalloc p (e.totalloc -. totalloc0); - p.intcount <- p.intcount + e.intcount - intcount0 + 1; - p.immcount <- p.immcount + 1; - if not (p==e) then - (match !stack with [] -> assert false | _::s -> stack := s); - last_alloc := get_alloc (); - r - with reraise -> - let dw = spent_alloc () in - let dt = get_time () - t in - e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; - ajoute_ownalloc e dw; - ajoute_totalloc e dw; - p.owntime <- p.owntime - dt; - ajoute_totalloc p (e.totalloc -. totalloc0); - p.intcount <- p.intcount + e.intcount - intcount0 + 1; - p.immcount <- p.immcount + 1; - if not (p==e) then - (match !stack with [] -> assert false | _::s -> stack := s); - last_alloc := get_alloc (); - raise reraise - -let profile8 e f a b c d g h i j = - let dw = spent_alloc () in - match !stack with [] -> assert false | p::_ -> - (* We add spent alloc since last measure to current caller own/total alloc *) - ajoute_ownalloc p dw; - ajoute_totalloc p dw; - e.owncount <- e.owncount + 1; - if not (p==e) then stack := e::!stack; - let totalloc0 = e.totalloc in - let intcount0 = e.intcount in - let t = get_time () in - try - last_alloc := get_alloc (); - let r = f a b c d g h i j in - let dw = spent_alloc () in - let dt = get_time () - t in - e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; - ajoute_ownalloc e dw; - ajoute_totalloc e dw; - p.owntime <- p.owntime - dt; - ajoute_totalloc p (e.totalloc -. totalloc0); - p.intcount <- p.intcount + e.intcount - intcount0 + 1; - p.immcount <- p.immcount + 1; - if not (p==e) then - (match !stack with [] -> assert false | _::s -> stack := s); - last_alloc := get_alloc (); - r - with reraise -> - let dw = spent_alloc () in - let dt = get_time () - t in - e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt; - ajoute_ownalloc e dw; - ajoute_totalloc e dw; - p.owntime <- p.owntime - dt; - ajoute_totalloc p (e.totalloc -. totalloc0); - p.intcount <- p.intcount + e.intcount - intcount0 + 1; - p.immcount <- p.immcount + 1; - if not (p==e) then - (match !stack with [] -> assert false | _::s -> stack := s); - last_alloc := get_alloc (); - raise reraise - -let print_logical_stats a = - let (c, s, d) = CObj.obj_stats a in - Printf.printf "Expanded size: %10d (str: %8d) Depth: %6d\n" (s+c) c d - -let print_stats a = - let (c1, s, d) = CObj.obj_stats a in - let c2 = CObj.size a in - Printf.printf "Size: %8d (exp: %10d) Depth: %6d\n" - c2 (s + c1) d -(* -let _ = Gc.set { (Gc.get()) with Gc.verbose = 13 } -*) diff --git a/lib/profile.mli b/lib/profile.mli deleted file mode 100644 index cae4397a1..000000000 --- a/lib/profile.mli +++ /dev/null @@ -1,119 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* unit - -val print_profile : unit -> unit -val reset_profile : unit -> unit -val init_profile : unit -> unit -val declare_profile : string -> profile_key - -val profile1 : profile_key -> ('a -> 'b) -> 'a -> 'b -val profile2 : profile_key -> ('a -> 'b -> 'c) -> 'a -> 'b -> 'c -val profile3 : - profile_key -> ('a -> 'b -> 'c -> 'd) -> 'a -> 'b -> 'c -> 'd -val profile4 : - profile_key -> ('a -> 'b -> 'c -> 'd -> 'e) -> 'a -> 'b -> 'c -> 'd -> 'e -val profile5 : - profile_key -> - ('a -> 'b -> 'c -> 'd -> 'e -> 'f) -> 'a -> 'b -> 'c -> 'd -> 'e -> 'f -val profile6 : - profile_key -> - ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g) - -> 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -val profile7 : - profile_key -> - ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h) - -> 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -val profile8 : - profile_key -> - ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i) - -> 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i - - -(** Some utilities to compute the logical and physical sizes and depth - of ML objects *) - -(** Print logical size (in words) and depth of its argument - This function does not disturb the heap *) -val print_logical_stats : 'a -> unit - -(** Print physical size, logical size (in words) and depth of its argument - This function allocates itself a lot (the same order of magnitude - as the physical size of its argument) *) -val print_stats : 'a -> unit diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index c0060c5a7..ee34161dd 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -361,8 +361,8 @@ end) = struct end (* let my_type_of env evars c = Typing.e_type_of env evars c *) -(* let mytypeofkey = Profile.declare_profile "my_type_of";; *) -(* let my_type_of = Profile.profile3 mytypeofkey my_type_of *) +(* let mytypeofkey = CProfile.declare_profile "my_type_of";; *) +(* let my_type_of = CProfile.profile3 mytypeofkey my_type_of *) let type_app_poly env env evd f args = @@ -2084,8 +2084,8 @@ let get_hyp gl (c,l) clause l2r = let general_rewrite_flags = { under_lambdas = false; on_morphisms = true } -(* let rewriteclaustac_key = Profile.declare_profile "cl_rewrite_clause_tac";; *) -(* let cl_rewrite_clause_tac = Profile.profile5 rewriteclaustac_key cl_rewrite_clause_tac *) +(* let rewriteclaustac_key = CProfile.declare_profile "cl_rewrite_clause_tac";; *) +(* let cl_rewrite_clause_tac = CProfile.profile5 rewriteclaustac_key cl_rewrite_clause_tac *) (** Setoid rewriting when called with "rewrite" *) let general_s_rewrite cl l2r occs (c,l) ~new_goals = diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index e5776d2ec..cb8844623 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1063,8 +1063,8 @@ let evar_conv_x ts = evar_conv_x (ts, true) (* Profiling *) let evar_conv_x = if Flags.profile then - let evar_conv_xkey = Profile.declare_profile "evar_conv_x" in - Profile.profile6 evar_conv_xkey evar_conv_x + let evar_conv_xkey = CProfile.declare_profile "evar_conv_x" in + CProfile.profile6 evar_conv_xkey evar_conv_x else evar_conv_x let evar_conv_hook_get, evar_conv_hook_set = Hook.make ~default:evar_conv_x () diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 2f8e5b964..30fc5f321 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1269,11 +1269,11 @@ let nf_all env sigma = (* Conversion *) (********************************************************************) (* -let fkey = Profile.declare_profile "fhnf";; -let fhnf info v = Profile.profile2 fkey fhnf info v;; +let fkey = CProfile.declare_profile "fhnf";; +let fhnf info v = CProfile.profile2 fkey fhnf info v;; -let fakey = Profile.declare_profile "fhnf_apply";; -let fhnf_apply info k h a = Profile.profile4 fakey fhnf_apply info k h a;; +let fakey = CProfile.declare_profile "fhnf_apply";; +let fhnf_apply info k h a = CProfile.profile4 fakey fhnf_apply info k h a;; *) let is_transparent e k = diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index f8f086fad..00b175c48 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -227,8 +227,8 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty = (* let f,_,_,_ = retype ~polyprop sigma in *) (* if lax then f env c else anomaly_on_error (f env) c *) -(* let get_type_of_key = Profile.declare_profile "get_type_of" *) -(* let get_type_of = Profile.profile5 get_type_of_key get_type_of *) +(* let get_type_of_key = CProfile.declare_profile "get_type_of" *) +(* let get_type_of = CProfile.profile5 get_type_of_key get_type_of *) (* let get_type_of ?(polyprop=true) ?(lax=false) env sigma c = *) (* get_type_of polyprop lax env sigma c *) diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 85383ba39..5a522e06a 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -927,8 +927,8 @@ let whd_simpl_orelse_delta_but_fix_old env sigma c = let whd_simpl_stack = if Flags.profile then - let key = Profile.declare_profile "whd_simpl_stack" in - Profile.profile3 key whd_simpl_stack + let key = CProfile.declare_profile "whd_simpl_stack" in + CProfile.profile3 key whd_simpl_stack else whd_simpl_stack (* Same as [whd_simpl] but also reduces constants that do not hide a diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 2e213a51d..b49da57a4 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -552,8 +552,8 @@ let solve_all_instances env evd filter unique split fail = Hook.get get_solve_all_instances env evd filter unique split fail (** Profiling resolution of typeclasses *) -(* let solve_classeskey = Profile.declare_profile "solve_typeclasses" *) -(* let solve_problem = Profile.profile5 solve_classeskey solve_problem *) +(* let solve_classeskey = CProfile.declare_profile "solve_typeclasses" *) +(* let solve_problem = CProfile.profile5 solve_classeskey solve_problem *) let resolve_typeclasses ?(fast_path = true) ?(filter=no_goals) ?(unique=get_typeclasses_unique_solutions ()) ?(split=true) ?(fail=true) env evd = diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 84ffab426..08329391d 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -2015,8 +2015,8 @@ let w_unify env evd cv_pb flags ty1 ty2 = let w_unify = if Flags.profile then - let wunifkey = Profile.declare_profile "w_unify" in - Profile.profile6 wunifkey w_unify + let wunifkey = CProfile.declare_profile "w_unify" in + CProfile.profile6 wunifkey w_unify else w_unify let w_unify env evd cv_pb ?(flags=default_unify_flags ()) ty1 ty2 = diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 3e3313eb5..cd2b10906 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -30,8 +30,8 @@ let refiner pr goal_sigma = (* Profiling refiner *) let refiner = if Flags.profile then - let refiner_key = Profile.declare_profile "refiner" in - Profile.profile2 refiner_key refiner + let refiner_key = CProfile.declare_profile "refiner" in + CProfile.profile2 refiner_key refiner else refiner (*********************) diff --git a/tactics/auto.ml b/tactics/auto.ml index fa8435d1f..e7e21b5f4 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -514,8 +514,8 @@ let delta_auto debug mod_delta n lems dbnames = let delta_auto = if Flags.profile then - let key = Profile.declare_profile "delta_auto" in - Profile.profile5 key delta_auto + let key = CProfile.declare_profile "delta_auto" in + CProfile.profile5 key delta_auto else delta_auto let auto ?(debug=Off) n = delta_auto debug false n diff --git a/tactics/eauto.ml b/tactics/eauto.ml index f5c6ab879..b5cfbe68b 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -405,8 +405,8 @@ let e_search_auto debug (in_depth,p) lems db_list gl = pr_info_nop d; user_err Pp.(str "eauto: search failed") -(* let e_search_auto_key = Profile.declare_profile "e_search_auto" *) -(* let e_search_auto = Profile.profile5 e_search_auto_key e_search_auto *) +(* let e_search_auto_key = CProfile.declare_profile "e_search_auto" *) +(* let e_search_auto = CProfile.profile5 e_search_auto_key e_search_auto *) let eauto_with_bases ?(debug=Off) np lems db_list = tclTRY (e_search_auto debug np lems db_list) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index e072bd95f..cb2a77558 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1976,11 +1976,11 @@ let cut_and_apply c = (* Exact tactics *) (********************************************************************) -(* let convert_leqkey = Profile.declare_profile "convert_leq";; *) -(* let convert_leq = Profile.profile3 convert_leqkey convert_leq *) +(* let convert_leqkey = CProfile.declare_profile "convert_leq";; *) +(* let convert_leq = CProfile.profile3 convert_leqkey convert_leq *) -(* let refine_no_checkkey = Profile.declare_profile "refine_no_check";; *) -(* let refine_no_check = Profile.profile2 refine_no_checkkey refine_no_check *) +(* let refine_no_checkkey = CProfile.declare_profile "refine_no_check";; *) +(* let refine_no_check = CProfile.profile2 refine_no_checkkey refine_no_check *) let exact_no_check c = Refine.refine ~typecheck:false (fun h -> (h,c)) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 553da2dc0..b62396317 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -756,7 +756,7 @@ let init_toplevel arglist = (* Coq's init process, phase 1: - OCaml parameters, and basic structures and IO *) - Profile.init_profile (); + CProfile.init_profile (); init_gc (); Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *) let init_feeder = Feedback.add_feeder coqtop_init_feed in @@ -846,7 +846,7 @@ let start () = let sigma, env = Pfedit.get_current_context () in Feedback.msg_notice (Flags.(with_option raw_print (Prettyp.print_full_pure_context env) sigma) ++ fnl ()) end; - Profile.print_profile (); + CProfile.print_profile (); exit 0 (* [Coqtop.start] will be called by the code produced by coqmktop *) -- cgit v1.2.3 From 598e3ae4a8eb8d9bce316e13d71ee48d9ba1a01f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 28 Oct 2017 21:02:48 +0200 Subject: [build] Remove coqmktop in favor of ocamlfind. We remove coqmktop in favor of a couple of simple makefile rules using ocamlfind. In order to do that, we introduce a new top-level file that calls the coqtop main entry. This is very convenient in order to use other builds systems such as `ocamlbuild` or `jbuilder`. An additional consideration is that we must perform a side-effect on init depending on whether we have an OCaml toplevel available [byte] or not. We do that by using two different object files, one for the bytecode version other for the native one, but we may want to review our choice. We also perform some smaller cleanups taking profit from ocamlfind. --- Makefile | 2 +- Makefile.build | 73 +++++----- Makefile.checker | 4 +- Makefile.common | 2 - Makefile.install | 3 +- config/coq_config.mli | 4 - configure.ml | 15 +-- dev/build/windows/ReadMe.txt | 2 - dev/doc/setup.txt | 2 +- doc/refman/RefMan-uti.tex | 56 +++----- lib/envars.ml | 12 +- lib/flags.ml | 8 -- lib/flags.mli | 6 - man/coqmktop.1 | 71 ---------- tools/CoqMakefile.in | 1 - tools/coqmktop.ml | 314 ------------------------------------------- toplevel/coqtop.ml | 2 - toplevel/coqtop_bin.ml | 6 + toplevel/coqtop_byte_bin.ml | 21 +++ toplevel/coqtop_opt_bin.ml | 3 + 20 files changed, 100 insertions(+), 507 deletions(-) delete mode 100644 man/coqmktop.1 delete mode 100644 tools/coqmktop.ml create mode 100644 toplevel/coqtop_bin.ml create mode 100644 toplevel/coqtop_byte_bin.ml create mode 100644 toplevel/coqtop_opt_bin.ml diff --git a/Makefile b/Makefile index 620fec546..0078dba20 100644 --- a/Makefile +++ b/Makefile @@ -246,7 +246,7 @@ archclean: clean-ide optclean voclean rm -f $(ALLSTDLIB).* optclean: - rm -f $(COQTOPEXE) $(COQMKTOP) $(CHICKEN) + rm -f $(COQTOPEXE) $(CHICKEN) rm -f $(TOOLS) $(PRIVATEBINARIES) $(CSDPCERT) find . -name '*.cmx' -o -name '*.cmx[as]' -o -name '*.[soa]' -o -name '*.so' | xargs rm -f diff --git a/Makefile.build b/Makefile.build index 39b793d2b..3e4c5a0b4 100644 --- a/Makefile.build +++ b/Makefile.build @@ -228,8 +228,8 @@ endef define bestocaml $(if $(OPT),\ -$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) $(LINKMETADATA) -o $@ $(1) $(addsuffix .cmxa,$(2)) $^ && $(STRIP) $@ && $(CODESIGN) $@,\ -$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(CUSTOM) -o $@ $(1) $(addsuffix .cma,$(2)) $^) +$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) $(LINKMETADATA) -o $@ -linkpkg $(1) $^ && $(STRIP) $@ && $(CODESIGN) $@,\ +$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(CUSTOM) -o $@ -linkpkg $(1) $^) endef # Camlp5 settings @@ -239,9 +239,8 @@ CAMLP4USE=pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION) PR_O := $(if $(READABLE_ML4),pr_o.cmo,pr_dump.cmo) -SYSMOD:=str unix dynlink threads -SYSCMA:=$(addsuffix .cma,$(SYSMOD)) -SYSCMXA:=$(addsuffix .cmxa,$(SYSMOD)) +# Main packages linked by Coq. +SYSMOD:=-package num,str,unix,dynlink,threads # We do not repeat the dependencies already in SYSMOD here P4CMA:=gramlib.cma @@ -370,19 +369,30 @@ grammar/%.cmi: grammar/%.mli ########################################################################### -# Main targets (coqmktop, coqtop.opt, coqtop.byte) +# Main targets (coqtop.opt, coqtop.byte) ########################################################################### .PHONY: coqbinaries coqbyte -coqbinaries: $(COQMKTOP) $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE) +coqbinaries: $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE) coqbyte: $(COQTOPBYTE) $(CHICKENBYTE) +COQTOP_OPT_MLTOP=toplevel/coqtop_opt_bin.cmx +COQTOP_BYTE_MLTOP=toplevel/coqtop_byte_bin.cmo + +$(COQTOP_BYTE_MLTOP): toplevel/coqtop_byte_bin.ml + $(SHOW)'OCAMLC $<' + $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -package compiler-libs.toplevel -c $< + ifeq ($(BEST),opt) -$(COQTOPEXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs) +$(COQTOPEXE): tools/tolink.cmx $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs) $(COQTOP_OPT_MLTOP) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) $(LINKMETADATA) -o $@ + $(HIDE)$(OCAMLOPT) -linkall -linkpkg -I vernac -I toplevel -I tools \ + -I kernel/byterun/ -cclib -lcoqrun \ + $(SYSMOD) -package camlp5.gramlib \ + tools/tolink.cmx $(LINKCMX) $(OPTFLAGS) $(LINKMETADATA) \ + $(COQTOP_OPT_MLTOP) toplevel/coqtop_bin.ml -o $@ $(STRIP) $@ $(CODESIGN) $@ else @@ -390,21 +400,18 @@ $(COQTOPEXE): $(COQTOPBYTE) cp $< $@ endif -$(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA) +# Are "-cclib lcoqrun -dllib -lcoqrun" necessary? +$(COQTOPBYTE): tools/tolink.cmo $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA) $(COQTOP_BYTE_MLTOP) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(COQMKTOP) -boot -top $(BYTEFLAGS) -o $@ - -# coqmktop - -COQMKTOPCMO:=lib/clib.cma lib/cErrors.cmo tools/tolink.cmo tools/coqmktop.cmo - -$(COQMKTOP): $(call bestobj, $(COQMKTOPCMO)) - $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD)) + $(HIDE)$(OCAMLC) -linkall -linkpkg -I vernac -I toplevel -I tools \ + -I kernel/byterun -dllpath $(abspath kernel/byterun) -cclib -lcoqrun -dllib -lcoqrun \ + $(SYSMOD) -package camlp5.gramlib,compiler-libs.toplevel \ + tools/tolink.cmo $(LINKCMO) $(BYTEFLAGS) \ + $(COQTOP_BYTE_MLTOP) toplevel/coqtop_bin.ml -o $@ tools/tolink.ml: Makefile.build Makefile.common $(SHOW)"ECHO... >" $@ - $(HIDE)echo "let copts = \"-cclib -lcoqrun\"" > $@ + $(HIDE)echo "let static_modules = \""$(STATICPLUGINS)"\"" > $@ $(HIDE)echo "let core_libs = \""$(LINKCMO)"\"" >> $@ $(HIDE)echo "let core_objs = \""$(OBJSMOD)"\"" >> $@ @@ -414,7 +421,7 @@ COQCCMO:=lib/clib.cma lib/cErrors.cmo toplevel/usage.cmo tools/coqc.cmo $(COQC): $(call bestobj, $(COQCCMO)) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD)) + $(HIDE)$(call bestocaml, $(SYSMOD)) ########################################################################### # other tools @@ -451,11 +458,11 @@ tools/coqdep_boot.cmx : tools/coqdep_common.cmx $(COQDEPBOOT): $(call bestobj, $(COQDEPBOOTSRC)) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml, -I tools, unix) + $(HIDE)$(call bestocaml, -I tools -package unix) $(OCAMLLIBDEP): $(call bestobj, tools/ocamllibdep.cmo) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml, -I tools, unix) + $(HIDE)$(call bestocaml, -I tools -package unix) # The full coqdep (unused by this build, but distributed by make install) @@ -466,36 +473,36 @@ COQDEPCMO:=lib/clib.cma lib/cErrors.cmo lib/cWarnings.cmo \ $(COQDEP): $(call bestobj, $(COQDEPCMO)) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD)) + $(HIDE)$(call bestocaml, $(SYSMOD)) $(GALLINA): $(call bestobj, tools/gallina_lexer.cmo tools/gallina.cmo) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml,,) + $(HIDE)$(call bestocaml,) COQMAKEFILECMO:=lib/clib.cma tools/coq_makefile.cmo $(COQMAKEFILE): $(call bestobj,$(COQMAKEFILECMO)) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml,,str unix threads) + $(HIDE)$(call bestocaml, -package str,unix,threads) $(COQTEX): $(call bestobj, tools/coq_tex.cmo) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml,,str) + $(HIDE)$(call bestocaml, -package str) $(COQWC): $(call bestobj, tools/coqwc.cmo) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml,,) + $(HIDE)$(call bestocaml, -package str) COQDOCCMO:=lib/clib.cma $(addprefix tools/coqdoc/, \ cdglobals.cmo alpha.cmo index.cmo tokens.cmo output.cmo cpretty.cmo main.cmo ) $(COQDOC): $(call bestobj, $(COQDOCCMO)) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml,,str unix) + $(HIDE)$(call bestocaml, -package str,unix) $(COQWORKMGR): $(call bestobj, lib/clib.cma stm/coqworkmgrApi.cmo tools/coqworkmgr.cmo) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml,, $(SYSMOD)) + $(HIDE)$(call bestocaml, $(SYSMOD)) # fake_ide : for debugging or test-suite purpose, a fake ide simulating # a connection to coqtop -ideslave @@ -506,13 +513,13 @@ FAKEIDECMO:= lib/clib.cma lib/cErrors.cmo lib/spawn.cmo ide/document.cmo \ $(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOPLOOPCMA:.cma=$(BESTDYN)) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml,-I ide,str unix threads) + $(HIDE)$(call bestocaml, -I ide -package str,unix,threads) # votour: a small vo explorer (based on the checker) bin/votour: $(call bestobj, lib/cObj.cmo checker/analyze.cmo checker/values.cmo checker/votour.cmo) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml, -I checker,) + $(HIDE)$(call bestocaml, -I checker) ########################################################################### # Csdp to micromega special targets @@ -524,7 +531,7 @@ CSDPCERTCMO:=lib/clib.cma $(addprefix plugins/micromega/, \ $(CSDPCERT): $(call bestobj, $(CSDPCERTCMO)) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml,,nums unix) + $(HIDE)$(call bestocaml, -package num,unix) ########################################################################### # tests diff --git a/Makefile.checker b/Makefile.checker index 435d8e8f6..b14f705be 100644 --- a/Makefile.checker +++ b/Makefile.checker @@ -29,7 +29,7 @@ CHKLIBS:= -I config -I lib -I checker ifeq ($(BEST),opt) $(CHICKEN): checker/check.cmxa checker/main.ml $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(SYSCMXA) $(CHKLIBS) $(OPTFLAGS) $(LINKMETADATA) -o $@ $^ + $(HIDE)$(OCAMLOPT) -linkpkg $(SYSMOD) $(CHKLIBS) $(OPTFLAGS) $(LINKMETADATA) -o $@ $^ $(STRIP) $@ $(CODESIGN) $@ else @@ -39,7 +39,7 @@ endif $(CHICKENBYTE): checker/check.cma checker/main.ml $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(SYSCMA) $(CHKLIBS) $(BYTEFLAGS) $(CUSTOM) -o $@ $^ + $(HIDE)$(OCAMLC) -linkpkg $(SYSMOD) $(CHKLIBS) $(BYTEFLAGS) $(CUSTOM) -o $@ $^ checker/check.cma: checker/check.mllib | md5chk $(SHOW)'OCAMLC -a -o $@' diff --git a/Makefile.common b/Makefile.common index 4d63b08e2..f436d3e8f 100644 --- a/Makefile.common +++ b/Makefile.common @@ -12,8 +12,6 @@ # Executables ########################################################################### -COQMKTOP:=bin/coqmktop$(EXE) - COQTOPBYTE:=bin/coqtop.byte$(EXE) COQTOPEXE:=bin/coqtop$(EXE) diff --git a/Makefile.install b/Makefile.install index b590aad54..750d57ba0 100644 --- a/Makefile.install +++ b/Makefile.install @@ -103,7 +103,6 @@ INSTALLCMI = $(sort \ install-devfiles: $(MKDIR) $(FULLBINDIR) - $(INSTALLBIN) $(COQMKTOP) $(FULLBINDIR) $(MKDIR) $(FULLCOQLIB) $(INSTALLSH) $(FULLCOQLIB) $(GRAMMARCMA) $(INSTALLSH) $(FULLCOQLIB) $(INSTALLCMI) @@ -136,7 +135,7 @@ install-coq-info: install-coq-manpages install-emacs install-latex MANPAGES:=man/coq-tex.1 man/coqdep.1 man/gallina.1 \ man/coqc.1 man/coqtop.1 man/coqtop.byte.1 man/coqtop.opt.1 \ man/coqwc.1 man/coqdoc.1 man/coqide.1 \ - man/coq_makefile.1 man/coqmktop.1 man/coqchk.1 + man/coq_makefile.1 man/coqchk.1 install-coq-manpages: $(MKDIR) $(FULLMANDIR)/man1 diff --git a/config/coq_config.mli b/config/coq_config.mli index 6a834a304..40661f428 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -41,12 +41,8 @@ val caml_flags : string (* arguments passed to ocamlc (ie. CAMLFLAGS) *) val best : string (* byte/opt *) val arch : string (* architecture *) val arch_is_win32 : bool -val osdeplibs : string (* OS dependent link options for ocamlc *) val vmbyteflags : string list (* -custom/-dllib -lcoqrun *) - -(* val defined : string list (* options for lib/ocamlpp *) *) - val version : string (* version number of Coq *) val caml_version : string (* OCaml version used to compile Coq *) val caml_version_nums : int list (* OCaml version used to compile Coq by components *) diff --git a/configure.ml b/configure.ml index c7d25bfc8..3ce0b03d7 100644 --- a/configure.ml +++ b/configure.ml @@ -16,7 +16,7 @@ let coq_macos_version = "8.7.90" (** "[...] should be a string comprised of three non-negative, period-separated integers [...]" *) let vo_magic = 8791 let state_magic = 58791 -let distributed_exec = ["coqtop";"coqc";"coqchk";"coqdoc";"coqmktop";"coqworkmgr"; +let distributed_exec = ["coqtop";"coqc";"coqchk";"coqdoc";"coqworkmgr"; "coqdoc";"coq_makefile";"coq-tex";"gallina";"coqwc";"csdpcert";"coqdep"] let verbose = ref false (* for debugging this script *) @@ -666,17 +666,15 @@ let natdynlinkflag = (** * OS dependent libraries *) -let osdeplibs = "-cclib -lunix" - -let operating_system, osdeplibs = +let operating_system = if starts_with arch "sun4" then let os, _ = run "uname" ["-r"] in if starts_with os "5" then - "Sun Solaris "^os, osdeplibs^" -cclib -lnsl -cclib -lsocket" + "Sun Solaris "^os else - "Sun OS "^os, osdeplibs + "Sun OS "^os else - (try Sys.getenv "OS" with Not_found -> ""), osdeplibs + (try Sys.getenv "OS" with Not_found -> "") (** Num library *) @@ -1001,7 +999,6 @@ let print_summary () = pr " Operating system : %s\n" operating_system; pr " Coq VM bytecode link flags : %s\n" (String.concat " " vmbyteflags); pr " Other bytecode link flags : %s\n" custom_flag; - pr " OS dependent libraries : %s\n" osdeplibs; pr " OCaml version : %s\n" caml_version; pr " OCaml binaries in : %s\n" (esc camlbin); pr " OCaml library in : %s\n" (esc camllib); @@ -1094,7 +1091,6 @@ let write_configml f = pr_s "cflags" cflags; pr_s "caml_flags" caml_flags; pr_s "best" best_compiler; - pr_s "osdeplibs" osdeplibs; pr_s "version" coq_version; pr_s "caml_version" caml_version; pr_li "caml_version_nums" caml_version_nums; @@ -1225,7 +1221,6 @@ let write_makefile f = pr "# Supplementary libs for some systems, currently:\n"; pr "# . Sun Solaris: -cclib -lunix -cclib -lnsl -cclib -lsocket\n"; pr "# . others : -cclib -lunix\n"; - pr "OSDEPLIBS=%s\n\n" osdeplibs; pr "# executable files extension, currently:\n"; pr "# Unix systems:\n"; pr "# Win32 systems : .exe\n"; diff --git a/dev/build/windows/ReadMe.txt b/dev/build/windows/ReadMe.txt index a6d8e4462..7e80e33c6 100644 --- a/dev/build/windows/ReadMe.txt +++ b/dev/build/windows/ReadMe.txt @@ -418,7 +418,6 @@ Binary file ./bin/coqchk.exe matches Binary file ./bin/coqdep.exe matches Binary file ./bin/coqdoc.exe matches Binary file ./bin/coqide.exe matches -Binary file ./bin/coqmktop.exe matches Binary file ./bin/coqtop.byte.exe matches Binary file ./bin/coqtop.exe matches Binary file ./bin/coqworkmgr.exe matches @@ -438,7 +437,6 @@ Binary file ./bin/ocamldoc.exe matches Binary file ./bin/ocamldoc.opt.exe matches Binary file ./bin/ocamlfind.exe matches Binary file ./bin/ocamlmklib.exe matches -Binary file ./bin/ocamlmktop.exe matches Binary file ./bin/ocamlobjinfo.exe matches Binary file ./bin/ocamlopt.exe matches Binary file ./bin/ocamlopt.opt.exe matches diff --git a/dev/doc/setup.txt b/dev/doc/setup.txt index 0c6d3ee80..26f3d0ddc 100644 --- a/dev/doc/setup.txt +++ b/dev/doc/setup.txt @@ -279,7 +279,7 @@ You can load them by switching to the window holding the "ocamldebug" shell and Some of the functions were you might want to set a breakpoint and see what happens next --------------------------------------------------------------------------------------- -- Coqtop.start : This function is called by the code produced by "coqmktop". +- Coqtop.start : This function is the main entry point of coqtop. - Coqtop.parse_args : This function is responsible for parsing command-line arguments. - Coqloop.loop : This function implements the read-eval-print loop. - Vernacentries.interp : This function is called to execute the Vernacular command user have typed.\ diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex index c411db100..002e9625c 100644 --- a/doc/refman/RefMan-uti.tex +++ b/doc/refman/RefMan-uti.tex @@ -4,53 +4,27 @@ The distribution provides utilities to simplify some tedious works beside proof development, tactics writing or documentation. -\section[Building a toplevel extended with user tactics]{Building a toplevel extended with user tactics\label{Coqmktop}\ttindex{coqmktop}} +\section[Using Coq as a library]{Using Coq as a library} -The native-code version of \Coq\ cannot dynamically load user tactics -using {\ocaml} code. It is possible to build a toplevel of \Coq, -with {\ocaml} code statically linked, with the tool {\tt - coqmktop}. - -For example, one can build a native-code \Coq\ toplevel extended with a tactic -which source is in {\tt tactic.ml} with the command -\begin{verbatim} - % coqmktop -opt -o mytop.out tactic.cmx -\end{verbatim} -where {\tt tactic.ml} has been compiled with the native-code -compiler {\tt ocamlopt}. This command generates an executable -called {\tt mytop.out}. To use this executable to compile your \Coq\ -files, use {\tt coqc -image mytop.out}. - -A basic example is the native-code version of \Coq\ ({\tt coqtop.opt}), -which can be generated by {\tt coqmktop -opt -o coqopt.opt}. - - -\paragraph[Application: how to use the {\ocaml} debugger with Coq.]{Application: how to use the {\ocaml} debugger with Coq.\index{Debugger}} - -One useful application of \texttt{coqmktop} is to build a \Coq\ toplevel in -order to debug your tactics with the {\ocaml} debugger. -You need to have configured and compiled \Coq\ for debugging -(see the file \texttt{INSTALL} included in the distribution). -Then, you must compile the Caml modules of your tactic with the -option \texttt{-g} (with the bytecode compiler) and build a stand-alone -bytecode toplevel with the following command: +In previous versions, \texttt{coqmktop} was used to build custom +toplevels --- for example for better debugging or custom static +linking. Nowadays, the preferred method is to use \texttt{ocamlfind}. +The most basic custom toplevel is built using: \begin{quotation} -\texttt{\% coqmktop -g -o coq-debug}~\emph{} +\texttt{\% make tools/tolink.cmx} +\texttt{\% ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg + -package coq.toplevel -I tools tolink.cmx toplevel/coqtop\_bin.ml -o my\_toplevel.native} \end{quotation} +For example, to statically link LTAC, you can add it to \texttt{tools/tolink.ml} and use: +\begin{quotation} +\texttt{\% make tools/tolink.cmx} +\texttt{\% ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg + -package coq.toplevel -package coq.ltac -I tools tolink.cmx toplevel/coqtop\_bin.ml -o my\_toplevel.native} +\end{quotation} -To launch the \ocaml\ debugger with the image you need to execute it in -an environment which correctly sets the \texttt{COQLIB} variable. -Moreover, you have to indicate the directories in which -\texttt{ocamldebug} should search for Caml modules. - -A possible solution is to use a wrapper around \texttt{ocamldebug} -which detects the executables containing the word \texttt{coq}. In -this case, the debugger is called with the required additional -arguments. In other cases, the debugger is simply called without additional -arguments. Such a wrapper can be found in the \texttt{dev/} -subdirectory of the sources. +We will remove the need for the \texttt{tolink} file in the future. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% diff --git a/lib/envars.ml b/lib/envars.ml index 206d75033..8ebf84057 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -153,19 +153,17 @@ let coqpath = let exe s = s ^ Coq_config.exec_extension -let ocamlfind () = - if !Flags.ocamlfind_spec then !Flags.ocamlfind else Coq_config.ocamlfind +let ocamlfind () = Coq_config.ocamlfind (** {2 Camlp4 paths} *) let guess_camlp4bin () = which (user_path ()) (exe Coq_config.camlp4) let camlp4bin () = - if !Flags.camlp4bin_spec then !Flags.camlp4bin else - if !Flags.boot then Coq_config.camlp4bin else - try guess_camlp4bin () - with Not_found -> - Coq_config.camlp4bin + if !Flags.boot then Coq_config.camlp4bin else + try guess_camlp4bin () + with Not_found -> + Coq_config.camlp4bin let camlp4 () = camlp4bin () / exe Coq_config.camlp4 diff --git a/lib/flags.ml b/lib/flags.ml index ddc8f8482..97795faa6 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -179,14 +179,6 @@ let is_standard_doc_url url = let coqlib_spec = ref false let coqlib = ref "(not initialized yet)" -(* Options for changing ocamlfind (used by coqmktop) *) -let ocamlfind_spec = ref false -let ocamlfind = ref Coq_config.camlbin - -(* Options for changing camlp4bin (used by coqmktop) *) -let camlp4bin_spec = ref false -let camlp4bin = ref Coq_config.camlp4bin - (* Level of inlining during a functor application *) let default_inline_level = 100 diff --git a/lib/flags.mli b/lib/flags.mli index c4afb8318..e4710a126 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -143,12 +143,6 @@ val is_standard_doc_url : string -> bool val coqlib_spec : bool ref val coqlib : string ref -(** Options for specifying where OCaml binaries reside *) -val ocamlfind_spec : bool ref -val ocamlfind : string ref -val camlp4bin_spec : bool ref -val camlp4bin : string ref - (** Level of inlining during a functor application *) val set_inline_level : int -> unit val get_inline_level : unit -> int diff --git a/man/coqmktop.1 b/man/coqmktop.1 deleted file mode 100644 index 810df782c..000000000 --- a/man/coqmktop.1 +++ /dev/null @@ -1,71 +0,0 @@ -.TH COQ 1 "April 25, 2001" - -.SH NAME -coqmktop \- The Coq Proof Assistant user-tactics linker - - -.SH SYNOPSIS -.B coqmktop -[ -.I options -] -.I files - - -.SH DESCRIPTION - -.B coqmktop -builds a new Coq toplevel extended with user-tactics. -.IR files \& -are the Objective Caml object or library files -(i.e. with suffix .cmo, .cmx, .cma or .cmxa) to link with the Coq system. -The linker produces an executable Coq toplevel which can be called -directly or through coqc(1), using the \-image option. - -.SH OPTIONS - -.TP -.BI \-h -Help. List the available options. - -.TP -.BI \-srcdir \ dir -Specify where the Coq source files are - -.TP -.BI \-o \ exec\-file -Specify the name of the resulting toplevel - -.TP -.B \-opt -Compile in native code - -.TP -.B \-full -Link high level tactics - -.TP -.B \-top -Build Coq on a ocaml toplevel (incompatible with -.BR \-opt ) - -.TP -.BI \-R \ dir -Specify recursively directories for Ocaml - -.TP -.B \-v8 -Link with V8 grammar - - -.SH SEE ALSO - -.BR coqtop (1), -.BR ocamlmktop (1). -.BR ocamlc (1). -.BR ocamlopt (1). -.br -.I -The Coq Reference Manual. -.I -The Coq web site: http://coq.inria.fr diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 7fd942908..61c53bc1d 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -87,7 +87,6 @@ COQCHK ?= "$(COQBIN)coqchk" COQDEP ?= "$(COQBIN)coqdep" GALLINA ?= "$(COQBIN)gallina" COQDOC ?= "$(COQBIN)coqdoc" -COQMKTOP ?= "$(COQBIN)coqmktop" COQMKFILE ?= "$(COQBIN)coq_makefile" # Timing scripts diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml deleted file mode 100644 index 950ed53cc..000000000 --- a/tools/coqmktop.ml +++ /dev/null @@ -1,314 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Str.split spaces str - -[@@@ocaml.warning "-3"] (* String.uncapitalize_ascii since 4.03.0 GPR#124 *) -let capitalize = String.capitalize -[@@@ocaml.warning "+3"] - -let (/) = Filename.concat - -(** Which user files do we support (and propagate to ocamlopt) ? -*) -let supported_suffix f = match CUnix.get_extension f with - | ".ml" | ".cmx" | ".cmo" | ".cmxa" | ".cma" | ".c" -> true - | _ -> false - -let supported_flambda_option f = List.mem f Coq_config.flambda_flags - -(** From bytecode extension to native -*) -let native_suffix f = match CUnix.get_extension f with - | ".cmo" -> (Filename.chop_suffix f ".cmo") ^ ".cmx" - | ".cma" -> (Filename.chop_suffix f ".cma") ^ ".cmxa" - | ".a" -> f - | _ -> failwith ("File "^f^" has not extension .cmo, .cma or .a") - -(** Transforms a file name in the corresponding Caml module name. -*) -let module_of_file name = - capitalize (try Filename.chop_extension name with Invalid_argument _ -> name) - -(** Run a command [prog] with arguments [args]. - We do not use [Sys.command] anymore, see comment in [CUnix.sys_command]. -*) -let run_command prog args = - match CUnix.sys_command prog args with - | Unix.WEXITED 127 -> failwith ("no such command "^prog) - | Unix.WEXITED n -> n - | Unix.WSIGNALED n -> failwith (prog^" killed by signal "^string_of_int n) - | Unix.WSTOPPED n -> failwith (prog^" stopped by signal "^string_of_int n) - - - -(** {6 Coqmktop options} *) - -let opt = ref false -let top = ref false -let echo = ref false -let no_start = ref false - -let is_ocaml4 = Coq_config.caml_version.[0] <> '3' - -(** {6 Includes options} *) - -(** Since the Coq core .cma are given with their relative paths - (e.g. "lib/clib.cma"), we only need to include directories mentionned in - the temp main ml file below (for accessing the corresponding .cmi). *) - -let std_includes basedir = - let rebase d = match basedir with None -> d | Some base -> base / d in - ["-I"; rebase "."; - "-I"; rebase "lib"; - "-I"; rebase "vernac"; (* For Mltop *) - "-I"; rebase "toplevel"; - "-I"; rebase "kernel/byterun"; - "-I"; Envars.camlp4lib () ] @ - (if is_ocaml4 then ["-I"; "+compiler-libs"] else []) - -(** For the -R option, visit all directories under [dir] and add - corresponding -I to the [opts] option list (in reversed order) *) -let incl_all_subdirs dir opts = - let l = ref opts in - let add f = l := f :: "-I" :: !l in - let rec traverse dir = - if Sys.file_exists dir && Sys.is_directory dir then - let () = add dir in - let subdirs = try Sys.readdir dir with any -> [||] in - Array.iter (fun f -> traverse (dir/f)) subdirs - in - traverse dir; !l - - -(** {6 Objects to link} *) - -(** NB: dynlink is now always linked, it is used for loading plugins - and compiled vm code (see native-compiler). We now reject platforms - with ocamlopt but no dynlink.cmxa during ./configure, and give - instructions there about how to build a dummy dynlink.cmxa, - cf. dev/dynlink.ml. *) - -(** OCaml + CamlpX libraries *) - -let ocaml_libs = ["str.cma";"unix.cma";"nums.cma";"dynlink.cma";"threads.cma"] -let camlp4_libs = ["gramlib.cma"] -let libobjs = ocaml_libs @ camlp4_libs - -(** Toplevel objects *) - -let ocaml_topobjs = - if is_ocaml4 then - ["ocamlcommon.cma";"ocamlbytecomp.cma";"ocamltoplevel.cma"] - else - ["toplevellib.cma"] - -let camlp4_topobjs = ["camlp5_top.cma"; "pa_o.cmo"; "pa_extend.cmo"] - -let topobjs = ocaml_topobjs @ camlp4_topobjs - -(** Coq Core objects *) - -let copts = (split_list Coq_config.osdeplibs) @ (split_list Tolink.copts) -let core_objs = split_list Tolink.core_objs -let core_libs = split_list Tolink.core_libs - -(** Build the list of files to link and the list of modules names -*) -let files_to_link userfiles = - let top = if !top then topobjs else [] in - let modules = List.map module_of_file (top @ core_objs @ userfiles) in - let objs = libobjs @ top @ core_libs in - let objs' = (if !opt then List.map native_suffix objs else objs) @ userfiles - in (modules, objs') - - -(** {6 Parsing of the command-line} *) - -let usage () = - prerr_endline "Usage: coqmktop files\ -\nFlags are:\ -\n -coqlib dir Specify where the Coq object files are\ -\n -ocamlfind dir Specify where the ocamlfind binary is\ -\n -camlp4bin dir Specify where the Camlp4/5 binaries are\ -\n -o exec-file Specify the name of the resulting toplevel\ -\n -boot Run in boot mode\ -\n -echo Print calls to external commands\ -\n -opt Compile in native code\ -\n -top Build Coq on a OCaml toplevel (incompatible with -opt)\ -\n -R dir Add recursively dir to OCaml search path\ -\n"; - exit 1 - -let parse_args () = - let rec parse (op,fl) = function - | [] -> List.rev op, List.rev fl - - (* Directories *) - | "-coqlib" :: d :: rem -> - Flags.coqlib_spec := true; Flags.coqlib := d ; parse (op,fl) rem - | "-ocamlfind" :: d :: rem -> - Flags.ocamlfind_spec := true; Flags.ocamlfind := d ; parse (op,fl) rem - | "-camlp4bin" :: d :: rem -> - Flags.camlp4bin_spec := true; Flags.camlp4bin := d ; parse (op,fl) rem - | "-R" :: d :: rem -> parse (incl_all_subdirs d op,fl) rem - | ("-coqlib"|"-camlbin"|"-camlp4bin"|"-R") :: [] -> usage () - - (* Boolean options of coqmktop *) - | "-boot" :: rem -> Flags.boot := true; parse (op,fl) rem - | "-opt" :: rem -> opt := true ; parse (op,fl) rem - | "-top" :: rem -> top := true ; parse (op,fl) rem - | "-no-start" :: rem -> no_start:=true; parse (op, fl) rem - | "-echo" :: rem -> echo := true ; parse (op,fl) rem - - (* Extra options with arity 0 or 1, directly passed to ocamlc/ocamlopt *) - | ("-noassert"|"-compact"|"-g"|"-p"|"-thread"|"-dtypes" as o) :: rem -> - parse (o::op,fl) rem - | ("-cclib"|"-ccopt"|"-I"|"-o"|"-w" as o) :: rem' -> - begin - match rem' with - | a :: rem -> parse (a::o::op,fl) rem - | [] -> usage () - end - - | ("-h"|"-help"|"--help") :: _ -> usage () - | f :: rem when supported_flambda_option f -> parse (op,fl) rem - | f :: rem when supported_suffix f -> parse (op,f::fl) rem - | f :: _ -> prerr_endline ("Don't know what to do with " ^ f); exit 1 - in - parse ([],[]) (List.tl (Array.to_list Sys.argv)) - - -(** {6 Temporary main file} *) - -(** remove the temporary main file -*) -let clean file = - let rm f = if Sys.file_exists f then Sys.remove f in - let basename = Filename.chop_suffix file ".ml" in - if not !echo then begin - rm file; - rm (basename ^ ".o"); - rm (basename ^ ".cmi"); - rm (basename ^ ".cmo"); - rm (basename ^ ".cmx") - end - -(** Initializes the kind of loading in the main program -*) -let declare_loading_string () = - if not !top then - "Mltop.remove ();;" - else - "begin try\ -\n (* Enable rectypes in the toplevel if it has the directive #rectypes *)\ -\n begin match Hashtbl.find Toploop.directive_table \"rectypes\" with\ -\n | Toploop.Directive_none f -> f ()\ -\n | _ -> ()\ -\n end\ -\n with\ -\n | Not_found -> ()\ -\n end;;\ -\n\ -\n let ppf = Format.std_formatter;;\ -\n Mltop.set_top\ -\n {Mltop.load_obj=\ -\n (fun f -> if not (Topdirs.load_file ppf f)\ -\n then CErrors.user_err Pp.(str (\"Could not load plugin \"^f)));\ -\n Mltop.use_file=Topdirs.dir_use ppf;\ -\n Mltop.add_dir=Topdirs.dir_directory;\ -\n Mltop.ml_loop=(fun () -> Toploop.loop ppf) };;\ -\n" - -(** create a temporary main file to link -*) -let create_tmp_main_file modules = - let main_name,oc = Filename.open_temp_file "coqmain" ".ml" in - try - (* Add the pre-linked modules *) - output_string oc "List.iter Mltop.add_known_module [\""; - output_string oc (String.concat "\";\"" modules); - output_string oc "\"];;\n"; - (* Initializes the kind of loading *) - output_string oc (declare_loading_string()); - (* Start the toplevel loop *) - if not !no_start then output_string oc "Coqtop.start();;\n"; - close_out oc; - main_name - with reraise -> - clean main_name; raise reraise - -(* TODO: remove once OCaml 4.04 is adopted *) -let split_on_char sep s = - let r = ref [] in - let j = ref (String.length s) in - for i = String.length s - 1 downto 0 do - if s.[i] = sep then begin - r := String.sub s (i + 1) (!j - i - 1) :: !r; - j := i - end - done; - String.sub s 0 !j :: !r - -(** {6 Main } *) - -let main () = - let (options, userfiles) = parse_args () in - (* Directories: *) - let () = Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x)) in - let basedir = if !Flags.boot then None else Some (Envars.coqlib ()) in - (* Which ocaml compiler to invoke *) - let prog = if !opt then "opt" else "ocamlc" in - (* Which arguments ? *) - if !opt && !top then failwith "no custom toplevel in native code!"; - let flags = if !opt then Coq_config.flambda_flags else Coq_config.vmbyteflags in - let topstart = if !top then [ "topstart.cmo" ] else [] in - let (modules, tolink) = files_to_link userfiles in - let main_file = create_tmp_main_file modules in - try - (* - We add topstart.cmo explicitly because we shunted ocamlmktop wrapper. - - With the coq .cma, we MUST use the -linkall option. *) - let coq_camlflags = - List.filter ((<>) "") (split_on_char ' ' Coq_config.caml_flags) in - let args = - coq_camlflags @ "-linkall" :: "-w" :: "-31" :: flags @ copts @ options @ - (std_includes basedir) @ tolink @ [ main_file ] @ topstart - in - if !echo then begin - let command = String.concat " " (Envars.ocamlfind ()::prog::args) in - print_endline command; - print_endline - ("(command length is " ^ - (string_of_int (String.length command)) ^ " characters)"); - flush Pervasives.stdout - end; - let exitcode = run_command (Envars.ocamlfind ()) (prog::args) in - clean main_file; - exitcode - with reraise -> clean main_file; raise reraise - -let pr_exn = function - | Failure msg -> msg - | Unix.Unix_error (err,fn,arg) -> fn^" "^arg^" : "^Unix.error_message err - | any -> Printexc.to_string any - -let _ = - try exit (main ()) - with any -> Printf.eprintf "Error: %s\n" (pr_exn any); exit 1 diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index b62396317..6a3993ad4 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -848,5 +848,3 @@ let start () = end; CProfile.print_profile (); exit 0 - -(* [Coqtop.start] will be called by the code produced by coqmktop *) diff --git a/toplevel/coqtop_bin.ml b/toplevel/coqtop_bin.ml new file mode 100644 index 000000000..62459003b --- /dev/null +++ b/toplevel/coqtop_bin.ml @@ -0,0 +1,6 @@ +(* Main coqtop initialization *) +let () = + (* XXX: We should make this a configure option *) + List.iter Mltop.add_known_module Str.(split (regexp " ") Tolink.static_modules); + (* Start the toplevel loop *) + Coqtop.start() diff --git a/toplevel/coqtop_byte_bin.ml b/toplevel/coqtop_byte_bin.ml new file mode 100644 index 000000000..7d8354ec3 --- /dev/null +++ b/toplevel/coqtop_byte_bin.ml @@ -0,0 +1,21 @@ +let drop_setup () = + begin try + (* Enable rectypes in the toplevel if it has the directive #rectypes *) + begin match Hashtbl.find Toploop.directive_table "rectypes" with + | Toploop.Directive_none f -> f () + | _ -> () + end + with + | Not_found -> () + end; + let ppf = Format.std_formatter in + Mltop.(set_top + { load_obj = (fun f -> if not (Topdirs.load_file ppf f) + then CErrors.user_err Pp.(str ("Could not load plugin "^f)) + ); + use_file = Topdirs.dir_use ppf; + add_dir = Topdirs.dir_directory; + ml_loop = (fun () -> Toploop.loop ppf); + }) + +let _ = drop_setup () diff --git a/toplevel/coqtop_opt_bin.ml b/toplevel/coqtop_opt_bin.ml new file mode 100644 index 000000000..410b4679a --- /dev/null +++ b/toplevel/coqtop_opt_bin.ml @@ -0,0 +1,3 @@ +let drop_setup () = Mltop.remove () + +let _ = drop_setup () -- cgit v1.2.3 From f5cb7eb3e68e4b7d1bb5eeb8d9c58666201945d4 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 10 Dec 2017 03:31:55 +0100 Subject: [make] remove unneeded generated file "tolink.ml" When statically linking plugins, the "DECLARE PLUGIN" macro takes care of properly setting up the loaded module table. This setup was also done by `coqmktop`, thus in order to ease bisecting, we didn't take care of it in the `coqmktop` deprecation. Fixes #6364. --- .gitignore | 1 - Makefile | 2 +- Makefile.build | 18 ++++++------------ doc/refman/RefMan-uti.tex | 11 ++++------- toplevel/coqtop_bin.ml | 6 +----- 5 files changed, 12 insertions(+), 26 deletions(-) diff --git a/.gitignore b/.gitignore index 36536ec96..cec51986d 100644 --- a/.gitignore +++ b/.gitignore @@ -157,7 +157,6 @@ plugins/ssr/ssrvernac.ml kernel/byterun/coq_jumptbl.h kernel/copcodes.ml -tools/tolink.ml ide/index_urls.txt .lia.cache checker/names.ml diff --git a/Makefile b/Makefile index 0078dba20..2637996ed 100644 --- a/Makefile +++ b/Makefile @@ -87,7 +87,7 @@ EXISTINGMLI := $(call find, '*.mli') ## Files that will be generated GENML4FILES:= $(ML4FILES:.ml4=.ml) -export GENMLFILES:=$(LEXFILES:.mll=.ml) tools/tolink.ml kernel/copcodes.ml +export GENMLFILES:=$(LEXFILES:.mll=.ml) kernel/copcodes.ml export GENHFILES:=kernel/byterun/coq_jumptbl.h export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) diff --git a/Makefile.build b/Makefile.build index 3e4c5a0b4..f11719c07 100644 --- a/Makefile.build +++ b/Makefile.build @@ -386,12 +386,12 @@ $(COQTOP_BYTE_MLTOP): toplevel/coqtop_byte_bin.ml $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -package compiler-libs.toplevel -c $< ifeq ($(BEST),opt) -$(COQTOPEXE): tools/tolink.cmx $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs) $(COQTOP_OPT_MLTOP) +$(COQTOPEXE): $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs) $(COQTOP_OPT_MLTOP) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(OCAMLOPT) -linkall -linkpkg -I vernac -I toplevel -I tools \ + $(HIDE)$(OCAMLOPT) -linkall -linkpkg -I toplevel \ -I kernel/byterun/ -cclib -lcoqrun \ $(SYSMOD) -package camlp5.gramlib \ - tools/tolink.cmx $(LINKCMX) $(OPTFLAGS) $(LINKMETADATA) \ + $(LINKCMX) $(OPTFLAGS) $(LINKMETADATA) \ $(COQTOP_OPT_MLTOP) toplevel/coqtop_bin.ml -o $@ $(STRIP) $@ $(CODESIGN) $@ @@ -401,20 +401,14 @@ $(COQTOPEXE): $(COQTOPBYTE) endif # Are "-cclib lcoqrun -dllib -lcoqrun" necessary? -$(COQTOPBYTE): tools/tolink.cmo $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA) $(COQTOP_BYTE_MLTOP) +$(COQTOPBYTE): $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA) $(COQTOP_BYTE_MLTOP) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(OCAMLC) -linkall -linkpkg -I vernac -I toplevel -I tools \ + $(HIDE)$(OCAMLC) -linkall -linkpkg -I toplevel \ -I kernel/byterun -dllpath $(abspath kernel/byterun) -cclib -lcoqrun -dllib -lcoqrun \ $(SYSMOD) -package camlp5.gramlib,compiler-libs.toplevel \ - tools/tolink.cmo $(LINKCMO) $(BYTEFLAGS) \ + $(LINKCMO) $(BYTEFLAGS) \ $(COQTOP_BYTE_MLTOP) toplevel/coqtop_bin.ml -o $@ -tools/tolink.ml: Makefile.build Makefile.common - $(SHOW)"ECHO... >" $@ - $(HIDE)echo "let static_modules = \""$(STATICPLUGINS)"\"" > $@ - $(HIDE)echo "let core_libs = \""$(LINKCMO)"\"" >> $@ - $(HIDE)echo "let core_objs = \""$(OBJSMOD)"\"" >> $@ - # coqc COQCCMO:=lib/clib.cma lib/cErrors.cmo toplevel/usage.cmo tools/coqc.cmo diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex index 002e9625c..962aa98b6 100644 --- a/doc/refman/RefMan-uti.tex +++ b/doc/refman/RefMan-uti.tex @@ -12,19 +12,16 @@ linking. Nowadays, the preferred method is to use \texttt{ocamlfind}. The most basic custom toplevel is built using: \begin{quotation} -\texttt{\% make tools/tolink.cmx} \texttt{\% ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg - -package coq.toplevel -I tools tolink.cmx toplevel/coqtop\_bin.ml -o my\_toplevel.native} + -package coq.toplevel toplevel/coqtop\_bin.ml -o my\_toplevel.native} \end{quotation} -For example, to statically link LTAC, you can add it to \texttt{tools/tolink.ml} and use: +For example, to statically link LTAC, you can just do: \begin{quotation} -\texttt{\% make tools/tolink.cmx} \texttt{\% ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg - -package coq.toplevel -package coq.ltac -I tools tolink.cmx toplevel/coqtop\_bin.ml -o my\_toplevel.native} + -package coq.toplevel -package coq.ltac toplevel/coqtop\_bin.ml -o my\_toplevel.native} \end{quotation} - -We will remove the need for the \texttt{tolink} file in the future. +and similarly for other plugins. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% diff --git a/toplevel/coqtop_bin.ml b/toplevel/coqtop_bin.ml index 62459003b..56aced92a 100644 --- a/toplevel/coqtop_bin.ml +++ b/toplevel/coqtop_bin.ml @@ -1,6 +1,2 @@ (* Main coqtop initialization *) -let () = - (* XXX: We should make this a configure option *) - List.iter Mltop.add_known_module Str.(split (regexp " ") Tolink.static_modules); - (* Start the toplevel loop *) - Coqtop.start() +let () = Coqtop.start() -- cgit v1.2.3