From b28e9663968e55b0edd79af09581f8fe31337821 Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 18 Apr 2013 16:56:17 +0000 Subject: 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 --- tools/coqc.ml | 193 +++++++++++++++++++++++++++++++++ tools/coqmktop.ml | 310 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 503 insertions(+) create mode 100644 tools/coqc.ml create mode 100644 tools/coqmktop.ml (limited to 'tools') 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 *) +(* ". +*) + +(* 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 *) +(* 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 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 -- cgit v1.2.3