Merge PR#709: Bytecode compilation apart from 'make world', again

6 files changed, 123 insertions, 18 deletions

diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index c25ad1f37..5e223a0b4 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -115,6 +115,17 @@ TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
 
 OPT?=
 
+# The DYNOBJ and DYNLIB variables are used by "coqdep -dyndep var" in .v.d
+ifeq '$(OPT)' '-byte'
+USEBYTE:=true
+DYNOBJ:=.cmo
+DYNLIB:=.cma
+else
+USEBYTE:=
+DYNOBJ:=.cmxs
+DYNLIB:=.cmxs
+endif
+
 COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS)
 COQCHKFLAGS?=-silent -o $(COQLIBS) 
 COQDOCFLAGS?=-interpolate -utf8 $(COQLIBS_NOML)
@@ -213,7 +224,6 @@ CMOFILESTOINSTALL = $(filter-out $(addsuffix .cmo,$(PACKEDFILES)),$(CMOFILES))
 OBJFILES = $(call vo_to_obj,$(VOFILES))
 ALLNATIVEFILES = \
 	$(OBJFILES:.o=.cmi) \
-	$(OBJFILES:.o=.cmo) \
 	$(OBJFILES:.o=.cmx) \
 	$(OBJFILES:.o=.cmxs)
 # trick: wildcard filters out non-existing files
@@ -223,8 +233,9 @@ FILESTOINSTALL = \
 	$(VFILES) \
 	$(GLOBFILES) \
 	$(NATIVEFILESTOINSTALL) \
+	$(CMIFILESTOINSTALL)
+BYTEFILESTOINSTALL = \
 	$(CMOFILESTOINSTALL) \
-	$(CMIFILESTOINSTALL) \
 	$(CMAFILES)
 ifeq '$(HASNATDYNLINK)' 'true'
 DO_NATDYNLINK = yes
@@ -256,9 +267,15 @@ post-all::
 	@# Extension point
 .PHONY: post-all
 
-real-all: $(VOFILES) $(CMOFILES) $(CMAFILES) $(if $(DO_NATDYNLINK),$(CMXSFILES))
+real-all: $(VOFILES) $(if $(USEBYTE),bytefiles,optfiles)
 .PHONY: real-all
 
+bytefiles: $(CMOFILES) $(CMAFILES)
+.PHONY: bytefiles
+
+optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES))
+.PHONY: optfiles
+
 # FIXME, see Ralph's bugreport
 quick: $(VOFILES:.vo=.vio)
 .PHONY: quick
@@ -350,6 +367,18 @@ install-extra::
 	@# Extension point
 .PHONY: install install-extra
 
+install-byte:
+	$(HIDE)for f in $(BYTEFILESTOINSTALL); do\
+	 df="`$(COQMF_MAKEFILE) -destination-of "$$f" $(COQLIBS)`";\
+	 if [ -z "$$df" ]; then\
+	   echo SKIP "$$f" since it has no logical path;\
+	 else\
+	   install -d "$(DESTDIR)$(COQLIBINSTALL)/$$df"; \
+	   install -m 0644 "$$f" "$(DESTDIR)$(COQLIBINSTALL)/$$df"; \
+	   echo INSTALL "$$f" "$(DESTDIR)$(COQLIBINSTALL)/$$df";\
+	 fi;\
+	done
+
 install-doc:: html mlihtml
 	@# Extension point
 	$(HIDE)install -d "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html"
@@ -561,7 +590,7 @@ $(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack
 
 $(addsuffix .d,$(VFILES)): %.v.d: %.v
 	$(SHOW)'COQDEP $<'
-	$(HIDE)$(COQDEP) $(COQLIBS) -c "$<" $(redir_if_ok)
+	$(HIDE)$(COQDEP) $(COQLIBS) -dyndep var -c "$<" $(redir_if_ok)
 
 # Misc ########################################################################
 
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 044399544..cba9c3eb0 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -320,19 +320,25 @@ let treat_coq_file chan =
         List.fold_left (fun accu v -> mark_v_done from accu v) acc strl
       | Declare sl ->
         let declare suff dir s =
-          let base = file_name s dir in
-          let opt = if !option_natdynlk then " " ^ base ^ ".cmxs" else "" in
-          (escape base, suff ^ opt)
+          let base = escape (file_name s dir) in
+          match !option_dynlink with
+          | No -> []
+          | Byte -> [base,suff]
+          | Opt -> [base,".cmxs"]
+          | Both -> [base,suff; base,".cmxs"]
+          | Variable ->
+             if suff=".cmo" then [base,"$(DYNOBJ)"]
+             else [base,"$(DYNLIB)"]
         in
         let decl acc str =
           let s = basename_noext str in
           if not (StrSet.mem s !deja_vu_ml) then
             let () = deja_vu_ml := StrSet.add s !deja_vu_ml in
             match search_mllib_known s with
-            | Some mldir -> (declare ".cma" mldir s) :: acc
+            | Some mldir -> (declare ".cma" mldir s) @ acc
             | None ->
               match search_ml_known s with
-              | Some mldir -> (declare ".cmo" mldir s) :: acc
+              | Some mldir -> (declare ".cmo" mldir s) @ acc
               | None -> acc
           else acc
         in
@@ -449,6 +455,7 @@ let usage () =
   eprintf "  -coqlib dir : set the coq standard library directory\n";
   eprintf "  -suffix s : \n";
   eprintf "  -slash : deprecated, no effect\n";
+  eprintf "  -dyndep (opt|byte|both|no|var) : set how dependencies over ML modules are printed";
   exit 1
 
 let split_period = Str.split (Str.regexp (Str.quote "."))
@@ -476,17 +483,22 @@ let rec parse = function
   | "-slash" :: ll ->
     Printf.eprintf "warning: option -slash has no effect and is deprecated.\n";
     parse ll
+  | "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll
+  | "-dyndep" :: "opt" :: ll -> option_dynlink := Opt; parse ll
+  | "-dyndep" :: "byte" :: ll -> option_dynlink := Byte; parse ll
+  | "-dyndep" :: "both" :: ll -> option_dynlink := Both; parse ll
+  | "-dyndep" :: "var" :: ll -> option_dynlink := Variable; parse ll
   | ("-h"|"--help"|"-help") :: _ -> usage ()
   | f :: ll -> treat_file None f; parse ll
   | [] -> ()
 
 let coqdep () =
   if Array.length Sys.argv < 2 then usage ();
+  if not Coq_config.has_natdynlink then option_dynlink := No;
   parse (List.tl (Array.to_list Sys.argv));
   (* Add current dir with empty logical path if not set by options above. *)
   (try ignore (Coqdep_common.find_dir_logpath (Sys.getcwd()))
    with Not_found -> add_norec_dir_import add_known "." []);
-  if not Coq_config.has_natdynlink then option_natdynlk := false;
   (* NOTE: These directories are searched from last to first *)
   if !option_boot then begin
     add_rec_dir_import add_known "theories" ["Coq"];
diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml
index 6fc826833..25f62d2be 100644
--- a/tools/coqdep_boot.ml
+++ b/tools/coqdep_boot.ml
@@ -16,7 +16,11 @@ open Coqdep_common
 *)
 
 let rec parse = function
-  | "-natdynlink" :: "no" :: ll -> option_natdynlk := false; parse ll
+  | "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll
+  | "-dyndep" :: "opt" :: ll -> option_dynlink := Opt; parse ll
+  | "-dyndep" :: "byte" :: ll -> option_dynlink := Byte; parse ll
+  | "-dyndep" :: "both" :: ll -> option_dynlink := Both; parse ll
+  | "-dyndep" :: "var" :: ll -> option_dynlink := Variable; parse ll
   | "-c" :: ll -> option_c := true; parse ll
   | "-boot" :: ll -> parse ll (* We're already in boot mode by default *)
   | "-mldep" :: ocamldep :: ll ->
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index f5e93527c..bf8bcd0c4 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -15,7 +15,7 @@ open Minisys
     behavior is the one of [coqdep -boot]. Its only dependencies
     are [Coqdep_lexer], [Unix] and [Minisys], and it should stay so.
     If it need someday some additional information, pass it via
-    options (see for instance [option_natdynlk] below).
+    options (see for instance [option_dynlink] below).
 *)
 
 module StrSet = Set.Make(String)
@@ -26,9 +26,11 @@ module StrListMap = Map.Make(StrList)
 let stderr = Pervasives.stderr
 let stdout = Pervasives.stdout
 
+type dynlink = Opt | Byte | Both | No | Variable
+
 let option_c = ref false
 let option_noglob = ref false
-let option_natdynlk = ref true
+let option_dynlink = ref Both
 let option_boot = ref false
 let option_mldep = ref None
 
@@ -383,10 +385,16 @@ let rec traite_fichier_Coq suffixe verbose f =
        		end) strl
 	  | Declare sl ->
 	      let declare suff dir s =
-		let base = file_name s dir in
-		let opt = if !option_natdynlk then " "^base^".cmxs" else "" in
-		printf " %s%s%s" (escape base) suff opt
-	      in
+		let base = escape (file_name s dir) in
+                match !option_dynlink with
+                | No -> ()
+                | Byte -> printf " %s%s" base suff
+                | Opt -> printf " %s.cmxs" base
+                | Both -> printf " %s%s %s.cmxs" base suff base
+                | Variable ->
+                   printf " %s%s" base
+                    (if suff=".cmo" then "$(DYNOBJ)" else "$(DYNLIB)")
+              in
 	      let decl str =
                 let s = basename_noext str in
 		if not (StrSet.mem s !deja_vu_ml) then begin
diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli
index 10da0240d..8c1787d31 100644
--- a/tools/coqdep_common.mli
+++ b/tools/coqdep_common.mli
@@ -19,7 +19,10 @@ val find_dir_logpath: string -> string list
 val option_c : bool ref
 val option_noglob : bool ref
 val option_boot : bool ref
-val option_natdynlk : bool ref
+
+type dynlink = Opt | Byte | Both | No | Variable
+
+val option_dynlink : dynlink ref
 val option_mldep : string option ref
 val norec_dirs : StrSet.t ref
 val suffixe : string ref
diff --git a/tools/coqdoc/cdglobals.mli b/tools/coqdoc/cdglobals.mli
new file mode 100644
index 000000000..2c9b3fb8e
--- /dev/null
+++ b/tools/coqdoc/cdglobals.mli
@@ -0,0 +1,49 @@
+type target_language = LaTeX | HTML | TeXmacs | Raw
+val target_language : target_language ref
+type output_t = StdOut | MultFiles | File of string
+val output_dir : string ref
+val out_to : output_t ref
+val out_channel : out_channel ref
+val ( / ) : string -> string -> string
+val coqdoc_out : string -> string
+val open_out_file : string -> unit
+val close_out_file : unit -> unit
+type glob_source_t = NoGlob | DotGlob | GlobFile of string
+val glob_source : glob_source_t ref
+val normalize_path : string -> string
+val normalize_filename : string -> string * string
+val guess_coqlib : unit -> string
+val header_trailer : bool ref
+val header_file : string ref
+val header_file_spec : bool ref
+val footer_file : string ref
+val footer_file_spec : bool ref
+val quiet : bool ref
+val light : bool ref
+val gallina : bool ref
+val short : bool ref
+val index : bool ref
+val multi_index : bool ref
+val index_name : string ref
+val toc : bool ref
+val page_title : string ref
+val title : string ref
+val externals : bool ref
+val coqlib : string ref
+val coqlib_path : string ref
+val raw_comments : bool ref
+val parse_comments : bool ref
+val plain_comments : bool ref
+val toc_depth : int option ref
+val lib_name : string ref
+val lib_subtitles : bool ref
+val interpolate : bool ref
+val inline_notmono : bool ref
+val charset : string ref
+val inputenc : string ref
+val latin1 : bool ref
+val utf8 : bool ref
+val set_latin1 : unit -> unit
+val set_utf8 : unit -> unit
+type coq_module = string
+type file = Vernac_file of string * coq_module | Latex_file of string