aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile.build12
-rw-r--r--man/coqdep.14
-rw-r--r--myocamlbuild.ml2
-rw-r--r--tools/coq_makefile.ml8
-rw-r--r--tools/coqdep.ml4
-rw-r--r--tools/coqdep_boot.ml1
-rw-r--r--tools/coqdep_common.ml16
-rw-r--r--tools/coqdep_common.mli1
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 04:49:18 +0000