summaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2016-12-27 16:53:30 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2016-12-27 16:53:30 +0100
commita4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch)
tree26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /tools
parent164c6861860e6b52818c031f901ffeff91fca16a (diff)
Imported Upstream version 8.6upstream/8.6
Diffstat (limited to 'tools')
-rw-r--r--tools/compat5.ml13
-rw-r--r--tools/compat5.mlp23
-rw-r--r--tools/compat5b.ml13
-rw-r--r--tools/compat5b.mlp23
-rw-r--r--tools/coq_makefile.ml393
-rw-r--r--tools/coqc.ml29
-rw-r--r--tools/coqdep.ml19
-rw-r--r--tools/coqdep_common.ml95
-rw-r--r--tools/coqdep_common.mli8
-rw-r--r--tools/coqdep_lexer.mll126
-rw-r--r--tools/coqdoc/cpretty.mll235
-rw-r--r--tools/coqdoc/index.ml26
-rw-r--r--tools/coqdoc/output.ml3
-rw-r--r--tools/coqmktop.ml17
-rw-r--r--tools/fake_ide.ml37
-rw-r--r--tools/ocamllibdep.mll217
16 files changed, 724 insertions, 553 deletions
diff --git a/tools/compat5.ml b/tools/compat5.ml
deleted file mode 100644
index 33c1cd60..00000000
--- a/tools/compat5.ml
+++ /dev/null
@@ -1,13 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(* This file is meant for camlp5, for which there is nothing to
- add to gain camlp5 compatibility :-).
-
- See [compat5.mlp] for the [camlp4] counterpart
-*)
diff --git a/tools/compat5.mlp b/tools/compat5.mlp
deleted file mode 100644
index 8473a1fb..00000000
--- a/tools/compat5.mlp
+++ /dev/null
@@ -1,23 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(** Adding a bit of camlp5 syntax to camlp4 for compatibility:
- - GEXTEND ... becomes EXTEND ...
-*)
-
-open Camlp4.PreCast
-
-let rec my_token_filter = parser
- | [< '(KEYWORD "GEXTEND", loc); s >] ->
- [< '(KEYWORD "EXTEND", loc); my_token_filter s >]
- | [< 'tokloc; s >] -> [< 'tokloc; my_token_filter s >]
- | [< >] -> [< >]
-
-let _ =
- Token.Filter.define_filter (Gram.get_filter())
- (fun prev strm -> prev (my_token_filter strm))
diff --git a/tools/compat5b.ml b/tools/compat5b.ml
deleted file mode 100644
index 37cb487c..00000000
--- a/tools/compat5b.ml
+++ /dev/null
@@ -1,13 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(* This file is meant for camlp5, for which there is nothing to
- add to gain camlp5 compatibility :-).
-
- See [compat5b.mlp] for the [camlp4] counterpart
-*)
diff --git a/tools/compat5b.mlp b/tools/compat5b.mlp
deleted file mode 100644
index 46802a82..00000000
--- a/tools/compat5b.mlp
+++ /dev/null
@@ -1,23 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(** Adding a bit of camlp5 syntax to camlp4 for compatibility:
- - EXTEND ... becomes EXTEND Gram ...
-*)
-
-open Camlp4.PreCast
-
-let rec my_token_filter = parser
- | [< '(KEYWORD "EXTEND",_ as t); s >] ->
- [< 't; '(UIDENT "Gram", Loc.ghost); my_token_filter s >]
- | [< 'tokloc; s >] -> [< 'tokloc; my_token_filter s >]
- | [< >] -> [< >]
-
-let _ =
- Token.Filter.define_filter (Gram.get_filter())
- (fun prev strm -> prev (my_token_filter strm))
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 478cf887..eab909f5 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -27,8 +27,9 @@ let rec print_list sep = function
| x :: l -> print x; print sep; print_list sep l
| [] -> ()
-let list_iter_i f =
- let rec aux i = function [] -> () | a::l -> f i a; aux (i+1) l in aux 1
+let rec print_prefix_list sep = function
+ | x :: l -> print sep; print x; print_prefix_list sep l
+ | [] -> ()
let section s =
let l = String.length s in
@@ -43,6 +44,17 @@ let section s =
print_com (String.make (l+2) '#');
print "\n"
+(* These are the Coq library directories that are used for
+ * plugin development
+ *)
+let lib_dirs =
+ ["kernel"; "lib"; "library"; "parsing";
+ "pretyping"; "interp"; "printing"; "intf";
+ "proofs"; "tactics"; "tools"; "ltacprof";
+ "toplevel"; "stm"; "grammar"; "config";
+ "ltac"; "engine"]
+
+
let usage () =
output_string stderr "Usage summary:
@@ -93,17 +105,28 @@ let is_genrule r = (* generic rule (like bar%foo: ...) *)
Str.string_match genrule r 0
let string_prefix a b =
- let rec aux i = try if a.[i] = b.[i] then aux (i+1) else i with |Invalid_argument _ -> i in
- String.sub a 0 (aux 0)
+ let rec aux i =
+ try if a.[i] = b.[i] then aux (i+1) else i with Invalid_argument _ -> i
+ in
+ String.sub a 0 (aux 0)
let is_prefix dir1 dir2 =
let l1 = String.length dir1 in
let l2 = String.length dir2 in
- dir1 = dir2 || (l1 < l2 && String.sub dir2 0 l1 = dir1 && dir2.[l1] = '/')
+ let sep = Filename.dir_sep in
+ if dir1 = dir2 then true
+ else if l1 + String.length sep <= l2 then
+ let dir1' = String.sub dir2 0 l1 in
+ let sep' = String.sub dir2 l1 (String.length sep) in
+ dir1' = dir1 && sep' = sep
+ else false
let physical_dir_of_logical_dir ldir =
let le = String.length ldir - 1 in
- let pdir = if le >= 0 && ldir.[le] = '.' then String.sub ldir 0 (le - 1) else String.copy ldir in
+ let pdir =
+ if le >= 0 && ldir.[le] = '.' then String.sub ldir 0 (le - 1)
+ else String.copy ldir
+ in
for i = 0 to le - 1 do
if pdir.[i] = '.' then pdir.[i] <- '/';
done;
@@ -118,62 +141,74 @@ let standard opt =
print "\"\n\n"
let classify_files_by_root var files (inc_ml,inc_i,inc_r) =
- if not (List.exists (fun (pdir,_,_) -> pdir = ".") inc_r)
- && not (List.exists (fun (pdir,_,_) -> pdir = ".") inc_i) then
- begin
- let absdir_of_files = List.rev_map
+ if List.exists (fun (pdir,_,_) -> pdir = ".") inc_r ||
+ List.exists (fun (pdir,_,_) -> pdir = ".") inc_i
+ then ()
+ else
+ let absdir_of_files =List.rev_map
(fun x -> CUnix.canonical_path_name (Filename.dirname x))
- files in
- (* files in scope of a -I option (assuming they are no overlapping) *)
- let has_inc_i = List.exists (fun (_,a) -> List.mem a absdir_of_files) inc_ml in
- if has_inc_i then
- begin
- printf "%sINC=" var;
- List.iter (fun (pdir,absdir) ->
- if List.mem absdir absdir_of_files
- then printf
- "$(filter $(wildcard %s/*),$(%s)) "
- pdir var
- ) inc_ml;
- printf "\n";
- end;
- (* Files in the scope of a -R option (assuming they are disjoint) *)
- list_iter_i (fun i (pdir,_,abspdir) ->
- if List.exists (is_prefix abspdir) absdir_of_files then
- printf "%s%d=$(patsubst %s/%%,%%,$(filter %s/%%,$(%s)))\n"
- var i pdir pdir var)
- (inc_i@inc_r);
- end
+ files
+ in
+ (* files in scope of a -I option (assuming they are no overlapping) *)
+ if List.exists (fun (_,a) -> List.mem a absdir_of_files) inc_ml then
+ begin
+ printf "%sINC=" var;
+ List.iter (fun (pdir,absdir) ->
+ if List.mem absdir absdir_of_files
+ then printf "$(filter $(wildcard %s/*),$(%s)) " pdir var)
+ inc_ml;
+ printf "\n";
+ end;
+ (* Files in the scope of a -R option (assuming they are disjoint) *)
+ List.iteri (fun i (pdir,_,abspdir) ->
+ if List.exists (is_prefix abspdir) absdir_of_files then
+ printf "%s%d=$(patsubst %s/%%,%%,$(filter %s/%%,$(%s)))\n"
+ var i pdir pdir var)
+ (inc_i@inc_r)
let vars_to_put_by_root var_x_files_l (inc_ml,inc_i,inc_r) =
- let var_x_absdirs_l = List.rev_map
- (fun (v,l) -> (v,List.rev_map (fun x -> CUnix.canonical_path_name (Filename.dirname x)) l))
- var_x_files_l in
- let var_filter f g = List.fold_left (fun acc (var,dirs) ->
- if f dirs
- then (g var)::acc else acc) [] var_x_absdirs_l in
- (* All files caught by a -R . option (assuming it is the only one) *)
+ let var_x_absdirs_l =
+ List.rev_map
+ (fun (v,l) ->
+ (v,List.rev_map
+ (fun x -> CUnix.canonical_path_name (Filename.dirname x)) l))
+ var_x_files_l
+ in
+ let var_filter f g =
+ List.fold_left
+ (fun acc (var,dirs) -> if f dirs then (g var)::acc else acc)
+ [] var_x_absdirs_l
+ in
+ (* All files caught by a -R . option (assuming it is the only one) *)
match inc_i@inc_r with
- |[(".",t,_)] -> (None,[".",physical_dir_of_logical_dir t,List.rev_map fst var_x_files_l])
+ |[(".",t,_)] ->
+ (None,[".",physical_dir_of_logical_dir t,List.rev_map fst var_x_files_l])
|l ->
try
let out = List.assoc "." (List.rev_map (fun (p,l,_) -> (p,l)) l) in
- let () = prerr_string "Warning: install rule assumes that -R/-Q . _ is the only -R/-Q option\n" in
+ let () = prerr_string "Warning: install rule assumes that -R/-Q . _ is the only -R/-Q option\n"
+ in
(None,[".",physical_dir_of_logical_dir out,List.rev_map fst var_x_files_l])
with Not_found ->
- (
(* vars for -Q options *)
- Some (var_filter (fun l -> List.exists (fun (_,a) -> List.mem a l) inc_ml) (fun x -> x)),
+ let varq = var_filter
+ (fun l -> List.exists (fun (_,a) -> List.mem a l) inc_ml)
+ (fun x -> x)
+ in
(* (physical dir, physical dir of logical path,vars) for -R options
(assuming physical dirs are disjoint) *)
- if l = [] then
- [".","$(INSTALLDEFAULTROOT)",[]]
- else
- Util.List.fold_left_i (fun i out (pdir,ldir,abspdir) ->
- let vars_r = var_filter (List.exists (is_prefix abspdir)) (fun x -> x^string_of_int i) in
- let pdir' = physical_dir_of_logical_dir ldir in
- (pdir,pdir',vars_r)::out) 1 [] l
- )
+ let other =
+ if l = [] then
+ [".","$(INSTALLDEFAULTROOT)",[]]
+ else
+ Util.List.fold_left_i (fun i out (pdir,ldir,abspdir) ->
+ let vars_r = var_filter
+ (List.exists (is_prefix abspdir))
+ (fun x -> x^string_of_int i)
+ in
+ let pdir' = physical_dir_of_logical_dir ldir in
+ (pdir,pdir',vars_r)::out) 0 [] l
+ in (Some varq, other)
let install_include_by_root perms =
let install_dir for_i (pdir,pdir',vars) =
@@ -249,33 +284,38 @@ let where_put_doc = function
install-doc will put anything in $INSTALLDEFAULTROOT\n" in
"$(INSTALLDEFAULTROOT)"
-let install (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,sds) inc = function
+let install (vfiles,(mlis,ml4s,mls,mllibs,mlpacks),_,sds) inc = function
|Project_file.NoInstall -> ()
|is_install ->
let not_empty = function |[] -> false |_::_ -> true in
- let cmofiles = List.rev_append mlpackfiles (List.rev_append mlfiles ml4files) in
- let cmifiles = List.rev_append mlifiles cmofiles in
- let cmxsfiles = List.rev_append cmofiles mllibfiles in
- let where_what_cmxs = vars_to_put_by_root [("CMXSFILES",cmxsfiles)] inc in
+ let cmos = List.rev_append mlpacks (List.rev_append mls ml4s) in
+ let cmis = List.rev_append mlis cmos in
+ let cmxss = List.rev_append cmos mllibs in
+ let where_what_cmxs = vars_to_put_by_root [("CMXSFILES",cmxss)] inc in
let where_what_oth = vars_to_put_by_root
- [("VOFILES",vfiles);("VFILES",vfiles);("GLOBFILES",vfiles);("NATIVEFILES",vfiles);("CMOFILES",cmofiles);("CMIFILES",cmifiles);("CMAFILES",mllibfiles)]
+ [("VOFILES",vfiles);("VFILES",vfiles);
+ ("GLOBFILES",vfiles);("NATIVEFILES",vfiles);
+ ("CMOFILES",cmos);("CMIFILES",cmis);("CMAFILES",mllibs)]
inc in
let doc_dir = where_put_doc inc in
- let () = if is_install = Project_file.UnspecInstall then
- print "userinstall:\n\t+$(MAKE) USERINSTALL=true install\n\n" in
- if (not_empty cmxsfiles) then begin
+ if is_install = Project_file.UnspecInstall then begin
+ print "userinstall:\n\t+$(MAKE) USERINSTALL=true install\n\n"
+ end;
+ if not_empty cmxss then begin
print "install-natdynlink:\n";
install_include_by_root "0755" where_what_cmxs;
print "\n";
end;
- if (not_empty cmxsfiles) then begin
+ if not_empty cmxss then begin
print "install-toploop: $(MLLIBFILES:.mllib=.cmxs)\n";
printf "\t install -d \"$(DSTROOT)\"$(COQTOPINSTALL)/\n";
printf "\t install -m 0755 $? \"$(DSTROOT)\"$(COQTOPINSTALL)/\n";
print "\n";
end;
print "install:";
- if (not_empty cmxsfiles) then print "$(if $(HASNATDYNLINK_OR_EMPTY),install-natdynlink)";
+ if not_empty cmxss then begin
+ print "$(if $(HASNATDYNLINK_OR_EMPTY),install-natdynlink)";
+ end;
print "\n";
install_include_by_root "0644" where_what_oth;
List.iter
@@ -290,7 +330,7 @@ let install (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,sds) in
print "\tdone\n" in
print "install-doc:\n";
if not_empty vfiles then install_one_kind "html" doc_dir;
- if not_empty mlifiles then install_one_kind "mlihtml" doc_dir;
+ if not_empty mlis then install_one_kind "mlihtml" doc_dir;
print "\n";
let uninstall_one_kind kind dir =
printf "\tprintf 'cd \"$${DSTROOT}\"$(COQDOCINSTALL)/%s \\\\\\n' >> \"$@\"\n" dir;
@@ -300,10 +340,10 @@ let install (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,sds) in
in
printf "uninstall_me.sh: %s\n" !makefile_name;
print "\techo '#!/bin/sh' > $@\n";
- if (not_empty cmxsfiles) then uninstall_by_root where_what_cmxs;
+ if not_empty cmxss then uninstall_by_root where_what_cmxs;
uninstall_by_root where_what_oth;
if not_empty vfiles then uninstall_one_kind "html" doc_dir;
- if not_empty mlifiles then uninstall_one_kind "mlihtml" doc_dir;
+ if not_empty mlis then uninstall_one_kind "mlihtml" doc_dir;
print "\tchmod +x $@\n";
print "\n";
print "uninstall: uninstall_me.sh\n";
@@ -322,11 +362,14 @@ let make_makefile sds =
let clean sds sps =
print "clean::\n";
- if !some_mlfile || !some_mlifile || !some_ml4file || !some_mllibfile || !some_mlpackfile then begin
- print "\trm -f $(ALLCMOFILES) $(CMIFILES) $(CMAFILES)\n";
- print "\trm -f $(ALLCMOFILES:.cmo=.cmx) $(CMXAFILES) $(CMXSFILES) $(ALLCMOFILES:.cmo=.o) $(CMXAFILES:.cmxa=.a)\n";
- print "\trm -f $(addsuffix .d,$(MLFILES) $(MLIFILES) $(ML4FILES) $(MLLIBFILES) $(MLPACKFILES))\n";
- end;
+ if !some_mlfile || !some_mlifile || !some_ml4file
+ || !some_mllibfile || !some_mlpackfile
+ then
+ begin
+ print "\trm -f $(ALLCMOFILES) $(CMIFILES) $(CMAFILES)\n";
+ print "\trm -f $(ALLCMOFILES:.cmo=.cmx) $(CMXAFILES) $(CMXSFILES) $(ALLCMOFILES:.cmo=.o) $(CMXAFILES:.cmxa=.a)\n";
+ print "\trm -f $(addsuffix .d,$(MLFILES) $(MLIFILES) $(ML4FILES) $(MLLIBFILES) $(MLPACKFILES))\n";
+ end;
if !some_vfile then
begin
print "\trm -f $(OBJFILES) $(OBJFILES:.o=.native) $(NATIVEFILES)\n";
@@ -355,7 +398,7 @@ let clean sds sps =
sds;
print "\n";
print "printenv:\n\t@\"$(COQBIN)coqtop\" -config\n";
- print "\t@echo 'CAMLC =\t$(CAMLC)'\n\t@echo 'CAMLOPTC =\t$(CAMLOPTC)'\n\t@echo 'PP =\t$(PP)'\n\t@echo 'COQFLAGS =\t$(COQFLAGS)'\n";
+ print "\t@echo 'OCAMLFIND =\t$(OCAMLFIND)'\n\t@echo 'PP =\t$(PP)'\n\t@echo 'COQFLAGS =\t$(COQFLAGS)'\n";
print "\t@echo 'COQLIBINSTALL =\t$(COQLIBINSTALL)'\n\t@echo 'COQDOCINSTALL =\t$(COQDOCINSTALL)'\n\n"
let header_includes () = ()
@@ -363,48 +406,78 @@ let header_includes () = ()
let implicit () =
section "Implicit rules.";
let mli_rules () =
- print "$(MLIFILES:.mli=.cmi): %.cmi: %.mli\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
+ print "$(MLIFILES:.mli=.cmi): %.cmi: %.mli\n";
+ print "\t$(SHOW)'CAMLC -c $<'\n";
+ print "\t$(HIDE)$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
print "$(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli\n";
- print "\t$(OCAMLDEP) -slash $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
+ print "\t$(SHOW)'CAMLDEP $<'\n";
+ print "\t$(HIDE)$(CAMLDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"
+ in
let ml4_rules () =
- print "$(ML4FILES:.ml4=.cmo): %.cmo: %.ml4\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n";
+ print "$(ML4FILES:.ml4=.cmo): %.cmo: %.ml4\n";
+ print "\t$(SHOW)'CAMLC -pp -c $<'\n";
+ print "\t$(HIDE)$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n";
print "$(filter-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(ML4FILES:.ml4=.cmx)): %.cmx: %.ml4\n";
- print "\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n";
+ print "\t$(SHOW)'CAMLOPT -pp -c $<'\n";
+ print "\t$(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n";
print "$(addsuffix .d,$(ML4FILES)): %.ml4.d: %.ml4\n";
- print "\t$(OCAMLDEP) -slash $(OCAMLLIBS) $(PP) -impl \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
+ print "\t$(SHOW)'CAMLDEP -pp $<'\n";
+ print "\t$(HIDE)$(CAMLDEP) $(OCAMLLIBS) $(PP) -impl \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
let ml_rules () =
- print "$(MLFILES:.ml=.cmo): %.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
+ print "$(MLFILES:.ml=.cmo): %.cmo: %.ml\n";
+ print "\t$(SHOW)'CAMLC -c $<'\n";
+ print "\t$(HIDE)$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
print "$(filter-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(MLFILES:.ml=.cmx)): %.cmx: %.ml\n";
- print "\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
+ print "\t$(SHOW)'CAMLOPT -c $<'\n";
+ print "\t$(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
print "$(addsuffix .d,$(MLFILES)): %.ml.d: %.ml\n";
- print "\t$(OCAMLDEP) -slash $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
+ print "\t$(SHOW)'CAMLDEP $<'\n";
+ print "\t$(HIDE)$(CAMLDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
let cmxs_rules () = (* order is important here when there is foo.ml and foo.mllib *)
- print "$(filter-out $(MLLIBFILES:.mllib=.cmxs),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs) $(MLPACKFILES:.mlpack=.cmxs)): %.cmxs: %.cmx
-\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $<\n\n";
- print "$(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -linkall -shared -o $@ $<\n\n" in
+ print "$(filter-out $(MLLIBFILES:.mllib=.cmxs),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs) $(MLPACKFILES:.mlpack=.cmxs)): %.cmxs: %.cmx\n";
+ print "\t$(SHOW)'CAMLOPT -shared -o $@'\n";
+ print "\t$(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $<\n\n";
+ print "$(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa\n";
+ print "\t$(SHOW)'CAMLOPT -shared -o $@'\n";
+ print "\t$(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -linkall -shared -o $@ $<\n\n"
+ in
let mllib_rules () =
- print "$(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib\n\t$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n";
- print "$(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n";
+ print "$(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib\n";
+ print "\t$(SHOW)'CAMLC -a -o $@'\n";
+ print "\t$(HIDE)$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n";
+ print "$(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib\n";
+ print "\t$(SHOW)'CAMLOPT -a -o $@'\n";
+ print "\t$(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n";
print "$(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib\n";
- print "\t$(COQDEP) $(OCAMLLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
+ print "\t$(SHOW)'COQDEP $<'\n";
+ print "\t$(HIDE)$(COQDEP) $(OCAMLLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"
+ in
let mlpack_rules () =
- print "$(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack\n\t$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^\n\n";
- print "$(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^\n\n";
+ print "$(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack\n";
+ print "\t$(SHOW)'CAMLC -pack -o $@'\n";
+ print "\t$(HIDE)$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^\n\n";
+ print "$(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack\n";
+ print "\t$(SHOW)'CAMLOPT -pack -o $@'\n";
+ print "\t$(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^\n\n";
print "$(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack\n";
- print "\t$(COQDEP) $(OCAMLLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n";
-in
+ print "\t$(SHOW)'COQDEP $<'\n";
+ print "\t$(HIDE)$(COQDEP) $(OCAMLLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"
+ in
let v_rules () =
- print "$(VOFILES): %.vo: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n";
- print "$(GLOBFILES): %.glob: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n";
- print "$(VFILES:.v=.vio): %.vio: %.v\n\t$(COQC) -quick $(COQDEBUG) $(COQFLAGS) $*\n\n";
+ print "$(VOFILES): %.vo: %.v\n";
+ print "\t$(SHOW)COQC $<\n";
+ print "\t$(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) $<\n\n";
+ print "$(GLOBFILES): %.glob: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $<\n\n";
+ print "$(VFILES:.v=.vio): %.vio: %.v\n\t$(COQC) -quick $(COQDEBUG) $(COQFLAGS) $<\n\n";
print "$(GFILES): %.g: %.v\n\t$(GALLINA) $<\n\n";
print "$(VFILES:.v=.tex): %.tex: %.v\n\t$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@\n\n";
print "$(HTMLFILES): %.html: %.v %.glob\n\t$(COQDOC) $(COQDOCFLAGS) -html $< -o $@\n\n";
print "$(VFILES:.v=.g.tex): %.g.tex: %.v\n\t$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@\n\n";
print "$(GHTMLFILES): %.g.html: %.v %.glob\n\t$(COQDOC) $(COQDOCFLAGS) -html -g $< -o $@\n\n";
print "$(addsuffix .d,$(VFILES)): %.v.d: %.v\n";
- print "\t$(COQDEP) $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n";
- print "$(addsuffix .beautified,$(VFILES)): %.v.beautified:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*\n\n"
+ print "\t$(SHOW)'COQDEP $<'\n";
+ print "\t$(HIDE)$(COQDEP) $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n";
+ print "$(addsuffix .beautified,$(VFILES)): %.v.beautified:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*.v\n\n"
in
if !some_mlifile then mli_rules ();
if !some_ml4file then ml4_rules ();
@@ -446,26 +519,24 @@ let variables is_install opt (args,defs) =
end;
(* Caml executables and relative variables *)
if !some_ml4file || !some_mlfile || !some_mlifile then begin
- print "COQSRCLIBS?=-I \"$(COQLIB)kernel\" -I \"$(COQLIB)lib\" \\
- -I \"$(COQLIB)library\" -I \"$(COQLIB)parsing\" -I \"$(COQLIB)pretyping\" \\
- -I \"$(COQLIB)interp\" -I \"$(COQLIB)printing\" -I \"$(COQLIB)intf\" \\
- -I \"$(COQLIB)proofs\" -I \"$(COQLIB)tactics\" -I \"$(COQLIB)tools\" \\
- -I \"$(COQLIB)toplevel\" -I \"$(COQLIB)stm\" -I \"$(COQLIB)grammar\" \\
- -I \"$(COQLIB)config\"";
+ print "COQSRCLIBS?=" ;
+ List.iter (fun c -> print "-I \"$(COQLIB)"; print c ; print "\" \\\n") lib_dirs ;
List.iter (fun c -> print " \\
-I \"$(COQLIB)/"; print c; print "\"") Coq_config.plugins_dirs; print "\n";
print "ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)\n\n";
- print "CAMLC?=$(OCAMLC) -c -rectypes -thread\n";
- print "CAMLOPTC?=$(OCAMLOPT) -c -rectypes -thread\n";
- print "CAMLLINK?=$(OCAMLC) -rectypes -thread\n";
- print "CAMLOPTLINK?=$(OCAMLOPT) -rectypes -thread\n";
+ print "CAMLC?=$(OCAMLFIND) ocamlc -c -rectypes -thread\n";
+ print "CAMLOPTC?=$(OCAMLFIND) opt -c -rectypes -thread\n";
+ print "CAMLLINK?=$(OCAMLFIND) ocamlc -rectypes -thread\n";
+ print "CAMLOPTLINK?=$(OCAMLFIND) opt -rectypes -thread\n";
+ print "CAMLDEP?=$(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack\n";
+ print "CAMLLIB?=$(shell $(OCAMLFIND) printconf stdlib)\n";
print "GRAMMARS?=grammar.cma\n";
print "ifeq ($(CAMLP4),camlp5)
-CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma
+CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo
else
-CAMLP4EXTEND=threads.cma
+CAMLP4EXTEND=
endif\n";
- print "PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(CAMLLIB)threads/ $(COQSRCLIBS) compat5.cmo \\
+ print "PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(COQLIB)/grammar compat5.cmo \\
$(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'\n\n";
end;
match is_install with
@@ -502,39 +573,50 @@ let parameters () =
print "# TIMECMD set a command to log .v compilation time;\n";
print "# TIMED if non empty, use the default time command as TIMECMD;\n";
print "# ZDEBUG/COQDEBUG to specify debug flags for ocamlc&ocamlopt/coqc;\n";
- print "# DSTROOT to specify a prefix to install path.\n\n";
+ print "# DSTROOT to specify a prefix to install path.\n";
+ print "# VERBOSE to disable the short display of compilation rules.\n\n";
+ print "VERBOSE?=\n";
+ print "SHOW := $(if $(VERBOSE),@true \"\",@echo \"\")\n";
+ print "HIDE := $(if $(VERBOSE),,@)\n\n";
print "# Here is a hack to make $(eval $(shell works:\n";
print "define donewline\n\n\nendef\n";
print "includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr -d '\\r' | tr '\\n' '@'; })))\n";
print "$(call includecmdwithout@,$(COQBIN)coqtop -config)\n\n";
- print "TIMED=\nTIMECMD=\nSTDTIME?=/usr/bin/time -f \"$* (user: %U mem: %M ko)\"\n";
+ print "TIMED?=\nTIMECMD?=\nSTDTIME?=/usr/bin/time -f \"$* (user: %U mem: %M ko)\"\n";
print "TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))\n\n";
print "vo_to_obj = $(addsuffix .o,\\\n";
print " $(filter-out Warning: Error:,\\\n";
print " $(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(1))))\n\n"
-let include_dirs (inc_ml,inc_i,inc_r) =
+let include_dirs (inc_ml,inc_q,inc_r) =
let parse_ml_includes l = List.map (fun (x,_) -> "-I \"" ^ x ^ "\"") l in
- let parse_includes l = List.map (fun (x,l,_) ->
- let l' = if l = "" then "\"\"" else l in
- "-Q \"" ^ x ^ "\" " ^ l' ^"") l in
- let parse_rec_includes l = List.map (fun (p,l,_) ->
- let l' = if l = "" then "\"\"" else l in
- "-R \"" ^ p ^ "\" " ^ l' ^"") l in
+ let includes =
+ List.map (fun (p,l,_) ->
+ let l' = if l = "" then "\"\"" else l in
+ " \"" ^ p ^ "\" " ^ l' ^"") in
let str_ml = parse_ml_includes inc_ml in
- let str_i = parse_includes inc_i in
- let str_r = parse_rec_includes inc_r in
- section "Libraries definitions.";
- if !some_ml4file || !some_mlfile || !some_mlifile then begin
- print "OCAMLLIBS?="; print_list "\\\n " str_ml; print "\n";
- end;
- if !some_vfile || !some_mllibfile || !some_mlpackfile then begin
- print "COQLIBS?="; print_list "\\\n " str_i;
- List.iter (fun x -> print "\\\n "; print x) str_r;
- List.iter (fun x -> print "\\\n "; print x) str_ml; print "\n";
- print "COQDOCLIBS?="; print_list "\\\n " str_i;
- List.iter (fun x -> print "\\\n "; print x) str_r; print "\n\n";
- end
+ section "Libraries definitions.";
+ if !some_ml4file || !some_mlfile || !some_mlifile then begin
+ print "OCAMLLIBS?="; print_list "\\\n " str_ml; print "\n";
+ end;
+ if !some_vfile || !some_mllibfile || !some_mlpackfile then begin
+ print "COQLIBS?=";
+ print_prefix_list "\\\n -Q" (includes inc_q);
+ print_prefix_list "\\\n -R" (includes inc_r);
+ print_prefix_list "\\\n " str_ml;
+ print "\n";
+ end;
+ if !some_vfile then begin
+ print "COQCHKLIBS?=";
+ print_prefix_list "\\\n -R" (includes inc_q);
+ print_prefix_list "\\\n -R" (includes inc_r);
+ print "\n";
+ print "COQDOCLIBS?=";
+ print_prefix_list "\\\n -R" (includes inc_q);
+ print_prefix_list "\\\n -R" (includes inc_r);
+ print "\n";
+ end;
+ print "\n"
let double_colon = ["clean"; "cleanall"; "archclean"]
@@ -565,10 +647,13 @@ let forpacks l =
let () = if l <> [] then section "Ad-hoc implicit rules for mlpack." in
List.iter (fun it ->
let h = Filename.chop_extension it in
+ let pk = String.capitalize (Filename.basename h) in
printf "$(addsuffix .cmx,$(filter $(basename $(MLFILES)),$(%s_MLPACK_DEPENDENCIES))): %%.cmx: %%.ml\n" h;
- printf "\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -for-pack %s $<\n\n" (String.capitalize (Filename.basename h));
+ printf "\t$(SHOW)'CAMLOPT -c -for-pack %s $<'\n" pk;
+ printf "\t$(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -for-pack %s $<\n\n" pk;
printf "$(addsuffix .cmx,$(filter $(basename $(ML4FILES)),$(%s_MLPACK_DEPENDENCIES))): %%.cmx: %%.ml4\n" h;
- printf "\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -for-pack %s $(PP) -impl $<\n\n" (String.capitalize (Filename.basename h))
+ printf "\t$(SHOW)'CAMLOPT -c -pp -for-pack %s $<'\n" pk;
+ printf "\t$(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -for-pack %s $(PP) -impl $<\n\n" pk
) l
let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other_targets inc =
@@ -682,9 +767,9 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other
begin
print "mlihtml: $(MLIFILES:.mli=.cmi)\n";
print "\t mkdir $@ || rm -rf $@/*\n";
- print "\t$(OCAMLDOC) -html -rectypes -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
+ print "\t$(OCAMLFIND) ocamldoc -html -rectypes -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
print "all-mli.tex: $(MLIFILES:.mli=.cmi)\n";
- print "\t$(OCAMLDOC) -latex -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
+ print "\t$(OCAMLFIND) ocamldoc -latex -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
end;
if !some_vfile then
begin
@@ -707,7 +792,7 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other
print "all-gal.pdf: $(VFILES)\n";
print "\t$(COQDOC) -toc $(COQDOCFLAGS) -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n";
print "validate: $(VOFILES)\n";
- print "\t$(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $(notdir $(^:.vo=))\n\n";
+ print "\t$(COQCHK) $(COQCHKFLAGS) $(COQCHKLIBS) $(notdir $(^:.vo=))\n\n";
print "beautify: $(VFILES:=.beautified)\n";
print "\tfor file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done\n";
print "\t@echo \'Do not do \"make clean\" until you are sure that everything went well!\'\n";
@@ -760,22 +845,24 @@ let command_line args =
print_list args;
print "\n#\n\n"
-let ensure_root_dir (v,(mli,ml4,ml,mllib,mlpack),_,_) ((ml_inc,i_inc,r_inc) as l) =
+let ensure_root_dir (vfiles,(mlis,ml4s,mls,mllibs,mlpacks),_,_) inc =
+ let (ml_inc,i_inc,r_inc) = inc in
let here = Sys.getcwd () in
- let not_tops =List.for_all (fun s -> s <> Filename.basename s) in
+ let not_tops = List.for_all (fun s -> s <> Filename.basename s) in
if List.exists (fun (_,_,x) -> x = here) i_inc
|| List.exists (fun (_,_,x) -> is_prefix x here) r_inc
- || (not_tops v && not_tops mli && not_tops ml4 && not_tops ml
- && not_tops mllib && not_tops mlpack) then
- l
+ || (not_tops vfiles && not_tops mlis && not_tops ml4s && not_tops mls
+ && not_tops mllibs && not_tops mlpacks)
+ then
+ inc
else
((".",here)::ml_inc,i_inc,(".","Top",here)::r_inc)
-let warn_install_at_root_directory
- (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,_) (inc_ml,inc_i,inc_r) =
+let warn_install_at_root_directory (vfiles,(mlis,ml4s,mls,mllibs,mlpacks),_,_) inc =
+ let (inc_ml,inc_i,inc_r) = inc in
let inc_top = List.filter (fun (_,ldir,_) -> ldir = "") (inc_r@inc_i) in
let inc_top_p = List.map (fun (p,_,_) -> p) inc_top in
- let files = vfiles @ mlifiles @ ml4files @ mlfiles @ mllibfiles @ mlpackfiles in
+ let files = vfiles @ mlis @ ml4s @ mls @ mllibs @ mlpacks in
if List.exists (fun f -> List.mem (Filename.dirname f) inc_top_p) files
then
Printf.eprintf "Warning: install target will copy files at the first level of the coq contributions installation directory; option -R or -Q %sis recommended\n"
@@ -793,12 +880,29 @@ let check_overlapping_include (_,inc_i,inc_r) =
Printf.eprintf "Warning: in options -R/-Q, %s and %s overlap\n" pdir pdir') l;
in aux (inc_i@inc_r)
+(* Generate a .merlin file that references the standard library and
+ * any -I included paths.
+ *)
+let merlin targets (ml_inc,_,_) =
+ print ".merlin:\n";
+ print "\t@echo 'FLG -rectypes' > .merlin\n" ;
+ List.iter (fun c ->
+ printf "\t@echo \"B $(COQLIB)%s\" >> .merlin\n" c)
+ lib_dirs ;
+ List.iter (fun (_,c) ->
+ printf "\t@echo \"B %s\" >> .merlin\n" c;
+ printf "\t@echo \"S %s\" >> .merlin\n" c)
+ ml_inc;
+ print "\n"
+
let do_makefile args =
let has_file var = function
|[] -> var := false
|_::_ -> var := true in
let (project_file,makefile,is_install,opt),l =
- try Project_file.process_cmd_line Filename.current_dir_name (None,None,Project_file.UnspecInstall,true) [] args
+ try
+ Project_file.process_cmd_line Filename.current_dir_name
+ (None,None,Project_file.UnspecInstall,true) [] args
with Project_file.Parsing_error -> usage () in
let (v_f,(mli_f,ml4_f,ml_f,mllib_f,mlpack_f),sps,sds as targets), inc, defs =
Project_file.split_arguments l in
@@ -822,7 +926,9 @@ let do_makefile args =
List.iter check_dep (Str.split (Str.regexp "[ \t]+") dependencies)) sps;
let inc = ensure_root_dir targets inc in
- if is_install <> Project_file.NoInstall then warn_install_at_root_directory targets inc;
+ if is_install <> Project_file.NoInstall then begin
+ warn_install_at_root_directory targets inc;
+ end;
check_overlapping_include inc;
banner ();
header_includes ();
@@ -835,6 +941,7 @@ let do_makefile args =
section "Special targets.";
standard opt;
install targets inc is_install;
+ merlin targets inc;
clean sds sps;
make_makefile sds;
implicit ();
diff --git a/tools/coqc.ml b/tools/coqc.ml
index b7910e13..b12d4871 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -70,17 +70,6 @@ let parse_args () =
| "-byte" :: rem -> binary := "coqtop.byte"; parse (cfiles,args) rem
| "-opt" :: rem -> binary := "coqtop"; parse (cfiles,args) rem
-(* Obsolete options *)
-
- | "-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
-
(* Informative options *)
| ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
@@ -99,13 +88,12 @@ let parse_args () =
(* Options for coqtop : a) options with 0 argument *)
- | ("-notactics"|"-bt"|"-debug"|"-nolib"|"-boot"|"-time"
+ | ("-notactics"|"-bt"|"-debug"|"-nolib"|"-boot"|"-time"|"-profile-ltac"
|"-batch"|"-noinit"|"-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"|"-native-compiler"
- |"-verbose-compat-notations"|"-no-compat-notations"
|"-indices-matter"|"-quick"|"-type-in-type"
|"-async-proofs-always-delegate"|"-async-proofs-never-reopen-branch"
as o) :: rem ->
@@ -118,27 +106,18 @@ let parse_args () =
|"-load-ml-source"|"-require"|"-load-ml-object"
|"-init-file"|"-dump-glob"|"-compat"|"-coqlib"|"-top"
|"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs" |"-w"
+ |"-o"|"-profile-ltac-cutoff"
as o) :: rem ->
begin
match rem with
| s :: rem' -> parse (cfiles,s::o::args) rem'
| [] -> usage ()
end
+ | ("-I"|"-include" as o) :: s :: rem -> parse (cfiles,s::o::args) rem
(* Options for coqtop : c) options with 1 argument and possibly more *)
- | ("-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
- | "-Q" :: s :: t :: rem -> parse (cfiles,t::s::"-Q"::args) rem
+ | ("-R"|"-Q" as o) :: s :: t :: rem -> parse (cfiles,t::s::o::args) rem
| ("-schedule-vio-checking"
|"-check-vio-tasks" | "-schedule-vio2vo" as o) :: s :: rem ->
let nodash, rem =
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 79662a5d..a7c32e1d 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -9,6 +9,7 @@
open Printf
open Coqdep_lexer
open Coqdep_common
+open System
(** The basic parts of coqdep (i.e. the parts used by [coqdep -boot])
are now in [Coqdep_common]. The code that remains here concerns
@@ -459,21 +460,14 @@ let rec parse = function
| "-boot" :: ll -> option_boot := true; parse ll
| "-sort" :: ll -> option_sort := true; parse ll
| ("-noglob" | "-no-glob") :: ll -> option_noglob := true; parse ll
- | "-I" :: r :: "-as" :: ln :: ll ->
- add_rec_dir_no_import add_known r [];
- add_rec_dir_no_import add_known r (split_period ln);
- parse ll
- | "-I" :: r :: "-as" :: [] -> usage ()
| "-I" :: r :: ll -> add_caml_dir r; parse ll
| "-I" :: [] -> usage ()
- | "-R" :: r :: "-as" :: ln :: ll -> add_rec_dir_import add_known r (split_period ln); parse ll
- | "-R" :: r :: "-as" :: [] -> usage ()
| "-R" :: r :: ln :: ll -> add_rec_dir_import add_known r (split_period ln); parse ll
| "-Q" :: r :: ln :: ll -> add_rec_dir_no_import add_known r (split_period ln); parse ll
| "-R" :: ([] | [_]) -> usage ()
| "-dumpgraph" :: f :: ll -> option_dump := Some (false, f); parse ll
| "-dumpgraphbox" :: f :: ll -> option_dump := Some (true, f); parse ll
- | "-exclude-dir" :: r :: ll -> norec_dirnames := StrSet.add r !norec_dirnames; parse ll
+ | "-exclude-dir" :: r :: ll -> System.exclude_directory r; parse ll
| "-exclude-dir" :: [] -> usage ()
| "-coqlib" :: r :: ll -> Flags.coqlib_spec := true; Flags.coqlib := r; parse ll
| "-coqlib" :: [] -> usage ()
@@ -497,17 +491,18 @@ let coqdep () =
if !option_boot then begin
add_rec_dir_import add_known "theories" ["Coq"];
add_rec_dir_import add_known "plugins" ["Coq"];
+ add_caml_dir "tactics";
add_rec_dir_import (fun _ -> add_caml_known) "theories" ["Coq"];
add_rec_dir_import (fun _ -> add_caml_known) "plugins" ["Coq"];
end else begin
- Envars.set_coqlib ~fail:Errors.error;
+ Envars.set_coqlib ~fail:CErrors.error;
let coqlib = Envars.coqlib () in
add_rec_dir_import add_coqlib_known (coqlib//"theories") ["Coq"];
add_rec_dir_import add_coqlib_known (coqlib//"plugins") ["Coq"];
let user = coqlib//"user-contrib" in
if Sys.file_exists user then add_rec_dir_no_import add_coqlib_known user [];
List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s [])
- (Envars.xdg_dirs (fun x -> Pp.msg_warning (Pp.str x)));
+ (Envars.xdg_dirs (fun x -> Feedback.msg_warning (Pp.str x)));
List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s []) Envars.coqpath;
end;
List.iter (fun (f,d) -> add_mli_known f d ".mli") !mliAccu;
@@ -530,6 +525,6 @@ let coqdep () =
let _ =
try
coqdep ()
- with Errors.UserError(s,p) ->
+ with CErrors.UserError(s,p) ->
let pp = if s <> "_" then Pp.(str s ++ str ": " ++ p) else p in
- Pp.msgerrnl pp
+ Feedback.msg_error pp
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 58c8e884..0064aebd 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -9,10 +9,11 @@
open Printf
open Coqdep_lexer
open Unix
+open Minisys
(** [coqdep_boot] is a stripped-down version of [coqdep], whose
behavior is the one of [coqdep -boot]. Its only dependencies
- are [Coqdep_lexer] and [Unix], and it should stay so.
+ are [Coqdep_lexer], [Unix] and [Minisys], and it should stay so.
If it need someday some additional information, pass it via
options (see for instance [option_natdynlk] below).
*)
@@ -32,26 +33,11 @@ let option_boot = ref false
let option_mldep = ref None
let norec_dirs = ref StrSet.empty
-let norec_dirnames = ref (List.fold_right StrSet.add ["CVS"; "_darcs"] StrSet.empty)
let suffixe = ref ".vo"
type dir = string option
-(* 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 = ':'
- | _ -> assert false
-
-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
the extension. When no extension match, [(f,"")] is returned *)
@@ -179,11 +165,6 @@ let warning_module_notfound f s =
eprintf "*** Warning: in file %s, library %s is required and has not been found in the loadpath!\n%!"
f (String.concat "." s)
-let warning_notfound f s =
- eprintf "*** Warning: in file %s, the file " f;
- eprintf "%s.v is required and has not been found!\n" s;
- flush stderr
-
let warning_declare f s =
eprintf "*** Warning: in file %s, declared ML module " f;
eprintf "%s has not been found!\n" s;
@@ -203,6 +184,10 @@ let warning_clash file dir =
eprintf "%s and %s; used the latter)\n" d2 d1
| _ -> assert false
+let warning_cannot_open_dir dir =
+ eprintf "*** Warning: cannot open %s\n" dir;
+ flush stderr
+
let safe_assoc from verbose file k =
if verbose && StrListMap.mem k !clash_v then warning_clash file k;
match search_v_known ?from k with
@@ -460,7 +445,7 @@ let mL_dependencies () =
let efullname = escape fullname in
printf "%s_MLLIB_DEPENDENCIES:=%s\n" efullname dep;
printf "%s.cma:$(addsuffix .cmo,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname;
- printf "%s.cmxa %s.cmxs:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname efullname;
+ printf "%s.cmxa:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname;
flush stdout)
(List.rev !mllibAccu);
List.iter
@@ -470,7 +455,7 @@ let mL_dependencies () =
let efullname = escape fullname in
printf "%s_MLPACK_DEPENDENCIES:=%s\n" efullname dep;
printf "%s.cmo:$(addsuffix .cmo,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname;
- printf "%s.cmx %s.cmxs:$(addsuffix .cmx,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname efullname;
+ printf "%s.cmx:$(addsuffix .cmx,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname;
flush stdout)
(List.rev !mlpackAccu)
@@ -504,15 +489,15 @@ let add_caml_known phys_dir _ f =
| _ -> ()
let add_coqlib_known recur phys_dir log_dir f =
- match get_extension f [".vo"] with
- | (basename,".vo") ->
+ match get_extension f [".vo"; ".vio"] with
+ | (basename, (".vo" | ".vio")) ->
let name = log_dir@[basename] in
let paths = if recur then suffixes name else [name] in
List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths
| _ -> ()
let add_known recur phys_dir log_dir f =
- match get_extension f [".v";".vo"] with
+ match get_extension f [".v"; ".vo"; ".vio"] with
| (basename,".v") ->
let name = log_dir@[basename] in
let file = phys_dir//basename in
@@ -521,37 +506,30 @@ let add_known recur phys_dir log_dir f =
let paths = List.tl (suffixes name) in
let iter n = safe_hash_add compare_file clash_v vKnown (n, (file, false)) in
List.iter iter paths
- | (basename,".vo") when not(!option_boot) ->
+ | (basename, (".vo" | ".vio")) when not(!option_boot) ->
let name = log_dir@[basename] in
let paths = if recur then suffixes name else [name] in
List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths
| _ -> ()
-(** Visit directory [phys_dir] (recursively unless [recur=false]) and
- apply function add_file to each regular file encountered.
- [log_dir] is the logical name of the [phys_dir].
- [add_file] takes both directory names and the file. *)
+(* Visits all the directories under [dir], including [dir] *)
+
+let is_not_seen_directory phys_f =
+ not (StrSet.mem phys_f !norec_dirs)
+
let rec add_directory recur add_file phys_dir log_dir =
- let dirh = opendir phys_dir in
register_dir_logpath phys_dir log_dir;
- try
- while true do
- let f = readdir dirh in
- (* we avoid all files and subdirs starting by '.' (e.g. .svn),
- plus CVS and _darcs and any subdirs given via -exclude-dirs *)
- if f.[0] <> '.' then
- let phys_f = if phys_dir = "." then f else phys_dir//f in
- match try (stat phys_f).st_kind with _ -> S_BLK with
- | S_DIR when recur ->
- if StrSet.mem f !norec_dirnames then ()
- else
- if StrSet.mem phys_f !norec_dirs then ()
- else (* TODO: warn if already seen this physycal dir? *)
- add_directory recur add_file phys_f (log_dir@[f])
- | S_REG -> add_file phys_dir log_dir f
- | _ -> ()
- done
- with End_of_file -> closedir dirh
+ let f = function
+ | FileDir (phys_f,f) ->
+ if is_not_seen_directory phys_f && recur then
+ add_directory true add_file phys_f (log_dir @ [f])
+ | FileRegular f ->
+ add_file phys_dir log_dir f
+ in
+ if exists_dir phys_dir then
+ process_directory f phys_dir
+ else
+ warning_cannot_open_dir phys_dir
(** Simply add this directory and imports it, no subdirs. This is used
by the implicit adding of the current path (which is not recursive). *)
@@ -564,12 +542,18 @@ let add_rec_dir_no_import add_file phys_dir log_dir =
(** -R semantic: go in subdirs and suffixes of logical paths are known. *)
let add_rec_dir_import add_file phys_dir log_dir =
- handle_unix_error (add_directory true (add_file true) phys_dir) log_dir
+ add_directory true (add_file true) phys_dir log_dir
+
+(** -R semantic but only on immediate capitalized subdirs *)
+
+let add_rec_uppercase_subdirs add_file phys_dir log_dir =
+ process_subdirectories (fun phys_dir f ->
+ add_directory true (add_file true) phys_dir (log_dir@[String.capitalize f]))
+ phys_dir
(** -I semantic: do not go in subdirs. *)
let add_caml_dir phys_dir =
- handle_unix_error (add_directory false add_caml_known phys_dir) []
-
+ add_directory false add_caml_known phys_dir []
let rec treat_file old_dirname old_name =
let name = Filename.basename old_name
@@ -584,15 +568,12 @@ let rec treat_file old_dirname old_name =
match try (stat complete_name).st_kind with _ -> S_BLK with
| S_DIR ->
(if name.[0] <> '.' then
- let dir=opendir complete_name in
let newdirname =
match dirname with
| None -> name
| Some d -> d//name
in
- try
- while true do treat_file (Some newdirname) (readdir dir) done
- with End_of_file -> closedir dir)
+ Array.iter (treat_file (Some newdirname)) (Sys.readdir complete_name))
| S_REG ->
(match get_extension name [".v";".ml";".mli";".ml4";".mllib";".mlpack"] with
| (base,".v") ->
diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli
index 97bdfaef..633c474a 100644
--- a/tools/coqdep_common.mli
+++ b/tools/coqdep_common.mli
@@ -22,10 +22,8 @@ val option_boot : bool ref
val option_natdynlk : bool ref
val option_mldep : string option ref
val norec_dirs : StrSet.t ref
-val norec_dirnames : StrSet.t ref
val suffixe : string ref
type dir = string option
-val ( // ) : string -> string -> string
val get_extension : string -> string list -> string * string
val basename_noext : string -> string
val mlAccu : (string * string * dir) list ref
@@ -51,9 +49,6 @@ val suffixes : 'a list -> 'a list list
val add_known : bool -> string -> string list -> string -> unit
val add_coqlib_known : bool -> string -> string list -> string -> unit
val add_caml_known : string -> string list -> string -> unit
-val add_directory :
- bool ->
- (string -> string list -> string -> unit) -> string -> string list -> unit
val add_caml_dir : string -> unit
(** Simply add this directory and imports it, no subdirs. This is used
@@ -69,5 +64,8 @@ val add_rec_dir_no_import :
val add_rec_dir_import :
(bool -> string -> string list -> string -> unit) -> string -> string list -> unit
+val add_rec_uppercase_subdirs :
+ (bool -> string -> string list -> string -> unit) -> string -> string list -> unit
+
val treat_file : dir -> string -> unit
val error_cannot_parse : string -> int * int -> 'a
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
index b16dd338..eb233b8f 100644
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -25,13 +25,6 @@
exception Fin_fichier
exception Syntax_error of int*int
- let module_current_name = ref []
- let module_names = ref []
- let ml_module_name = ref ""
- let loadpath = ref ""
-
- let mllist = ref ([] : string list)
-
let field_name s = String.sub s 1 (String.length s - 1)
let unquote_string s =
@@ -46,11 +39,6 @@
let syntax_error lexbuf =
raise (Syntax_error (Lexing.lexeme_start lexbuf, Lexing.lexeme_end lexbuf))
-
- (** This is the prefix that should be pre-prepended to files due to the use
- ** of [From], i.e. [From Xxx... Require ...]
- **)
- let from_pre_ident = ref None
}
let space = [' ' '\t' '\n' '\r']
@@ -81,9 +69,9 @@ let dot = '.' ( space+ | eof)
rule coq_action = parse
| "Require" space+
- { require_modifiers lexbuf }
+ { require_modifiers None lexbuf }
| "Local"? "Declare" space+ "ML" space+ "Module" space+
- { mllist := []; modules lexbuf }
+ { modules [] lexbuf }
| "Load" space+
{ load_file lexbuf }
| "Add" space+ "LoadPath" space+
@@ -109,38 +97,34 @@ and from_rule = parse
| space+
{ from_rule lexbuf }
| coq_ident
- { module_current_name := [Lexing.lexeme lexbuf];
- from_pre_ident := Some (coq_qual_id_tail lexbuf);
- module_names := [];
- consume_require lexbuf }
+ { let from = coq_qual_id_tail [Lexing.lexeme lexbuf] lexbuf in
+ consume_require (Some from) lexbuf }
| eof
{ syntax_error lexbuf }
| _
{ syntax_error lexbuf }
-and require_modifiers = parse
+and require_modifiers from = parse
| "(*"
- { comment lexbuf; require_modifiers lexbuf }
+ { comment lexbuf; require_modifiers from lexbuf }
| "Import" space+
- { require_file lexbuf }
+ { require_file from lexbuf }
| "Export" space+
- { require_file lexbuf }
+ { require_file from lexbuf }
| space+
- { require_modifiers lexbuf }
+ { require_modifiers from lexbuf }
| eof
{ syntax_error lexbuf }
| _
- { backtrack lexbuf ; require_file lexbuf }
+ { backtrack lexbuf ; require_file from lexbuf }
-and consume_require = parse
+and consume_require from = parse
| "(*"
- { comment lexbuf; consume_require lexbuf }
+ { comment lexbuf; consume_require from lexbuf }
| space+
- { consume_require lexbuf }
+ { consume_require from lexbuf }
| "Require" space+
- { require_modifiers lexbuf }
- | eof
- { syntax_error lexbuf }
+ { require_modifiers from lexbuf }
| _
{ syntax_error lexbuf }
@@ -152,20 +136,19 @@ and add_loadpath = parse
| eof
{ syntax_error lexbuf }
| '"' [^ '"']* '"' (*'"'*)
- { loadpath := unquote_string (lexeme lexbuf);
- add_loadpath_as lexbuf }
+ { add_loadpath_as (unquote_string (lexeme lexbuf)) lexbuf }
-and add_loadpath_as = parse
+and add_loadpath_as path = parse
| "(*"
- { comment lexbuf; add_loadpath_as lexbuf }
+ { comment lexbuf; add_loadpath_as path lexbuf }
| space+
- { add_loadpath_as lexbuf }
+ { add_loadpath_as path lexbuf }
| "as"
{ let qid = coq_qual_id lexbuf in
skip_to_dot lexbuf;
- AddRecLoadPath (!loadpath,qid) }
+ AddRecLoadPath (path, qid) }
| dot
- { AddLoadPath !loadpath }
+ { AddLoadPath path }
and caml_action = parse
| space +
@@ -176,8 +159,7 @@ and caml_action = parse
{ caml_action lexbuf }
| caml_low_ident { caml_action lexbuf }
| caml_up_ident
- { ml_module_name := Lexing.lexeme lexbuf;
- qual_id lexbuf }
+ { qual_id (Lexing.lexeme lexbuf) lexbuf }
| ['0'-'9']+
| '0' ['x' 'X'] ['0'-'9' 'A'-'F' 'a'-'f']+
| '0' ['o' 'O'] ['0'-'7']+
@@ -260,18 +242,15 @@ and load_file = parse
| _
{ syntax_error lexbuf }
-and require_file = parse
+and require_file from = parse
| "(*"
- { comment lexbuf; require_file lexbuf }
+ { comment lexbuf; require_file from lexbuf }
| space+
- { require_file lexbuf }
+ { require_file from lexbuf }
| coq_ident
- { module_current_name := [Lexing.lexeme lexbuf];
- module_names := [coq_qual_id_tail lexbuf];
- let qid = coq_qual_id_list lexbuf in
+ { let name = coq_qual_id_tail [Lexing.lexeme lexbuf] lexbuf in
+ let qid = coq_qual_id_list [name] lexbuf in
parse_dot lexbuf;
- let from = !from_pre_ident in
- from_pre_ident := None;
Require (from, qid) }
| eof
{ syntax_error lexbuf }
@@ -294,66 +273,55 @@ and coq_qual_id = parse
| space+
{ coq_qual_id lexbuf }
| coq_ident
- { module_current_name := [Lexing.lexeme lexbuf];
- coq_qual_id_tail lexbuf }
- | eof
- { syntax_error lexbuf }
+ { coq_qual_id_tail [Lexing.lexeme lexbuf] lexbuf }
| _
- { backtrack lexbuf;
- let qid = List.rev !module_current_name in
- module_current_name := [];
- qid }
+ { syntax_error lexbuf }
-and coq_qual_id_tail = parse
+and coq_qual_id_tail module_name = parse
| "(*"
- { comment lexbuf; coq_qual_id_tail lexbuf }
+ { comment lexbuf; coq_qual_id_tail module_name lexbuf }
| space+
- { coq_qual_id_tail lexbuf }
+ { coq_qual_id_tail module_name lexbuf }
| coq_field
- { module_current_name :=
- field_name (Lexing.lexeme lexbuf) :: !module_current_name;
- coq_qual_id_tail lexbuf }
+ { coq_qual_id_tail (field_name (Lexing.lexeme lexbuf) :: module_name) lexbuf }
| eof
{ syntax_error lexbuf }
| _
{ backtrack lexbuf;
- let qid = List.rev !module_current_name in
- module_current_name := [];
- qid }
+ List.rev module_name }
-and coq_qual_id_list = parse
+and coq_qual_id_list module_names = parse
| "(*"
- { comment lexbuf; coq_qual_id_list lexbuf }
+ { comment lexbuf; coq_qual_id_list module_names lexbuf }
| space+
- { coq_qual_id_list lexbuf }
+ { coq_qual_id_list module_names lexbuf }
| coq_ident
- { module_current_name := [Lexing.lexeme lexbuf];
- module_names := coq_qual_id_tail lexbuf :: !module_names;
- coq_qual_id_list lexbuf
+ { let name = coq_qual_id_tail [Lexing.lexeme lexbuf] lexbuf in
+ coq_qual_id_list (name :: module_names) lexbuf
}
| eof
{ syntax_error lexbuf }
| _
{ backtrack lexbuf;
- List.rev !module_names }
+ List.rev module_names }
-and modules = parse
+and modules mllist = parse
| space+
- { modules lexbuf }
+ { modules mllist lexbuf }
| "(*"
- { comment lexbuf; modules lexbuf }
+ { comment lexbuf; modules mllist lexbuf }
| '"' [^'"']* '"'
{ let lex = (Lexing.lexeme lexbuf) in
let str = String.sub lex 1 (String.length lex - 2) in
- mllist := str :: !mllist; modules lexbuf}
+ modules (str :: mllist) lexbuf}
| eof
{ syntax_error lexbuf }
| _
- { (Declare (List.rev !mllist)) }
+ { Declare (List.rev mllist) }
-and qual_id = parse
- | '.' [^ '.' '(' '['] {
- Use_module (String.uncapitalize !ml_module_name) }
+and qual_id ml_module_name = parse
+ | '.' [^ '.' '(' '[']
+ { Use_module (String.uncapitalize ml_module_name) }
| eof { raise Fin_fichier }
| _ { caml_action lexbuf }
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 431080c6..919f37b9 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -75,7 +75,7 @@
let stop_env () = if !r then stop (); r := false in
(fun x -> !r), start_env, stop_env
- let in_emph, start_emph, stop_emph = in_env Output.start_emph Output.stop_emph
+ let _, start_emph, stop_emph = in_env Output.start_emph Output.stop_emph
let in_quote, start_quote, stop_quote = in_env Output.start_quote Output.stop_quote
let url_buffer = Buffer.create 40
@@ -111,12 +111,6 @@
Cdglobals.gallina := s.st_gallina;
Cdglobals.light := s.st_light
- let without_ref r f x = save_state (); r := false; f x; restore_state ()
-
- let without_gallina = without_ref Cdglobals.gallina
-
- let without_light = without_ref Cdglobals.light
-
let begin_show () = save_state (); Cdglobals.gallina := false; Cdglobals.light := false
let end_show () = restore_state ()
@@ -245,6 +239,12 @@
let s = String.sub s isp (String.length s - isp) in
Output.keyword s (lexeme_start lexbuf + isp)
+ let only_gallina () =
+ !Cdglobals.gallina && !in_proof <> None
+
+ let parse_comments () =
+ !Cdglobals.parse_comments && not (only_gallina ())
+
}
(*s Regular expressions *)
@@ -486,7 +486,7 @@ rule coq_bol = parse
in if eol then coq_bol lexbuf else coq lexbuf }
| space* end_kw {
let eol =
- if not (!in_proof <> None && !Cdglobals.gallina) then
+ if not (only_gallina ()) then
begin backtrack lexbuf; body_bol lexbuf end
else skip_to_dot lexbuf
in
@@ -535,14 +535,15 @@ rule coq_bol = parse
coq_bol lexbuf }
| space* "(*"
{ comment_level := 1;
- if !Cdglobals.parse_comments then begin
- let s = lexeme lexbuf in
- let nbsp,isp = count_spaces s in
- Output.indentation nbsp;
- Output.start_comment ();
- end;
- let eol = comment lexbuf in
- if eol then coq_bol lexbuf else coq lexbuf }
+ let eol =
+ if parse_comments () then begin
+ let s = lexeme lexbuf in
+ let nbsp, isp = count_spaces s in
+ Output.indentation nbsp;
+ Output.start_comment ();
+ comment lexbuf
+ end else skipped_comment lexbuf in
+ if eol then coq_bol lexbuf else coq lexbuf }
| eof
{ () }
| _
@@ -550,7 +551,7 @@ rule coq_bol = parse
if not !Cdglobals.gallina then
begin backtrack lexbuf; body_bol lexbuf end
else
- skip_to_dot lexbuf
+ skip_to_dot_or_brace lexbuf
in
if eol then coq_bol lexbuf else coq lexbuf }
@@ -558,7 +559,7 @@ rule coq_bol = parse
and coq = parse
| nl
- { if not (!in_proof <> None && !Cdglobals.gallina) then Output.line_break(); coq_bol lexbuf }
+ { if not (only_gallina ()) then Output.line_break(); coq_bol lexbuf }
| "(**" space_nl
{ Output.end_coq (); Output.start_doc ();
let eol = doc_bol lexbuf in
@@ -566,16 +567,12 @@ and coq = parse
if eol then coq_bol lexbuf else coq lexbuf }
| "(*"
{ comment_level := 1;
- if !Cdglobals.parse_comments then begin
- let s = lexeme lexbuf in
- let nbsp,isp = count_spaces s in
- Output.indentation nbsp;
- Output.start_comment ();
- end;
- let eol = comment lexbuf in
- if eol then coq_bol lexbuf
- else coq lexbuf
- }
+ let eol =
+ if parse_comments () then begin
+ Output.start_comment ();
+ comment lexbuf
+ end else skipped_comment lexbuf in
+ if eol then coq_bol lexbuf else coq lexbuf }
| nl+ space* "]]"
{ if not !formatted then
begin
@@ -650,7 +647,7 @@ and coq = parse
if not !Cdglobals.gallina then
begin backtrack lexbuf; body lexbuf end
else
- skip_to_dot lexbuf
+ skip_to_dot_or_brace lexbuf
in
if eol then coq_bol lexbuf else coq lexbuf}
@@ -678,7 +675,7 @@ and doc_bol = parse
in
match check_start_list line with
| Neither -> backtrack_past_newline lexbuf; doc None lexbuf
- | List n -> Output.paragraph ();
+ | List n -> if lines > 0 then Output.paragraph ();
Output.item 1; doc (Some [n]) lexbuf
| Rule -> Output.rule (); doc None lexbuf
}
@@ -739,24 +736,7 @@ and doc_list_bol indents = parse
in
let (n_spaces,_) = count_spaces buf in
match find_level indents n_spaces with
- | InLevel _ ->
- Output.paragraph ();
- backtrack_past_newline lexbuf;
- doc_list_bol indents lexbuf
- | StartLevel n ->
- if n = 1 then
- begin
- Output.stop_item ();
- backtrack_past_newline lexbuf;
- doc_bol lexbuf
- end
- else
- begin
- Output.paragraph ();
- backtrack_past_newline lexbuf;
- doc_list_bol indents lexbuf
- end
- | Before ->
+ | StartLevel 1 | Before ->
(* Here we were at the beginning of a line, and it was blank.
The next line started before any list items. So: insert
a paragraph for the empty line, rewind to whatever's just
@@ -766,6 +746,10 @@ and doc_list_bol indents = parse
Output.paragraph ();
backtrack_past_newline lexbuf;
doc_bol lexbuf
+ | StartLevel _ | InLevel _ ->
+ Output.paragraph ();
+ backtrack_past_newline lexbuf;
+ doc_list_bol indents lexbuf
}
| space* _
@@ -774,10 +758,7 @@ and doc_list_bol indents = parse
| Before -> Output.stop_item (); backtrack lexbuf;
doc_bol lexbuf
| StartLevel n ->
- (if n = 1 then
- Output.stop_item ()
- else
- Output.reach_item_level (n-1));
+ Output.reach_item_level (n-1);
backtrack lexbuf;
doc (Some (take (n-1) indents)) lexbuf
| InLevel (n,_) ->
@@ -820,9 +801,10 @@ and doc indents = parse
| Some is -> doc_list_bol is
| None -> doc_bol
in
- let eol = comment lexbuf in
- if eol then bol_parse lexbuf else doc indents lexbuf
- }
+ let eol =
+ if !Cdglobals.parse_comments then comment lexbuf
+ else skipped_comment lexbuf in
+ if eol then bol_parse lexbuf else doc indents lexbuf }
| '*'* "*)" space_nl* "(**"
{(match indents with
| Some _ -> Output.stop_item ()
@@ -941,7 +923,9 @@ and escaped_coq = parse
Output.sublexer_in_doc '['; escaped_coq lexbuf }
| "(*"
{ Tokens.flush_sublexer (); comment_level := 1;
- ignore (comment lexbuf); escaped_coq lexbuf }
+ ignore (if !Cdglobals.parse_comments then comment lexbuf
+ else skipped_comment lexbuf);
+ escaped_coq lexbuf }
| "*)"
{ (* likely to be a syntax error: we escape *) backtrack lexbuf }
| eof
@@ -981,76 +965,101 @@ and comments = parse
| _
{ Output.char (lexeme_char lexbuf 0); comments lexbuf }
-(*s Skip comments *)
+and skipped_comment = parse
+ | "(*"
+ { incr comment_level;
+ skipped_comment lexbuf }
+ | "*)" space* nl
+ { decr comment_level;
+ if !comment_level > 0 then skipped_comment lexbuf else true }
+ | "*)"
+ { decr comment_level;
+ if !comment_level > 0 then skipped_comment lexbuf else false }
+ | eof { false }
+ | _ { skipped_comment lexbuf }
and comment = parse
- | "(*" { incr comment_level;
- if !Cdglobals.parse_comments then Output.start_comment ();
- comment lexbuf }
- | "*)" space* nl {
- if !Cdglobals.parse_comments then
- (Output.end_comment (); Output.line_break ());
- decr comment_level; if !comment_level > 0 then comment lexbuf else true }
- | "*)" {
- if !Cdglobals.parse_comments then (Output.end_comment ());
- decr comment_level; if !comment_level > 0 then comment lexbuf else false }
- | "[" {
- if !Cdglobals.parse_comments then
- if !Cdglobals.plain_comments then Output.char '['
+ | "(*"
+ { incr comment_level;
+ Output.start_comment ();
+ comment lexbuf }
+ | "*)" space* nl
+ { Output.end_comment ();
+ Output.line_break ();
+ decr comment_level;
+ if !comment_level > 0 then comment lexbuf else true }
+ | "*)"
+ { Output.end_comment ();
+ decr comment_level;
+ if !comment_level > 0 then comment lexbuf else false }
+ | "["
+ { if !Cdglobals.plain_comments then Output.char '['
else (brackets := 1; Output.start_inline_coq ();
escaped_coq lexbuf; Output.end_inline_coq ());
- comment lexbuf }
- | "[[" nl {
- if !Cdglobals.parse_comments then
- if !Cdglobals.plain_comments then (Output.char '['; Output.char '[')
+ comment lexbuf }
+ | "[[" nl
+ { if !Cdglobals.plain_comments then (Output.char '['; Output.char '[')
else (formatted := true;
Output.start_inline_coq_block ();
let _ = body_bol lexbuf in
Output.end_inline_coq_block (); formatted := false);
- comment lexbuf}
+ comment lexbuf }
| "$"
- { if !Cdglobals.parse_comments then
- if !Cdglobals.plain_comments then Output.char '$'
- else (Output.start_latex_math (); escaped_math_latex lexbuf);
+ { if !Cdglobals.plain_comments then Output.char '$'
+ else (Output.start_latex_math (); escaped_math_latex lexbuf);
comment lexbuf }
| "$$"
- { if !Cdglobals.parse_comments
- then
- (if !Cdglobals.plain_comments then Output.char '$'; Output.char '$');
- doc None lexbuf }
+ { if !Cdglobals.plain_comments then Output.char '$';
+ Output.char '$';
+ comment lexbuf }
| "%"
- { if !Cdglobals.parse_comments
- then
- if !Cdglobals.plain_comments then Output.char '%'
- else escaped_latex lexbuf; comment lexbuf }
+ { if !Cdglobals.plain_comments then Output.char '%'
+ else escaped_latex lexbuf;
+ comment lexbuf }
| "%%"
- { if !Cdglobals.parse_comments
- then
- (if !Cdglobals.plain_comments then Output.char '%'; Output.char '%');
+ { if !Cdglobals.plain_comments then Output.char '%';
+ Output.char '%';
comment lexbuf }
| "#"
- { if !Cdglobals.parse_comments
- then
- if !Cdglobals.plain_comments then Output.char '$'
- else escaped_html lexbuf; comment lexbuf }
+ { if !Cdglobals.plain_comments then Output.char '#'
+ else escaped_html lexbuf;
+ comment lexbuf }
| "##"
- { if !Cdglobals.parse_comments
- then
- (if !Cdglobals.plain_comments then Output.char '#'; Output.char '#');
+ { if !Cdglobals.plain_comments then Output.char '#';
+ Output.char '#';
comment lexbuf }
| eof { false }
- | space+ { if !Cdglobals.parse_comments
- then Output.indentation (fst (count_spaces (lexeme lexbuf)));
- comment lexbuf }
- | nl { if !Cdglobals.parse_comments
- then Output.line_break (); comment lexbuf }
- | _ { if !Cdglobals.parse_comments then Output.char (lexeme_char lexbuf 0);
- comment lexbuf }
+ | space+
+ { Output.indentation (fst (count_spaces (lexeme lexbuf)));
+ comment lexbuf }
+ | nl
+ { Output.line_break ();
+ comment lexbuf }
+ | _ { Output.char (lexeme_char lexbuf 0);
+ comment lexbuf }
and skip_to_dot = parse
| '.' space* nl { true }
| eof | '.' space+ { false }
- | "(*" { comment_level := 1; ignore (comment lexbuf); skip_to_dot lexbuf }
+ | "(*"
+ { comment_level := 1;
+ ignore (skipped_comment lexbuf);
+ skip_to_dot lexbuf }
+ | _ { skip_to_dot lexbuf }
+
+and skip_to_dot_or_brace = parse
+ | '.' space* nl { true }
+ | eof | '.' space+ { false }
+ | "(*"
+ { comment_level := 1;
+ ignore (skipped_comment lexbuf);
+ skip_to_dot_or_brace lexbuf }
+ | "}" space* nl
+ { true }
+ | "}"
+ { false }
+ | space*
+ { skip_to_dot_or_brace lexbuf }
| _ { skip_to_dot lexbuf }
and body_bol = parse
@@ -1120,12 +1129,18 @@ and body = parse
let eol = doc_bol lexbuf in
Output.end_doc (); Output.start_coq ();
if eol then body_bol lexbuf else body lexbuf }
- | "(*" { Tokens.flush_sublexer(); comment_level := 1;
- if !Cdglobals.parse_comments then Output.start_comment ();
- let eol = comment lexbuf in
- if eol
- then begin if not !Cdglobals.parse_comments then Output.line_break(); body_bol lexbuf end
- else body lexbuf }
+ | "(*"
+ { Tokens.flush_sublexer(); comment_level := 1;
+ let eol =
+ if parse_comments () then begin
+ Output.start_comment ();
+ comment lexbuf
+ end else begin
+ let eol = skipped_comment lexbuf in
+ if eol then Output.line_break();
+ eol
+ end in
+ if eol then body_bol lexbuf else body lexbuf }
| "where"
{ Tokens.flush_sublexer();
Output.ident (lexeme lexbuf) None;
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index 47acc7b4..9be791a8 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.ml
@@ -77,32 +77,6 @@ let find m l = Hashtbl.find reftable (m, l)
let find_string m s = let (m,s,t) = Hashtbl.find byidtable s in Ref (m,s,t)
-(*s Manipulating path prefixes *)
-
-type stack = string list
-
-let rec string_of_stack st =
- match st with
- | [] -> ""
- | x::[] -> x
- | x::tl -> (string_of_stack tl) ^ "." ^ x
-
-let empty_stack = []
-
-let module_stack = ref empty_stack
-let section_stack = ref empty_stack
-
-let push st p = st := p::!st
-let pop st =
- match !st with
- | [] -> ()
- | _::tl -> st := tl
-
-let head st =
- match st with
- | [] -> ""
- | x::_ -> x
-
(* Coq modules *)
let split_sp s =
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 2b269096..82d3d62b 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -953,7 +953,7 @@ module TeXmacs = struct
(*s Latex preamble *)
- let (preamble : string Queue.t) =
+ let (_ : string Queue.t) =
in_doc := false; Queue.create ()
let header () =
@@ -1122,7 +1122,6 @@ module Raw = struct
for i = 0 to String.length s - 1 do char s.[i] done
let start_module () = ()
- let end_module () = ()
let start_latex_math () = ()
let stop_latex_math () = ()
diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml
index a45c625b..eaf938e8 100644
--- a/tools/coqmktop.ml
+++ b/tools/coqmktop.ml
@@ -149,7 +149,7 @@ 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 -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\
@@ -167,8 +167,8 @@ let parse_args () =
(* Directories *)
| "-coqlib" :: d :: rem ->
Flags.coqlib_spec := true; Flags.coqlib := d ; parse (op,fl) rem
- | "-camlbin" :: d :: rem ->
- Flags.camlbin_spec := true; Flags.camlbin := 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
@@ -235,7 +235,7 @@ let declare_loading_string () =
\n Mltop.set_top\
\n {Mltop.load_obj=\
\n (fun f -> if not (Topdirs.load_file ppf f)\
-\n then Errors.error (\"Could not load plugin \"^f));\
+\n then CErrors.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) };;\
@@ -265,11 +265,10 @@ let create_tmp_main_file modules =
let main () =
let (options, userfiles) = parse_args () in
(* Directories: *)
- let () = Envars.set_coqlib ~fail:Errors.error in
- let camlbin = Envars.camlbin () in
+ let () = Envars.set_coqlib ~fail:CErrors.error in
let basedir = if !Flags.boot then None else Some (Envars.coqlib ()) in
(* Which ocaml compiler to invoke *)
- let prog = camlbin/(if !opt then "ocamlopt" else "ocamlc") in
+ 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 [] else Coq_config.vmbyteflags in
@@ -284,14 +283,14 @@ let main () =
(std_includes basedir) @ tolink @ [ main_file ] @ topstart
in
if !echo then begin
- let command = String.concat " " (prog::args) in
+ 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 prog args in
+ let exitcode = run_command (Envars.ocamlfind ()) (prog::args) in
clean main_file;
exitcode
with reraise -> clean main_file; raise reraise
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index 1fdda04c..8fcca535 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -17,7 +17,19 @@ type coqtop = {
xml_parser : Xml_parser.t;
}
-let logger level content = prerr_endline content
+let print_xml chan xml =
+ let rec print = function
+ | Xml_datatype.PCData s -> output_string chan s
+ | Xml_datatype.Element (_, _, children) -> List.iter print children
+ in
+ print xml
+
+let error_xml s =
+ Printf.eprintf "fake_id: error: %a\n%!" print_xml s;
+ exit 1
+
+let logger level content =
+ Printf.eprintf "%a\n%! " print_xml (Richpp.repr content)
let base_eval_call ?(print=true) ?(fail=true) call coqtop =
if print then prerr_endline (Xmlprotocol.pr_call call);
@@ -25,21 +37,20 @@ let base_eval_call ?(print=true) ?(fail=true) call coqtop =
Xml_printer.print coqtop.xml_printer xml_query;
let rec loop () =
let xml = Xml_parser.parse coqtop.xml_parser in
- if Pp.is_message xml then
- let message = Pp.to_message xml in
- let level = message.Pp.message_level in
- let content = message.Pp.message_content in
+ match Xmlprotocol.is_message xml with
+ | Some (level, _loc, content) ->
logger level content;
loop ()
- else if Feedback.is_feedback xml then
- loop ()
- else (Xmlprotocol.to_answer call xml)
+ | None ->
+ if Xmlprotocol.is_feedback xml then
+ loop ()
+ else Xmlprotocol.to_answer call xml
in
let res = loop () in
if print then prerr_endline (Xmlprotocol.pr_full_value call res);
match res with
- | Interface.Fail (_,_,s) when fail -> error s
- | Interface.Fail (_,_,s) as x -> prerr_endline s; x
+ | Interface.Fail (_,_,s) when fail -> error_xml (Richpp.repr s)
+ | Interface.Fail (_,_,s) as x -> Printf.eprintf "%a\n%!" print_xml (Richpp.repr s); x
| x -> x
let eval_call c q = ignore(base_eval_call c q)
@@ -188,7 +199,7 @@ let print_document () =
module GUILogic = struct
let after_add = function
- | Interface.Fail (_,_,s) -> error s
+ | Interface.Fail (_,_,s) -> error_xml (Richpp.repr s)
| Interface.Good (id, (Util.Inl (), _)) ->
Document.assign_tip_id doc id
| Interface.Good (id, (Util.Inr tip, _)) ->
@@ -200,7 +211,7 @@ module GUILogic = struct
let at id id' _ = Stateid.equal id' id
let after_edit_at (id,need_unfocus) = function
- | Interface.Fail (_,_,s) -> error s
+ | Interface.Fail (_,_,s) -> error_xml (Richpp.repr s)
| Interface.Good (Util.Inl ()) ->
if need_unfocus then Document.unfocus doc;
ignore(Document.cut_at doc id);
@@ -323,7 +334,7 @@ let main =
let finish () =
match base_eval_call (Xmlprotocol.status true) coq with
| Interface.Good _ -> exit 0
- | Interface.Fail (_,_,s) -> error s in
+ | Interface.Fail (_,_,s) -> error_xml (Richpp.repr s) in
(* The main loop *)
init ();
while true do
diff --git a/tools/ocamllibdep.mll b/tools/ocamllibdep.mll
new file mode 100644
index 00000000..bf82be09
--- /dev/null
+++ b/tools/ocamllibdep.mll
@@ -0,0 +1,217 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+{
+ exception Syntax_error of int*int
+
+ let syntax_error lexbuf =
+ raise (Syntax_error (Lexing.lexeme_start lexbuf, Lexing.lexeme_end lexbuf))
+}
+
+let space = [' ' '\t' '\n' '\r']
+let lowercase = ['a'-'z' '\223'-'\246' '\248'-'\255']
+let uppercase = ['A'-'Z' '\192'-'\214' '\216'-'\222']
+let identchar =
+ ['A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9']
+let caml_up_ident = uppercase identchar*
+let caml_low_ident = lowercase identchar*
+
+rule mllib_list = parse
+ | caml_up_ident { let s = String.uncapitalize (Lexing.lexeme lexbuf)
+ in s :: mllib_list lexbuf }
+ | "*predef*" { mllib_list lexbuf }
+ | space+ { mllib_list lexbuf }
+ | eof { [] }
+ | _ { syntax_error lexbuf }
+
+{
+open Printf
+open Unix
+
+(* Makefile's escaping rules are awful: $ is escaped by doubling and
+ other special characters are escaped by backslash prefixing while
+ backslashes themselves must be escaped only if part of a sequence
+ followed by a special character (i.e. in case of ambiguity with a
+ use of it as escaping character). Moreover (even if not crucial)
+ it is apparently not possible to directly escape ';' and leading '\t'. *)
+
+let escape =
+ let s' = Buffer.create 10 in
+ fun s ->
+ Buffer.clear s';
+ for i = 0 to String.length s - 1 do
+ let c = s.[i] in
+ if c = ' ' || c = '#' || c = ':' (* separators and comments *)
+ || c = '%' (* pattern *)
+ || c = '?' || c = '[' || c = ']' || c = '*' (* expansion in filenames *)
+ || i=0 && c = '~' && (String.length s = 1 || s.[1] = '/' ||
+ 'A' <= s.[1] && s.[1] <= 'Z' ||
+ 'a' <= s.[1] && s.[1] <= 'z') (* homedir expansion *)
+ then begin
+ let j = ref (i-1) in
+ while !j >= 0 && s.[!j] = '\\' do
+ Buffer.add_char s' '\\'; decr j (* escape all preceding '\' *)
+ done;
+ Buffer.add_char s' '\\';
+ end;
+ if c = '$' then Buffer.add_char s' '$';
+ Buffer.add_char s' c
+ done;
+ Buffer.contents s'
+
+(* 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 = ':'
+ | _ -> assert false
+
+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
+ the extension. When no extension match, [(f,"")] is returned *)
+
+let rec get_extension f = function
+ | [] -> (f, "")
+ | s :: _ when Filename.check_suffix f s -> (Filename.chop_suffix f s, s)
+ | _ :: l -> get_extension f l
+
+let file_name s = function
+ | None -> s
+ | Some "." -> s
+ | Some d -> d // s
+
+type dir = string option
+
+let add_directory add_file phys_dir =
+ Array.iter (fun f ->
+ (* we avoid all files starting by '.' *)
+ if f.[0] <> '.' then
+ let phys_f = if phys_dir = "." then f else phys_dir//f in
+ match try (stat phys_f).st_kind with _ -> S_BLK with
+ | S_REG -> add_file phys_dir f
+ | _ -> ()) (Sys.readdir phys_dir)
+
+let error_cannot_parse s (i,j) =
+ Printf.eprintf "File \"%s\", characters %i-%i: Syntax error\n" s i j;
+ exit 1
+
+let warning_ml_clash x s suff s' suff' =
+ if suff = suff' then
+ eprintf
+ "*** Warning: %s%s already found in %s (discarding %s%s)\n" x suff
+ (match s with None -> "." | Some d -> d)
+ ((match s' with None -> "." | Some d -> d) // x) suff
+
+let mkknown () =
+ let h = (Hashtbl.create 19 : (string, dir * string) Hashtbl.t) in
+ let add x s suff =
+ try let s',suff' = Hashtbl.find h x in warning_ml_clash x s' suff' s suff
+ with Not_found -> Hashtbl.add h x (s,suff)
+ and search x =
+ try Some (fst (Hashtbl.find h x))
+ with Not_found -> None
+ in add, search
+
+let add_ml_known, search_ml_known = mkknown ()
+let add_mlpack_known, search_mlpack_known = mkknown ()
+
+let mllibAccu = ref ([] : (string * dir) list)
+let mlpackAccu = ref ([] : (string * dir) list)
+
+let add_caml_known phys_dir f =
+ let basename,suff = get_extension f [".ml";".ml4";".mlpack"] in
+ match suff with
+ | ".ml"|".ml4" -> add_ml_known basename (Some phys_dir) suff
+ | ".mlpack" -> add_mlpack_known basename (Some phys_dir) suff
+ | _ -> ()
+
+let add_caml_dir phys_dir =
+ handle_unix_error (add_directory add_caml_known) phys_dir
+
+let traite_fichier_modules md ext =
+ try
+ let chan = open_in (md ^ ext) in
+ let list = mllib_list (Lexing.from_channel chan) in
+ List.fold_left
+ (fun acc str ->
+ match search_mlpack_known str with
+ | Some mldir -> (file_name str mldir) :: acc
+ | None ->
+ match search_ml_known str with
+ | Some mldir -> (file_name str mldir) :: acc
+ | None -> acc) [] (List.rev list)
+ with
+ | Sys_error _ -> []
+ | Syntax_error (i,j) -> error_cannot_parse (md^ext) (i,j)
+
+let addQueue q v = q := v :: !q
+
+let treat_file old_name =
+ let name = Filename.basename old_name in
+ let dirname = Some (Filename.dirname old_name) in
+ match get_extension name [".mllib";".mlpack"] with
+ | (base,".mllib") -> addQueue mllibAccu (base,dirname)
+ | (base,".mlpack") -> addQueue mlpackAccu (base,dirname)
+ | _ -> ()
+
+let mllib_dependencies () =
+ List.iter
+ (fun (name,dirname) ->
+ let fullname = file_name name dirname in
+ let deps = traite_fichier_modules fullname ".mllib" in
+ let sdeps = String.concat " " deps in
+ let efullname = escape fullname in
+ printf "%s_MLLIB_DEPENDENCIES:=%s\n" efullname sdeps;
+ printf "%s.cma:$(addsuffix .cmo,$(%s_MLLIB_DEPENDENCIES))\n"
+ efullname efullname;
+ printf "%s.cmxa:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n"
+ efullname efullname;
+ flush Pervasives.stdout)
+ (List.rev !mllibAccu)
+
+let mlpack_dependencies () =
+ List.iter
+ (fun (name,dirname) ->
+ let fullname = file_name name dirname in
+ let modname = String.capitalize name in
+ let deps = traite_fichier_modules fullname ".mlpack" in
+ let sdeps = String.concat " " deps in
+ let efullname = escape fullname in
+ printf "%s_MLPACK_DEPENDENCIES:=%s\n" efullname sdeps;
+ List.iter (fun d -> printf "%s_FORPACK:= -for-pack %s\n" d modname) deps;
+ printf "%s.cmo:$(addsuffix .cmo,$(%s_MLPACK_DEPENDENCIES))\n"
+ efullname efullname;
+ printf "%s.cmx:$(addsuffix .cmx,$(%s_MLPACK_DEPENDENCIES))\n"
+ efullname efullname;
+ flush Pervasives.stdout)
+ (List.rev !mlpackAccu)
+
+let rec parse = function
+ | "-I" :: r :: ll ->
+ (* To solve conflict (e.g. same filename in kernel and checker)
+ we allow to state an explicit order *)
+ add_caml_dir r;
+ parse ll
+ | f :: ll -> treat_file f; parse ll
+ | [] -> ()
+
+let main () =
+ if Array.length Sys.argv < 2 then exit 1;
+ parse (List.tl (Array.to_list Sys.argv));
+ mllib_dependencies ();
+ mlpack_dependencies ()
+
+let _ = Printexc.catch main ()
+}
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-27 17:02:37 +0000