From aaf82265aca43a22006e6cf80f1b3cbe1fd594aa Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 3 Feb 2009 09:43:13 +0000 Subject: Allow to turn contrib/subtac into a (nat)dynlink'able plugin Main issue was declare_summary being triggered too late in subtac_obligations, hence the associated init_function was _not_ being done by Lib.init(). Fixed for the moment by an ad-hoc launch of this init_function in subtac_obligations. In other plugins, this issue doesn't appear, since init_function is mostly putting back some empty set into a reference that was initially empty. No need to really run init_function in this case. For future plugins, we will nonetheless have to be careful about that. Of course, the (ref Obj.magic) was not exactly helpful in debugging this matter, see http://caml.inria.fr/mantis/view.php?id=4707 As said by Xavier, naughty naughty boys... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11877 85f007b7-540e-0410-9357-904b9bb8a0f7 --- Makefile.common | 4 ++-- contrib/subtac/subtac_obligations.ml | 8 +++++++- library/summary.mli | 6 +++++- toplevel/mltop.ml4 | 2 +- 4 files changed, 15 insertions(+), 5 deletions(-) diff --git a/Makefile.common b/Makefile.common index a74126dfe..0b714d1f6 100644 --- a/Makefile.common +++ b/Makefile.common @@ -344,9 +344,9 @@ CONTRIBSTATIC:=\ $(FUNINDCMO) ifneq ($(HASNATDYNLINK),false) - CONTRIBSTATIC:=$(SUBTACCMO) + CONTRIBSTATIC:= INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) $(DPCMA) \ - $(XMLCMA) $(FUNINDCMA) #$(SUBTACCMA) + $(XMLCMA) $(FUNINDCMA) $(SUBTACCMA) PLUGINS:=$(INITPLUGINS) \ $(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) \ $(QUOTECMA) $(RINGCMA) $(NEWRINGCMA) $(FIELDCMA) \ diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml index 839597ece..df700e1b1 100644 --- a/contrib/subtac/subtac_obligations.ml +++ b/contrib/subtac/subtac_obligations.ml @@ -63,7 +63,7 @@ let assumption_message id = Flags.if_verbose message ((string_of_id id) ^ " is assumed") let default_tactic : Proof_type.tactic ref = ref Refiner.tclIDTAC -let default_tactic_expr : Tacexpr.glob_tactic_expr ref = ref (Obj.magic ()) +let default_tactic_expr : Tacexpr.glob_tactic_expr ref = ref (Tacexpr.TacId []) let set_default_tactic t = default_tactic_expr := t; default_tactic := Tacinterp.eval_tactic t @@ -134,6 +134,12 @@ let unfreeze (v, t) = from_prg := v; set_default_tactic t let init () = from_prg := ProgMap.empty; set_default_tactic (Subtac_utils.tactics_call "obligation_tactic" []) +(** Beware: if this code is dynamically loaded via dynlink after the start + of Coq, then this [init] function will not be run by [Lib.init ()]. + Luckily, here we can launch [init] at load-time. *) + +let _ = init () + let _ = Summary.declare_summary "program-tcc-table" { Summary.freeze_function = freeze; diff --git a/library/summary.mli b/library/summary.mli index 7f300a996..3e6375b0e 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -28,5 +28,9 @@ val section_unfreeze_summaries : frozen -> unit val module_unfreeze_summaries : frozen -> unit val init_summaries : unit -> unit - +(** Beware: if some code is dynamically loaded via dynlink after the + initialization of Coq, the init functions of any summary declared + by this code may not be run. It is hence the responsability of + plugins to initialize themselves properly. +*) diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index d1910c145..9bac42c93 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -231,7 +231,7 @@ let stdlib_use_plugins = Coq_config.has_natdynlink let initial_plugins = [ "Extraction_plugin"; "Cc_plugin"; "Ground_plugin"; "Dp_plugin"; - "Recdef_plugin"; (*"subtac_plugin";*) "Xml_plugin"; ] + "Recdef_plugin"; "Subtac_plugin"; "Xml_plugin"; ] (** Other plugins of the standard library. We need their list to avoid trying to load them if they have been statically compiled -- cgit v1.2.3