Checking that a library name is valid before compilation.

Fixes bug #3333.

2 files changed, 22 insertions, 26 deletions

diff --git a/library/library.ml b/library/library.ml
index fc74d25b45..4f023ce6df 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -663,6 +663,25 @@ let check_coq_overwriting p id =
       (strbrk ("Cannot build module "^DirPath.to_string p^"."^Id.to_string id^
       ": 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 f =
   let paths = Loadpath.get_paths () in
   let _, longf =
@@ -673,7 +692,9 @@ let start_library f =
       Loadpath.logical lp
     with Not_found -> Nameops.default_root_prefix
   in
-  let id = Id.of_string (Filename.basename f) in
+  let file = Filename.basename f 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
   OpaqueTables.reset ();
diff --git a/tools/coqc.ml b/tools/coqc.ml
index 0a9ea4e89f..90585c763b 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -23,30 +23,6 @@ let image = ref ""
 
 let verbose = ref false
 
-(* Verifies that a string starts by a letter and do not contain
-   others caracters than letters, digits, or `_` *)
-
-let check_module_name s =
-  let err c =
-    output_string stderr "Invalid module name: ";
-    output_string stderr s;
-    output_string stderr " character ";
-    if c = '\'' then
-      output_string stderr "\"'\""
-    else
-      (output_string stderr"'"; output_char stderr c; output_string stderr"'");
-    output_string stderr " is not allowed in module names\n";
-    exit 1
-  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 rec make_compilation_args = function
   | [] -> []
   | file :: fl ->
@@ -55,7 +31,6 @@ let rec make_compilation_args = function
           Filename.chop_suffix file ".v"
         else file
       in
-      check_module_name (Filename.basename file_noext);
       (if !verbose then "-compile-verbose" else "-compile")
       :: file_noext :: (make_compilation_args fl)