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 --- .gitignore | 2 +- .typerex | 1 - Makefile | 2 +- Makefile.build | 2 +- Makefile.common | 6 +- _tags | 6 +- myocamlbuild.ml | 6 +- scripts/coqc.ml | 193 -------------------------------- scripts/coqmktop.ml | 310 ---------------------------------------------------- tools/coqc.ml | 193 ++++++++++++++++++++++++++++++++ tools/coqmktop.ml | 310 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 11 files changed, 514 insertions(+), 517 deletions(-) delete mode 100644 scripts/coqc.ml delete mode 100644 scripts/coqmktop.ml create mode 100644 tools/coqc.ml create mode 100644 tools/coqmktop.ml diff --git a/.gitignore b/.gitignore index 8418d9346f..8f0a9a4098 100644 --- a/.gitignore +++ b/.gitignore @@ -145,7 +145,7 @@ ide/coqide_main_opt.ml kernel/byterun/coq_jumptbl.h kernel/copcodes.ml -scripts/tolink.ml +tools/tolink.ml theories/Numbers/Natural/BigN/NMake_gen.v ide/index_urls.txt diff --git a/.typerex b/.typerex index 9ccd4e7efc..95921c8fa2 100644 --- a/.typerex +++ b/.typerex @@ -9,7 +9,6 @@ library plugins pretyping proofs -scripts states tactics theories diff --git a/Makefile b/Makefile index 9e1742a56c..1d235d5b23 100644 --- a/Makefile +++ b/Makefile @@ -78,7 +78,7 @@ EXISTINGMLI := $(call find, '*.mli') GENML4FILES:= $(ML4FILES:.ml4=.ml) GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) \ - scripts/tolink.ml kernel/copcodes.ml + tools/tolink.ml kernel/copcodes.ml GENMLIFILES:=$(YACCFILES:.mly=.mli) GENPLUGINSMOD:=$(filter plugins/%,$(MLLIBFILES:%.mllib=%_mod.ml)) export GENHFILES:=kernel/byterun/coq_jumptbl.h diff --git a/Makefile.build b/Makefile.build index 6c24357026..b42432d48d 100644 --- a/Makefile.build +++ b/Makefile.build @@ -254,7 +254,7 @@ $(COQMKTOP): $(patsubst %.cma,%$(BESTLIB),$(COQMKTOPCMO:.cmo=$(BESTOBJ))) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD)) -scripts/tolink.ml: Makefile.build Makefile.common +tools/tolink.ml: Makefile.build Makefile.common $(SHOW)"ECHO... >" $@ $(HIDE)echo "let copts = \"-cclib -lcoqrun\"" > $@ $(HIDE)echo "let core_libs = \""$(LINKCMO)"\"" >> $@ diff --git a/Makefile.common b/Makefile.common index 63834dcb04..1934fd4938 100644 --- a/Makefile.common +++ b/Makefile.common @@ -72,7 +72,7 @@ PLUGINS:=\ SRCDIRS:=\ $(CORESRCDIRS) \ - tools tools/coqdoc scripts \ + tools tools/coqdoc \ $(addprefix plugins/, $(PLUGINS)) IDESRCDIRS:=\ @@ -224,9 +224,9 @@ IDEMOD:=$(shell cat ide/ide.mllib) COQENVCMO:=lib/clib.cma lib/loc.cmo lib/errors.cmo -COQMKTOPCMO:=$(COQENVCMO) scripts/tolink.cmo scripts/coqmktop.cmo +COQMKTOPCMO:=$(COQENVCMO) tools/tolink.cmo tools/coqmktop.cmo -COQCCMO:=$(COQENVCMO) toplevel/usage.cmo scripts/coqc.cmo +COQCCMO:=$(COQENVCMO) toplevel/usage.cmo tools/coqc.cmo ## Misc diff --git a/_tags b/_tags index 8404c91cd2..5bb8564801 100644 --- a/_tags +++ b/_tags @@ -1,8 +1,8 @@ ## tags for binaries - : use_str, use_unix - : use_str, use_unix + : use_str, use_unix + : use_str, use_unix : use_unix : use_str, use_unix : use_str @@ -68,8 +68,6 @@ "pretyping": include "printing": include "proofs": include -"scripts": include -"states": include "tactics": include "theories": include "tools": include diff --git a/myocamlbuild.ml b/myocamlbuild.ml index f869b4ca73..a0e2e7ef76 100644 --- a/myocamlbuild.ml +++ b/myocamlbuild.ml @@ -111,7 +111,7 @@ let core_cma = List.map (fun s -> s^".cma") core_libs let core_cmxa = List.map (fun s -> s^".cmxa") core_libs let core_mllib = List.map (fun s -> s^".mllib") core_libs -let tolink = "scripts/tolink.ml" +let tolink = "tools/tolink.ml" let c_headers_base = ["coq_fix_code.h";"coq_instruct.h"; "coq_memory.h"; "int64_emul.h"; @@ -155,7 +155,7 @@ let coqdepdeps = theoriesv @ pluginsv @ pluginsmllib let coqtop = "toplevel/coqtop" let coqide = "ide/coqide" let coqdepboot = "tools/coqdep_boot" -let coqmktop = "scripts/coqmktop" +let coqmktop = "tools/coqmktop" (** The list of binaries to build: (name of link in bin/, name in _build, install both or only best) *) @@ -167,7 +167,7 @@ let all_binaries = [ "coqtop", coqtop, Both; "coqide", "ide/coqide_main", Ide; "coqmktop", coqmktop, Both; - "coqc", "scripts/coqc", Both; + "coqc", "tools/coqc", Both; "coqchk", "checker/main", Both; "coqdep_boot", coqdepboot, Best; "coqdep", "tools/coqdep", Best; diff --git a/scripts/coqc.ml b/scripts/coqc.ml deleted file mode 100644 index e15a1768c2..0000000000 --- a/scripts/coqc.ml +++ /dev/null @@ -1,193 +0,0 @@ -(************************************************************************) -(* 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/scripts/coqmktop.ml b/scripts/coqmktop.ml deleted file mode 100644 index 81f0686e02..0000000000 --- a/scripts/coqmktop.ml +++ /dev/null @@ -1,310 +0,0 @@ -(************************************************************************) -(* 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 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