From 251b34ac94d8797637b3ca5acce5db593950d0c5 Mon Sep 17 00:00:00 2001 From: letouzey Date: Sun, 18 Sep 2011 21:51:16 +0000 Subject: avoid dependency nightmare by creating coqdep_{lexer,common}.mli Sequel to commit 14476 : in fact, even with "tools" in .PHONY, we still may have coqdep stuff being recompiled in a "make" that follows a successful "make". This seems to related to the hacks I've introduced to prevent ocamlopt from erasing and recreating .cmi when there's no .mli around (cf. comment around line 823 in Makefile.build). Scenario: - First we build coqdep_boot directly out of coqdep_lexer.ml and co. When ocamlopt is around, this creates some .cmx and .cmi, but no .cmo. - Later we build coqdep, which need coqdep_lexer.cmx and co. Now "make" checks whether these .cmx are up-to-date. But our hacks made these .cmx depend on the corresponding .cmi. Then "make" checks whether these .cmi are up-to-date. But our hacks made these .cmi depend on the corresponding .cmo. These .cmo doesn't exist yet, we run ocamlc, which recreates the .cmi with same content but a different timestamp. For some strange reason, even with refreshed .cmi, the .cmx are not remade by this run, but will be on the next run. Conclusion: what a mess. Implicit rules about .cmx / .cmo / .cmi should be improved, but I see currently no simple solution. In the meantime, an simple ad-hoc fix is to create these two .mli ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14479 85f007b7-540e-0410-9357-904b9bb8a0f7 --- Makefile.build | 13 +++++++++++-- tools/coqdep_common.mli | 49 +++++++++++++++++++++++++++++++++++++++++++++++++ tools/coqdep_lexer.mli | 23 +++++++++++++++++++++++ tools/coqdep_lexer.mll | 2 -- 4 files changed, 83 insertions(+), 4 deletions(-) create mode 100644 tools/coqdep_common.mli create mode 100644 tools/coqdep_lexer.mli diff --git a/Makefile.build b/Makefile.build index 857cb39142..2c6e73c5a9 100644 --- a/Makefile.build +++ b/Makefile.build @@ -496,9 +496,18 @@ printers: $(DEBUGPRINTERS) tools:: $(TOOLS) $(DEBUGPRINTERS) $(COQDEPBOOT) -# coqdep_boot : a basic version of coqdep, with almost no dependencies +# coqdep_boot : a basic version of coqdep, with almost no dependencies. -$(COQDEPBOOT): tools/coqdep_lexer.ml tools/coqdep_common.ml tools/coqdep_boot.ml +# Here it is important to mention .ml files instead of .cmo in order +# to avoid using implicit rules and hence .ml.d files that would need +# coqdep_boot. + +COQDEPBOOTSRC:= \ + tools/coqdep_lexer.mli tools/coqdep_lexer.ml \ + tools/coqdep_common.mli tools/coqdep_common.ml \ + tools/coqdep_boot.ml + +$(COQDEPBOOT): $(COQDEPBOOTSRC) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml, -I tools, unix) diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli new file mode 100644 index 0000000000..53c3ba17cb --- /dev/null +++ b/tools/coqdep_common.mli @@ -0,0 +1,49 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* string -> string +val get_extension : string -> string list -> string * string +val basename_noext : string -> string +val mlAccu : (string * string * dir) list ref +val mliAccu : (string * dir) list ref +val mllibAccu : (string * dir) list ref +val vAccu : (string * string) list ref +val addQueue : 'a list ref -> 'a -> unit +val add_ml_known : string -> dir -> unit +val iter_ml_known : (string -> dir -> unit) -> unit +val search_ml_known : string -> dir option +val add_mli_known : string -> dir -> unit +val iter_mli_known : (string -> dir -> unit) -> unit +val search_mli_known : string -> dir option +val add_mllib_known : string -> dir -> unit +val search_mllib_known : string -> dir option +val vKnown : (string list, string) Hashtbl.t +val coqlibKnown : (string list, unit) Hashtbl.t +val file_name : string -> string option -> string +val escape : string -> string +val canonize : string -> string +val mL_dependencies : unit -> unit +val coq_dependencies : unit -> unit +val suffixes : 'a list -> 'a list list +val add_known : string -> string list -> string -> unit +val add_directory : + bool -> + (string -> string list -> string -> unit) -> string -> string list -> unit +val add_dir : + (string -> string list -> string -> unit) -> string -> string list -> unit +val add_rec_dir : + (string -> string list -> string -> unit) -> string -> string list -> unit +val treat_file : dir -> string -> unit diff --git a/tools/coqdep_lexer.mli b/tools/coqdep_lexer.mli new file mode 100644 index 0000000000..2605862707 --- /dev/null +++ b/tools/coqdep_lexer.mli @@ -0,0 +1,23 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* coq_token +val caml_action : Lexing.lexbuf -> mL_token +val mllib_list : Lexing.lexbuf -> string list +val ocamldep_parse : Lexing.lexbuf -> string list diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll index 09433ff760..e0bf1daec7 100644 --- a/tools/coqdep_lexer.mll +++ b/tools/coqdep_lexer.mll @@ -13,8 +13,6 @@ type mL_token = Use_module of string - type spec = bool - type coq_token = | Require of string list list | RequireString of string -- cgit v1.2.3