diff options
Diffstat (limited to 'scripts')
| -rw-r--r-- | scripts/coqc.ml | 189 | ||||
| -rw-r--r-- | scripts/coqmktop.ml | 319 |
2 files changed, 0 insertions, 508 deletions
diff --git a/scripts/coqc.ml b/scripts/coqc.ml deleted file mode 100644 index 8cdac0c5..00000000 --- a/scripts/coqc.ml +++ /dev/null @@ -1,189 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* Afin de rendre Coq plus portable, ce programme Caml remplace le script - coqc. - - Ici, on trie la ligne de commande pour en extraire les fichiers à compiler, - puis on les compile un par un en passant le reste de la ligne de commande - à un process "coqtop -batch -load-vernac-source <fichier>". - - On essaye au maximum d'utiliser les modules Sys et Filename pour que la - portabilité soit maximale, mais il reste encore des appels à des fonctions - du module Unix. Ceux-ci sont préfixés par "Unix." -*) - -(* environment *) - -let environment = Unix.environment () - -let best = if Coq_config.arch = "win32" then "" else ("."^Coq_config.best) -let binary = ref ("coqtop" ^ best) -let image = ref "" - -(* coqc options *) - -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 name_no_suffix = - if Filename.check_suffix file ".v" then - Filename.chop_suffix file ".v" - else - file - in - let modulename = Filename.basename name_no_suffix in - check_module_name modulename; - (if !verbose then "-compile-verbose" else "-compile") - :: name_no_suffix :: (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 - -(* parsing of the command line - * - * special treatment for -bindir and -i. - * other options are passed to coqtop *) - -let usage () = - Usage.print_usage_coqc () ; - flush stderr ; - exit 1 - -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 -> - binary := "coqtop.opt"; parse (cfiles,args) rem - | "-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 - - | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () - | ("-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 - | ("-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 - - | ("-notactics"|"-debug"|"-nolib"|"-boot" - |"-batch"|"-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" as o) :: rem -> - parse (cfiles,o::args) rem - - | ("-where") :: _ -> - (try print_endline (Envars.coqlib ()) - with Util.UserError(_,pps) -> Pp.msgerrnl (Pp.hov 0 pps)); - exit 0 - - | ("-config" | "--config") :: _ -> Usage.print_config (); exit 0 - - | ("-v"|"--version") :: _ -> - Usage.version 0 - | 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 eaecda5d..00000000 --- a/scripts/coqmktop.ml +++ /dev/null @@ -1,319 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \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 *) - -(* 1. Core objects *) -let ocamlobjs = ["str.cma";"unix.cma";"nums.cma"] -let dynobjs = ["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 () 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 dyn_objs = - if not !opt || Coq_config.has_natdynlink then dynobjs else [] in - let toplevel_objs = - if !top then topobjs else if !opt then notopobjs else [] in - let objs = dyn_objs @ libobjs @ core_objs @ toplevel_objs in - let modules = List.map module_of_file (objs @ userfiles) - in - let libs = dyn_objs @ 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 - -(* 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 - tmp - -(* 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 Util.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 - (*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 = options @ includes () @ copts @ tolink @ dynlink in - let args = args @ [ 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 |