From a665fd808b7fdaa11f84b35a87e0b8066cce1eda Mon Sep 17 00:00:00 2001 From: Pierre Boutillier Date: Fri, 20 Dec 2013 16:59:59 +0100 Subject: Coqdep always uses / as dir_sep --- Makefile.build | 12 ++++++------ man/coqdep.1 | 4 ---- myocamlbuild.ml | 2 +- tools/coq_makefile.ml | 8 ++++---- tools/coqdep.ml | 4 +++- tools/coqdep_boot.ml | 1 - tools/coqdep_common.ml | 16 ++++++++++++---- tools/coqdep_common.mli | 1 - 8 files changed, 26 insertions(+), 22 deletions(-) diff --git a/Makefile.build b/Makefile.build index 563c35595..f0a4f9c52 100644 --- a/Makefile.build +++ b/Makefile.build @@ -108,7 +108,7 @@ OCAMLOPT := $(TYPEREX) $(OCAMLOPT) $(CAMLFLAGS) BYTEFLAGS=$(CAMLDEBUG) $(USERFLAGS) OPTFLAGS=$(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) -DEPFLAGS= -slash $(LOCALINCLUDES) +DEPFLAGS= $(LOCALINCLUDES) define bestocaml $(if $(OPT),\ @@ -923,11 +923,11 @@ OCAMLDEP_NG = $(COQDEPBOOT) -mldep $(OCAMLDEP) checker/%.ml.d: $(D_DEPEND_BEFORE_SRC) checker/%.ml $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES) $(SHOW)'OCAMLDEP $<' - $(HIDE)$(OCAMLDEP_NG) -slash $(LOCALCHKLIBS) "$<" $(TOTARGET) + $(HIDE)$(OCAMLDEP_NG) $(LOCALCHKLIBS) "$<" $(TOTARGET) checker/%.mli.d: $(D_DEPEND_BEFORE_SRC) checker/%.mli $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES) $(SHOW)'OCAMLDEP $<' - $(HIDE)$(OCAMLDEP_NG) -slash $(LOCALCHKLIBS) "$<" $(TOTARGET) + $(HIDE)$(OCAMLDEP_NG) $(LOCALCHKLIBS) "$<" $(TOTARGET) %.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES) $(SHOW)'OCAMLDEP $<' @@ -939,15 +939,15 @@ checker/%.mli.d: $(D_DEPEND_BEFORE_SRC) checker/%.mli $(D_DEPEND_AFTER_SRC) $(CO checker/%.mllib.d: $(D_DEPEND_BEFORE_SRC) checker/%.mllib $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES) $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEPBOOT) -slash -I checker -c "$<" $(TOTARGET) + $(HIDE)$(COQDEPBOOT) -I checker -c "$<" $(TOTARGET) %.mllib.d: $(D_DEPEND_BEFORE_SRC) %.mllib $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES) $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEPBOOT) -slash -I kernel -I tools/coqdoc -c "$<" $(TOTARGET) + $(HIDE)$(COQDEPBOOT) -I kernel -I tools/coqdoc -c "$<" $(TOTARGET) %.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENVFILES) $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEPBOOT) $(DEPNATDYN) -slash "$<" $(TOTARGET) + $(HIDE)$(COQDEPBOOT) $(DEPNATDYN) "$<" $(TOTARGET) %_stubs.c.d: $(D_DEPEND_BEFORE_SRC) %_stubs.c $(D_DEPEND_AFTER_SRC) $(SHOW)'CCDEP $<' diff --git a/man/coqdep.1 b/man/coqdep.1 index e9e0dd3e3..5a6cd609e 100644 --- a/man/coqdep.1 +++ b/man/coqdep.1 @@ -78,10 +78,6 @@ of each Coq file given as argument and complete (if needed) the list of Caml modules. The new command is printed on the standard output. No dependency is computed with this option. .TP -.BI \-slash -Prints paths using a slash instead of the OS specific separator. This -option is useful when developping under Cygwin. -.TP .BI \-I \ directory The files .v .ml .mli of the directory .IR directory \& diff --git a/myocamlbuild.ml b/myocamlbuild.ml index 9a062220a..5669dccab 100644 --- a/myocamlbuild.ml +++ b/myocamlbuild.ml @@ -402,7 +402,7 @@ let extra_rules () = begin (fun env _ -> let v = env "%.v" and vd = env "%.v.depends" in (** NB: this relies on all .v files being already in _build. *) - Cmd (S [P coqdep_boot;dep_dynlink;A"-slash";P v;Sh">";Px vd])); + Cmd (S [P coqdep_boot;dep_dynlink;P v;Sh">";Px vd])); (** Coq files compilation *) diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index bd77bb1ba..bf2a09180 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -331,7 +331,7 @@ let implicit () = print "%.cmo: %.ml4\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n"; print "%.cmx: %.ml4\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n"; print "%.ml4.d: %.ml4\n"; - print "\t$(COQDEP) -slash $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in + print "\t$(COQDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in let ml_rules () = print "%.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; print "%.cmx: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; @@ -344,12 +344,12 @@ let implicit () = print "%.cma: | %.mllib\n\t$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n"; print "%.cmxa: | %.mllib\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n"; print "%.mllib.d: %.mllib\n"; - print "\t$(COQDEP) -slash $(COQLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in + print "\t$(COQDEP) $(COQLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in let mlpack_rules () = print "%.cmo: | %.mlpack\n\t$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^\n\n"; print "%.cmx: | %.mlpack\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^\n\n"; print "%.mlpack.d: %.mlpack\n"; - print "\t$(COQDEP) -slash $(COQLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"; + print "\t$(COQDEP) $(COQLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"; in let v_rules () = print "%.vo %.glob: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n"; @@ -360,7 +360,7 @@ in print "%.g.tex: %.v\n\t$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@\n\n"; print "%.g.html: %.v %.glob\n\t$(COQDOC) $(COQDOCFLAGS) -html -g $< -o $@\n\n"; print "%.v.d: %.v\n"; - print "\t$(COQDEP) -slash $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"; + print "\t$(COQDEP) $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"; print "%.v.beautified:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*\n\n" in if !some_mlifile then mli_rules (); diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 16e5bbde8..8a514f7f4 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -184,7 +184,9 @@ let rec parse = function | "-coqlib" :: [] -> usage () | "-suffix" :: s :: ll -> suffixe := s ; parse ll | "-suffix" :: [] -> usage () - | "-slash" :: ll -> option_slash := true; parse ll + | "-slash" :: ll -> + Printf.eprintf "warning: option -slash has no effect and is deprecated."; + parse ll | ("-h"|"--help"|"-help") :: _ -> usage () | f :: ll -> treat_file None f; parse ll | [] -> () diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml index 15fcdc600..588bf2dcf 100644 --- a/tools/coqdep_boot.ml +++ b/tools/coqdep_boot.ml @@ -16,7 +16,6 @@ open Coqdep_common *) let rec parse = function - | "-slash" :: ll -> option_slash := true; parse ll | "-natdynlink" :: "no" :: ll -> option_natdynlk := false; parse ll | "-c" :: ll -> option_c := true; parse ll | "-boot" :: ll -> parse ll (* We're already in boot mode by default *) diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 8c5e5b1ee..759b0cf96 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -22,7 +22,6 @@ let stdout = Pervasives.stdout let option_c = ref false let option_noglob = ref false -let option_slash = ref false let option_natdynlk = ref true let option_mldep = ref None @@ -33,9 +32,18 @@ let suffixe = ref ".vo" type dir = string option -(* filename for printing *) -let (//) s1 s2 = - if !option_slash then s1^"/"^s2 else Filename.concat s1 s2 +(* Filename.concat but always with a '/' *) +let is_dir_sep s i = + match Sys.os_type with + | "Unix" -> s.[i] = '/' + | "Cygwin" | "Win32" -> + let c = s.[i] in c = '/' || c = '\\' || c = ':' + +let (//) dirname filename = + let l = String.length dirname in + if l = 0 || is_dir_sep dirname (l-1) + then dirname ^ filename + else dirname ^ "/" ^ filename (** [get_extension f l] checks whether [f] has one of the extensions listed in [l]. It returns [f] without its extension, alongside with diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli index d9ca3ca81..37be010ea 100644 --- a/tools/coqdep_common.mli +++ b/tools/coqdep_common.mli @@ -8,7 +8,6 @@ val option_c : bool ref val option_noglob : bool ref -val option_slash : bool ref val option_natdynlk : bool ref val option_mldep : string option ref val norec_dirs : string list ref -- cgit v1.2.3