From 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 15 Jul 2015 10:36:12 +0200 Subject: Imported Upstream version 8.5~beta2+dfsg --- tools/coq_makefile.ml | 80 +++++++++++++++++++++++++++++------------------- tools/coq_tex.ml | 3 +- tools/coqc.ml | 4 +-- tools/coqdoc/cpretty.mll | 12 ++------ tools/coqdoc/output.ml | 1 - 5 files changed, 56 insertions(+), 44 deletions(-) (limited to 'tools') diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index d660f420..0931fd55 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -46,9 +46,10 @@ let section s = let usage () = output_string stderr "Usage summary: -coq_makefile [subdirectory] .... [file.v] ... [file.ml[i4]?] ... - [file.ml{lib,pack}] ... [-extra[-phony] result dependencies command] - ... [-I dir] ... [-R physicalpath logicalpath] ... [VARIABLE = value] +coq_makefile .... [file.v] ... [file.ml[i4]?] ... [file.ml{lib,pack}] + ... [any] ... [-extra[-phony] result dependencies command] + ... [-I dir] ... [-R physicalpath logicalpath] + ... [-Q physicalpath logicalpath] ... [VARIABLE = value] ... [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file] [-h] [--help] @@ -56,8 +57,8 @@ coq_makefile [subdirectory] .... [file.v] ... [file.ml[i4]?] ... [file.ml[i4]?]: Objective Caml file to be compiled [file.ml{lib,pack}]: ocamlbuild file that describes a Objective Caml library/module -[subdirectory] : subdirectory that should be \"made\" and has a - Makefile itself to do so. +[any] : subdirectory that should be \"made\" and has a Makefile itself + to do so. Very fragile and discouraged. [-extra result dependencies command]: add target \"result\" with command \"command\" and dependencies \"dependencies\". If \"result\" is not generic (do not contains a %), \"result\" is built by _make all_ and @@ -157,7 +158,7 @@ let vars_to_put_by_root var_x_files_l (inc_ml,inc_i,inc_r) = |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" 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 -> ( @@ -297,7 +298,7 @@ let install (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,sds) in print "\tprintf 'cd \"$${DSTROOT}\"$(COQDOCINSTALL) && "; printf "find %s/%s -maxdepth 0 -and -empty -exec rmdir -p \\{\\} \\;\\n' >> \"$@\"\n" dir kind in - print "uninstall_me.sh:\n"; + printf "uninstall_me.sh: %s\n" !makefile_name; print "\techo '#!/bin/sh' > $@ \n"; if (not_empty cmxsfiles) then uninstall_by_root where_what_cmxs; uninstall_by_root where_what_oth; @@ -320,7 +321,7 @@ let make_makefile sds = end let clean sds sps = - print "clean:\n"; + 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"; @@ -329,6 +330,7 @@ let clean sds sps = if !some_vfile then begin print "\trm -f $(OBJFILES) $(OBJFILES:.o=.native) $(NATIVEFILES)\n"; + print "\tfind . -name .coq-native -type d -empty -delete\n"; print "\trm -f $(VOFILES) $(VOFILES:.vo=.vio) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)\n" end; print "\trm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex\n"; @@ -342,7 +344,11 @@ let clean sds sps = (fun x -> print "\t+cd "; print x; print " && $(MAKE) clean\n") sds; print "\n"; - print "archclean:\n"; + let () = + if !some_vfile then + let () = print "cleanall:: clean\n" in + print "\trm -f $(patsubst %.v,.%.aux,$(VFILES))\n\n" in + print "archclean::\n"; print "\trm -f *.cmx *.o\n"; List.iter (fun x -> print "\t+cd "; print x; print " && $(MAKE) archclean\n") @@ -365,7 +371,7 @@ let implicit () = 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 "$(addsuffix .d,$(ML4FILES)): %.ml4.d: %.ml4\n"; - print "\t$(COQDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in + print "\t$(OCAMLDEP) -slash $(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 "$(filter-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(MLFILES:.ml=.cmx)): %.cmx: %.ml\n"; @@ -457,7 +463,7 @@ let variables is_install opt (args,defs) = print "ifeq ($(CAMLP4),camlp5) CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma else -CAMLP4EXTEND= +CAMLP4EXTEND=threads.cma endif\n"; print "PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(CAMLLIB)threads/ $(COQSRCLIBS) compat5.cmo \\ $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'\n\n"; @@ -530,9 +536,13 @@ let include_dirs (inc_ml,inc_i,inc_r) = List.iter (fun x -> print "\\\n "; print x) str_r; print "\n\n"; end +let double_colon = ["clean"; "cleanall"; "archclean"] + let custom sps = let pr_path (file,dependencies,is_phony,com) = - print file; print ": "; print dependencies; print "\n"; + print file; + print (if List.mem file double_colon then ":: " else ": "); + print dependencies; print "\n"; if com <> "" then (print "\t"; print com; print "\n"); print "\n" in @@ -543,7 +553,12 @@ let subdirs sds = let pr_subdir s = print s; print ":\n\t+cd \""; print s; print "\" && $(MAKE) all\n\n" in - if sds <> [] then section "Subdirectories."; + if sds <> [] then + let () = + Format.eprintf "@[Warning: Targets for subdirectories are very fragile.@ " in + let () = + Format.eprintf "For example,@ nothing is done to handle dependencies@ with them.@]@." in + section "Subdirectories."; List.iter pr_subdir sds let forpacks l = @@ -695,22 +710,25 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other end let all_target (vfiles, (_,_,_,_,mlpackfiles as mlfiles), sps, sds) inc = - let other_targets = CList.map_filter - (fun (n,_,is_phony,_) -> if not (is_phony || is_genrule n) then Some n else None) - sps @ sds in + let other_targets = + CList.map_filter + (fun (n,_,is_phony,_) -> if not (is_phony || is_genrule n) then Some n else None) + sps @ sds in main_targets vfiles mlfiles other_targets inc; - print ".PHONY: "; - print_list " " - ("all" :: "opt" :: "byte" :: "archclean" :: "clean" :: "install" :: - "uninstall_me.sh" :: "uninstall" :: "userinstall" :: "depend" :: - "html" :: "validate" :: - (sds@(CList.map_filter - (fun (n,_,is_phony,_) -> - if is_phony then Some n else None) sps))); - print "\n\n"; - custom sps; - subdirs sds; - forpacks mlpackfiles + print ".PHONY: "; + print_list + " " + ("all" :: "archclean" :: "beautify" :: "byte" :: "clean" :: "cleanall" + :: "gallina" :: "gallinahtml" :: "html" :: "install" :: "install-doc" + :: "install-natdynlink" :: "install-toploop" :: "opt" :: "printenv" + :: "quick" :: "uninstall" :: "userinstall" :: "validate" :: "vio2vo" + :: (sds@(CList.map_filter + (fun (n,_,is_phony,_) -> + if is_phony then Some n else None) sps))); + print "\n\n"; + custom sps; + subdirs sds; + forpacks mlpackfiles let banner () = print (Printf.sprintf @@ -750,7 +768,7 @@ let ensure_root_dir (v,(mli,ml4,ml,mllib,mlpack),_,_) ((ml_inc,i_inc,r_inc) as l let warn_install_at_root_directory (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,_) (inc_ml,inc_i,inc_r) = - let inc_top = List.filter (fun (_,ldir,_) -> ldir = "") inc_r@inc_i 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 if List.exists (fun f -> List.mem (Filename.dirname f) inc_top_p) files @@ -764,10 +782,10 @@ let check_overlapping_include (_,inc_i,inc_r) = | [] -> () | (pdir,_,abspdir)::l -> if not (is_prefix pwd abspdir) then - Printf.eprintf "Warning: in option -R, %s is not a subdirectory of the current directory\n" pdir; + Printf.eprintf "Warning: in option -R/-Q, %s is not a subdirectory of the current directory\n" pdir; List.iter (fun (pdir',_,abspdir') -> if is_prefix abspdir abspdir' || is_prefix abspdir' abspdir then - Printf.eprintf "Warning: in options -R, %s and %s overlap\n" pdir pdir') l; + Printf.eprintf "Warning: in options -R/-Q, %s and %s overlap\n" pdir pdir') l; in aux (inc_i@inc_r) let do_makefile args = diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml index 383a68df..a2cc8384 100644 --- a/tools/coq_tex.ml +++ b/tools/coq_tex.ml @@ -79,7 +79,7 @@ let expos = Str.regexp "^" let tex_escaped s = let dollar = "\\$" and backslash = "\\\\" and expon = "\\^" in - let delims = Str.regexp ("[_{}&%#" ^ dollar ^ backslash ^ expon ^"~ <>']") in + let delims = Str.regexp ("[_{}&%#" ^ dollar ^ backslash ^ expon ^"~ <>'`]") in let adapt_delim = function | "_" | "{" | "}" | "&" | "%" | "#" | "$" as c -> "\\"^c | "\\" -> "{\\char'134}" @@ -89,6 +89,7 @@ let tex_escaped s = | "<" -> "{<}" | ">" -> "{>}" | "'" -> "{\\textquotesingle}" + | "`" -> "\\`{}" | _ -> assert false in let adapt = function diff --git a/tools/coqc.ml b/tools/coqc.ml index f636ffd8..7e822dbe 100644 --- a/tools/coqc.ml +++ b/tools/coqc.ml @@ -111,7 +111,7 @@ let parse_args () = |"-dont-load-proofs"|"-load-proofs"|"-force-load-proofs" |"-impredicative-set"|"-vm"|"-no-native-compiler" |"-verbose-compat-notations"|"-no-compat-notations" - |"-indices-matter"|"-quick"|"-color" + |"-indices-matter"|"-quick"|"-color"|"-type-in-type" |"-async-proofs-always-delegate"|"-async-proofs-never-reopen-branch" as o) :: rem -> parse (cfiles,o::args) rem @@ -121,7 +121,7 @@ let parse_args () = | ("-outputstate"|"-inputstate"|"-is"|"-exclude-dir" |"-load-vernac-source"|"-l"|"-load-vernac-object" |"-load-ml-source"|"-require"|"-load-ml-object" - |"-init-file"|"-dump-glob"|"-compat"|"-coqlib" + |"-init-file"|"-dump-glob"|"-compat"|"-coqlib"|"-top" |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs" as o) :: rem -> begin diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index edf7ee8e..cb704146 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -405,7 +405,7 @@ let set_kw = let gallina_kw_to_hide = "Implicit" space+ "Arguments" - | "Ltac" + | ("Local" space+)? "Ltac" | "Require" | "Import" | "Export" @@ -456,13 +456,7 @@ rule coq_bol = parse { begin_show (); coq_bol lexbuf } | space* end_show { end_show (); coq_bol lexbuf } - | space* ("Local"|"Global") - { - in_proof := None; - let s = lexeme lexbuf in - output_indented_keyword s lexbuf; - coq_bol lexbuf } - | space* gallina_kw_to_hide + | space* (("Local"|"Global") space+)? gallina_kw_to_hide { let s = lexeme lexbuf in if !Cdglobals.light && section_or_end s then let eol = skip_to_dot lexbuf in @@ -596,7 +590,7 @@ and coq = parse end } | eof { () } - | gallina_kw_to_hide + | (("Local"|"Global") space+)? gallina_kw_to_hide { let s = lexeme lexbuf in if !Cdglobals.light && section_or_end s then begin diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index ae6e6388..06030c45 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -595,7 +595,6 @@ module Html = struct | '<' -> Buffer.add_string buff "<" | '>' -> Buffer.add_string buff ">" | '&' -> Buffer.add_string buff "&" - | '\'' -> Buffer.add_string buff "´" | '\"' -> Buffer.add_string buff """ | c -> Buffer.add_char buff c done; -- cgit v1.2.3