From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- tools/README.coq-tex | 13 --- tools/README.emacs | 0 tools/coq-sl.sty | 0 tools/coq_makefile.ml | 23 +++--- tools/coq_tex.ml | 203 ++++++++++++++++++++++------------------------- tools/coqc.ml | 15 ++-- tools/coqdep.ml | 64 +++++++-------- tools/coqdep_boot.ml | 6 +- tools/coqdep_common.ml | 155 ++++++++++++++++++++++++------------ tools/coqdep_common.mli | 10 ++- tools/coqdep_lexer.mli | 3 +- tools/coqdep_lexer.mll | 16 +--- tools/coqdoc/cpretty.mll | 1 + tools/coqdoc/main.ml | 8 +- tools/coqdoc/output.ml | 7 +- tools/coqwc.mll | 4 +- tools/fake_ide.ml | 6 +- tools/gallina.ml | 5 +- 18 files changed, 276 insertions(+), 263 deletions(-) delete mode 100755 tools/README.coq-tex mode change 100755 => 100644 tools/README.emacs mode change 100755 => 100644 tools/coq-sl.sty (limited to 'tools') diff --git a/tools/README.coq-tex b/tools/README.coq-tex deleted file mode 100755 index 5c7606a9..00000000 --- a/tools/README.coq-tex +++ /dev/null @@ -1,13 +0,0 @@ -DESCRIPTION. - -The coq-tex filter extracts Coq phrases embedded in LaTeX files, -evaluates them, and insert the outcome of the evaluation after each -phrase. - -The filter is written in Perl, so you'll need Perl version 4 installed -on your machine. - -USAGE. See the manual page (coq-tex.1). - -AUTHOR. Jean-Christophe Filliatre (jcfillia@lip.ens-lyon.fr) - from caml-tex of Xavier Leroy. diff --git a/tools/README.emacs b/tools/README.emacs old mode 100755 new mode 100644 diff --git a/tools/coq-sl.sty b/tools/coq-sl.sty old mode 100755 new mode 100644 diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 0931fd55..d3374675 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -299,7 +299,7 @@ let install (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,sds) in printf "find %s/%s -maxdepth 0 -and -empty -exec rmdir -p \\{\\} \\;\\n' >> \"$@\"\n" dir kind in printf "uninstall_me.sh: %s\n" !makefile_name; - print "\techo '#!/bin/sh' > $@ \n"; + print "\techo '#!/bin/sh' > $@\n"; if (not_empty cmxsfiles) then uninstall_by_root where_what_cmxs; uninstall_by_root where_what_oth; if not_empty vfiles then uninstall_one_kind "html" doc_dir; @@ -386,12 +386,12 @@ let implicit () = 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 "$(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib\n"; - print "\t$(COQDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in + print "\t$(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 "$(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack\n"; - print "\t$(COQDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"; + print "\t$(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"; @@ -496,7 +496,7 @@ endif\n"; print "\n" let parameters () = - print ".DEFAULT_GOAL := all\n\n# \n"; + print ".DEFAULT_GOAL := all\n\n"; print "# This Makefile may take arguments passed as environment variables:\n"; print "# COQBIN to specify the directory where Coq binaries resides;\n"; print "# TIMECMD set a command to log .v compilation time;\n"; @@ -575,8 +575,13 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other let decl_var var = function |[] -> () |l -> - printf "%s:=" var; print_list "\\\n " l; print "\n"; - printf "\n-include $(addsuffix .d,$(%s))\n.SECONDARY: $(addsuffix .d,$(%s))\n\n" var var + printf "%s:=" var; print_list "\\\n " l; print "\n\n"; + print "ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),)\n"; + printf "-include $(addsuffix .d,$(%s))\n" var; + print "else\nifeq ($(MAKECMDGOALS),)\n"; + printf "-include $(addsuffix .d,$(%s))\n" var; + print "endif\nendif\n\n"; + printf ".SECONDARY: $(addsuffix .d,$(%s))\n\n" var in section "Files dispatching."; decl_var "VFILES" vfiles; @@ -764,7 +769,7 @@ let ensure_root_dir (v,(mli,ml4,ml,mllib,mlpack),_,_) ((ml_inc,i_inc,r_inc) as l && not_tops mllib && not_tops mlpack) then l else - ((".",here)::ml_inc,(".","Top",here)::i_inc,r_inc) + ((".",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) = @@ -837,11 +842,9 @@ let do_makefile args = if not (makefile = None) then close_out !output_channel; exit 0 -let main () = +let _ = let args = if Array.length Sys.argv = 1 then usage (); List.tl (Array.to_list Sys.argv) in do_makefile args - -let _ = Printexc.catch main () diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml index a2cc8384..dbdc2e9d 100644 --- a/tools/coq_tex.ml +++ b/tools/coq_tex.ml @@ -24,10 +24,7 @@ let hrule = ref false let small = ref false let boot = ref false -let coq_prompt = Str.regexp "Coq < " -let any_prompt = Str.regexp "^[A-Z0-9a-z_\\$']* < " - -let remove_prompt s = Str.replace_first any_prompt "" s +let any_prompt = Str.regexp "[A-Z0-9a-z_\\$']* < " (* First pass: extract the Coq phrases to evaluate from [texfile] * and put them into the file [inputv] *) @@ -58,30 +55,19 @@ let extract texfile inputv = ("Set Printing Width " ^ (string_of_int !linelen) ^".\n"); outside () with End_of_file -> - begin close_in chan_in; close_out chan_out end + (* a dummy command, just in case the last line was a comment *) + output_string chan_out "Set Printing Width 78.\n"; + close_in chan_in; + close_out chan_out (* Second pass: insert the answers of Coq from [coq_output] into the * TeX file [texfile]. The result goes in file [result]. *) -let begin_coq_example = - Str.regexp "\\\\begin{coq_\\(example\\|example\\*\\|example\\#\\)}[ \t]*$" -let begin_coq_eval = Str.regexp "\\\\begin{coq_eval}[ \t]*$" -let end_coq_example = Str.regexp "\\\\end{coq_\\(example\\|example\\*\\|example\\#\\)}[ \t]*$" -let end_coq_eval = Str.regexp "\\\\end{coq_eval}[ \t]*$" -let dot_end_line = Str.regexp "\\.[ \t]*\\((\\*.*\\*)\\)?[ \t]*$" - -let has_match r s = - try let _ = Str.search_forward r s 0 in true with Not_found -> false - -let percent = Str.regexp "%" -let bang = Str.regexp "!" -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 "[_{}&%#$\\^~ <>'`]" in let adapt_delim = function - | "_" | "{" | "}" | "&" | "%" | "#" | "$" as c -> "\\"^c + | "{" | "}" | "&" | "%" | "#" | "$" as c -> "\\"^c + | "_" -> "{\\char`\\_}" | "\\" -> "{\\char'134}" | "^" -> "{\\char'136}" | "~" -> "{\\char'176}" @@ -111,99 +97,106 @@ let insert texfile coq_output result = let c_tex = open_in texfile in let c_coq = open_in coq_output in let c_out = open_out result in - (* next_block k : this function reads the next block of Coq output - * removing the k leading prompts. - * it returns the block as a list of string) *) - let last_read = ref "" in - let next_block k = - if !last_read = "" then last_read := input_line c_coq; - (* skip k prompts *) - for _i = 1 to k do - last_read := remove_prompt !last_read; - done; + (* read lines until a prompt is found (starting from the second line), + purge prompts on the first line and return their number *) + let last_read = ref (input_line c_coq) in + let read_output () = + let first = !last_read in + let nb = ref 0 in + (* remove the leading prompts *) + let rec skip_prompts pos = + if Str.string_match any_prompt first pos then + let () = incr nb in + skip_prompts (Str.match_end ()) + else pos in + let first = + let start = skip_prompts 0 in + String.sub first start (String.length first - start) in (* read and return the following lines until a prompt is found *) let rec read_lines () = let s = input_line c_coq in if Str.string_match any_prompt s 0 then begin last_read := s; [] end else - s :: (read_lines ()) - in - let first = !last_read in first :: (read_lines ()) - in - (* we are just after \end{coq_...} block *) - let rec just_after () = + s :: read_lines () in + (first :: read_lines (), !nb) in + let unhandled_output = ref None in + let read_output () = + match !unhandled_output with + | Some some -> unhandled_output := None; some + | None -> read_output () in + (* we are inside a \begin{coq_...} ... \end{coq_...} block + * show_... tell what kind of block it is *) + let rec inside show_answers show_questions not_first discarded = let s = input_line c_tex in - if Str.string_match begin_coq_example s 0 then begin - inside (Str.matched_group 1 s <> "example*") - (Str.matched_group 1 s <> "example#") 0 false - end - else begin - if !hrule then output_string c_out "\\hrulefill\\\\\n"; - output_string c_out "\\end{flushleft}\n"; - if !small then output_string c_out "\\end{small}\n"; - if Str.string_match begin_coq_eval s 0 then - eval 0 + if s = "" then + inside show_answers show_questions not_first (discarded + 1) + else if not (Str.string_match end_coq s 0) then begin + let (bl,n) = read_output () in + assert (n > discarded); + let n = n - discarded in + if not_first then output_string c_out "\\medskip\n"; + if !verbose then Printf.printf "Coq < %s\n" s; + if show_questions then encapsule false c_out ("Coq < " ^ s); + let rec read_lines k = + if k = 0 then [] + else + let s = input_line c_tex in + if Str.string_match end_coq s 0 then [] + else s :: read_lines (k - 1) in + let al = read_lines (n - 1) in + if !verbose then List.iter (Printf.printf " %s\n") al; + if show_questions then + List.iter (fun s -> encapsule false c_out (" " ^ s)) al; + let la = n - 1 - List.length al in + if la <> 0 then + (* this happens when the block ends with a comment; the output + is for the command at the beginning of the next block *) + unhandled_output := Some (bl, la) else begin - output_string c_out (s ^ "\n"); - outside () + if !verbose then List.iter print_endline bl; + if show_answers then print_block c_out bl; + inside show_answers show_questions (show_answers || show_questions) 0 end - end + end else if discarded > 0 then begin + (* this happens when the block ends with an empty line *) + let (bl,n) = read_output () in + assert (n > discarded); + unhandled_output := Some (bl, n - discarded) + end in (* we are outside of a \begin{coq_...} ... \end{coq_...} block *) - and outside () = - let s = input_line c_tex in - if Str.string_match begin_coq_example s 0 then begin + let rec outside just_after = + let start_block () = if !small then output_string c_out "\\begin{small}\n"; output_string c_out "\\begin{flushleft}\n"; + if !hrule then output_string c_out "\\hrulefill\\\\\n" in + let end_block () = if !hrule then output_string c_out "\\hrulefill\\\\\n"; - inside (Str.matched_group 1 s <> "example*") - (Str.matched_group 1 s <> "example#") 0 true - end else if Str.string_match begin_coq_eval s 0 then - eval 0 - else begin - output_string c_out (s ^ "\n"); - outside () - end - (* we are inside a \begin{coq_example?} ... \end{coq_example?} block - * show_answers tells what kind of block it is - * k is the number of lines read until now *) - and inside show_answers show_questions k first_block = + output_string c_out "\\end{flushleft}\n"; + if !small then output_string c_out "\\end{small}\n" in let s = input_line c_tex in - if Str.string_match end_coq_example s 0 then begin - just_after () + if Str.string_match begin_coq s 0 then begin + let kind = Str.matched_group 1 s in + if kind = "eval" then begin + if just_after then end_block (); + inside false false false 0; + outside false + end else begin + let show_answers = kind <> "example*" in + let show_questions = kind <> "example#" in + if not just_after then start_block (); + inside show_answers show_questions just_after 0; + outside true + end end else begin - let prompt = if k = 0 then "Coq < " else " " in - if !verbose then Printf.printf "%s%s\n" prompt s; - if (not first_block) && k=0 then output_string c_out "\\medskip\n"; - if show_questions then encapsule false c_out (prompt ^ s); - if has_match dot_end_line s then begin - let bl = next_block (succ k) in - if !verbose then List.iter print_endline bl; - if show_answers then print_block c_out bl; - inside show_answers show_questions 0 false - end else - inside show_answers show_questions (succ k) first_block - end - (* we are inside a \begin{coq_eval} ... \end{coq_eval} block - * k is the number of lines read until now *) - and eval k = - let s = input_line c_tex in - if Str.string_match end_coq_eval s 0 then - outside () - else begin - if !verbose then Printf.printf "Coq < %s\n" s; - if has_match dot_end_line s then - let bl = next_block (succ k) in - if !verbose then List.iter print_endline bl; - eval 0 - else - eval (succ k) - end - in + if just_after then end_block (); + output_string c_out (s ^ "\n"); + outside false + end in try - let _ = next_block 0 in (* to skip the Coq banner *) - let _ = next_block 0 in (* to skip the Coq answer to Set Printing Width *) - outside () + let _ = read_output () in (* to skip the Coq banner *) + let _ = read_output () in (* to skip the Coq answer to Set Printing Width *) + outside false with End_of_file -> begin close_in c_tex; close_in c_coq; @@ -212,7 +205,7 @@ let insert texfile coq_output result = (* Process of one TeX file *) -let rm f = try Sys.remove f with any -> () +let rm f = try Sys.remove f with _ -> () let one_file texfile = let inputv = Filename.temp_file "coq_tex" ".v" in @@ -249,7 +242,7 @@ let files = ref [] let parse_cl () = Arg.parse [ "-o", Arg.String (fun s -> output_specified := true; output := s), - "output-file Specifiy the resulting LaTeX file"; + "output-file Specify the resulting LaTeX file"; "-n", Arg.Int (fun n -> linelen := n), "line-width Set the line width"; "-image", Arg.String (fun s -> image := s), @@ -265,7 +258,7 @@ let parse_cl () = "-small", Arg.Set small, " Coq parts are written in small font"; "-boot", Arg.Set boot, - " Launch coqtop with the -boot option" + " Launch coqtop with the -boot option" ] (fun s -> files := s :: !files) "coq-tex [options] file ..." @@ -281,7 +274,7 @@ let find_coqtop () = "coqtop" end -let main () = +let _ = parse_cl (); if !image = "" then image := Filename.quote (find_coqtop ()); if !boot then image := !image ^ " -boot"; @@ -290,9 +283,7 @@ let main () = let _ = Sys.command (!image ^ " -batch") in exit 1 end else begin - Printf.printf "Your version of coqtop seems OK\n"; + (*Printf.printf "Your version of coqtop seems OK\n";*) flush stdout end; List.iter one_file (List.rev !files) - -let _ = Printexc.catch main () diff --git a/tools/coqc.ml b/tools/coqc.ml index 7e822dbe..e7239da6 100644 --- a/tools/coqc.ml +++ b/tools/coqc.ml @@ -30,13 +30,8 @@ let verbose = ref false let rec make_compilation_args = function | [] -> [] | file :: fl -> - let file_noext = - if Filename.check_suffix file ".v" then - Filename.chop_suffix file ".v" - else file - in (if !verbose then "-compile-verbose" else "-compile") - :: file_noext :: (make_compilation_args fl) + :: file :: (make_compilation_args fl) (* compilation of files [files] with command [command] and args [args] *) @@ -109,20 +104,20 @@ let parse_args () = |"-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"|"-no-native-compiler" + |"-impredicative-set"|"-vm"|"-native-compiler" |"-verbose-compat-notations"|"-no-compat-notations" - |"-indices-matter"|"-quick"|"-color"|"-type-in-type" + |"-indices-matter"|"-quick"|"-type-in-type" |"-async-proofs-always-delegate"|"-async-proofs-never-reopen-branch" as o) :: rem -> parse (cfiles,o::args) rem (* Options for coqtop : b) options with 1 argument *) - | ("-outputstate"|"-inputstate"|"-is"|"-exclude-dir" + | ("-outputstate"|"-inputstate"|"-is"|"-exclude-dir"|"-color" |"-load-vernac-source"|"-l"|"-load-vernac-object" |"-load-ml-source"|"-require"|"-load-ml-object" |"-init-file"|"-dump-glob"|"-compat"|"-coqlib"|"-top" - |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs" + |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs" |"-w" as o) :: rem -> begin match rem with diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 2e0cce6e..110d3060 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -36,14 +36,6 @@ let warning_mult suf iter = in iter check -let add_coqlib_known recur phys_dir log_dir f = - match get_extension f [".vo"] with - | (basename,".vo") -> - 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 sort () = let seen = Hashtbl.create 97 in let rec loop file = @@ -55,13 +47,13 @@ let sort () = try while true do match coq_action lb with - | Require sl -> + | Require (from, sl) -> List.iter (fun s -> - try loop (Hashtbl.find vKnown s) - with Not_found -> ()) + match search_v_known ?from s with + | None -> () + | Some f -> loop f) sl - | RequireString s -> loop s | _ -> () done with Fin_fichier -> @@ -297,18 +289,24 @@ struct module DAG = DAG(struct type t = string let compare = compare end) (** TODO: we should share this code with Coqdep_common *) +module VData = struct + type t = string list option * string list + let compare = Pervasives.compare +end + +module VCache = Set.Make(VData) + let treat_coq_file chan = let buf = Lexing.from_channel chan in - let deja_vu_v = ref ([]: string list list) - and deja_vu_ml = ref ([] : string list) in - let mark_v_done acc str = - let seen = List.mem str !deja_vu_v in + let deja_vu_v = ref VCache.empty in + let deja_vu_ml = ref StrSet.empty in + let mark_v_done from acc str = + let seen = VCache.mem (from, str) !deja_vu_v in if not seen then - let () = addQueue deja_vu_v str in - try - let file_str = Hashtbl.find vKnown str in - (canonize file_str, !suffixe) :: acc - with Not_found -> acc + let () = deja_vu_v := VCache.add (from, str) !deja_vu_v in + match search_v_known ?from str with + | None -> acc + | Some file_str -> (canonize file_str, !suffixe) :: acc else acc in let rec loop acc = @@ -317,11 +315,8 @@ let treat_coq_file chan = | None -> acc | Some action -> let acc = match action with - | Require strl -> - List.fold_left mark_v_done acc strl - | RequireString s -> - let str = Filename.basename s in - mark_v_done acc [str] + | Require (from, strl) -> + List.fold_left (fun accu v -> mark_v_done from accu v) acc strl | Declare sl -> let declare suff dir s = let base = file_name s dir in @@ -330,8 +325,8 @@ let treat_coq_file chan = in let decl acc str = let s = basename_noext str in - if not (List.mem s !deja_vu_ml) then - let () = addQueue deja_vu_ml s in + if not (StrSet.mem s !deja_vu_ml) then + let () = deja_vu_ml := StrSet.add s !deja_vu_ml in match search_mllib_known s with | Some mldir -> (declare ".cma" mldir s) :: acc | None -> @@ -343,13 +338,12 @@ let treat_coq_file chan = List.fold_left decl acc sl | Load str -> let str = Filename.basename str in - let seen = List.mem [str] !deja_vu_v in + let seen = VCache.mem (None, [str]) !deja_vu_v in if not seen then - let () = addQueue deja_vu_v [str] in - try - let file_str = Hashtbl.find vKnown [str] in - (canonize file_str, ".v") :: acc - with Not_found -> acc + let () = deja_vu_v := VCache.add (None, [str]) !deja_vu_v in + match search_v_known [str] with + | None -> acc + | Some file_str -> (canonize file_str, ".v") :: acc else acc | AddLoadPath _ | AddRecLoadPath _ -> acc (** TODO *) in @@ -461,7 +455,7 @@ let rec parse = function | "-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 := r::!norec_dirnames; parse ll + | "-exclude-dir" :: r :: ll -> norec_dirnames := StrSet.add r !norec_dirnames; parse ll | "-exclude-dir" :: [] -> usage () | "-coqlib" :: r :: ll -> Flags.coqlib_spec := true; Flags.coqlib := r; parse ll | "-coqlib" :: [] -> usage () diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml index bc3435a6..64ce66d2 100644 --- a/tools/coqdep_boot.ml +++ b/tools/coqdep_boot.ml @@ -25,12 +25,12 @@ let rec parse = function (* To solve conflict (e.g. same filename in kernel and checker) we allow to state an explicit order *) add_caml_dir r; - norec_dirs:=r::!norec_dirs; + norec_dirs := StrSet.add r !norec_dirs; parse ll | f :: ll -> treat_file None f; parse ll | [] -> () -let coqdep_boot () = +let _ = let () = option_boot := true in if Array.length Sys.argv < 2 then exit 1; parse (List.tl (Array.to_list Sys.argv)); @@ -47,5 +47,3 @@ let coqdep_boot () = end; if !option_c then mL_dependencies (); coq_dependencies () - -let _ = Printexc.catch coqdep_boot () diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 2e6a15ce..c1111375 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -17,6 +17,11 @@ open Unix options (see for instance [option_natdynlk] below). *) +module StrSet = Set.Make(String) + +module StrList = struct type t = string list let compare = compare end +module StrListMap = Map.Make(StrList) + let stderr = Pervasives.stderr let stdout = Pervasives.stdout @@ -26,8 +31,8 @@ let option_natdynlk = ref true let option_boot = ref false let option_mldep = ref None -let norec_dirs = ref ([] : string list) -let norec_dirnames = ref ["CVS"; "_darcs"] +let norec_dirs = ref StrSet.empty +let norec_dirnames = ref (List.fold_right StrSet.add ["CVS"; "_darcs"] StrSet.empty) let suffixe = ref ".vo" @@ -86,18 +91,18 @@ let vAccu = ref ([] : (string * string) list) let addQueue q v = q := v :: !q -let safe_hash_add cmp clq q (k,v) = +let safe_hash_add cmp clq q (k, (v, b)) = try - let v2 = Hashtbl.find q k in + let (v2, _) = Hashtbl.find q k in if not (cmp v v2) then - let rec add_clash = function - (k1,l1)::cltl when k=k1 -> (k1,v::l1)::cltl - | cl::cltl -> cl::add_clash cltl - | [] -> [(k,[v;v2])] in - clq := add_clash !clq; + let nv = + try v :: StrListMap.find k !clq + with Not_found -> [v; v2] + in + clq := StrListMap.add k nv !clq; (* overwrite previous bindings, as coqc does *) - Hashtbl.add q k v - with Not_found -> Hashtbl.add q k v + Hashtbl.add q k (v, b) + with Not_found -> Hashtbl.add q k (v, b) (** Files found in the loadpaths. For the ML files, the string is the basename without extension. @@ -126,20 +131,53 @@ let add_mli_known, iter_mli_known, search_mli_known = mkknown () let add_mllib_known, _, search_mllib_known = mkknown () let add_mlpack_known, _, search_mlpack_known = mkknown () -let vKnown = (Hashtbl.create 19 : (string list, string) Hashtbl.t) +let vKnown = (Hashtbl.create 19 : (string list, string * bool) Hashtbl.t) +(** The associated boolean is true if this is a root path. *) let coqlibKnown = (Hashtbl.create 19 : (string list, unit) Hashtbl.t) -let clash_v = ref ([]: (string list * string list) list) +let get_prefix p l = + let rec drop_prefix_rec = function + | (h1::tp, h2::tl) when h1 = h2 -> drop_prefix_rec (tp,tl) + | ([], tl) -> Some tl + | _ -> None + in + drop_prefix_rec (p, l) + +let search_table (type r) is_root table ?from s = match from with +| None -> Hashtbl.find table s +| Some from -> + let module M = struct exception Found of r end in + let iter logpath binding = + if is_root binding then match get_prefix from logpath with + | None -> () + | Some rem -> + match get_prefix (List.rev s) (List.rev rem) with + | None -> () + | Some _ -> raise (M.Found binding) + in + try Hashtbl.iter iter table; raise Not_found + with M.Found s -> s + +let search_v_known ?from s = + let is_root (_, root) = root in + try + let (phys_dir, _) = search_table is_root vKnown ?from s in + Some phys_dir + with Not_found -> None + +let is_in_coqlib ?from s = + let is_root _ = true in + try search_table is_root coqlibKnown ?from s; true with Not_found -> false + +let clash_v = ref (StrListMap.empty : string list StrListMap.t) let error_cannot_parse s (i,j) = Printf.eprintf "File \"%s\", characters %i-%i: Syntax error\n" s i j; exit 1 let warning_module_notfound f s = - eprintf "*** Warning: in file %s, library " f; - eprintf "%s.v is required and has not been found in the loadpath!\n" - (String.concat "." s); - flush stderr + 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; @@ -152,7 +190,7 @@ let warning_declare f s = flush stderr let warning_clash file dir = - match List.assoc dir !clash_v with + match StrListMap.find dir !clash_v with (f1::f2::fl) -> let f = Filename.basename f1 in let d1 = Filename.dirname f1 in @@ -165,9 +203,11 @@ let warning_clash file dir = eprintf "%s and %s; used the latter)\n" d2 d1 | _ -> assert false -let safe_assoc verbose file k = - if verbose && List.mem_assoc k !clash_v then warning_clash file k; - Hashtbl.find vKnown k +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 + | None -> raise Not_found + | Some path -> path let absolute_dir dir = let current = Sys.getcwd () in @@ -222,16 +262,16 @@ let autotraite_fichier_ML md ext = try let chan = open_in (md ^ ext) in let buf = Lexing.from_channel chan in - let deja_vu = ref [md] in + let deja_vu = ref (StrSet.singleton md) in let a_faire = ref "" in let a_faire_opt = ref "" in begin try while true do let (Use_module str) = caml_action buf in - if List.mem str !deja_vu then + if StrSet.mem str !deja_vu then () else begin - addQueue deja_vu str; + deja_vu := StrSet.add str !deja_vu; let byte,opt = depend_ML str in a_faire := !a_faire ^ byte; a_faire_opt := !a_faire_opt ^ opt @@ -307,38 +347,39 @@ let canonize f = | (f,_) :: _ -> escape f | _ -> escape f +module VData = struct + type t = string list option * string list + let compare = Pervasives.compare +end + +module VCache = Set.Make(VData) + let rec traite_fichier_Coq suffixe verbose f = try let chan = open_in f in let buf = Lexing.from_channel chan in - let deja_vu_v = ref ([]: string list list) - and deja_vu_ml = ref ([] : string list) in + let deja_vu_v = ref VCache.empty in + let deja_vu_ml = ref StrSet.empty in try while true do let tok = coq_action buf in match tok with - | Require strl -> + | Require (from, strl) -> List.iter (fun str -> - if not (List.mem str !deja_vu_v) then begin - addQueue deja_vu_v str; + if not (VCache.mem (from, str) !deja_vu_v) then begin + deja_vu_v := VCache.add (from, str) !deja_vu_v; try - let file_str = safe_assoc verbose f str in + let file_str = safe_assoc from verbose f str in printf " %s%s" (canonize file_str) suffixe with Not_found -> - if verbose && not (Hashtbl.mem coqlibKnown str) then + if verbose && not (is_in_coqlib ?from str) then + let str = + match from with + | None -> str + | Some pth -> pth @ str + in warning_module_notfound f str end) strl - | RequireString s -> - let str = Filename.basename s in - if not (List.mem [str] !deja_vu_v) then begin - addQueue deja_vu_v [str]; - try - let file_str = Hashtbl.find vKnown [str] in - printf " %s%s" (canonize file_str) suffixe - with Not_found -> - if not (Hashtbl.mem coqlibKnown [str]) then - warning_notfound f s - end | Declare sl -> let declare suff dir s = let base = file_name s dir in @@ -347,8 +388,8 @@ let rec traite_fichier_Coq suffixe verbose f = in let decl str = let s = basename_noext str in - if not (List.mem s !deja_vu_ml) then begin - addQueue deja_vu_ml s; + if not (StrSet.mem s !deja_vu_ml) then begin + deja_vu_ml := StrSet.add s !deja_vu_ml; match search_mllib_known s with | Some mldir -> declare ".cma" mldir s | None -> @@ -362,10 +403,10 @@ let rec traite_fichier_Coq suffixe verbose f = in List.iter decl sl | Load str -> let str = Filename.basename str in - if not (List.mem [str] !deja_vu_v) then begin - addQueue deja_vu_v [str]; + if not (VCache.mem (None, [str]) !deja_vu_v) then begin + deja_vu_v := VCache.add (None, [str]) !deja_vu_v; try - let file_str = Hashtbl.find vKnown [str] in + let (file_str, _) = Hashtbl.find vKnown [str] in let canon = canonize file_str in printf " %s.v" canon; traite_fichier_Coq suffixe true (canon ^ ".v") @@ -449,14 +490,24 @@ let add_caml_known phys_dir _ f = | ".mlpack" -> add_mlpack_known basename (Some phys_dir) suff | _ -> () +let add_coqlib_known recur phys_dir log_dir f = + match get_extension f [".vo"] with + | (basename,".vo") -> + 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 | (basename,".v") -> let name = log_dir@[basename] in let file = phys_dir//basename in - let paths = if recur then suffixes name else [name] in - List.iter - (fun n -> safe_hash_add compare_file clash_v vKnown (n,file)) paths + let () = safe_hash_add compare_file clash_v vKnown (name, (file, true)) in + if recur then + 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) -> let name = log_dir@[basename] in let paths = if recur then suffixes name else [name] in @@ -477,9 +528,9 @@ let rec add_directory recur add_file phys_dir log_dir = 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 List.mem f !norec_dirnames then () + if StrSet.mem f !norec_dirnames then () else - if List.mem phys_f !norec_dirs then () + if StrSet.mem phys_f !norec_dirs then () else add_directory recur add_file phys_f (log_dir@[f]) | S_REG -> add_file phys_dir log_dir f diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli index 71b96ca0..d610a055 100644 --- a/tools/coqdep_common.mli +++ b/tools/coqdep_common.mli @@ -6,13 +6,15 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +module StrSet : Set.S with type elt = string + val option_c : bool ref val option_noglob : bool ref val option_boot : bool ref val option_natdynlk : bool ref val option_mldep : string option ref -val norec_dirs : string list ref -val norec_dirnames : string list 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 @@ -31,8 +33,7 @@ val iter_mli_known : (string -> dir -> unit) -> unit val search_mli_known : string -> dir option val add_mllib_known : string -> dir -> string -> unit val search_mllib_known : string -> dir option -val vKnown : (string list, string) Hashtbl.t -val coqlibKnown : (string list, unit) Hashtbl.t +val search_v_known : ?from:string list -> string list -> string option val file_name : string -> string option -> string val escape : string -> string val canonize : string -> string @@ -40,6 +41,7 @@ val mL_dependencies : unit -> unit val coq_dependencies : unit -> unit 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 -> diff --git a/tools/coqdep_lexer.mli b/tools/coqdep_lexer.mli index b447030a..84c9ba79 100644 --- a/tools/coqdep_lexer.mli +++ b/tools/coqdep_lexer.mli @@ -11,8 +11,7 @@ type mL_token = Use_module of string type qualid = string list type coq_token = - Require of qualid list - | RequireString of string + Require of qualid option * qualid list | Declare of string list | Load of string | AddLoadPath of string diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll index 8ecc419c..291bc55f 100644 --- a/tools/coqdep_lexer.mll +++ b/tools/coqdep_lexer.mll @@ -16,8 +16,7 @@ type qualid = string list type coq_token = - | Require of qualid list - | RequireString of string + | Require of qualid option * qualid list | Declare of string list | Load of string | AddLoadPath of string @@ -271,16 +270,9 @@ and require_file = parse module_names := [coq_qual_id_tail lexbuf]; let qid = coq_qual_id_list lexbuf in parse_dot lexbuf; - match !from_pre_ident with - None -> - Require qid - | Some from -> - (from_pre_ident := None ; - Require (List.map (fun x -> from @ x) qid)) } - | '"' [^'"']* '"' (*'"'*) - { let s = Lexing.lexeme lexbuf in - parse_dot lexbuf; - RequireString (unquote_vfile_string s) } + let from = !from_pre_ident in + from_pre_ident := None; + Require (from, qid) } | eof { syntax_error lexbuf } | _ diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index cb704146..d2892167 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -320,6 +320,7 @@ let def_token = | "Instance" | "Declare" space+ "Instance" | "Global" space+ "Instance" + | "Functional" space+ "Scheme" let decl_token = "Hypothesis" diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index 9531cd2b..22febd6a 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -61,8 +61,8 @@ let usage () = prerr_endline " --coqlib_path set the path where Coq files are installed"; prerr_endline " -R map physical dir to Coq dir"; prerr_endline " -Q map physical dir to Coq dir"; - prerr_endline " --latin1 set ISO-8859-1 input language"; - prerr_endline " --utf8 set UTF-8 input language"; + prerr_endline " --latin1 set ISO-8859-1 mode"; + prerr_endline " --utf8 set UTF-8 mode"; prerr_endline " --charset set HTML charset"; prerr_endline " --inputenc set LaTeX input encoding"; prerr_endline " --interpolate try to typeset identifiers in comments using definitions in the same module"; @@ -557,10 +557,8 @@ let produce_output fl = (*s \textbf{Main program.} Print the banner, parse the command line, read the files and then call [produce_document] from module [Web]. *) -let main () = +let _ = let files = parse () in Index.init_coqlib_library (); if not !quiet then banner (); if files <> [] then produce_output files - -let _ = Printexc.catch main () diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 06030c45..8589f94a 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -197,8 +197,11 @@ module Latex = struct printf "\n"; printf "%%Warning: tipa declares many non-standard macros used by utf8x to\n"; printf "%%interpret utf8 characters but extra packages might have to be added\n"; - printf "%%(e.g. \"textgreek\" for Greek letters not already in tipa).\n"; - printf "%%Use coqdoc's option -p to add new packages.\n"; + printf "%%such as \"textgreek\" for Greek letters not already in tipa\n"; + printf "%%or \"stmaryrd\" for mathematical symbols.\n"; + printf "%%Utf8 codes missing a LaTeX interpretation can be defined by using\n"; + printf "%%\\DeclareUnicodeCharacter{code}{interpretation}.\n"; + printf "%%Use coqdoc's option -p to add new packages or declarations.\n"; printf "\\usepackage{tipa}\n"; printf "\n" diff --git a/tools/coqwc.mll b/tools/coqwc.mll index 417ec535..9a42553d 100644 --- a/tools/coqwc.mll +++ b/tools/coqwc.mll @@ -276,7 +276,7 @@ let rec parse = function (*s Main program. *) -let main () = +let _ = let files = parse (List.tl (Array.to_list Sys.argv)) in if not (!spec_only || !proof_only) then printf " spec proof comments\n"; @@ -285,8 +285,6 @@ let main () = | [f] -> process_file f | _ -> List.iter process_file files; print_totals () -let _ = Printexc.catch main () - (*i*)}(*i*) diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index c2b12668..a9a7251c 100644 --- a/tools/fake_ide.ml +++ b/tools/fake_ide.ml @@ -90,7 +90,7 @@ module Parser = struct (* {{{ *) in find ~-1 0 else raise (Err ("Balanced "^String.make 1 c^" not found in: "^s)) - let eat_blanks s = snd (eat_rex "[ \n\t]*") s + let eat_blanks s = snd (eat_rex "[ \r\n\t]*") s let s = ref "" @@ -257,6 +257,9 @@ let eval_print l coq = | [ Tok(_,"WAIT") ] -> let phrase = "Stm Wait." in eval_call (query (phrase,tip_id())) coq + | [ Tok(_,"JOIN") ] -> + let phrase = "Stm JoinDocument." in + eval_call (query (phrase,tip_id())) coq | [ Tok(_,"ASSERT"); Tok(_,"TIP"); Tok(_,id) ] -> let to_id, _ = get_id id in if not(Stateid.equal (Document.tip doc) to_id) then error "Wrong tip" @@ -273,6 +276,7 @@ let grammar = ; Seq [Item (eat_rex "EDIT_AT"); Item eat_id] ; Seq [Item (eat_rex "QUERY"); Opt (Item eat_id); Item eat_phrase] ; Seq [Item (eat_rex "WAIT")] + ; Seq [Item (eat_rex "JOIN")] ; Seq [Item (eat_rex "GOALS")] ; Seq [Item (eat_rex "FAILGOALS")] ; Seq [Item (eat_rex "ASSERT"); Item (eat_rex "TIP"); Item eat_id ] diff --git a/tools/gallina.ml b/tools/gallina.ml index 279919c5..5ce19e7f 100644 --- a/tools/gallina.ml +++ b/tools/gallina.ml @@ -39,7 +39,7 @@ let traite_stdin () = with Sys_error _ -> () -let gallina () = +let _ = let lg_command = Array.length Sys.argv in if lg_command < 2 then begin output_string stderr "Usage: gallina [-] [-stdout] file1 file2 ...\n"; @@ -59,6 +59,3 @@ let gallina () = traite_stdin () else List.iter traite_fichier !vfiles - -let _ = Printexc.catch gallina () - -- cgit v1.2.3