Permalink
Browse files

Coqdep always uses / as dir_sep

  • Loading branch information...
1 parent ca1305a commit a665fd808b7fdaa11f84b35a87e0b8066cce1eda @pirbo pirbo committed Dec 20, 2013
Showing with 26 additions and 22 deletions.
  1. +6 −6 Makefile.build
  2. +0 −4 man/coqdep.1
  3. +1 −1 myocamlbuild.ml
  4. +4 −4 tools/coq_makefile.ml
  5. +3 −1 tools/coqdep.ml
  6. +0 −1 tools/coqdep_boot.ml
  7. +12 −4 tools/coqdep_common.ml
  8. +0 −1 tools/coqdep_common.mli
View
@@ -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 $<'
View
@@ -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 \&
View
@@ -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 *)
View
@@ -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 ();
View
@@ -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
| [] -> ()
View
@@ -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 *)
View
@@ -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
View
@@ -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

0 comments on commit a665fd8

Please sign in to comment.