From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 tools/coqdep_common.ml | 70 ++++++++++++++++++++++++++++++++------------------
 1 file changed, 45 insertions(+), 25 deletions(-)

(limited to 'tools/coqdep_common.ml')

diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 0064aebd..db69a3b7 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Printf
@@ -15,7 +17,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 +28,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
 
@@ -36,6 +40,10 @@ let norec_dirs = ref StrSet.empty
 
 let suffixe = ref ".vo"
 
+[@@@ocaml.warning "-3"]       (* String.capitalize_ascii since 4.03.0 GPR#124 *)
+let capitalize = String.capitalize
+[@@@ocaml.warning "+3"]
+
 type dir = string option
 
 (** [get_extension f l] checks whether [f] has one of the extensions
@@ -94,8 +102,18 @@ let safe_hash_add cmp clq q (k, (v, b)) =
     For the ML files, the string is the basename without extension.
 *)
 
+let same_path_opt s s' =
+  let nf s = (* ./foo/a.ml and foo/a.ml are the same file *)
+    if Filename.is_implicit s
+    then "." // s
+    else s
+  in
+  let s = match s with None -> "." | Some s -> nf s in
+  let s' = match s' with None -> "." | Some s' -> nf s' in
+  s = s'
+
 let warning_ml_clash x s suff s' suff' =
-  if suff = suff' then
+  if suff = suff' && not (same_path_opt s s') then
   eprintf
     "*** Warning: %s%s already found in %s (discarding %s%s)\n" x suff
     (match s with None -> "." | Some d -> d)
@@ -219,7 +237,6 @@ let register_dir_logpath,find_dir_logpath =
 
 let file_name s = function
   | None     -> s
-  | Some "." -> s
   | Some d   -> d // s
 
 let depend_ML str =
@@ -293,15 +310,15 @@ let traite_fichier_modules md ext =
       (fun a_faire str -> match search_mlpack_known str with
 	| Some mldir ->
 	  let file = file_name str mldir in
-	  a_faire^" "^file
+          a_faire @ [file]
 	| None ->
 	  match search_ml_known str with
 	    | Some mldir ->
 	      let file = file_name str mldir in
-	      a_faire^" "^file
-	    | None -> a_faire) "" list
+              a_faire @ [file]
+            | None -> a_faire) [] list
   with
-    | Sys_error _ -> ""
+    | Sys_error _ -> []
     | Syntax_error (i,j) -> error_cannot_parse (md^ext) (i,j)
 
 (* Makefile's escaping rules are awful: $ is escaped by doubling and
@@ -380,10 +397,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
@@ -443,7 +466,7 @@ let mL_dependencies () =
        let fullname = file_name name dirname in
        let dep = traite_fichier_modules fullname ".mllib" in
        let efullname = escape fullname in
-       printf "%s_MLLIB_DEPENDENCIES:=%s\n" efullname dep;
+       printf "%s_MLLIB_DEPENDENCIES:=%s\n" efullname (String.concat " " dep);
        printf "%s.cma:$(addsuffix .cmo,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname;
        printf "%s.cmxa:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname;
        flush stdout)
@@ -453,9 +476,13 @@ let mL_dependencies () =
        let fullname = file_name name dirname in
        let dep = traite_fichier_modules fullname ".mlpack" in
        let efullname = escape fullname in
-       printf "%s_MLPACK_DEPENDENCIES:=%s\n" efullname dep;
+       printf "%s_MLPACK_DEPENDENCIES:=%s\n" efullname (String.concat " " dep);
        printf "%s.cmo:$(addsuffix .cmo,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname;
        printf "%s.cmx:$(addsuffix .cmx,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname;
+       let efullname_capital = capitalize (Filename.basename efullname) in
+       List.iter (fun dep ->
+         printf "%s.cmx : FOR_PACK=-for-pack %s\n" dep efullname_capital)
+         dep;
        flush stdout)
     (List.rev !mlpackAccu)
 
@@ -544,13 +571,6 @@ let add_rec_dir_no_import add_file phys_dir log_dir =
 let add_rec_dir_import add_file phys_dir log_dir =
   add_directory true (add_file true) phys_dir log_dir
 
-(** -R semantic but only on immediate capitalized subdirs *)
-
-let add_rec_uppercase_subdirs add_file phys_dir log_dir =
-  process_subdirectories (fun phys_dir f ->
-    add_directory true (add_file true) phys_dir (log_dir@[String.capitalize f]))
-    phys_dir
-
 (** -I semantic: do not go in subdirs. *)
 let add_caml_dir phys_dir =
   add_directory false add_caml_known phys_dir []
-- 
cgit v1.2.3