coqc and coqmktop migrated in tools/, get rid of scripts/ subdir

 No need to place these binaries apart, and anyway they aren't
 (shell) scripts since ages.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16432 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 503 insertions, 0 deletions

diff --git a/tools/coqc.ml b/tools/coqc.ml
new file mode 100644
index 0000000000..e15a1768c2
--- /dev/null
+++ b/tools/coqc.ml
@@ -0,0 +1,193 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Coq compiler : coqc *)
+
+(** For improving portability, coqc is now an OCaml program instead
+    of a shell script. We use as much as possible the Sys and Filename
+    module for better portability, but the Unix module is still used
+    here and there (with explicitly qualified function names Unix.foo).
+
+    We process here the commmand line to extract names of files to compile,
+    then we compile them one by one while passing by the rest of the command
+    line to a process running "coqtop -batch -compile <file>".
+*)
+
+(* Environment *)
+
+let environment = Unix.environment ()
+
+let binary = ref "coqtop"
+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 ->
+      let file_noext =
+        if Filename.check_suffix file ".v" then
+          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)
+
+(* compilation of files [files] with command [command] and args [args] *)
+
+let compile command args files =
+  let args' = command :: args @ (make_compilation_args files) in
+  match Sys.os_type with
+  | "Win32" ->
+     let pid =
+        Unix.create_process_env command (Array.of_list args') environment
+        Unix.stdin Unix.stdout Unix.stderr
+     in
+     let status = snd (Unix.waitpid [] pid) in
+     let errcode =
+       match status with Unix.WEXITED c|Unix.WSTOPPED c|Unix.WSIGNALED c -> c
+     in
+     exit errcode
+  | _ ->
+     Unix.execvpe command (Array.of_list args') environment
+
+let usage () =
+  Usage.print_usage_coqc () ;
+  flush stderr ;
+  exit 1
+
+(* parsing of the command line *)
+
+let parse_args () =
+  let rec parse (cfiles,args) = function
+    | [] ->
+	List.rev cfiles, List.rev args
+    | ("-verbose" | "--verbose") :: rem ->
+	verbose := true ; parse (cfiles,args) rem
+    | "-image" :: f :: rem -> image := f; parse (cfiles,args) rem
+    | "-image" :: [] ->	usage ()
+    | "-byte" :: rem -> binary := "coqtop.byte"; parse (cfiles,args) rem
+    | "-opt" :: rem -> (* now a no-op *) parse (cfiles,args) rem
+
+(* Obsolete options *)
+
+    | "-libdir" :: _ :: rem ->
+        print_string "Warning: option -libdir deprecated and ignored\n";
+        flush stdout;
+        parse (cfiles,args) rem
+    | ("-db"|"-debugger") :: rem ->
+        print_string "Warning: option -db/-debugger deprecated and ignored\n";
+        flush stdout;
+        parse (cfiles,args) rem
+
+(* Informative options *)
+
+    | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
+
+    | ("-v"|"--version") :: _ -> Usage.version 0
+
+    | ("-where") :: _ ->
+	print_endline (Envars.coqlib (fun x -> x)); exit 0
+
+    | ("-config" | "--config") :: _ -> Usage.print_config (); exit 0
+
+(* Options for coqtop : a) options with 0 argument *)
+
+    | ("-notactics"|"-debug"|"-nolib"|"-boot"|"-time"
+      |"-batch"|"-noinit"|"-nois"|"-noglob"|"-no-glob"
+      |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet"
+      |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-beautify"|"-strict-implicit"
+      |"-dont-load-proofs"|"-load-proofs"|"-force-load-proofs"
+      |"-impredicative-set"|"-vm"|"-no-native-compiler"
+      |"-verbose-compat-notations"|"-no-compat-notations" as o) :: rem ->
+	parse (cfiles,o::args) rem
+
+(* Options for coqtop : a) options with 1 argument *)
+
+    | ("-outputstate"|"-inputstate"|"-is"|"-exclude-dir"
+      |"-load-vernac-source"|"-l"|"-load-vernac-object"
+      |"-load-ml-source"|"-require"|"-load-ml-object"
+      |"-init-file"|"-dump-glob"|"-compat"|"-coqlib" as o) :: rem ->
+	begin
+	  match rem with
+	    | s :: rem' -> parse (cfiles,s::o::args) rem'
+	    | []        -> usage ()
+	end
+
+(* Options for coqtop : a) options with 1 argument and possibly more *)
+
+    | ("-I"|"-include" as o) :: rem ->
+	begin
+	  match rem with
+	  | s :: "-as" :: t :: rem' -> parse (cfiles,t::"-as"::s::o::args) rem'
+	  | s :: "-as" :: [] -> usage ()
+	  | s :: rem' -> parse (cfiles,s::o::args) rem'
+	  | []        -> usage ()
+	end
+    | "-R" :: s :: "-as" :: t :: rem ->	parse (cfiles,t::"-as"::s::"-R"::args) rem
+    | "-R" :: s :: "-as" :: [] -> usage ()
+    | "-R" :: s :: t :: rem -> parse (cfiles,t::s::"-R"::args) rem
+
+(* Anything else is interpreted as a file *)
+
+    | f :: rem ->
+	if Sys.file_exists f then
+	  parse (f::cfiles,args) rem
+	else
+	  let fv = f ^ ".v" in
+	  if Sys.file_exists fv then
+	    parse (fv::cfiles,args) rem
+	  else begin
+	    prerr_endline ("coqc: "^f^": no such file or directory") ;
+	    exit 1
+	  end
+  in
+  parse ([],[]) (List.tl (Array.to_list Sys.argv))
+
+(* main: we parse the command line, define the command to compile files
+ * and then call the compilation on each file *)
+
+let main () =
+  let cfiles, args = parse_args () in
+    if cfiles = [] then begin
+      prerr_endline "coqc: too few arguments" ;
+      usage ()
+    end;
+    let coqtopname =
+      if !image <> "" then !image
+      else Filename.concat Envars.coqbin (!binary ^ Coq_config.exec_extension)
+    in
+      (*  List.iter (compile coqtopname args) cfiles*)
+      Unix.handle_unix_error (compile coqtopname args) cfiles
+
+let _ = Printexc.print main ()
diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml
new file mode 100644
index 0000000000..81f0686e02
--- /dev/null
+++ b/tools/coqmktop.ml
@@ -0,0 +1,310 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* coqmktop is a script to link Coq, analogous to ocamlmktop.
+   The command line contains options specific to coqmktop, options for the
+   Ocaml linker and files to link (in addition to the default Coq files). *)
+
+open Unix
+
+(* In Win32 outside cygwin, Sys.command calls cmd.exe. When it executes
+   a command that may contains many double-quote, we should double-quote
+   the whole ! *)
+
+let safe_sys_command =
+  if Sys.os_type = "Win32" then
+    fun cmd -> Sys.command ("\""^cmd^"\"")
+  else Sys.command
+
+(* Objects to link *)
+
+(* NB: dynlink is now always linked, it is used for loading plugins
+   and compiled vm code (see native-compiler). We now reject platforms
+   with ocamlopt but no dynlink.cmxa during ./configure, and give
+   instructions there about how to build a dummy dynlink.cmxa,
+   cf. dev/dynlink.ml. *)
+
+(* 1. Core objects *)
+let ocamlobjs = ["str.cma";"unix.cma";"nums.cma";"dynlink.cma"]
+let camlp4objs =
+  if Coq_config.camlp4 = "camlp5" then ["gramlib.cma"] else ["camlp4lib.cma"]
+let libobjs = ocamlobjs @ camlp4objs
+
+let spaces = Str.regexp "[ \t\n]+"
+let split_list l = Str.split spaces l
+
+let copts     = split_list Tolink.copts
+let core_objs = split_list Tolink.core_objs
+let core_libs = split_list Tolink.core_libs
+
+(* 3. Toplevel objects *)
+let camlp4topobjs =
+  if Coq_config.camlp4 = "camlp5" then
+    ["camlp5_top.cma"; "pa_o.cmo"; "pa_extend.cmo"]
+  else
+    [ "Camlp4Top.cmo";
+      "Camlp4Parsers/Camlp4OCamlRevisedParser.cmo";
+      "Camlp4Parsers/Camlp4OCamlParser.cmo";
+      "Camlp4Parsers/Camlp4GrammarParser.cmo" ]
+let topobjs = camlp4topobjs
+
+let gramobjs = []
+let notopobjs = gramobjs
+
+(* 4. High-level tactics objects *)
+
+(* environment *)
+let opt        = ref false
+let full       = ref false
+let top        = ref false
+let echo       = ref false
+let no_start   = ref false
+
+let is_ocaml4 = Coq_config.caml_version.[0] <> '3'
+
+(* Since the .cma are given with their relative paths (e.g. "lib/clib.cma"),
+   we only need to include directories mentionned in the temp main ml file
+   below (for accessing the corresponding .cmi). *)
+
+let src_dirs =
+  [ []; ["lib"]; ["toplevel"]; ["kernel";"byterun"]  ]
+
+let includes () =
+  let coqlib = if !Flags.boot then "." else Envars.coqlib ~fail:Errors.error in
+  let mkdir d = "\"" ^ List.fold_left Filename.concat coqlib d ^ "\"" in
+  (List.fold_right (fun d l -> "-I" :: mkdir d :: l) src_dirs [])
+  @ ["-I"; "\"" ^ Envars.camlp4lib () ^ "\""]
+  @ (if is_ocaml4 then ["-I"; "+compiler-libs"] else [])
+
+(* Transform bytecode object file names in native object file names *)
+let native_suffix f =
+  if Filename.check_suffix f ".cmo" then
+    (Filename.chop_suffix f ".cmo") ^ ".cmx"
+  else if Filename.check_suffix f ".cma" then
+    (Filename.chop_suffix f ".cma") ^ ".cmxa"
+  else
+    if Filename.check_suffix f ".a" then f
+    else
+      failwith ("File "^f^" has not extension .cmo, .cma or .a")
+
+(* Transforms a file name in the corresponding Caml module name. *)
+let rem_ext_regexpr = Str.regexp "\\(.*\\)\\.\\(cm..?\\|ml\\)"
+
+let module_of_file name =
+  let s = Str.replace_first rem_ext_regexpr "\\1" (Filename.basename name) in
+  String.capitalize s
+
+(* Build the list of files to link and the list of modules names *)
+let files_to_link userfiles =
+  let toplevel_objs =
+    if !top then topobjs else if !opt then notopobjs else [] in
+  let objs = libobjs @ core_objs @ toplevel_objs in
+  let modules = List.map module_of_file (objs @ userfiles)
+  in
+  let libs = libobjs @ core_libs @ toplevel_objs in
+  let libstolink =
+    (if !opt then List.map native_suffix libs else libs) @ userfiles
+  in
+  (modules, libstolink)
+
+(* Gives the list of all the directories under [dir].
+   Uses [Unix] (it is hard to do without it). *)
+let all_subdirs dir =
+  let l = ref [dir] in
+  let add f = l := f :: !l in
+  let rec traverse dir =
+    let dirh =
+      try opendir dir with Unix_error _ -> invalid_arg "all_subdirs"
+    in
+    try
+      while true do
+	let f = readdir dirh in
+	if f <> "." && f <> ".." then
+	  let file = Filename.concat dir f in
+	  if (stat file).st_kind = S_DIR then begin
+	    add file;
+	    traverse file
+	  end
+      done
+    with End_of_file ->
+      closedir dirh
+  in
+  traverse dir; List.rev !l
+
+(* usage *)
+let usage () =
+  prerr_endline "Usage: coqmktop <options> <ocaml options> files\
+\nFlags are:\
+\n  -coqlib dir    Specify where the Coq object files are\
+\n  -camlbin dir   Specify where the OCaml binaries are\
+\n  -camlp4bin dir Specify where the Camlp4/5 binaries are\
+\n  -o exec-file   Specify the name of the resulting toplevel\
+\n  -boot          Run in boot mode\
+\n  -echo          Print calls to external commands\
+\n  -full          Link high level tactics\
+\n  -opt           Compile in native code\
+\n  -top           Build Coq on a OCaml toplevel (incompatible with -opt)\
+\n  -R dir         Add recursively dir to OCaml search path\
+\n";
+  exit 1
+
+(* parsing of the command line *)
+let parse_args () =
+  let rec parse (op,fl) = function
+    | [] -> List.rev op, List.rev fl
+    | "-coqlib" :: d :: rem ->
+	Flags.coqlib_spec := true; Flags.coqlib := d ; parse (op,fl) rem
+    | "-coqlib" :: _        -> usage ()
+    | "-camlbin" :: d :: rem ->
+	Flags.camlbin_spec := true; Flags.camlbin := d ; parse (op,fl) rem
+    | "-camlbin" :: _        -> usage ()
+    | "-camlp4bin" :: d :: rem ->
+	Flags.camlp4bin_spec := true; Flags.camlp4bin := d ; parse (op,fl) rem
+    | "-camlp4bin" :: _        -> usage ()
+    | "-boot" :: rem -> Flags.boot := true; parse (op,fl) rem
+    | "-opt" :: rem -> opt := true ; parse (op,fl) rem
+    | "-full" :: rem -> full := true ; parse (op,fl) rem
+    | "-top" :: rem -> top := true ; parse (op,fl) rem
+    | "-v8" :: rem ->
+	Printf.eprintf "warning: option -v8 deprecated";
+	parse (op,fl) rem
+    | "-echo" :: rem -> echo := true ; parse (op,fl) rem
+    | ("-cclib"|"-ccopt"|"-I"|"-o"|"-w" as o) :: rem' ->
+	begin
+	  match rem' with
+	    | a :: rem -> parse (a::o::op,fl) rem
+	    | []       -> usage ()
+	end
+    | "-R" :: a :: rem ->
+        parse ((List.rev(List.flatten (List.map (fun d -> ["-I";d])
+					 (all_subdirs a))))@op,fl) rem
+    | "-R" :: [] -> usage ()
+    | ("-noassert"|"-compact"|"-g"|"-p"|"-thread"|"-dtypes" as o) :: rem ->
+        parse (o::op,fl) rem
+    | ("-h"|"--help") :: _ -> usage ()
+    | ("-no-start") :: rem -> no_start:=true; parse (op, fl) rem
+    | f :: rem ->
+	if Filename.check_suffix f ".ml"
+	  or Filename.check_suffix f ".cmx"
+	  or Filename.check_suffix f ".cmo"
+	  or Filename.check_suffix f ".cmxa"
+	  or Filename.check_suffix f ".cma"
+	  or Filename.check_suffix f ".c" then
+	    parse (op,f::fl) rem
+	else begin
+	  prerr_endline ("Don't know what to do with " ^ f);
+	  exit 1
+	end
+  in
+  parse ([Coq_config.osdeplibs],[]) (List.tl (Array.to_list Sys.argv))
+
+let clean file =
+  let rm f = if Sys.file_exists f then Sys.remove f in
+  let basename = Filename.chop_suffix file ".ml" in
+  if not !echo then begin
+    rm file;
+    rm (basename ^ ".o");
+    rm (basename ^ ".cmi");
+    rm (basename ^ ".cmo");
+    rm (basename ^ ".cmx")
+  end
+
+(* Initializes the kind of loading in the main program *)
+let declare_loading_string () =
+  if not !top then
+    "Mltop.remove ();;"
+  else
+    "begin try\
+\n       (* Enable rectypes in the toplevel if it has the directive #rectypes *)\
+\n       begin match Hashtbl.find Toploop.directive_table \"rectypes\" with\
+\n         | Toploop.Directive_none f -> f ()\
+\n         | _ -> ()\
+\n       end\
+\n     with\
+\n       | Not_found -> ()\
+\n     end;;\
+\n\
+\n     let ppf = Format.std_formatter;;\
+\n     Mltop.set_top\
+\n       {Mltop.load_obj=\
+\n         (fun f -> if not (Topdirs.load_file ppf f) then Errors.error (\"Could not load plugin \"^f));\
+\n        Mltop.use_file=Topdirs.dir_use ppf;\
+\n        Mltop.add_dir=Topdirs.dir_directory;\
+\n        Mltop.ml_loop=(fun () -> Toploop.loop ppf) };;\
+\n"
+
+(* create a temporary main file to link *)
+let create_tmp_main_file modules =
+  let main_name,oc = Filename.open_temp_file "coqmain" ".ml" in
+  try
+    (* Add the pre-linked modules *)
+    output_string oc "List.iter Mltop.add_known_module [\"";
+    output_string oc (String.concat "\";\"" modules);
+    output_string oc "\"];;\n";
+    (* Initializes the kind of loading *)
+    output_string oc (declare_loading_string());
+    (* Start the toplevel loop *)
+    if not !no_start then
+    output_string oc "Coqtop.start();;\n";
+    close_out oc;
+    main_name
+  with reraise ->
+    clean main_name; raise reraise
+
+(* main part *)
+let main () =
+  let (options, userfiles) = parse_args () in
+  (* which ocaml command to invoke *)
+  let camlbin = Envars.camlbin () in
+  let prog =
+    if !opt then begin
+      (* native code *)
+      if !top then failwith "no custom toplevel in native code !";
+      let ocamloptexec = Filename.quote (Filename.concat camlbin "ocamlopt") in
+        ocamloptexec^" -linkall"
+    end else
+      (* bytecode (we shunt ocamlmktop script which fails on win32) *)
+      let ocamlmktoplib = if is_ocaml4
+	then " ocamlcommon.cma ocamlbytecomp.cma ocamltoplevel.cma"
+	else " toplevellib.cma" in
+      let ocamlcexec = Filename.quote (Filename.concat camlbin "ocamlc") in
+      let ocamlccustom = Printf.sprintf "%s %s -linkall "
+        ocamlcexec Coq_config.coqrunbyteflags in
+      (if !top then ocamlccustom^ocamlmktoplib else ocamlccustom)
+  in
+  (* files to link *)
+  let (modules, tolink) = files_to_link userfiles in
+  (* the list of the loaded modules *)
+  let main_file = create_tmp_main_file modules in
+  try
+    let args =
+      options @ (includes ()) @ copts @ tolink @ [ Filename.quote main_file ]
+    in
+    (* add topstart.cmo explicitly because we shunted ocamlmktop wrapper *)
+    let args = if !top then args @ [ "topstart.cmo" ] else args in
+      (* Now, with the .cma, we MUST use the -linkall option *)
+    let command = String.concat " " (prog::"-rectypes"::args) in
+      if !echo then
+	begin
+	  print_endline command;
+	  print_endline
+	    ("(command length is " ^
+	       (string_of_int (String.length command)) ^ " characters)");
+	  flush Pervasives.stdout
+	end;
+      let retcode = safe_sys_command command in
+	clean main_file;
+	(* command gives the exit code in HSB, and signal in LSB !!! *)
+	if retcode > 255 then retcode lsr 8 else retcode
+  with reraise ->
+    clean main_file; raise reraise
+
+let retcode =
+  try Printexc.print main () with any -> 1
+
+let _ = exit retcode