aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/derive/derive.ml5
-rw-r--r--plugins/extraction/g_extraction.ml410
-rw-r--r--plugins/funind/glob_term_to_relation.ml2
-rw-r--r--plugins/funind/indfun.ml13
-rw-r--r--plugins/funind/merge.ml6
-rw-r--r--plugins/funind/recdef.ml28
-rw-r--r--plugins/ltac/profile_ltac.ml29
-rw-r--r--plugins/ltac/profile_ltac.mli37
-rw-r--r--plugins/ltac/profile_ltac_tactics.ml436
-rw-r--r--plugins/ltac/rewrite.ml11
-rw-r--r--plugins/ltac/tacinterp.ml16
-rw-r--r--plugins/micromega/MExtraction.v17
12 files changed, 155 insertions, 55 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index fb65a8639a..c8c4c2dad9 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -38,9 +38,8 @@ let start_deriving f suchthat lemma =
let f_type = EConstr.Unsafe.to_constr f_type in
let ef = EConstr.Unsafe.to_constr ef in
let env' = Environ.push_named (LocalDef (f, ef, f_type)) env in
- let evdref = ref sigma in
- let suchthat = Constrintern.interp_type_evars env' evdref suchthat in
- TCons ( env' , !evdref , suchthat , (fun sigma _ ->
+ let sigma, suchthat = Constrintern.interp_type_evars env' sigma suchthat in
+ TCons ( env' , sigma , suchthat , (fun sigma _ ->
TNil sigma))))))
in
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index 23452febdc..24c70bccfb 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -42,14 +42,20 @@ ARGUMENT EXTEND int_or_id
END
let pr_language = function
- | Ocaml -> str "Ocaml"
+ | Ocaml -> str "OCaml"
| Haskell -> str "Haskell"
| Scheme -> str "Scheme"
| JSON -> str "JSON"
+let warn_deprecated_ocaml_spelling =
+ CWarnings.create ~name:"deprecated-ocaml-spelling" ~category:"deprecated"
+ (fun () ->
+ strbrk ("The spelling \"OCaml\" should be used instead of \"Ocaml\"."))
+
VERNAC ARGUMENT EXTEND language
PRINTED BY pr_language
-| [ "Ocaml" ] -> [ Ocaml ]
+| [ "Ocaml" ] -> [ let _ = warn_deprecated_ocaml_spelling () in Ocaml ]
+| [ "OCaml" ] -> [ Ocaml ]
| [ "Haskell" ] -> [ Haskell ]
| [ "Scheme" ] -> [ Scheme ]
| [ "JSON" ] -> [ JSON ]
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index fa43536304..889c064b24 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1497,7 +1497,7 @@ let do_build_inductive
let _time2 = System.get_time () in
try
with_full_print
- (Flags.silently (Command.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false))
+ (Flags.silently (ComInductive.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false))
Decl_kinds.Finite
with
| UserError(s,msg) as e ->
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 9e22ad3063..071599d9c5 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -158,8 +158,8 @@ let build_newrecursive
(fun (env,impls) (((_,recname),_),bl,arityc,_) ->
let arityc = Constrexpr_ops.mkCProdN bl arityc in
let arity,ctx = Constrintern.interp_type env0 sigma arityc in
- let evdref = ref (Evd.from_env env0) in
- let _, (_, impls') = Constrintern.interp_context_evars env evdref bl in
+ let evd = Evd.from_env env0 in
+ let evd, (_, (_, impls')) = Constrintern.interp_context_evars env evd bl in
let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity impls' in
let open Context.Named.Declaration in
(Environ.push_named (LocalAssum (recname,arity)) env, Id.Map.add recname impl impls))
@@ -406,7 +406,8 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
match fixpoint_exprl with
| [(((_,fname),pl),_,bl,ret_type,body),_] when not is_rec ->
let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in
- Command.do_definition
+ ComDefinition.do_definition
+ ~program_mode:false
fname
(Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition) pl
bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ()));
@@ -426,7 +427,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
in
evd,List.rev rev_pconstants
| _ ->
- Command.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl;
+ ComFixpoint.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl;
let evd,rev_pconstants =
List.fold_left
(fun (evd,l) ((((_,fname),_),_,_,_,_),_) ->
@@ -616,8 +617,8 @@ and rebuild_nal aux bk bl' nal typ =
let rebuild_bl aux bl typ = rebuild_bl aux bl typ
let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) =
- let fixl,ntns = Command.extract_fixpoint_components false fixpoint_exprl in
- let ((_,_,typel),_,ctx,_) = Command.interp_fixpoint fixl ntns in
+ let fixl,ntns = ComFixpoint.extract_fixpoint_components false fixpoint_exprl in
+ let ((_,_,typel),_,ctx,_) = ComFixpoint.interp_fixpoint ~cofix:false fixl ntns in
let constr_expr_typel =
with_full_print (List.map (fun c -> Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx) (EConstr.of_constr c))) typel in
let fixpoint_exprl_with_new_bl =
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 9e2774ff32..9fcb35f89e 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -889,11 +889,11 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
} in *)
let indexpr = glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in
(* Declare inductive *)
- let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in
- let mie,pl,impls = Command.interp_mutual_inductive indl []
+ let indl,_,_ = ComInductive.extract_mutual_inductive_declaration_components [(indexpr,[])] in
+ let mie,pl,impls = ComInductive.interp_mutual_inductive indl []
false (* non-cumulative *) false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in
(* Declare the mutual inductive block with its associated schemes *)
- ignore (Command.declare_mutual_inductive_with_eliminations mie pl impls)
+ ignore (ComInductive.declare_mutual_inductive_with_eliminations mie pl impls)
(* Find infos on identifier id. *)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 766adfc63a..363ad5dfc9 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1427,7 +1427,7 @@ let com_terminate
nb_args ctx
hook =
let start_proof ctx (tac_start:tactic) (tac_end:tactic) =
- let evmap, env = Pfedit.get_current_context () in
+ let evd, env = Pfedit.get_current_context () in
Lemmas.start_proof thm_name
(Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env)
ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) hook;
@@ -1479,13 +1479,13 @@ let (com_eqn : int -> Id.t ->
| ConstRef c -> is_opaque_constant c
| _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant.")
in
- let evmap, env = Pfedit.get_current_context () in
- let evmap = Evd.from_ctx (Evd.evar_universe_context evmap) in
+ let evd, env = Pfedit.get_current_context () in
+ let evd = Evd.from_ctx (Evd.evar_universe_context evd) in
let f_constr = constr_of_global f_ref in
let equation_lemma_type = subst1 f_constr equation_lemma_type in
(Lemmas.start_proof eq_name (Global, false, Proof Lemma)
~sign:(Environ.named_context_val env)
- evmap
+ evd
(EConstr.of_constr equation_lemma_type)
(Lemmas.mk_hook (fun _ _ -> ()));
ignore (by
@@ -1528,14 +1528,14 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
let open Constr in
let open CVars in
let env = Global.env() in
- let evd = ref (Evd.from_env env) in
- let function_type = interp_type_evars env evd type_of_f in
+ let evd = Evd.from_env env in
+ let evd, function_type = interp_type_evars env evd type_of_f in
let function_type = EConstr.Unsafe.to_constr function_type in
let env = push_named (Context.Named.Declaration.LocalAssum (function_name,function_type)) env in
(* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *)
- let ty = interp_type_evars env evd ~impls:rec_impls eq in
+ let evd, ty = interp_type_evars env evd ~impls:rec_impls eq in
let ty = EConstr.Unsafe.to_constr ty in
- let evm, nf = Evarutil.nf_evars_and_universes !evd in
+ let evd, nf = Evarutil.nf_evars_and_universes evd in
let equation_lemma_type = nf_betaiotazeta (EConstr.of_constr (nf ty)) in
let function_type = nf function_type in
let equation_lemma_type = EConstr.Unsafe.to_constr equation_lemma_type in
@@ -1560,16 +1560,16 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
let functional_id = add_suffix function_name "_F" in
let term_id = add_suffix function_name "_terminate" in
let functional_ref =
- let univs = Entries.Monomorphic_const_entry (Evd.universe_context_set evm) in
+ let univs = Entries.Monomorphic_const_entry (Evd.universe_context_set evd) in
declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~univs res
in
(* Refresh the global universes, now including those of _F *)
- let evm = Evd.from_env (Global.env ()) in
+ let evd = Evd.from_env (Global.env ()) in
let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> LocalAssum (x,t)) pre_rec_args) env in
let relation, evuctx =
- interp_constr env_with_pre_rec_args evm r
+ interp_constr env_with_pre_rec_args evd r
in
- let evm = Evd.from_ctx evuctx in
+ let evd = Evd.from_ctx evuctx in
let tcc_lemma_name = add_suffix function_name "_tcc" in
let tcc_lemma_constr = ref Undefined in
(* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *)
@@ -1599,7 +1599,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
and functional_ref = destConst (constr_of_global functional_ref)
and eq_ref = destConst (constr_of_global eq_ref) in
generate_induction_principle f_ref tcc_lemma_constr
- functional_ref eq_ref rec_arg_num (EConstr.of_constr rec_arg_type) (nb_prod evm (EConstr.of_constr res)) (EConstr.of_constr relation);
+ functional_ref eq_ref rec_arg_num (EConstr.of_constr rec_arg_type) (nb_prod evd (EConstr.of_constr res)) (EConstr.of_constr relation);
Flags.if_verbose
msgnl (h 1 (Ppconstr.pr_id function_name ++
spc () ++ str"is defined" )++ fnl () ++
@@ -1618,5 +1618,5 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
term_id
using_lemmas
(List.length res_vars)
- evm (Lemmas.mk_hook hook))
+ evd (Lemmas.mk_hook hook))
()
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 5225420dc4..1615465281 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -289,7 +289,7 @@ let rec find_in_stack what acc = function
| { name } as x :: rest when String.equal name what -> Some(acc, x, rest)
| { name } as x :: rest -> find_in_stack what (x :: acc) rest
-let exit_tactic start_time c =
+let exit_tactic ~count_call start_time c =
let diff = time () -. start_time in
match Local.(!stack) with
| [] | [_] ->
@@ -304,7 +304,7 @@ let exit_tactic start_time c =
let node = { node with
total = node.total +. diff;
local = node.local +. diff;
- ncalls = node.ncalls + 1;
+ ncalls = node.ncalls + (if count_call then 1 else 0);
max_total = max node.max_total diff;
} in
(* updating the stack *)
@@ -341,7 +341,7 @@ let tclFINALLY tac (finally : unit Proofview.tactic) =
(fun v -> finally <*> Proofview.tclUNIT v)
(fun (exn, info) -> finally <*> Proofview.tclZERO ~info exn)
-let do_profile s call_trace tac =
+let do_profile s call_trace ?(count_call=true) tac =
let open Proofview.Notations in
Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
if !is_profiling then
@@ -359,7 +359,7 @@ let do_profile s call_trace tac =
tac
(Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
(match call_trace with
- | (_, c) :: _ -> exit_tactic start_time c
+ | (_, c) :: _ -> exit_tactic ~count_call start_time c
| [] -> ()))))
| None -> tac
@@ -397,6 +397,27 @@ let reset_profile () =
reset_profile_tmp ();
data := SM.empty
+(* ****************************** Named timers ****************************** *)
+
+let timer_data = ref M.empty
+
+let timer_name = function
+ | Some v -> v
+ | None -> ""
+
+let restart_timer name =
+ timer_data := M.add (timer_name name) (System.get_time ()) !timer_data
+
+let get_timer name =
+ try M.find (timer_name name) !timer_data
+ with Not_found -> System.get_time ()
+
+let finish_timing ~prefix name =
+ let tend = System.get_time () in
+ let tstart = get_timer name in
+ Feedback.msg_info(str prefix ++ pr_opt str name ++ str " ran for " ++
+ System.fmt_time_difference tstart tend)
+
(* ******************** *)
let print_results_filter ~cutoff ~filter =
diff --git a/plugins/ltac/profile_ltac.mli b/plugins/ltac/profile_ltac.mli
index 52827cb36b..adedf7ee91 100644
--- a/plugins/ltac/profile_ltac.mli
+++ b/plugins/ltac/profile_ltac.mli
@@ -9,9 +9,39 @@
(** Ltac profiling primitives *)
+(* Note(JasonGross): Ltac semantics are a bit insane. There isn't
+ really a good notion of how many times a tactic has been "called",
+ because tactics can be partially evaluated, and it's unclear
+ whether the number of "calls" should be the number of times the
+ body is fetched and unfolded, or the number of times the code is
+ executed to a value, etc. The logic in [Tacinterp.eval_tactic]
+ gives a decent approximation, which I believe roughly corresponds
+ to the number of times that the engine runs the tactic value which
+ results from evaluating the tactic expression bound to the name
+ we're considering. However, this is a poor approximation of the
+ time spent in the tactic; we want to consider time spent evaluating
+ a tactic expression to a tactic value to be time spent in the
+ expression, not just time spent in the caller of the expression.
+ So we need to wrap some nodes in additional profiling calls which
+ don't count towards to total call count. Whether or not a call
+ "counts" is indicated by the [count_call] boolean argument.
+
+ Unfortunately, at present, we can get very strange call graphs when
+ a named tactic expression never runs as a tactic value: if we have
+ [Ltac t0 := t.] and [Ltac t1 := t0.], then [t1] is considered to
+ run 0(!) times. It evaluates to [t] during tactic expression
+ evaluation, and although the call trace records the fact that it
+ was called by [t0] which was called by [t1], the tactic running
+ phase never sees this. Thus we get one call tree (from expression
+ evaluation) that has [t1] calls [t0] calls [t], and another call
+ tree which says that the caller of [t1] calls [t] directly; the
+ expression evaluation time goes in the first tree, and the call
+ count and tactic running time goes in the second tree. Alas, I
+ suspect that fixing this requires a redesign of how the profiler
+ hooks into the tactic engine. *)
val do_profile :
string -> ('a * Tacexpr.ltac_call_kind) list ->
- 'b Proofview.tactic -> 'b Proofview.tactic
+ ?count_call:bool -> 'b Proofview.tactic -> 'b Proofview.tactic
val set_profiling : bool -> unit
@@ -22,6 +52,10 @@ val print_results_tactic : string -> unit
val reset_profile : unit -> unit
+val restart_timer : string option -> unit
+
+val finish_timing : prefix:string -> string option -> unit
+
val do_print_results_at_close : unit -> unit
(* The collected statistics for a tactic. The timing data is collected over all
@@ -46,4 +80,3 @@ type treenode = {
(* Returns the profiling results known by the current process *)
val get_local_profiling_results : unit -> treenode
val feedback_results : treenode -> unit
-
diff --git a/plugins/ltac/profile_ltac_tactics.ml4 b/plugins/ltac/profile_ltac_tactics.ml4
index f095660638..9864ffeb65 100644
--- a/plugins/ltac/profile_ltac_tactics.ml4
+++ b/plugins/ltac/profile_ltac_tactics.ml4
@@ -18,6 +18,21 @@ DECLARE PLUGIN "ltac_plugin"
let tclSET_PROFILING b =
Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> set_profiling b))
+let tclRESET_PROFILE =
+ Proofview.tclLIFT (Proofview.NonLogical.make reset_profile)
+
+let tclSHOW_PROFILE ~cutoff =
+ Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> print_results ~cutoff))
+
+let tclSHOW_PROFILE_TACTIC s =
+ Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> print_results_tactic s))
+
+let tclRESTART_TIMER s =
+ Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> restart_timer s))
+
+let tclFINISH_TIMING ?(prefix="Timer") (s : string option) =
+ Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> finish_timing ~prefix s))
+
TACTIC EXTEND start_ltac_profiling
| [ "start" "ltac" "profiling" ] -> [ tclSET_PROFILING true ]
END
@@ -26,8 +41,27 @@ TACTIC EXTEND stop_ltac_profiling
| [ "stop" "ltac" "profiling" ] -> [ tclSET_PROFILING false ]
END
+TACTIC EXTEND reset_ltac_profile
+| [ "reset" "ltac" "profile" ] -> [ tclRESET_PROFILE ]
+END
+
+TACTIC EXTEND show_ltac_profile
+| [ "show" "ltac" "profile" ] -> [ tclSHOW_PROFILE ~cutoff:!Flags.profile_ltac_cutoff ]
+| [ "show" "ltac" "profile" "cutoff" int(n) ] -> [ tclSHOW_PROFILE ~cutoff:(float_of_int n) ]
+| [ "show" "ltac" "profile" string(s) ] -> [ tclSHOW_PROFILE_TACTIC s ]
+END
+
+TACTIC EXTEND restart_timer
+| [ "restart_timer" string_opt(s) ] -> [ tclRESTART_TIMER s ]
+END
+
+TACTIC EXTEND finish_timing
+| [ "finish_timing" string_opt(s) ] -> [ tclFINISH_TIMING ~prefix:"Timer" s ]
+| [ "finish_timing" "(" string(prefix) ")" string_opt(s) ] -> [ tclFINISH_TIMING ~prefix s ]
+END
+
VERNAC COMMAND EXTEND ResetLtacProfiling CLASSIFIED AS SIDEFF
- [ "Reset" "Ltac" "Profile" ] -> [ reset_profile() ]
+ [ "Reset" "Ltac" "Profile" ] -> [ reset_profile () ]
END
VERNAC COMMAND EXTEND ShowLtacProfile CLASSIFIED AS QUERY
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 2e14243d8a..a698b05dd7 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1781,7 +1781,9 @@ let declare_an_instance n s args =
let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
let anew_instance global binders instance fields =
- new_instance (Flags.is_universe_polymorphism ())
+ let program_mode = Flags.is_program_mode () in
+ let poly = Flags.is_universe_polymorphism () in
+ new_instance ~program_mode poly
binders instance (Some (true, CAst.make @@ CRecord (fields)))
~global ~generalize:false ~refine:false Hints.empty_hint_info
@@ -2012,9 +2014,10 @@ let add_morphism glob binders m s n =
[cHole; s; m]))
in
let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
- ignore(new_instance ~global:glob poly binders instance
- (Some (true, CAst.make @@ CRecord []))
- ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info)
+ let program_mode = Flags.is_program_mode () in
+ ignore(new_instance ~program_mode ~global:glob poly binders instance
+ (Some (true, CAst.make @@ CRecord []))
+ ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info)
(** Bind to "rewrite" too *)
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index ded902a8fb..ccded44179 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1158,10 +1158,14 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
Proofview.V82.tactic begin
tclSHOWHYPS (Proofview.V82.of_tactic (interp_tactic ist tac))
end
- | TacAbstract (tac,ido) ->
+ | TacAbstract (t,ido) ->
+ let call = LtacMLCall tac in
+ push_trace(None,call) ist >>= fun trace ->
+ Profile_ltac.do_profile "eval_tactic:TacAbstract" trace
+ (catch_error_tac trace begin
Proofview.Goal.enter begin fun gl -> Tactics.tclABSTRACT
- (Option.map (interp_ident ist (pf_env gl) (project gl)) ido) (interp_tactic ist tac)
- end
+ (Option.map (interp_ident ist (pf_env gl) (project gl)) ido) (interp_tactic ist t)
+ end end)
| TacThen (t1,t) ->
Tacticals.New.tclTHEN (interp_tactic ist t1) (interp_tactic ist t)
| TacDispatch tl ->
@@ -1272,7 +1276,8 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t =
let extra = TacStore.set extra f_trace trace in
let ist = { lfun = Id.Map.empty; extra = extra; } in
let appl = GlbAppl[r,[]] in
- val_interp ~appl ist (Tacenv.interp_ltac r)
+ Profile_ltac.do_profile "interp_ltac_reference" trace ~count_call:false
+ (val_interp ~appl ist (Tacenv.interp_ltac r))
and interp_tacarg ist arg : Val.t Ftactic.t =
match arg with
@@ -1338,7 +1343,8 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
let ist = {
lfun = newlfun;
extra = TacStore.set ist.extra f_trace []; } in
- catch_error_tac trace (val_interp ist body) >>= fun v ->
+ Profile_ltac.do_profile "interp_app" trace ~count_call:false
+ (catch_error_tac trace (val_interp ist body)) >>= fun v ->
Ftactic.return (name_vfun (push_appl appl largs) v)
end
begin fun (e, info) ->
diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v
index e5b5854f0a..362cc3a597 100644
--- a/plugins/micromega/MExtraction.v
+++ b/plugins/micromega/MExtraction.v
@@ -49,16 +49,13 @@ Extract Constant Rmult => "( * )".
Extract Constant Ropp => "fun x -> - x".
Extract Constant Rinv => "fun x -> 1 / x".
-(** We now extract to stdout, see comment in Makefile.build *)
-
-(*Extraction "plugins/micromega/micromega.ml" *)
-Recursive Extraction
- List.map simpl_cone (*map_cone indexes*)
- denorm Qpower vm_add
- n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find.
-
-
-
+(** In order to avoid annoying build dependencies the actual
+ extraction is only performed as a test in the test suite. *)
+(* Extraction "plugins/micromega/micromega.ml" *)
+(* Recursive Extraction *)
+(* List.map simpl_cone (*map_cone indexes*) *)
+(* denorm Qpower vm_add *)
+(* n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find. *)
(* Local Variables: *)
(* coding: utf-8 *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 15:56:05 +0000