From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- tools/compat5.ml | 13 -- tools/compat5.mlp | 23 --- tools/compat5b.ml | 13 -- tools/compat5b.mlp | 23 --- tools/coq_makefile.ml | 393 ++++++++++++++++++++++++++++++----------------- tools/coqc.ml | 29 +--- tools/coqdep.ml | 19 +-- tools/coqdep_common.ml | 95 +++++------- tools/coqdep_common.mli | 8 +- tools/coqdep_lexer.mll | 126 ++++++--------- tools/coqdoc/cpretty.mll | 235 +++++++++++++++------------- tools/coqdoc/index.ml | 26 ---- tools/coqdoc/output.ml | 3 +- tools/coqmktop.ml | 17 +- tools/fake_ide.ml | 37 +++-- tools/ocamllibdep.mll | 217 ++++++++++++++++++++++++++ 16 files changed, 724 insertions(+), 553 deletions(-) delete mode 100644 tools/compat5.ml delete mode 100644 tools/compat5.mlp delete mode 100644 tools/compat5b.ml delete mode 100644 tools/compat5b.mlp create mode 100644 tools/ocamllibdep.mll (limited to 'tools') 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 *) -(* ] -> - [< '(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 *) -(* ] -> - [< '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 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 *) +(* + 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 () +} -- cgit v1.2.3