Imported Upstream version 8.8.2upstream/8.8.2

1 files changed, 45 insertions, 66 deletions

diff --git a/library/library.ml b/library/library.ml
index d44f796a..56d2709d 100644
--- a/library/library.ml
+++ b/library/library.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 Pp
@@ -12,9 +14,8 @@ open Util
 
 open Names
 open Libnames
-open Nameops
-open Libobject
 open Lib
+open Libobject
 
 (************************************************************************)
 (*s Low-level interning/externing of libraries to files *)
@@ -97,7 +98,7 @@ type library_t = {
   library_deps : (compilation_unit_name * Safe_typing.vodigest) array;
   library_imports : compilation_unit_name array;
   library_digests : Safe_typing.vodigest;
-  library_extra_univs : Univ.universe_context_set;
+  library_extra_univs : Univ.ContextSet.t;
 }
 
 type library_summary = {
@@ -131,8 +132,8 @@ let find_library dir =
 let try_find_library dir =
   try find_library dir
   with Not_found ->
-    errorlabstrm "Library.find_library"
-      (str "Unknown library " ++ pr_dirpath dir)
+    user_err ~hdr:"Library.find_library"
+      (str "Unknown library " ++ DirPath.print dir)
 
 let register_library_filename dir f =
   (* Not synchronized: overwrite the previous binding if one existed *)
@@ -171,7 +172,7 @@ let register_loaded_library m =
     let prefix = Nativecode.mod_uid_of_dirpath libname ^ "." in
     let f = prefix ^ "cmo" in
     let f = Dynlink.adapt_filename f in
-    if not Coq_config.no_native_compiler then
+    if Coq_config.native_compiler then
       Nativelib.link_library ~prefix ~dirname ~basename:f
   in
   let rec aux = function
@@ -329,12 +330,12 @@ let locate_qualified_library ?root ?(warn = true) qid =
 
 let error_unmapped_dir qid =
   let prefix, _ = repr_qualid qid in
-  errorlabstrm "load_absolute_library_from"
+  user_err ~hdr:"load_absolute_library_from"
     (str "Cannot load " ++ pr_qualid qid ++ str ":" ++ spc () ++
-     str "no physical path bound to" ++ spc () ++ pr_dirpath prefix ++ fnl ())
+     str "no physical path bound to" ++ spc () ++ DirPath.print prefix ++ fnl ())
 
 let error_lib_not_found qid =
-  errorlabstrm "load_absolute_library_from"
+  user_err ~hdr:"load_absolute_library_from"
     (str"Cannot find library " ++ pr_qualid qid ++ str" in loadpath")
 
 let try_locate_absolute_library dir =
@@ -360,9 +361,9 @@ type 'a table_status =
   | Fetched of 'a Future.computation array
 
 let opaque_tables =
-  ref (LibraryMap.empty : (Term.constr table_status) LibraryMap.t)
+  ref (LibraryMap.empty : (Constr.constr table_status) LibraryMap.t)
 let univ_tables =
-  ref (LibraryMap.empty : (Univ.universe_context_set table_status) LibraryMap.t)
+  ref (LibraryMap.empty : (Univ.ContextSet.t table_status) LibraryMap.t)
 
 let add_opaque_table dp st =
   opaque_tables := LibraryMap.add dp st !opaque_tables
@@ -378,7 +379,7 @@ let access_table what tables dp i =
       let t =
         try fetch_delayed f
         with Faulty f ->
-          errorlabstrm "Library.access_table"
+          user_err ~hdr:"Library.access_table"
             (str "The file " ++ str f ++ str " (bound to " ++ str dir_path ++
              str ") is inaccessible or corrupted,\ncannot load some " ++
              str what ++ str " in it.\n")
@@ -408,9 +409,9 @@ let () =
 type seg_sum = summary_disk
 type seg_lib = library_disk
 type seg_univ = (* true = vivo, false = vi *)
-  Univ.universe_context_set Future.computation array * Univ.universe_context_set * bool
+  Univ.ContextSet.t Future.computation array * Univ.ContextSet.t * bool
 type seg_discharge = Opaqueproof.cooking_info list array
-type seg_proofs = Term.constr Future.computation array
+type seg_proofs = Constr.constr Future.computation array
 
 let mk_library sd md digests univs =
   {
@@ -463,10 +464,10 @@ let rec intern_library (needed, contents) (dir, f) from =
   let f = match f with Some f -> f | None -> try_locate_absolute_library dir in
   let m = intern_from_file f in
   if not (DirPath.equal dir m.library_name) then
-    errorlabstrm "load_physical_library"
+    user_err ~hdr:"load_physical_library"
       (str "The file " ++ str f ++ str " contains library" ++ spc () ++
-       pr_dirpath m.library_name ++ spc () ++ str "and not library" ++
-       spc() ++ pr_dirpath dir);
+       DirPath.print m.library_name ++ spc () ++ str "and not library" ++
+       spc() ++ DirPath.print dir);
   Feedback.feedback (Feedback.FileLoaded(DirPath.to_string dir, f));
   m.library_digests, intern_library_deps (needed, contents) dir m f
 
@@ -477,9 +478,9 @@ and intern_library_deps libs dir m from =
 and intern_mandatory_library caller from libs (dir,d) =
   let digest, libs = intern_library libs (dir, None) (Some from) in
   if not (Safe_typing.digest_match ~actual:digest ~required:d) then
-    errorlabstrm "" (str "Compiled library " ++ pr_dirpath caller ++
+    user_err (str "Compiled library " ++ DirPath.print caller ++
     str " (in file " ++ str from ++ str ") makes inconsistent assumptions \
-    over library " ++ pr_dirpath dir);
+    over library " ++ DirPath.print dir);
   libs
 
 let rec_intern_library libs (dir, f) =
@@ -551,8 +552,6 @@ let in_require : require_obj -> obj =
 (* Require libraries, import them if [export <> None], mark them for export
    if [export = Some true] *)
 
-let (f_xml_require, xml_require) = Hook.make ~default:ignore ()
-
 let warn_require_in_module =
   CWarnings.create ~name:"require-in-module" ~category:"deprecated"
                    (fun () -> strbrk "Require inside a module is" ++
@@ -574,16 +573,15 @@ let require_library_from_dirpath modrefl export =
       end
     else
       add_anonymous_leaf (in_require (needed,modrefl,export));
-    if !Flags.xml_export then List.iter (Hook.get f_xml_require) modrefl;
-  add_frozen_state ()
+  ()
 
 (* the function called by Vernacentries.vernac_import *)
 
-let safe_locate_module (loc,qid) =
+let safe_locate_module {CAst.loc;v=qid} =
   try Nametab.locate_module qid
   with Not_found ->
-    user_err_loc
-      (loc,"import_library", pr_qualid qid ++ str " is not a module")
+    user_err ?loc ~hdr:"import_library"
+      (pr_qualid qid ++ str " is not a module")
 
 let import_module export modl =
   (* Optimization: libraries in a raw in the list are imported
@@ -597,7 +595,7 @@ let import_module export modl =
     | [] -> ()
     | modl -> add_anonymous_leaf (in_import_library (List.rev modl, export)) in
   let rec aux acc = function
-    | (loc,dir as m) :: l ->
+    | ({CAst.loc; v=dir} as m) :: l ->
         let m,acc =
           try Nametab.locate_module dir, acc
           with Not_found-> flush acc; safe_locate_module m, [] in
@@ -607,8 +605,8 @@ let import_module export modl =
             flush acc;
             try Declaremods.import_module export mp; aux [] l
             with Not_found ->
-              user_err_loc (loc,"import_library",
-                pr_qualid dir ++ str " is not a module"))
+              user_err ?loc ~hdr:"import_library"
+                (pr_qualid dir ++ str " is not a module"))
     | [] -> flush acc
   in aux [] modl
 
@@ -619,39 +617,19 @@ let check_coq_overwriting p id =
   let l = DirPath.repr p in
   let is_empty = match l with [] -> true | _ -> false in
   if not !Flags.boot && not is_empty && Id.equal (List.last l) coq_root then
-    errorlabstrm ""
-      (str "Cannot build module " ++ pr_dirpath p ++ str "." ++ pr_id id ++ str "." ++ spc () ++
+    user_err 
+      (str "Cannot build module " ++ DirPath.print p ++ str "." ++ Id.print id ++ str "." ++ spc () ++
       str "it starts with prefix \"Coq\" which is reserved for the Coq library.")
 
-(* Verifies that a string starts by a letter and do not contain
-   others caracters than letters, digits, or `_` *)
-
-let check_module_name s =
-  let msg c =
-    strbrk "Invalid module name: " ++ str s ++ strbrk " character " ++
-    (if c = '\'' then str "\"'\"" else (str "'" ++ str (String.make 1 c) ++ str "'")) ++
-    strbrk " is not allowed in module names\n"
-  in
-  let err c = errorlabstrm "" (msg c) in
-  match String.get s 0 with
-    | 'a' .. 'z' | 'A' .. 'Z' ->
-        for i = 1 to (String.length s)-1 do
-          match String.get s i with
-            | 'a' .. 'z' | 'A' .. 'Z' | '0' .. '9' | '_'  -> ()
-            | c -> err c
-        done
-    | c -> err c
-
 let start_library fo =
   let ldir0 =
     try
       let lp = Loadpath.find_load_path (Filename.dirname fo) in
       Loadpath.logical lp
-    with Not_found -> Nameops.default_root_prefix
+    with Not_found -> Libnames.default_root_prefix
   in
   let file = Filename.chop_extension (Filename.basename fo) in
   let id = Id.of_string file in
-  check_module_name file;
   check_coq_overwriting ldir0 id;
   let ldir = add_dirpath_suffix ldir0 id in
   Declaremods.start_library ldir;
@@ -668,10 +646,10 @@ let load_library_todo f =
   let tasks, _, _ = System.marshal_in_segment f ch in
   let (s5 : seg_proofs), _, _ = System.marshal_in_segment f ch in
   close_in ch;
-  if tasks = None then errorlabstrm "restart" (str"not a .vio file");
-  if s2 = None then errorlabstrm "restart" (str"not a .vio file");
-  if s3 = None then errorlabstrm "restart" (str"not a .vio file");
-  if pi3 (Option.get s2) then errorlabstrm "restart" (str"not a .vio file");
+  if tasks = None then user_err ~hdr:"restart" (str"not a .vio file");
+  if s2 = None then user_err ~hdr:"restart" (str"not a .vio file");
+  if s3 = None then user_err ~hdr:"restart" (str"not a .vio file");
+  if pi3 (Option.get s2) then user_err ~hdr:"restart" (str"not a .vio file");
   longf, s0, s1, Option.get s2, Option.get s3, Option.get tasks, s5
 
 (************************************************************************)
@@ -687,8 +665,8 @@ let current_deps () =
 let current_reexports () = !libraries_exports_list
 
 let error_recursively_dependent_library dir =
-  errorlabstrm ""
-    (strbrk "Unable to use logical name " ++ pr_dirpath dir ++
+  user_err 
+    (strbrk "Unable to use logical name " ++ DirPath.print dir ++
      strbrk " to save current library because" ++
      strbrk " it already depends on a library of this name.")
 
@@ -706,7 +684,8 @@ let error_recursively_dependent_library dir =
 let save_library_to ?todo dir f otab =
   let except = match todo with
     | None ->
-        assert(!Flags.compilation_mode = Flags.BuildVo);
+        (* XXX *)
+        (* assert(!Flags.compilation_mode = Flags.BuildVo); *)
         assert(Filename.check_suffix f ".vo");
         Future.UUIDSet.empty
     | Some (l,_) ->
@@ -734,7 +713,7 @@ let save_library_to ?todo dir f otab =
       except Int.Set.empty in
   let is_done_or_todo i x = Future.is_val x || Int.Set.mem i except in
   Array.iteri (fun i x ->
-    if not(is_done_or_todo i x) then CErrors.errorlabstrm "library"
+    if not(is_done_or_todo i x) then CErrors.user_err ~hdr:"library"
       Pp.(str"Proof object "++int i++str" is not checked nor to be checked"))
     opaque_table;
   let sd = {
@@ -761,10 +740,10 @@ let save_library_to ?todo dir f otab =
     System.marshal_out_segment f' ch (opaque_table : seg_proofs);
     close_out ch;
     (* Writing native code files *)
-    if !Flags.native_compiler then
+    if !Flags.output_native_objects then
       let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in
       if not (Nativelib.compile_library dir ast fn) then
-	error "Could not compile the library to native code."
+	user_err Pp.(str "Could not compile the library to native code.")
    with reraise ->
     let reraise = CErrors.push reraise in
     let () = Feedback.msg_warning (str "Removed file " ++ str f') in