diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coq_makefile.ml | 27 | ||||
| -rw-r--r-- | tools/coqc.ml | 25 | ||||
| -rw-r--r-- | tools/coqdep.ml | 11 | ||||
| -rw-r--r-- | tools/coqdep_common.ml | 82 | ||||
| -rw-r--r-- | tools/coqdep_common.mli | 8 | ||||
| -rw-r--r-- | tools/coqdep_lexer.mll | 126 | ||||
| -rw-r--r-- | tools/coqmktop.ml | 13 | ||||
| -rw-r--r-- | tools/fake_ide.ml | 23 | ||||
| -rw-r--r-- | tools/ocamllibdep.mll | 201 |
9 files changed, 325 insertions, 191 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 80217587d5..7b76514e46 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -50,7 +50,7 @@ let lib_dirs = ["kernel"; "lib"; "library"; "parsing"; "pretyping"; "interp"; "printing"; "intf"; "proofs"; "tactics"; "tools"; "toplevel"; - "stm"; "grammar"; "config"] + "stm"; "grammar"; "config"; "ltac"; "engine"] let usage () = @@ -371,7 +371,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 () = () @@ -381,19 +381,19 @@ let implicit () = let mli_rules () = print "$(MLIFILES:.mli=.cmi): %.cmi: %.mli\n\t$(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$(OCAMLFIND) ocamldep -slash $(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 "$(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$(OCAMLDEP) -slash $(OCAMLLIBS) $(PP) -impl \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in + print "\t$(OCAMLFIND) 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"; print "\t$(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$(OCAMLFIND) ocamldep -slash $(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"; @@ -467,17 +467,18 @@ let variables is_install opt (args,defs) = 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 "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 else CAMLP4EXTEND=threads.cma endif\n"; - print "PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(CAMLLIB)threads/ $(COQSRCLIBS) compat5.cmo \\ + print "PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(CAMLLIB)/threads/ $(COQSRCLIBS) compat5.cmo \\ $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'\n\n"; end; match is_install with @@ -519,7 +520,7 @@ let parameters () = 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"; @@ -694,9 +695,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 diff --git a/tools/coqc.ml b/tools/coqc.ml index b7910e13a0..f957200ab5 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 () @@ -124,21 +113,11 @@ let parse_args () = | 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 79662a5d30..13705edaaa 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,6 +491,7 @@ 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 diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index a90264e261..c63e4aaa64 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -9,6 +9,7 @@ open Printf open Coqdep_lexer open Unix +open System (** [coqdep_boot] is a stripped-down version of [coqdep], whose behavior is the one of [coqdep -boot]. Its only dependencies @@ -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 @@ -527,31 +512,25 @@ let add_known recur phys_dir log_dir f = 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 + System.check_unix_dir (fun s -> eprintf "*** Warning: %s\n" s) phys_dir; + 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 +543,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 +569,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 97bdfaefb5..633c474ada 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 b16dd33804..eb233b8f94 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/coqmktop.ml b/tools/coqmktop.ml index a45c625bcc..6f3d8e2b8f 100644 --- a/tools/coqmktop.ml +++ b/tools/coqmktop.ml @@ -149,7 +149,7 @@ let usage () = prerr_endline "Usage: coqmktop <options> <ocaml options> files\ \nFlags are:\ \n -coqlib dir Specify where the Coq object files are\ -\n -camlbin dir Specify where the OCaml binaries are\ +\n -ocamlfind dir Specify where the ocamlfind binary is\ \n -camlp4bin dir Specify where the Camlp4/5 binaries are\ \n -o exec-file Specify the name of the resulting toplevel\ \n -boot Run in boot mode\ @@ -167,8 +167,8 @@ let parse_args () = (* Directories *) | "-coqlib" :: d :: rem -> Flags.coqlib_spec := true; Flags.coqlib := d ; parse (op,fl) rem - | "-camlbin" :: d :: rem -> - Flags.camlbin_spec := true; Flags.camlbin := d ; parse (op,fl) rem + | "-ocamlfind" :: d :: rem -> + Flags.ocamlfind_spec := true; Flags.ocamlfind := d ; parse (op,fl) rem | "-camlp4bin" :: d :: rem -> Flags.camlp4bin_spec := true; Flags.camlp4bin := d ; parse (op,fl) rem | "-R" :: d :: rem -> parse (incl_all_subdirs d op,fl) rem @@ -266,10 +266,9 @@ let main () = let (options, userfiles) = parse_args () in (* Directories: *) let () = Envars.set_coqlib ~fail:Errors.error in - let camlbin = Envars.camlbin () 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 1fdda04cba..e81f4038d6 100644 --- a/tools/fake_ide.ml +++ b/tools/fake_ide.ml @@ -17,7 +17,18 @@ 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 content let base_eval_call ?(print=true) ?(fail=true) call coqtop = if print then prerr_endline (Xmlprotocol.pr_call call); @@ -38,8 +49,8 @@ let base_eval_call ?(print=true) ?(fail=true) call coqtop = 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 0000000000..670ff487c5 --- /dev/null +++ b/tools/ocamllibdep.mll @@ -0,0 +1,201 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +{ + exception Syntax_error of int*int + + let syntax_error lexbuf = + raise (Syntax_error (Lexing.lexeme_start lexbuf, Lexing.lexeme_end lexbuf)) +} + +let space = [' ' '\t' '\n' '\r'] +let lowercase = ['a'-'z' '\223'-'\246' '\248'-'\255'] +let uppercase = ['A'-'Z' '\192'-'\214' '\216'-'\222'] +let identchar = + ['A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9'] +let caml_up_ident = uppercase identchar* +let caml_low_ident = lowercase identchar* + +rule mllib_list = parse + | caml_up_ident { let s = String.uncapitalize (Lexing.lexeme lexbuf) + in s :: mllib_list lexbuf } + | "*predef*" { mllib_list lexbuf } + | space+ { mllib_list lexbuf } + | eof { [] } + | _ { syntax_error lexbuf } + +{ +open Printf +open Unix + +(** [coqdep_boot] is a stripped-down version of [coqdep] used to treat + with mllib files. +*) + +(* Makefile's escaping rules are awful: $ is escaped by doubling and + other special characters are escaped by backslash prefixing while + backslashes themselves must be escaped only if part of a sequence + followed by a special character (i.e. in case of ambiguity with a + use of it as escaping character). Moreover (even if not crucial) + it is apparently not possible to directly escape ';' and leading '\t'. *) + +let escape = + let s' = Buffer.create 10 in + fun s -> + Buffer.clear s'; + for i = 0 to String.length s - 1 do + let c = s.[i] in + if c = ' ' || c = '#' || c = ':' (* separators and comments *) + || c = '%' (* pattern *) + || c = '?' || c = '[' || c = ']' || c = '*' (* expansion in filenames *) + || i=0 && c = '~' && (String.length s = 1 || s.[1] = '/' || + 'A' <= s.[1] && s.[1] <= 'Z' || + 'a' <= s.[1] && s.[1] <= 'z') (* homedir expansion *) + then begin + let j = ref (i-1) in + while !j >= 0 && s.[!j] = '\\' do + Buffer.add_char s' '\\'; decr j (* escape all preceding '\' *) + done; + Buffer.add_char s' '\\'; + end; + if c = '$' then Buffer.add_char s' '$'; + Buffer.add_char s' c + done; + Buffer.contents s' + +(* Filename.concat but always with a '/' *) +let is_dir_sep s i = + match Sys.os_type with + | "Unix" -> s.[i] = '/' + | "Cygwin" | "Win32" -> + let c = s.[i] in c = '/' || c = '\\' || c = ':' + | _ -> assert false + +let (//) dirname filename = + let l = String.length dirname in + if l = 0 || is_dir_sep dirname (l-1) + then dirname ^ filename + else dirname ^ "/" ^ filename + +(** [get_extension f l] checks whether [f] has one of the extensions + listed in [l]. It returns [f] without its extension, alongside with + the extension. When no extension match, [(f,"")] is returned *) + +let rec get_extension f = function + | [] -> (f, "") + | s :: _ when Filename.check_suffix f s -> (Filename.chop_suffix f s, s) + | _ :: l -> get_extension f l + +let file_name s = function + | None -> s + | Some "." -> s + | Some d -> d // s + +type dir = string option + +let add_directory add_file phys_dir = + Array.iter (fun f -> + (* we avoid all files starting by '.' *) + if f.[0] <> '.' then + let phys_f = if phys_dir = "." then f else phys_dir//f in + match try (stat phys_f).st_kind with _ -> S_BLK with + | S_REG -> add_file phys_dir f + | _ -> ()) (Sys.readdir phys_dir) + +let error_cannot_parse s (i,j) = + Printf.eprintf "File \"%s\", characters %i-%i: Syntax error\n" s i j; + exit 1 + +let warning_ml_clash x s suff s' suff' = + if suff = suff' then + eprintf + "*** Warning: %s%s already found in %s (discarding %s%s)\n" x suff + (match s with None -> "." | Some d -> d) + ((match s' with None -> "." | Some d -> d) // x) suff + +let mkknown () = + let h = (Hashtbl.create 19 : (string, dir * string) Hashtbl.t) in + let add x s suff = + try let s',suff' = Hashtbl.find h x in warning_ml_clash x s' suff' s suff + with Not_found -> Hashtbl.add h x (s,suff) + and search x = + try Some (fst (Hashtbl.find h x)) + with Not_found -> None + in add, search + +let add_ml_known, search_ml_known = mkknown () +let add_mlpack_known, search_mlpack_known = mkknown () + +let mllibAccu = ref ([] : (string * dir) list) + +let 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 a_faire str -> match search_mlpack_known str with + | Some mldir -> + let file = file_name str mldir in + a_faire^" "^file + | None -> + match search_ml_known str with + | Some mldir -> + let file = file_name str mldir in + a_faire^" "^file + | None -> a_faire) "" 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"] with + | (base,".mllib") -> addQueue mllibAccu (base,dirname) + | _ -> () + +let mllib_dependencies () = + List.iter + (fun (name,dirname) -> + let fullname = file_name name dirname in + let dep = traite_fichier_modules fullname ".mllib" in + 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; + flush Pervasives.stdout) + (List.rev !mllibAccu) + +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 coqdep_boot () = + if Array.length Sys.argv < 2 then exit 1; + parse (List.tl (Array.to_list Sys.argv)); + mllib_dependencies () + +let _ = Printexc.catch coqdep_boot () +} |