diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 34 | ||||
| -rw-r--r-- | tools/TimeFileMaker.py | 28 | ||||
| -rw-r--r-- | tools/coq_makefile.ml | 50 | ||||
| -rw-r--r-- | tools/coqdep.ml | 4 | ||||
| -rw-r--r-- | tools/coqmktop.ml | 314 | ||||
| -rw-r--r-- | tools/coqworkmgr.ml | 8 | ||||
| -rwxr-xr-x | tools/make-both-single-timing-files.py | 18 | ||||
| -rwxr-xr-x | tools/make-both-time-files.py | 18 | ||||
| -rw-r--r-- | tools/md5sum.ml | 24 |
9 files changed, 112 insertions, 386 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 7fd9429081..ca02c983d2 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -87,7 +87,6 @@ COQCHK ?= "$(COQBIN)coqchk" COQDEP ?= "$(COQBIN)coqdep" GALLINA ?= "$(COQBIN)gallina" COQDOC ?= "$(COQBIN)coqdoc" -COQMKTOP ?= "$(COQBIN)coqmktop" COQMKFILE ?= "$(COQBIN)coq_makefile" # Timing scripts @@ -120,6 +119,8 @@ CAMLPKGS ?= # Option for making timing files TIMING?= +# Option for changing sorting of timing output file +TIMING_SORT_BY ?= auto # Output file names for timed builds TIME_OF_BUILD_FILE ?= time-of-build.log TIME_OF_BUILD_BEFORE_FILE ?= time-of-build-before.log @@ -177,7 +178,7 @@ COQMAKEFILE_VERSION:=@COQ_VERSION@ COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)") -CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB) $(OCAML_API_FLAGS) +CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB) # ocamldoc fails with unknown argument otherwise CAMLDOCFLAGS=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS))) @@ -228,8 +229,9 @@ COQTOPINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)toploop) # We here define a bunch of variables about the files being part of the # Coq project in order to ease the writing of build target and build rules +VDFILE := .coqdeps + ALLSRCFILES := \ - $(VFILES) \ $(ML4FILES) \ $(MLFILES) \ $(MLPACKFILES) \ @@ -289,13 +291,15 @@ ALLNATIVEFILES = \ $(OBJFILES:.o=.cmi) \ $(OBJFILES:.o=.cmx) \ $(OBJFILES:.o=.cmxs) -# trick: wildcard filters out non-existing files -NATIVEFILESTOINSTALL = $(foreach f, $(ALLNATIVEFILES), $(wildcard $f)) +# trick: wildcard filters out non-existing files, so that `install` doesn't show +# warnings and `clean` doesn't pass to rm a list of files that is too long for +# the shell. +NATIVEFILES = $(wildcard $(ALLNATIVEFILES)) FILESTOINSTALL = \ $(VOFILES) \ $(VFILES) \ $(GLOBFILES) \ - $(NATIVEFILESTOINSTALL) \ + $(NATIVEFILES) \ $(CMIFILESTOINSTALL) BYTEFILESTOINSTALL = \ $(CMOFILESTOINSTALL) \ @@ -307,7 +311,7 @@ else DO_NATDYNLINK = endif -ALLDFILES = $(addsuffix .d,$(ALLSRCFILES)) +ALLDFILES = $(addsuffix .d,$(ALLSRCFILES) $(VDFILE)) # Compilation targets ######################################################### @@ -332,7 +336,7 @@ make-pretty-timed make-pretty-timed-before make-pretty-timed-after:: print-pretty-timed:: $(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) print-pretty-timed-diff:: - $(HIDE)$(COQMAKE_BOTH_TIME_FILES) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) + $(HIDE)$(COQMAKE_BOTH_TIME_FILES) --sort-by=$(TIMING_SORT_BY) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) ifeq (,$(BEFORE)) print-pretty-single-time-diff:: @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing' @@ -344,7 +348,7 @@ print-pretty-single-time-diff:: $(HIDE)false else print-pretty-single-time-diff:: - $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) $(BEFORE) $(AFTER) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) + $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) --sort-by=$(TIMING_SORT_BY) $(BEFORE) $(AFTER) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) endif endif pretty-timed: @@ -432,7 +436,7 @@ all.pdf: $(VFILES) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)` # FIXME: not quite right, since the output name is different -gallinahtml: GAL=g +gallinahtml: GAL=-g gallinahtml: html all-gal.ps: GAL=-g @@ -535,7 +539,7 @@ clean:: $(HIDE)rm -f $(CMOFILES:.cmo=.o) $(HIDE)rm -f $(CMXAFILES:.cmxa=.a) $(HIDE)rm -f $(ALLDFILES) - $(HIDE)rm -f $(ALLNATIVEFILES) + $(HIDE)rm -f $(NATIVEFILES) $(HIDE)find . -name .coq-native -type d -empty -delete $(HIDE)rm -f $(VOFILES) $(HIDE)rm -f $(VOFILES:.vo=.vio) @@ -563,7 +567,7 @@ cleanall:: clean archclean:: @# Extension point $(SHOW)'CLEAN *.cmx *.o' - $(HIDE)rm -f $(ALLNATIVEFILES) + $(HIDE)rm -f $(NATIVEFILES) $(HIDE)rm -f $(CMOFILES:%.cmo=%.cmx) .PHONY: archclean @@ -712,9 +716,9 @@ $(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack $(SHOW)'COQDEP $<' $(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok) -$(addsuffix .d,$(VFILES)): %.v.d: %.v - $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEP) $(COQLIBS) -dyndep var -c "$<" $(redir_if_ok) +$(VDFILE).d: $(VFILES) + $(SHOW)'COQDEP VFILES' + $(HIDE)$(COQDEP) $(COQLIBS) -dyndep var -c $(VFILES) $(redir_if_ok) # Misc ######################################################################## diff --git a/tools/TimeFileMaker.py b/tools/TimeFileMaker.py index a5a5fa8fe5..0d24332f1e 100644 --- a/tools/TimeFileMaker.py +++ b/tools/TimeFileMaker.py @@ -10,6 +10,20 @@ STRIP_REG = re.compile('^(coq/|contrib/|)(?:theories/|src/)?') STRIP_REP = r'\1' INFINITY = '\xe2\x88\x9e' +def parse_args(argv, USAGE, HELP_STRING): + sort_by = 'auto' + if any(arg.startswith('--sort-by=') for arg in argv[1:]): + sort_by = [arg for arg in argv[1:] if arg.startswith('--sort-by=')][-1][len('--sort-by='):] + args = [arg for arg in argv if not arg.startswith('--sort-by=')] + if len(args) < 3 or '--help' in args[1:] or '-h' in args[1:] or sort_by not in ('auto', 'absolute', 'diff'): + print(USAGE) + if '--help' in args[1:] or '-h' in args[1:]: + print(HELP_STRING) + if len(args) == 2: sys.exit(0) + sys.exit(1) + return sort_by, args + + def reformat_time_string(time): seconds, milliseconds = time.split('.') seconds = int(seconds) @@ -108,6 +122,7 @@ def format_percentage(num, signed=True): return sign + '%d.%02d%%' % (whole_part, frac_part) def make_diff_table_string(left_times_dict, right_times_dict, + sort_by='auto', descending=True, left_tag="After", tag="File Name", right_tag="Before", with_percent=True, change_tag="Change", percent_change_tag="% Change"): @@ -125,10 +140,15 @@ def make_diff_table_string(left_times_dict, right_times_dict, if rseconds != 0 else (INFINITY if lseconds > 0 else 'N/A'))) for name, lseconds, rseconds in prediff_times) # update to sort by approximate difference, first - get_key = make_sorting_key(all_names_dict, descending=descending) - all_names_dict = dict((name, (fix_sign_for_sorting(int(abs(to_seconds(diff_times_dict[name]))), descending=descending), get_key(name))) - for name in all_names_dict.keys()) - names = sorted(all_names_dict.keys(), key=all_names_dict.get) + get_key_abs = make_sorting_key(all_names_dict, descending=descending) + get_key_diff = (lambda name: fix_sign_for_sorting(int(abs(to_seconds(diff_times_dict[name]))), descending=descending)) + if sort_by == 'absolute': + get_key = get_key_abs + elif sort_by == 'diff': + get_key = get_key_diff + else: # sort_by == 'auto' + get_key = (lambda name: (get_key_diff(name), get_key_abs(name))) + names = sorted(all_names_dict.keys(), key=get_key) #names = get_sorted_file_list_from_times_dict(all_names_dict, descending=descending) # set the widths of each of the columns by the longest thing to go in that column left_sum = sum_times(left_times_dict.values()) diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 2feaaa04cd..091869407e 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -27,16 +27,8 @@ let rec print_prefix_list sep = function | x :: l -> print sep; print x; print_prefix_list sep l | [] -> () -let usage () = - output_string stderr "Usage summary:\ -\n\ -\ncoq_makefile .... [file.v] ... [file.ml[i4]?] ... [file.ml{lib,pack}]\ -\n ... [any] ... [-extra[-phony] result dependencies command]\ -\n ... [-I dir] ... [-R physicalpath logicalpath]\ -\n ... [-Q physicalpath logicalpath] ... [VARIABLE = value]\ -\n ... [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file]\ -\n [-h] [--help]\ -\n\ +let usage_common () = + output_string stderr "\ \n[file.v]: Coq file to be compiled\ \n[file.ml[i4]?]: Objective Caml file to be compiled\ \n[file.ml{lib,pack}]: ocamlbuild file that describes a Objective Caml\ @@ -65,10 +57,28 @@ let usage () = \n[-install opt]: where opt is \"user\" to force install into user directory,\ \n \"none\" to build a makefile with no install target or\ \n \"global\" to force install in $COQLIB directory\ +\n" + +let usage_coq_project () = + output_string stderr "Available arguments:"; + usage_common (); + exit 1 + +let usage_coq_makefile () = + output_string stderr "Usage summary:\ +\n\ +\ncoq_makefile .... [file.v] ... [file.ml[i4]?] ... [file.ml{lib,pack}]\ +\n ... [any] ... [-extra[-phony] result dependencies command]\ +\n ... [-I dir] ... [-R physicalpath logicalpath]\ +\n ... [-Q physicalpath logicalpath] ... [VARIABLE = value]\ +\n ... [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file]\ +\n [-h] [--help]\ +\n"; + usage_common (); + output_string stderr "\ \n[-f file]: take the contents of file as arguments\ -\n[-o file]: output should go in file file\ +\n[-o file]: output should go in file file (recommended)\ \n Output file outside the current directory is forbidden.\ -\n[-bypass-API]: when compiling plugins, bypass Coq API\ \n[-h]: print this usage summary\ \n[--help]: equivalent to [-h]\n"; exit 1 @@ -199,16 +209,10 @@ let windrive s = else s ;; -let generate_conf_coq_config oc args bypass_API = +let generate_conf_coq_config oc args = section oc "Coq configuration."; - let src_dirs = if bypass_API - then Coq_config.all_src_dirs - else Coq_config.api_dirs @ Coq_config.plugins_dirs in + let src_dirs = Coq_config.all_src_dirs in Envars.print_config ~prefix_var_name:"COQMF_" oc src_dirs; - if bypass_API then - Printf.fprintf oc "OCAML_API_FLAGS=\n" - else - Printf.fprintf oc "OCAML_API_FLAGS=-open API\n"; fprintf oc "COQMF_WINDRIVE=%s\n" (windrive Coq_config.coqlib) ;; @@ -267,7 +271,7 @@ let generate_conf oc project args = fprintf oc "# %s\n\n" (String.concat " " (List.map quote args)); generate_conf_files oc project; generate_conf_includes oc project; - generate_conf_coq_config oc args project.bypass_API; + generate_conf_coq_config oc args; generate_conf_defs oc project; generate_conf_doc oc project; generate_conf_extra_target oc project.extra_targets; @@ -380,8 +384,8 @@ let share_prefix s1 s2 = | _ -> false let _ = + let _fhandle = Feedback.(add_feeder (console_feedback_listener Format.err_formatter)) in let prog, args = - if Array.length Sys.argv = 1 then usage (); let args = Array.to_list Sys.argv in let prog = List.hd args in prog, List.tl args in @@ -392,7 +396,7 @@ let _ = let project = try cmdline_args_to_project ~curdir:Filename.current_dir_name args - with Parsing_error s -> prerr_endline s; usage () in + with Parsing_error s -> prerr_endline s; usage_coq_project () in if only_destination <> None then begin destination_of project (Option.get only_destination); diff --git a/tools/coqdep.ml b/tools/coqdep.ml index fd4be08b12..ca14b11bc1 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -455,7 +455,7 @@ let usage () = eprintf " -coqlib dir : set the coq standard library directory\n"; eprintf " -suffix s : \n"; eprintf " -slash : deprecated, no effect\n"; - eprintf " -dyndep (opt|byte|both|no|var) : set how dependencies over ML modules are printed"; + eprintf " -dyndep (opt|byte|both|no|var) : set how dependencies over ML modules are printed\n"; exit 1 let split_period = Str.split (Str.regexp (Str.quote ".")) @@ -539,4 +539,4 @@ let _ = coqdep () with CErrors.UserError(s,p) -> let pp = (match s with | None -> p | Some s -> Pp.(str s ++ str ": " ++ p)) in - Feedback.msg_error pp + Format.eprintf "%a@\n%!" Pp.pp_with pp diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml deleted file mode 100644 index 950ed53ccf..0000000000 --- a/tools/coqmktop.ml +++ /dev/null @@ -1,314 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** {1 Coqmktop} *) - -(** 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). *) - -(** {6 Utilities} *) - -(** Split a string at each blank -*) -let split_list = - let spaces = Str.regexp "[ \t\n]+" in - fun str -> Str.split spaces str - -[@@@ocaml.warning "-3"] (* String.uncapitalize_ascii since 4.03.0 GPR#124 *) -let capitalize = String.capitalize -[@@@ocaml.warning "+3"] - -let (/) = Filename.concat - -(** Which user files do we support (and propagate to ocamlopt) ? -*) -let supported_suffix f = match CUnix.get_extension f with - | ".ml" | ".cmx" | ".cmo" | ".cmxa" | ".cma" | ".c" -> true - | _ -> false - -let supported_flambda_option f = List.mem f Coq_config.flambda_flags - -(** From bytecode extension to native -*) -let native_suffix f = match CUnix.get_extension f with - | ".cmo" -> (Filename.chop_suffix f ".cmo") ^ ".cmx" - | ".cma" -> (Filename.chop_suffix f ".cma") ^ ".cmxa" - | ".a" -> f - | _ -> failwith ("File "^f^" has not extension .cmo, .cma or .a") - -(** Transforms a file name in the corresponding Caml module name. -*) -let module_of_file name = - capitalize (try Filename.chop_extension name with Invalid_argument _ -> name) - -(** Run a command [prog] with arguments [args]. - We do not use [Sys.command] anymore, see comment in [CUnix.sys_command]. -*) -let run_command prog args = - match CUnix.sys_command prog args with - | Unix.WEXITED 127 -> failwith ("no such command "^prog) - | Unix.WEXITED n -> n - | Unix.WSIGNALED n -> failwith (prog^" killed by signal "^string_of_int n) - | Unix.WSTOPPED n -> failwith (prog^" stopped by signal "^string_of_int n) - - - -(** {6 Coqmktop options} *) - -let opt = ref false -let top = ref false -let echo = ref false -let no_start = ref false - -let is_ocaml4 = Coq_config.caml_version.[0] <> '3' - -(** {6 Includes options} *) - -(** Since the Coq core .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 std_includes basedir = - let rebase d = match basedir with None -> d | Some base -> base / d in - ["-I"; rebase "."; - "-I"; rebase "lib"; - "-I"; rebase "vernac"; (* For Mltop *) - "-I"; rebase "toplevel"; - "-I"; rebase "kernel/byterun"; - "-I"; Envars.camlp4lib () ] @ - (if is_ocaml4 then ["-I"; "+compiler-libs"] else []) - -(** For the -R option, visit all directories under [dir] and add - corresponding -I to the [opts] option list (in reversed order) *) -let incl_all_subdirs dir opts = - let l = ref opts in - let add f = l := f :: "-I" :: !l in - let rec traverse dir = - if Sys.file_exists dir && Sys.is_directory dir then - let () = add dir in - let subdirs = try Sys.readdir dir with any -> [||] in - Array.iter (fun f -> traverse (dir/f)) subdirs - in - traverse dir; !l - - -(** {6 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. *) - -(** OCaml + CamlpX libraries *) - -let ocaml_libs = ["str.cma";"unix.cma";"nums.cma";"dynlink.cma";"threads.cma"] -let camlp4_libs = ["gramlib.cma"] -let libobjs = ocaml_libs @ camlp4_libs - -(** Toplevel objects *) - -let ocaml_topobjs = - if is_ocaml4 then - ["ocamlcommon.cma";"ocamlbytecomp.cma";"ocamltoplevel.cma"] - else - ["toplevellib.cma"] - -let camlp4_topobjs = ["camlp5_top.cma"; "pa_o.cmo"; "pa_extend.cmo"] - -let topobjs = ocaml_topobjs @ camlp4_topobjs - -(** Coq Core objects *) - -let copts = (split_list Coq_config.osdeplibs) @ (split_list Tolink.copts) -let core_objs = split_list Tolink.core_objs -let core_libs = split_list Tolink.core_libs - -(** Build the list of files to link and the list of modules names -*) -let files_to_link userfiles = - let top = if !top then topobjs else [] in - let modules = List.map module_of_file (top @ core_objs @ userfiles) in - let objs = libobjs @ top @ core_libs in - let objs' = (if !opt then List.map native_suffix objs else objs) @ userfiles - in (modules, objs') - - -(** {6 Parsing of the command-line} *) - -let usage () = - prerr_endline "Usage: coqmktop <options> <ocaml options> files\ -\nFlags are:\ -\n -coqlib dir Specify where the Coq object files are\ -\n -ocamlfind dir Specify where the ocamlfind binary is\ -\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 -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 - -let parse_args () = - let rec parse (op,fl) = function - | [] -> List.rev op, List.rev fl - - (* Directories *) - | "-coqlib" :: d :: rem -> - Flags.coqlib_spec := true; Flags.coqlib := d ; parse (op,fl) rem - | "-ocamlfind" :: d :: rem -> - Flags.ocamlfind_spec := true; Flags.ocamlfind := d ; parse (op,fl) rem - | "-camlp4bin" :: d :: rem -> - Flags.camlp4bin_spec := true; Flags.camlp4bin := d ; parse (op,fl) rem - | "-R" :: d :: rem -> parse (incl_all_subdirs d op,fl) rem - | ("-coqlib"|"-camlbin"|"-camlp4bin"|"-R") :: [] -> usage () - - (* Boolean options of coqmktop *) - | "-boot" :: rem -> Flags.boot := true; parse (op,fl) rem - | "-opt" :: rem -> opt := true ; parse (op,fl) rem - | "-top" :: rem -> top := true ; parse (op,fl) rem - | "-no-start" :: rem -> no_start:=true; parse (op, fl) rem - | "-echo" :: rem -> echo := true ; parse (op,fl) rem - - (* Extra options with arity 0 or 1, directly passed to ocamlc/ocamlopt *) - | ("-noassert"|"-compact"|"-g"|"-p"|"-thread"|"-dtypes" as o) :: rem -> - parse (o::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 - - | ("-h"|"-help"|"--help") :: _ -> usage () - | f :: rem when supported_flambda_option f -> parse (op,fl) rem - | f :: rem when supported_suffix f -> parse (op,f::fl) rem - | f :: _ -> prerr_endline ("Don't know what to do with " ^ f); exit 1 - in - parse ([],[]) (List.tl (Array.to_list Sys.argv)) - - -(** {6 Temporary main file} *) - -(** remove the temporary main file -*) -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)\ -\n then CErrors.user_err Pp.(str (\"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 - -(* TODO: remove once OCaml 4.04 is adopted *) -let split_on_char sep s = - let r = ref [] in - let j = ref (String.length s) in - for i = String.length s - 1 downto 0 do - if s.[i] = sep then begin - r := String.sub s (i + 1) (!j - i - 1) :: !r; - j := i - end - done; - String.sub s 0 !j :: !r - -(** {6 Main } *) - -let main () = - let (options, userfiles) = parse_args () in - (* Directories: *) - let () = Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x)) in - let basedir = if !Flags.boot then None else Some (Envars.coqlib ()) in - (* Which ocaml compiler to invoke *) - let prog = if !opt then "opt" else "ocamlc" in - (* Which arguments ? *) - if !opt && !top then failwith "no custom toplevel in native code!"; - let flags = if !opt then Coq_config.flambda_flags else Coq_config.vmbyteflags in - let topstart = if !top then [ "topstart.cmo" ] else [] in - let (modules, tolink) = files_to_link userfiles in - let main_file = create_tmp_main_file modules in - try - (* - We add topstart.cmo explicitly because we shunted ocamlmktop wrapper. - - With the coq .cma, we MUST use the -linkall option. *) - let coq_camlflags = - List.filter ((<>) "") (split_on_char ' ' Coq_config.caml_flags) in - let args = - coq_camlflags @ "-linkall" :: "-w" :: "-31" :: flags @ copts @ options @ - (std_includes basedir) @ tolink @ [ main_file ] @ topstart - in - if !echo then begin - let command = String.concat " " (Envars.ocamlfind ()::prog::args) in - print_endline command; - print_endline - ("(command length is " ^ - (string_of_int (String.length command)) ^ " characters)"); - flush Pervasives.stdout - end; - let exitcode = run_command (Envars.ocamlfind ()) (prog::args) in - clean main_file; - exitcode - with reraise -> clean main_file; raise reraise - -let pr_exn = function - | Failure msg -> msg - | Unix.Unix_error (err,fn,arg) -> fn^" "^arg^" : "^Unix.error_message err - | any -> Printexc.to_string any - -let _ = - try exit (main ()) - with any -> Printf.eprintf "Error: %s\n" (pr_exn any); exit 1 diff --git a/tools/coqworkmgr.ml b/tools/coqworkmgr.ml index e1d1c60d72..f4777c4fb7 100644 --- a/tools/coqworkmgr.ml +++ b/tools/coqworkmgr.ml @@ -14,7 +14,7 @@ type party = { sock : Unix.file_descr; cout : out_channel; mutable tokens : int; - priority : Flags.priority; + priority : priority; } let answer party msg = @@ -42,10 +42,10 @@ end = struct let is_empty q = !q = [] let rec split acc = function | [] -> List.rev acc, [] - | (_, { priority = Flags.Low }) :: _ as l -> List.rev acc, l + | (_, { priority = Low }) :: _ as l -> List.rev acc, l | x :: xs -> split (x :: acc) xs let push (_,{ priority } as item) q = - if priority = Flags.Low then q := !q @ [item] + if priority = Low then q := !q @ [item] else let high, low = split [] !q in q := high @ (item :: low) @@ -148,7 +148,7 @@ let check_alive s = | Some s -> let cout = Unix.out_channel_of_descr s in set_binary_mode_out cout true; - output_string cout (print_request (Hello Flags.Low)); flush cout; + output_string cout (print_request (Hello Low)); flush cout; output_string cout (print_request Ping); flush cout; begin match Unix.select [s] [] [] 1.0 with | [s],_,_ -> diff --git a/tools/make-both-single-timing-files.py b/tools/make-both-single-timing-files.py index 2d33503c36..32c52c7a17 100755 --- a/tools/make-both-single-timing-files.py +++ b/tools/make-both-single-timing-files.py @@ -3,16 +3,10 @@ import sys from TimeFileMaker import * if __name__ == '__main__': - USAGE = 'Usage: %s AFTER_FILE_NAME BEFORE_FILE_NAME [OUTPUT_FILE_NAME ..]' % sys.argv[0] + USAGE = 'Usage: %s [--sort-by=auto|absolute|diff] AFTER_FILE_NAME BEFORE_FILE_NAME [OUTPUT_FILE_NAME ..]' % sys.argv[0] HELP_STRING = r'''Formats timing information from the output of two invocations of `coqc -time` into a sorted table''' - if len(sys.argv) < 3 or '--help' in sys.argv[1:] or '-h' in sys.argv[1:]: - print(USAGE) - if '--help' in sys.argv[1:] or '-h' in sys.argv[1:]: - print(HELP_STRING) - if len(sys.argv) == 2: sys.exit(0) - sys.exit(1) - else: - left_dict = get_single_file_times(sys.argv[1]) - right_dict = get_single_file_times(sys.argv[2]) - table = make_diff_table_string(left_dict, right_dict, tag="Code") - print_or_write_table(table, sys.argv[3:]) + sort_by, args = parse_args(sys.argv, USAGE, HELP_STRING) + left_dict = get_single_file_times(args[1]) + right_dict = get_single_file_times(args[2]) + table = make_diff_table_string(left_dict, right_dict, tag="Code", sort_by=sort_by) + print_or_write_table(table, args[3:]) diff --git a/tools/make-both-time-files.py b/tools/make-both-time-files.py index 69ec5a6631..f730a8d6bd 100755 --- a/tools/make-both-time-files.py +++ b/tools/make-both-time-files.py @@ -3,20 +3,14 @@ import sys from TimeFileMaker import * if __name__ == '__main__': - USAGE = 'Usage: %s AFTER_FILE_NAME BEFORE_FILE_NAME [OUTPUT_FILE_NAME ..]' % sys.argv[0] + USAGE = 'Usage: %s [--sort-by=auto|absolute|diff] AFTER_FILE_NAME BEFORE_FILE_NAME [OUTPUT_FILE_NAME ..]' % sys.argv[0] HELP_STRING = r'''Formats timing information from the output of two invocations of `make TIMED=1` into a sorted table. The input is expected to contain lines in the format: FILE_NAME (...user: NUMBER_IN_SECONDS...) ''' - if len(sys.argv) < 3 or '--help' in sys.argv[1:] or '-h' in sys.argv[1:]: - print(USAGE) - if '--help' in sys.argv[1:] or '-h' in sys.argv[1:]: - print(HELP_STRING) - if len(sys.argv) == 2: sys.exit(0) - sys.exit(1) - else: - left_dict = get_times(sys.argv[1]) - right_dict = get_times(sys.argv[2]) - table = make_diff_table_string(left_dict, right_dict) - print_or_write_table(table, sys.argv[3:]) + sort_by, args = parse_args(sys.argv, USAGE, HELP_STRING) + left_dict = get_times(args[1]) + right_dict = get_times(args[2]) + table = make_diff_table_string(left_dict, right_dict, sort_by=sort_by) + print_or_write_table(table, args[3:]) diff --git a/tools/md5sum.ml b/tools/md5sum.ml new file mode 100644 index 0000000000..2fdcacc839 --- /dev/null +++ b/tools/md5sum.ml @@ -0,0 +1,24 @@ +let get_content file = + let ic = open_in_bin file in + let buf = Buffer.create 2048 in + let rec fill () = + match input_char ic with + | '\r' -> fill () (* NOTE: handles the case on Windows where the + git checkout has included return characters. + See: https://github.com/coq/coq/pull/6305 *) + | c -> Buffer.add_char buf c; fill () + | exception End_of_file -> close_in ic; Buffer.contents buf + in + fill () + +let () = + match Sys.argv with + | [|_; file|] -> + let content = get_content file in + let md5 = Digest.to_hex (Digest.string content) in + print_string (md5 ^ " " ^ file) + | _ -> + prerr_endline "Error: This program needs exactly one parameter."; + prerr_endline "Usage: ocaml md5sum.ml <FILE>"; + prerr_endline "Print MD5 (128-bit) checksum of the file content modulo \\r."; + exit 1 |