coqmktop

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

2 files changed, 323 insertions, 0 deletions

diff --git a/scripts/.cvsignore b/scripts/.cvsignore
new file mode 100644
index 0000000000..52ba6cec1c
--- /dev/null
+++ b/scripts/.cvsignore
@@ -0,0 +1,2 @@
+coqmktop
+tolink.ml
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
new file mode 100644
index 0000000000..6a244b9887
--- /dev/null
+++ b/scripts/coqmktop.ml
@@ -0,0 +1,321 @@
+
+(* $Id$ *)
+
+(* Ici, on trie la ligne de commande pour en extraire les options spécifiques
+   à coqmktop, puis on appelle "ocamlc" (ou "ocamlopt")
+   avec les autres options et la liste des fichiers à linker.
+
+   On essaye au maximum d'utiliser les modules Sys et Filename pour que la
+   portabilité soit maximale. *)
+
+open Unix
+
+(* Objects to link *)
+
+(* 1. Core objects *)
+let ocamlobjs = ["unix.cma"]
+let dynobjs = ["dynlink.cma"]
+let camlp4objs = ["gramlib.cma"]
+let configobjs = ["coq_config.cmo"]
+let launchobjs = ["usage.cmo"]
+let libobjs = ocamlobjs @ camlp4objs @ configobjs @ launchobjs
+
+let spaces = Str.regexp "[ \t\n]+"
+let split_cmo l = Str.split spaces l
+
+let lib = split_cmo Tolink.lib
+let kernel = split_cmo Tolink.kernel
+let library = split_cmo Tolink.library
+let pretyping = split_cmo Tolink.pretyping
+let parsing = split_cmo Tolink.parsing
+let proofs = split_cmo Tolink.proofs
+let tactics = split_cmo Tolink.tactics
+let toplevel = split_cmo Tolink.toplevel
+
+let core_objs = 
+  libobjs @ lib @ kernel @ library @ pretyping @ parsing @ 
+  proofs @ tactics
+
+(* 3. Files only in coqsearchisos (if option -searchisos is used) *)
+let coqsearch = ["version_searchisos.cmo"; "cmd_searchisos_line.cmo"]
+
+(* 4. Toplevel objects *)
+let camlp4objs =
+  ["camlp4_top.cma"; "pa_o.cmo"; "pa_op.cmo"; "pa_extend.cmo";
+   "q_coqast.cmo" ]
+let topobjs = camlp4objs
+
+let gramobjs = ["g_zsyntax.cmo"; "g_natsyntax.cmo"]
+let notopobjs = gramobjs
+
+(* 5. High-level tactics objects *)
+let cmotacsobjs = [
+  "prolog.cmo"; "equality.cmo"; "inv.cmo"; "leminv.cmo"; 
+  "point.cmo"; "progmach.cmo"; "program.cmo"; "propre.cmo";
+  "tauto.cmo"; "gelim.cmo"; "eqdecide.cmo"]
+
+(* environment *)
+let src_coqtop = ref Coq_config.coqtop
+let notactics  = ref false
+let opt        = ref false
+let top        = ref false
+let searchisos = ref false
+let echo       = ref false
+
+let includes () = 
+  List.fold_right
+    (fun d l -> "-I" :: List.fold_left Filename.concat !src_coqtop d :: l)
+    [ [ "config" ] ;
+      [ "scripts" ] ;
+      [ "lib" ] ;
+      [ "kernel" ] ;
+      [ "library" ] ;
+      [ "pretyping" ] ;
+      [ "parsing" ] ;
+      [ "proofs" ] ;
+      [ "tactics" ] ;
+      [ "toplevel" ]
+    ]
+    ["-I"; Coq_config.camlp4lib]
+
+(* 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 
+    failwith ("File "^f^" has not extension .cmo or .cma")
+
+(* 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 dyn_objs = if not !opt then dynobjs else [] in
+  let command_objs = if !searchisos then coqsearch else [] in
+  let tactic_objs = if !notactics then [] else cmotacsobjs in
+  let toplevel_objs = if !top then topobjs else if !opt then notopobjs else []
+  in
+  let objs = core_objs @ dyn_objs @ toplevel @ command_objs @ tactic_objs @
+    toplevel_objs in
+  let tolink =
+    if !opt then 
+      (List.map native_suffix objs) @ userfiles
+    else 
+      objs @ userfiles 
+  in
+  let modules = List.map module_of_file tolink in
+  (modules, tolink)
+
+(*Gives the list of all the directories under dir*)
+(*Uses Unix, sorry... But you can try to do the same thing without it.*)
+let all_subdirs dir =
+  let l = ref [] in
+  let add f = l := f :: !l in
+  let rec traverse dir =
+    Printf.printf "%s\n" 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
+Options are:
+  -srcdir dir   Specify where the Coq source files are
+  -notactics    Do not link high level tactics
+  -o exec-file  Specify the name of the resulting toplevel
+  -opt          Compile in native code
+  -top          Build Coq on a ocaml toplevel (incompatible with -opt)
+  -searchisos   Build a toplevel for SearchIsos (implies -notactics)
+  -R dir        Specify recursively directories for Ocaml\n";
+  exit 1
+
+(* parsing of the command line *)
+let parse_args () =
+  let rec parse (op,fl) = function
+    | [] -> List.rev op, List.rev fl
+    | "-srcdir" :: d :: rem -> src_coqtop := d ; parse (op,fl) rem
+    | "-srcdir" :: _        -> usage ()
+    | "-notactics" :: rem -> notactics := true ; parse (op,fl) rem
+    | "-opt" :: rem -> opt := true ; parse (op,fl) rem
+    | "-top" :: rem -> top := true ; parse (op,fl) rem
+    | "-searchisos" :: rem ->
+        searchisos := true; notactics := true; parse (op,fl) rem
+    | "-echo" :: rem -> echo := true ; parse (op,fl) rem
+    | ("-cclib"|"-ccopt"|"-I"|"-o" as o) :: rem' ->
+	begin
+	  match rem' with
+	    | a :: rem -> parse (a::o::op,fl) rem
+	    | []       -> usage ()
+	end
+    | "-R" :: rem' ->
+        begin
+	  match rem' with
+	    | a :: rem ->
+                parse ((List.rev(List.flatten (List.map (fun d -> ["-I";d])
+						 (all_subdirs a))))@op,fl) rem
+	    | []       -> usage ()
+	end
+    | ("-compact"|"-g"|"-p" as o) :: rem -> parse (o::op,fl) rem
+    | ("-h"|"--help") :: _ -> usage ()
+    | 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" 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
+
+(*Gives all modules in dir. Uses .cmi. Unix again sorry again*)
+let all_modules_in_dir dir=
+  try
+    let lst = ref []
+    and stg = ref ""
+    and dh = Unix.opendir dir in
+    try
+      while true do
+	let stg = Unix.readdir dh in
+        if (Filename.check_suffix stg ".cmi") then
+          lst := !lst @ [String.capitalize (Filename.chop_suffix stg ".cmi")]
+      done;
+      []
+    with End_of_file -> 
+      Unix.closedir dh; !lst
+  with Unix.Unix_error (_,"opendir",_) ->
+    failwith ("all_modules_in_dir: directory "^dir^" not found")
+
+(*Gives a part of command line (corresponding to dir) for extract_crc*)
+let crc_cmd dir =
+  " -I "^dir^(List.fold_right (fun x y -> " "^x^y) (all_modules_in_dir dir)
+  "")
+
+(*Same as crc_cmd but recursively*)
+let rec_crc_cmd dir =
+  List.fold_right (fun x y -> x^y) (List.map crc_cmd (all_subdirs dir)) ""
+
+(*Creates another temporary file for Dynlink if needed*)
+let tmp_dynlink()=
+  let tmp = Filename.temp_file "coqdynlink" ".ml" in
+  let _ = Sys.command ("echo \"Dynlink.init();;\" > "^tmp) in
+  let _ = Sys.command (Coq_config.camllib^"/extract_crc"^(crc_cmd
+      Coq_config.camllib)^(crc_cmd Coq_config.camlp4lib)^(rec_crc_cmd
+      (Coq_config.coqtop^"/src"))^" >> "^tmp) in
+  let _ = Sys.command ("echo \";;\" >> "^tmp) in
+  let _ = 
+    Sys.command ("echo \"Dynlink.add_available_units crc_unit_list;;\" >> "^
+		 tmp)
+  in
+  tmp
+
+(*Initializes the kind of loading in the main program*)
+let declare_loading_string()=
+  if !opt then
+    "Mltop.set Mltop.Native;;\n"
+  else if not !top then
+    "Mltop.set Mltop.WithoutTop;;\n"
+  else
+    "Mltop.set (Mltop.WithTop {Mltop.load_obj=Topdirs.dir_load;
+                                 Mltop.use_file=Topdirs.dir_use;
+                                 Mltop.add_dir=Topdirs.dir_directory});;\n"
+
+(* create a temporary main file to link *)
+let create_tmp_main_file modules =
+  let main_name = Filename.temp_file "coqmain" ".ml" in
+  let oc = open_out main_name 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 right toplevel loop: Coq or Coq_searchisos *)
+    if !searchisos then 
+      output_string oc "Cmd_searchisos_line.start();;\n"
+    else 
+      output_string oc "Coqtop.start();;\n";
+    (* Start the Ocaml toplevel if it exists *)
+    if !top then
+      output_string oc "Printexc.catch Toploop.loop(); exit 1;;\n";
+    close_out oc;
+    main_name
+  with e -> 
+    clean main_name; raise e
+
+(* main part *)
+let main () =
+  let (options, userfiles) = parse_args () in
+  (* which ocaml command to invoke *)
+  let prog =
+    if !opt then begin
+      (* native code *)
+      if !top then failwith "no custom toplevel in native code !";
+      "ocamlopt -linkall"
+    end else
+      (* bytecode *)
+      if !top then "ocamlmktop -custom -linkall" else "ocamlc -custom -linkall"
+  in
+  (* files to link *)
+  let (modules, tolink) = files_to_link userfiles in
+  (*file for dynlink *)
+  let dynlink=
+    if not (!opt || !top) then
+      [tmp_dynlink()]
+    else
+      []
+  in
+  (* the list of the loaded modules *)
+  let main_file = create_tmp_main_file modules in
+  try
+    let args = (includes ()) @ options @ tolink @ dynlink @ [ main_file ] in
+    (* Now, with the .cma, we MUST use the -linkall option *)
+    let command = String.concat " " ((prog^" -linkall")::args) in
+    if !echo then begin print_endline command; flush Pervasives.stdout end;
+    let retcode = 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 e -> 
+    clean main_file; raise e
+
+let retcode =
+  try Printexc.print main () with _ -> 1
+
+let _ = exit retcode