diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 26 | ||||
| -rw-r--r-- | tools/coqdep.ml | 465 | ||||
| -rw-r--r-- | tools/coqdep_boot.ml | 17 | ||||
| -rw-r--r-- | tools/coqdep_common.ml | 202 | ||||
| -rw-r--r-- | tools/coqdep_common.mli | 39 | ||||
| -rw-r--r-- | tools/coqdep_lexer.mli | 7 | ||||
| -rw-r--r-- | tools/coqdep_lexer.mll | 83 | ||||
| -rw-r--r-- | tools/coqdoc/cpretty.mll | 8 | ||||
| -rw-r--r-- | tools/dune | 10 | ||||
| -rw-r--r-- | tools/ocamllibdep.mll | 11 |
10 files changed, 99 insertions, 769 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 7cd5962d86..49fb88cd8c 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -91,6 +91,7 @@ COQDEP ?= "$(COQBIN)coqdep" COQDOC ?= "$(COQBIN)coqdoc" COQPP ?= "$(COQBIN)coqpp" COQMKFILE ?= "$(COQBIN)coq_makefile" +OCAMLLIBDEP ?= "$(COQBIN)ocamllibdep" # Timing scripts COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file.py" @@ -389,7 +390,11 @@ optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES)) .PHONY: optfiles # FIXME, see Ralf's bugreport -quick: $(VOFILES:.vo=.vio) +# quick is deprecated, now renamed vio +vio: $(VOFILES:.vo=.vio) +.PHONY: vio +quick: vio + $(warning "'make quick' is deprecated, use 'make vio' or consider using 'vos' files") .PHONY: quick vio2vo: @@ -397,8 +402,9 @@ vio2vo: -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio) .PHONY: vio2vo +# quick2vo is undocumented quick2vo: - $(HIDE)make -j $(J) quick + $(HIDE)make -j $(J) vio $(HIDE)VIOFILES=$$(for vofile in $(VOFILES); do \ viofile="$$(echo "$$vofile" | sed "s/\.vo$$/.vio/")"; \ if [ "$$vofile" -ot "$$viofile" -o ! -e "$$vofile" ]; then printf "$$viofile "; fi; \ @@ -450,13 +456,13 @@ all.ps: $(VFILES) $(SHOW)'COQDOC -ps $(GAL)' $(HIDE)$(COQDOC) \ -toc $(COQDOCFLAGS) -ps $(GAL) $(COQDOCLIBS) \ - -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)` + -o $@ `$(COQDEP) -sort $(VFILES)` all.pdf: $(VFILES) $(SHOW)'COQDOC -pdf $(GAL)' $(HIDE)$(COQDOC) \ -toc $(COQDOCFLAGS) -pdf $(GAL) $(COQDOCLIBS) \ - -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)` + -o $@ `$(COQDEP) -sort $(VFILES)` # FIXME: not quite right, since the output name is different gallinahtml: GAL=-g @@ -677,8 +683,8 @@ $(GLOBFILES): %.glob: %.v $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< $(VFILES:.v=.vio): %.vio: %.v - $(SHOW)COQC -quick $< - $(HIDE)$(TIMER) $(COQC) -quick $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< + $(SHOW)COQC -vio $< + $(HIDE)$(TIMER) $(COQC) -vio $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< $(VFILES:.v=.vos): %.vos: %.v $(SHOW)COQC -vos $< @@ -742,12 +748,12 @@ $(addsuffix .d,$(MLFILES)): %.ml.d: %.ml $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) $(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib - $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok) + $(SHOW)'OCAMLLIBDEP $<' + $(HIDE)$(OCAMLLIBDEP) -c $(OCAMLLIBS) "$<" $(redir_if_ok) $(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack - $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok) + $(SHOW)'OCAMLLIBDEP $<' + $(HIDE)$(OCAMLLIBDEP) -c $(OCAMLLIBS) "$<" $(redir_if_ok) # If this makefile is created using a _CoqProject we have coqdep get # options from it. This avoids argument length limits for pathological diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 2140014c58..a96173c057 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -9,9 +9,8 @@ (************************************************************************) open Format -open Coqdep_lexer -open Coqdep_common open Minisys +open Coqdep_common (** The basic parts of coqdep (i.e. the parts used by [coqdep -boot]) are now in [Coqdep_common]. The code that remains here concerns @@ -20,7 +19,6 @@ open Minisys As of today, this module depends on the following Coq modules: - - Flags - Envars - CoqProject_file @@ -28,424 +26,11 @@ open Minisys coqlib handling up so this can be bootstrapped earlier. *) -let option_D = ref false -let option_w = ref false let option_sort = ref false -let option_dump = ref None - -let warning_mult suf iter = - let tab = Hashtbl.create 151 in - let check f d = - begin try - let d' = Hashtbl.find tab f in - if (Filename.dirname (file_name f d)) - <> (Filename.dirname (file_name f d')) then begin - coqdep_warning "the file %s is defined twice!" (f ^ suf) - end - with Not_found -> () end; - Hashtbl.add tab f d - in - iter check - -let sort () = - let seen = Hashtbl.create 97 in - let rec loop file = - let file = canonize file in - if not (Hashtbl.mem seen file) then begin - Hashtbl.add seen file (); - let cin = open_in (file ^ ".v") in - let lb = Lexing.from_channel cin in - try - while true do - match coq_action lb with - | Require (from, sl) -> - List.iter - (fun s -> - match search_v_known ?from s with - | None -> () - | Some f -> loop f) - sl - | _ -> () - done - with Fin_fichier -> - close_in cin; - printf "%s%s " file !suffixe - end - in - List.iter (fun (name,_) -> loop name) !vAccu - -let (dep_tab : (string,string list) Hashtbl.t) = Hashtbl.create 151 - -let mL_dep_list b f = - try - Hashtbl.find dep_tab f - with Not_found -> - let deja_vu = ref ([] : string list) in - try - let chan = open_in f in - let buf = Lexing.from_channel chan in - try - while true do - let (Use_module str) = caml_action buf in - if str = b then begin - coqdep_warning "in file %s the notation %s. is useless !\n" f b - end else - if not (List.mem str !deja_vu) then addQueue deja_vu str - done; [] - with Fin_fichier -> begin - close_in chan; - let rl = List.rev !deja_vu in - Hashtbl.add dep_tab f rl; - rl - end - with Sys_error _ -> [] - -let affiche_Declare f dcl = - printf "\n*** In file %s: \n" f; - printf "Declare ML Module"; - List.iter (fun str -> printf " \"%s\"" str) dcl; - printf ".\n%!" - -let warning_Declare f dcl = - eprintf "*** Warning : in file %s, the ML modules declaration should be\n" f; - eprintf "*** Declare ML Module"; - List.iter (fun str -> eprintf " \"%s\"" str) dcl; - eprintf ".\n%!" - -let traite_Declare f = - let decl_list = ref ([] : string list) in - let rec treat = function - | s :: ll -> - let s' = basename_noext s in - (match search_ml_known s with - | Some mldir when not (List.mem s' !decl_list) -> - let fullname = file_name s' mldir in - let depl = mL_dep_list s (fullname ^ ".ml") in - treat depl; - decl_list := s :: !decl_list - | _ -> ()); - treat ll - | [] -> () - in - try - let chan = open_in f in - let buf = Lexing.from_channel chan in - begin try - while true do - let tok = coq_action buf in - (match tok with - | Declare sl -> - decl_list := []; - treat sl; - decl_list := List.rev !decl_list; - if !option_D then - affiche_Declare f !decl_list - else if !decl_list <> sl then - warning_Declare f !decl_list - | _ -> ()) - done - with Fin_fichier -> () end; - close_in chan - with Sys_error _ -> () - -let declare_dependencies () = - List.iter - (fun (name,_) -> - traite_Declare (name^".v"); - pp_print_flush std_formatter ()) - (List.rev !vAccu) - -(** DAGs guaranteed to be transitive reductions *) -module DAG (Node : Set.OrderedType) : -sig - type node = Node.t - type t - val empty : t - val add_transitive_edge : node -> node -> t -> t - val iter : (node -> node -> unit) -> t -> unit -end = -struct - type node = Node.t - module NSet = Set.Make(Node) - module NMap = Map.Make(Node) - - (** Associate to a node the set of its neighbours *) - type _t = NSet.t NMap.t - - (** Optimisation: construct the reverse graph at the same time *) - type t = { dir : _t; rev : _t; } - - - let node_equal x y = Node.compare x y = 0 - - let add_edge x y graph = - let set = try NMap.find x graph with Not_found -> NSet.empty in - NMap.add x (NSet.add y set) graph - - let remove_edge x y graph = - let set = try NMap.find x graph with Not_found -> NSet.empty in - let set = NSet.remove y set in - if NSet.is_empty set then NMap.remove x graph - else NMap.add x set graph - - let has_edge x y graph = - let set = try NMap.find x graph with Not_found -> NSet.empty in - NSet.mem y set - - let connected x y graph = - let rec aux rem seen = - if NSet.is_empty rem then false - else - let x = NSet.choose rem in - if node_equal x y then true - else - let rem = NSet.remove x rem in - if NSet.mem x seen then - aux rem seen - else - let seen = NSet.add x seen in - let next = try NMap.find x graph with Not_found -> NSet.empty in - let rem = NSet.union next rem in - aux rem seen - in - aux (NSet.singleton x) NSet.empty - - (** Check whether there is a path from a to b going through the edge - x -> y. *) - let connected_through a b x y graph = - let rec aux rem seen = - if NMap.is_empty rem then false - else - let (n, through) = NMap.choose rem in - if node_equal n b && through then true - else - let rem = NMap.remove n rem in - let is_seen = try Some (NMap.find n seen) with Not_found -> None in - match is_seen with - | None -> - let seen = NMap.add n through seen in - let next = try NMap.find n graph with Not_found -> NSet.empty in - let is_x = node_equal n x in - let push m accu = - let through = through || (is_x && node_equal m y) in - NMap.add m through accu - in - let rem = NSet.fold push next rem in - aux rem seen - | Some false -> - (* The path we took encountered x -> y but not the one in seen *) - if through then aux (NMap.add n true rem) (NMap.add n true seen) - else aux rem seen - | Some true -> aux rem seen - in - aux (NMap.singleton a false) NMap.empty - - let closure x graph = - let rec aux rem seen = - if NSet.is_empty rem then seen - else - let x = NSet.choose rem in - let rem = NSet.remove x rem in - if NSet.mem x seen then - aux rem seen - else - let seen = NSet.add x seen in - let next = try NMap.find x graph with Not_found -> NSet.empty in - let rem = NSet.union next rem in - aux rem seen - in - aux (NSet.singleton x) NSet.empty - - let empty = { dir = NMap.empty; rev = NMap.empty; } - - (** Online transitive reduction algorithm *) - let add_transitive_edge x y graph = - if connected x y graph.dir then graph - else - let dir = add_edge x y graph.dir in - let rev = add_edge y x graph.rev in - let graph = { dir; rev; } in - let ancestors = closure x rev in - let descendents = closure y dir in - let fold_ancestor a graph = - let fold_descendent b graph = - let to_remove = has_edge a b graph.dir in - let to_remove = to_remove && not (node_equal x a && node_equal y b) in - let to_remove = to_remove && connected_through a b x y graph.dir in - if to_remove then - let dir = remove_edge a b graph.dir in - let rev = remove_edge b a graph.rev in - { dir; rev; } - else graph - in - NSet.fold fold_descendent descendents graph - in - NSet.fold fold_ancestor ancestors graph - - let iter f graph = - let iter x set = NSet.iter (fun y -> f x y) set in - NMap.iter iter graph.dir - -end - -module Graph = -struct -(** Dumping a dependency graph **) - -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 = Util.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 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 () = 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 = - let token = try Some (coq_action buf) with Fin_fichier -> None in - match token with - | None -> acc - | Some action -> - let acc = match action with - | 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 = escape (file_name s dir) in - match !option_dynlink with - | No -> [] - | Byte -> [base,suff] - | Opt -> [base,".cmxs"] - | Both -> [base,suff; base,".cmxs"] - | Variable -> - if suff=".cmo" then [base,"$(DYNOBJ)"] - else [base,"$(DYNLIB)"] - in - let decl acc str = - let s = basename_noext str 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 -> - match search_ml_known s with - | Some mldir -> (declare ".cmo" mldir s) @ acc - | None -> acc - else acc - in - List.fold_left decl acc sl - | Load str -> - let str = Filename.basename str in - let seen = VCache.mem (None, [str]) !deja_vu_v in - if not seen then - 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 - loop acc - in - loop [] - -let treat_coq_file f = - let chan = try Some (open_in f) with Sys_error _ -> None in - match chan with - | None -> [] - | Some chan -> - try - let ans = treat_coq_file chan in - let () = close_in chan in - ans - with Syntax_error (i, j) -> close_in chan; error_cannot_parse f (i, j) - -type graph = - | Element of string - | Subgraph of string * graph list - -let rec insert_graph name path graphs = match path, graphs with - | [] , graphs -> (Element name) :: graphs - | (box :: boxes), (Subgraph (hd, names)) :: tl when hd = box -> - Subgraph (hd, insert_graph name boxes names) :: tl - | _, hd :: tl -> hd :: (insert_graph name path tl) - | (box :: boxes), [] -> [ Subgraph (box, insert_graph name boxes []) ] - -let print_graphs chan graph = - let rec print_aux name = function - | [] -> name - | (Element str) :: tl -> fprintf chan "\"%s\";\n" str; print_aux name tl - | Subgraph (box, names) :: tl -> - fprintf chan "subgraph cluster%n {\nlabel=\"%s\";\n" name box; - let name = print_aux (name + 1) names in - fprintf chan "}\n"; print_aux name tl - in - ignore (print_aux 0 graph) - -let rec pop_common_prefix = function - | [Subgraph (_, graphs)] -> pop_common_prefix graphs - | graphs -> graphs - -let split_path = Str.split (Str.regexp "/") - -let rec pop_last = function - | [] -> [] - | [ x ] -> [] - | x :: xs -> x :: pop_last xs - -let get_boxes path = pop_last (split_path path) - -let insert_raw_graph file = - insert_graph file (get_boxes file) - -let rec get_dependencies name args = - let vdep = treat_coq_file (name ^ ".v") in - let fold (deps, graphs, alseen) (dep, _) = - let dag = DAG.add_transitive_edge name dep deps in - if not (List.mem dep alseen) then - get_dependencies dep (dag, insert_raw_graph dep graphs, dep :: alseen) - else - (dag, graphs, alseen) - in - List.fold_left fold args vdep - -let coq_dependencies_dump chan dumpboxes = - let (deps, graphs, _) = - List.fold_left (fun ih (name, _) -> get_dependencies name ih) - (DAG.empty, List.fold_left (fun ih (file, _) -> insert_raw_graph file ih) [] !vAccu, - List.map fst !vAccu) !vAccu - in - fprintf chan "digraph dependencies {\n"; - if dumpboxes then print_graphs chan (pop_common_prefix graphs) - else List.iter (fun (name, _) -> fprintf chan "\"%s\"[label=\"%s\"]\n" name (basename_noext name)) !vAccu; - DAG.iter (fun name dep -> fprintf chan "\"%s\" -> \"%s\"\n" dep name) deps; - fprintf chan "}\n%!" - -end let usage () = eprintf " usage: coqdep [options] <filename>+\n"; eprintf " options:\n"; - eprintf " -c : Also print the dependencies of caml modules (=ocamldep).\n"; - (* Does not work anymore *) - (* eprintf " -w : Print informations on missing or wrong \"Declare - ML Module\" commands in coq files.\n"; *) - (* Does not work anymore: *) - (* eprintf " -D : Prints the missing ocmal module names. No dependency computed.\n"; *) eprintf " -boot : For coq developers, prints dependencies over coq library files (omitted by default).\n"; eprintf " -sort : output the given file name ordered by dependencies\n"; eprintf " -noglob | -no-glob : \n"; @@ -456,19 +41,14 @@ let usage () = eprintf " -R dir logname : add and import dir recursively to coq load path under logical name logname\n"; eprintf " -Q dir logname : add (recursively) and open (non recursively) dir to coq load path under logical name logname\n"; eprintf " -vos : also output dependencies about .vos files\n"; - eprintf " -dumpgraph f : print a dot dependency graph in file 'f'\n"; - eprintf " -dumpgraphbox f : print a dot dependency graph box in file 'f'\n"; eprintf " -exclude-dir dir : skip subdirectories named 'dir' during -R/-Q search\n"; eprintf " -coqlib dir : set the coq standard library directory\n"; - eprintf " -suffix s : \n"; - eprintf " -slash : deprecated, no effect\n"; eprintf " -dyndep (opt|byte|both|no|var) : set how dependencies over ML modules are printed\n"; exit 1 let split_period = Str.split (Str.regexp (Str.quote ".")) let add_q_include path l = add_rec_dir_no_import add_known path (split_period l) - let add_r_include path l = add_rec_dir_import add_known path (split_period l) let treat_coqproject f = @@ -482,9 +62,6 @@ let treat_coqproject f = iter_sourced (fun f -> treat_file None f) (all_files project) let rec parse = function - | "-c" :: ll -> option_c := true; parse ll - | "-D" :: ll -> option_D := true; parse ll - | "-w" :: ll -> option_w := true; parse ll | "-boot" :: ll -> option_boot := true; parse ll | "-sort" :: ll -> option_sort := true; parse ll | "-vos" :: ll -> write_vos := true; parse ll @@ -495,17 +72,10 @@ let rec parse = function | "-R" :: r :: ln :: ll -> add_r_include r ln; parse ll | "-Q" :: r :: ln :: ll -> add_q_include r 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 -> System.exclude_directory r; parse ll | "-exclude-dir" :: [] -> usage () | "-coqlib" :: r :: ll -> Envars.set_user_coqlib r; parse ll | "-coqlib" :: [] -> usage () - | "-suffix" :: s :: ll -> suffixe := s ; parse ll - | "-suffix" :: [] -> usage () - | "-slash" :: ll -> - coqdep_warning "warning: option -slash has no effect and is deprecated."; - parse ll | "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll | "-dyndep" :: "opt" :: ll -> option_dynlink := Opt; parse ll | "-dyndep" :: "byte" :: ll -> option_dynlink := Byte; parse ll @@ -525,19 +95,8 @@ let coqdep () = (* Add current dir with empty logical path if not set by options above. *) (try ignore (Coqdep_common.find_dir_logpath (Sys.getcwd())) with Not_found -> add_norec_dir_import add_known "." []); - (* NOTE: These directories are searched from last to first *) - if !option_boot then begin - add_rec_dir_import add_known "theories" ["Coq"]; - add_rec_dir_import add_known "plugins" ["Coq"]; - add_rec_dir_import (fun _ -> add_caml_known) "theories" ["Coq"]; - add_rec_dir_import (fun _ -> add_caml_known) "plugins" ["Coq"]; - let user = "user-contrib" in - if Sys.file_exists user then begin - add_rec_dir_no_import add_known user []; - add_rec_dir_no_import (fun _ -> add_caml_known) user []; - end; - end else begin - (* option_boot is actually always false in this branch *) + (* We don't setup any loadpath if the -boot is passed *) + if not !option_boot then begin Envars.set_coqlib ~fail:(fun msg -> raise (CoqlibError msg)); let coqlib = Envars.coqlib () in add_rec_dir_import add_coqlib_known (coqlib//"theories") ["Coq"]; @@ -548,23 +107,9 @@ let coqdep () = (Envars.xdg_dirs ~warn:(fun x -> coqdep_warning "%s" 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; - List.iter (fun (f,d) -> add_mllib_known f d ".mllib") !mllibAccu; - List.iter (fun (f,suff,d) -> add_ml_known f d suff) !mlAccu; - warning_mult ".mli" iter_mli_known; - warning_mult ".ml" iter_ml_known; if !option_sort then begin sort (); exit 0 end; - if !option_c && not !option_D then mL_dependencies (); - if not !option_D then coq_dependencies (); - if !option_w || !option_D then declare_dependencies (); - begin match !option_dump with - | None -> () - | Some (box, file) -> - let chan = open_out file in - let chan_fmt = formatter_of_out_channel chan in - try Graph.coq_dependencies_dump chan_fmt box; close_out chan - with e -> close_out chan; raise e - end + coq_dependencies (); + () let _ = try diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml index 1730dd3d68..1cebb3638e 100644 --- a/tools/coqdep_boot.ml +++ b/tools/coqdep_boot.ml @@ -19,6 +19,7 @@ open Coqdep_common let split_period = Str.split (Str.regexp (Str.quote ".")) let add_q_include path l = add_rec_dir_no_import add_known path (split_period l) +let add_r_include path l = add_rec_dir_import add_known path (split_period l) let rec parse = function | "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll @@ -26,16 +27,14 @@ let rec parse = function | "-dyndep" :: "byte" :: ll -> option_dynlink := Byte; parse ll | "-dyndep" :: "both" :: ll -> option_dynlink := Both; parse ll | "-dyndep" :: "var" :: ll -> option_dynlink := Variable; parse ll - | "-c" :: ll -> option_c := true; parse ll | "-boot" :: ll -> parse ll (* We're already in boot mode by default *) - | "-mldep" :: ocamldep :: ll -> - option_mldep := Some ocamldep; option_c := true; parse ll | "-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; norec_dirs := StrSet.add r !norec_dirs; parse ll + | "-R" :: r :: ln :: ll -> add_r_include r ln; parse ll | "-Q" :: r :: ln :: ll -> add_q_include r ln; parse ll | f :: ll -> treat_file None f; parse ll | [] -> () @@ -44,16 +43,4 @@ let _ = let () = option_boot := true in if Array.length Sys.argv < 2 then exit 1; parse (List.tl (Array.to_list Sys.argv)); - if !option_c then begin - add_rec_dir_import add_known "." []; - add_rec_dir_import (fun _ -> add_caml_known) "." ["Coq"]; - end - else 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; - if !option_c then mL_dependencies (); coq_dependencies () diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 775c528176..683165f026 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -31,16 +31,12 @@ module StrListMap = Map.Make(StrList) type dynlink = Opt | Byte | Both | No | Variable -let option_c = ref false let option_noglob = ref false let option_dynlink = ref Both let option_boot = ref false -let option_mldep = ref None let norec_dirs = ref StrSet.empty -let suffixe = ref ".vo" - type dir = string option (** [get_extension f l] checks whether [f] has one of the extensions @@ -59,18 +55,6 @@ let basename_noext filename = let fn = Filename.basename filename in try Filename.chop_extension fn with Invalid_argument _ -> fn -(** ML Files specified on the command line. In the entries: - - the first string is the basename of the file, without extension nor - directory part - - the second string of [mlAccu] is the extension (either .ml or .mlg) - - the [dir] part is the directory, with None used as the current directory -*) - -let mlAccu = ref ([] : (string * string * dir) list) -and mliAccu = ref ([] : (string * dir) list) -and mllibAccu = ref ([] : (string * dir) list) -and mlpackAccu = ref ([] : (string * dir) list) - (** Coq files specifies on the command line: - first string is the full filename, with only its extension removed - second string is the absolute version of the previous (via getcwd) @@ -126,8 +110,6 @@ let mkknown () = with Not_found -> None in add, iter, search -let add_ml_known, iter_ml_known, search_ml_known = mkknown () -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 () @@ -232,88 +214,6 @@ let file_name s = function | None -> s | Some d -> d // s -let depend_ML str = - match search_mli_known str, search_ml_known str with - | Some mlidir, Some mldir -> - let mlifile = file_name str mlidir - and mlfile = file_name str mldir in - (" "^mlifile^".cmi"," "^mlfile^".cmx") - | None, Some mldir -> - let mlfile = file_name str mldir in - (" "^mlfile^".cmo"," "^mlfile^".cmx") - | Some mlidir, None -> - let mlifile = file_name str mlidir in - (" "^mlifile^".cmi"," "^mlifile^".cmi") - | None, None -> "", "" - -let soustraite_fichier_ML dep md ext = - try - let chan = open_process_in (dep^" -modules "^md^ext) in - let list = ocamldep_parse (Lexing.from_channel chan) in - let a_faire = ref "" in - let a_faire_opt = ref "" in - List.iter - (fun str -> - let byte,opt = depend_ML str in - a_faire := !a_faire ^ byte; - a_faire_opt := !a_faire_opt ^ opt) - (List.rev list); - (!a_faire, !a_faire_opt) - with - | Sys_error _ -> ("","") - | _ -> - Printf.eprintf "Coqdep: subprocess %s failed on file %s%s\n" dep md ext; - exit 1 - -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 (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 StrSet.mem str !deja_vu then - () - else begin - 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 - end - done - with Fin_fichier -> () - end; - close_in chan; - (!a_faire, !a_faire_opt) - with Sys_error _ -> ("","") - -let traite_fichier_ML md ext = - match !option_mldep with - | Some dep -> soustraite_fichier_ML dep md ext - | None -> autotraite_fichier_ML md ext - -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) - (* 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 @@ -443,10 +343,7 @@ let rec find_dependencies basename = | None -> match search_mlpack_known s with | Some mldir -> declare ".cmo" mldir s - | None -> - match search_ml_known s with - | Some mldir -> declare ".cmo" mldir s - | None -> warning_declare f str + | None -> warning_declare f str end in List.iter decl sl @@ -474,59 +371,16 @@ let rec find_dependencies basename = with Sys_error _ -> [] (* TODO: report an error? *) -let mL_dependencies () = - List.iter - (fun (name,ext,dirname) -> - let fullname = file_name name dirname in - let (dep,dep_opt) = traite_fichier_ML fullname ext in - let intf = match search_mli_known name with - | None -> "" - | Some mldir -> " "^(file_name name mldir)^".cmi" - in - let efullname = escape fullname in - printf "%s.cmo:%s%s\n" efullname dep intf; - printf "%s.cmx:%s%s\n%!" efullname dep_opt intf) - (List.rev !mlAccu); - List.iter - (fun (name,dirname) -> - let fullname = file_name name dirname in - let (dep,_) = traite_fichier_ML fullname ".mli" in - printf "%s.cmi:%s\n%!" (escape fullname) dep) - (List.rev !mliAccu); - 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 (String.concat " " dep); - printf "%s.cma:$(addsuffix .cmo,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname; - printf "%s.cmxa:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n%!" efullname efullname) - (List.rev !mllibAccu); - List.iter - (fun (name,dirname) -> - let fullname = file_name name dirname in - let dep = traite_fichier_modules fullname ".mlpack" in - let efullname = escape fullname in - printf "%s_MLPACK_DEPENDENCIES:=%s\n" efullname (String.concat " " dep); - printf "%s.cmo:$(addsuffix .cmo,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname; - printf "%s.cmx:$(addsuffix .cmx,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname; - let efullname_capital = String.capitalize_ascii (Filename.basename efullname) in - List.iter (fun dep -> - printf "%s.cmx : FOR_PACK=-for-pack %s\n" dep efullname_capital) - dep; - printf "%!") - (List.rev !mlpackAccu) - let write_vos = ref false let coq_dependencies () = List.iter (fun (name,_) -> let ename = escape name in - let glob = if !option_noglob then "" else " "^ename^".glob" in + let glob = if !option_noglob then "" else ename^".glob " in let deps = find_dependencies name in - printf "%s%s%s %s.v.beautified %s.required_vo: %s.v %s\n" ename !suffixe glob ename ename ename - (string_of_dependency_list !suffixe deps); + printf "%s.vo %s%s.v.beautified %s.required_vo: %s.v %s\n" ename glob ename ename ename + (string_of_dependency_list ".vo" deps); printf "%s.vio: %s.v %s\n" ename ename (string_of_dependency_list ".vio" deps); if !write_vos then @@ -542,10 +396,8 @@ let rec suffixes = function let add_caml_known phys_dir _ f = let basename,suff = - get_extension f [".ml";".mli";".mlg";".mllib";".mlpack"] in + get_extension f [".mllib"; ".mlpack"] in match suff with - | ".ml"|".mlg" -> add_ml_known basename (Some phys_dir) suff - | ".mli" -> add_mli_known basename (Some phys_dir) suff | ".mllib" -> add_mllib_known basename (Some phys_dir) suff | ".mlpack" -> add_mlpack_known basename (Some phys_dir) suff | _ -> () @@ -630,14 +482,38 @@ let rec treat_file old_dirname old_name = in Array.iter (treat_file (Some newdirname)) (Sys.readdir complete_name)) | S_REG -> - (match get_extension name [".v";".ml";".mli";".mlg";".mllib";".mlpack"] with - | (base,".v") -> - let name = file_name base dirname - and absname = absolute_file_name base dirname in - addQueue vAccu (name, absname) - | (base,(".ml"|".mlg" as ext)) -> addQueue mlAccu (base,ext,dirname) - | (base,".mli") -> addQueue mliAccu (base,dirname) - | (base,".mllib") -> addQueue mllibAccu (base,dirname) - | (base,".mlpack") -> addQueue mlpackAccu (base,dirname) - | _ -> ()) + (match get_extension name [".v"] with + | base,".v" -> + let name = file_name base dirname + and absname = absolute_file_name base dirname in + addQueue vAccu (name, absname) + | _ -> ()) | _ -> () + +(* "[sort]" outputs `.v` files required by others *) +let sort () = + let seen = Hashtbl.create 97 in + let rec loop file = + let file = canonize file in + if not (Hashtbl.mem seen file) then begin + Hashtbl.add seen file (); + let cin = open_in (file ^ ".v") in + let lb = Lexing.from_channel cin in + try + while true do + match coq_action lb with + | Require (from, sl) -> + List.iter + (fun s -> + match search_v_known ?from s with + | None -> () + | Some f -> loop f) + sl + | _ -> () + done + with Fin_fichier -> + close_in cin; + printf "%s.v " file + end + in + List.iter (fun (name,_) -> loop name) !vAccu diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli index 6d49f7e06c..aca68cc780 100644 --- a/tools/coqdep_common.mli +++ b/tools/coqdep_common.mli @@ -20,45 +20,25 @@ val coqdep_warning : ('a, Format.formatter, unit, unit) format4 -> 'a twice.*) val find_dir_logpath: string -> string list -val option_c : bool ref +(** Options *) val option_noglob : bool ref val option_boot : bool ref - val write_vos : bool ref -(** output vos and vok dependencies *) type dynlink = Opt | Byte | Both | No | Variable - val option_dynlink : dynlink ref -val option_mldep : string option ref + val norec_dirs : StrSet.t ref -val suffixe : string ref + type dir = string option -val get_extension : string -> string list -> string * string -val basename_noext : string -> string -val mlAccu : (string * string * dir) list ref -val mliAccu : (string * dir) list ref -val mllibAccu : (string * dir) list ref -val vAccu : (string * string) list ref -val addQueue : 'a list ref -> 'a -> unit -val add_ml_known : string -> dir -> string -> unit -val iter_ml_known : (string -> dir -> unit) -> unit -val search_ml_known : string -> dir option -val add_mli_known : string -> dir -> string -> unit -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 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 -val mL_dependencies : unit -> unit +val treat_file : dir -> string -> unit + +(** ML-related manipulation *) 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 + +(* Used to locate plugins for [Declare ML Module] *) val add_caml_dir : string -> unit (** Simply add this directory and imports it, no subdirs. This is used @@ -74,5 +54,4 @@ val add_rec_dir_no_import : val add_rec_dir_import : (bool -> string -> string list -> string -> unit) -> string -> string list -> unit -val treat_file : dir -> string -> unit -val error_cannot_parse : string -> int * int -> 'a +val sort : unit -> unit diff --git a/tools/coqdep_lexer.mli b/tools/coqdep_lexer.mli index 018fc1b7a2..24452f203a 100644 --- a/tools/coqdep_lexer.mli +++ b/tools/coqdep_lexer.mli @@ -8,12 +8,10 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -type mL_token = Use_module of string - type qualid = string list type coq_token = - Require of qualid option * qualid list + | Require of qualid option * qualid list | Declare of string list | Load of string | AddLoadPath of string @@ -23,6 +21,3 @@ exception Fin_fichier exception Syntax_error of int * int val coq_action : Lexing.lexbuf -> coq_token -val caml_action : Lexing.lexbuf -> mL_token -val mllib_list : Lexing.lexbuf -> string list -val ocamldep_parse : Lexing.lexbuf -> string list diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll index 743da535b8..157c2b7dba 100644 --- a/tools/coqdep_lexer.mll +++ b/tools/coqdep_lexer.mll @@ -13,8 +13,6 @@ open Filename open Lexing - type mL_token = Use_module of string - type qualid = string list type coq_token = @@ -152,56 +150,6 @@ and add_loadpath_as path = parse | dot { AddLoadPath path } -and caml_action = parse - | space + - { caml_action lexbuf } - | "open" space* (caml_up_ident as id) - { Use_module (String.uncapitalize_ascii id) } - | "module" space+ caml_up_ident - { caml_action lexbuf } - | caml_low_ident { caml_action lexbuf } - | caml_up_ident - { qual_id (Lexing.lexeme lexbuf) lexbuf } - | ['0'-'9']+ - | '0' ['x' 'X'] ['0'-'9' 'A'-'F' 'a'-'f']+ - | '0' ['o' 'O'] ['0'-'7']+ - | '0' ['b' 'B'] ['0'-'1']+ - { caml_action lexbuf } - | ['0'-'9']+ ('.' ['0'-'9']*)? (['e' 'E'] ['+' '-']? ['0'-'9']+)? - { caml_action lexbuf } - | "\"" - { string lexbuf; caml_action lexbuf } - | "'" [^ '\\' '\''] "'" - { caml_action lexbuf } - | "'" '\\' ['\\' '\'' 'n' 't' 'b' 'r'] "'" - { caml_action lexbuf } - | "'" '\\' ['0'-'9'] ['0'-'9'] ['0'-'9'] "'" - { caml_action lexbuf } - | "(*" - { comment lexbuf; caml_action lexbuf } - | "#" | "&" | "&&" | "'" | "(" | ")" | "*" | "," | "?" | "->" | "." | ".." - | ".(" | ".[" | ":" | "::" | ":=" | ";" | ";;" | "<-" | "=" | "[" | "[|" - | "[<" | "]" | "_" | "{" | "|" | "||" | "|]" | ">]" | "}" | "!=" | "-" - | "-." { caml_action lexbuf } - - | ['!' '?' '~'] - ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~'] * - { caml_action lexbuf } - | ['=' '<' '>' '@' '^' '|' '&' '$'] - ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~'] * - { caml_action lexbuf } - | ['+' '-'] - ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~'] * - { caml_action lexbuf } - | "**" - ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~'] * - { caml_action lexbuf } - | ['*' '/' '%'] - ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~'] * - { caml_action lexbuf } - | eof { raise Fin_fichier } - | _ { caml_action lexbuf } - and comment = parse | "(*" { comment lexbuf; comment lexbuf } @@ -218,20 +166,6 @@ and comment = parse | _ { comment lexbuf } -and string = parse - | '"' (* '"' *) - { () } - | '\\' ("\010" | "\013" | "\010\013") [' ' '\009'] * - { string lexbuf } - | '\\' ['\\' '"' 'n' 't' 'b' 'r'] (*'"'*) - { string lexbuf } - | '\\' ['0'-'9'] ['0'-'9'] ['0'-'9'] - { string lexbuf } - | eof - { raise Fin_fichier } - | _ - { string lexbuf } - and load_file = parse | '"' [^ '"']* '"' (*'"'*) { let s = lexeme lexbuf in @@ -320,20 +254,3 @@ and modules mllist = parse { syntax_error lexbuf } | _ { Declare (List.rev mllist) } - -and qual_id ml_module_name = parse - | '.' [^ '.' '(' '['] - { Use_module (String.uncapitalize_ascii ml_module_name) } - | eof { raise Fin_fichier } - | _ { caml_action lexbuf } - -and mllib_list = parse - | caml_up_ident { let s = String.uncapitalize_ascii (Lexing.lexeme lexbuf) - in s :: mllib_list lexbuf } - | "*predef*" { mllib_list lexbuf } - | space+ { mllib_list lexbuf } - | eof { [] } - | _ { syntax_error lexbuf } - -and ocamldep_parse = parse - | [^ ':' ]* ':' { mllib_list lexbuf } diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index a44ddf7467..13913cabc3 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -547,6 +547,9 @@ rule coq_bol = parse comment lexbuf end else skipped_comment lexbuf in if eol then coq_bol lexbuf else coq lexbuf } + | space* "#[" { + let eol = begin backtrack lexbuf; body_bol lexbuf end + in if eol then coq_bol lexbuf else coq lexbuf } | eof { () } | _ @@ -643,6 +646,11 @@ and coq = parse Output.ident s None; let eol = body lexbuf in if eol then coq_bol lexbuf else coq lexbuf } + | "#[" + { ignore(lexeme lexbuf); + Output.char '#'; Output.char '['; + let eol = body lexbuf in + if eol then coq_bol lexbuf else coq lexbuf } | space+ { Output.char ' '; coq lexbuf } | eof { () } diff --git a/tools/dune b/tools/dune index 204bd09535..c0e4e20f72 100644 --- a/tools/dune +++ b/tools/dune @@ -29,7 +29,15 @@ (modules coqdep_lexer coqdep_common coqdep) (libraries coq.lib)) -(ocamllex coqdep_lexer) +; Bare-bones mllib/mlpack parser +(executable + (name ocamllibdep) + (public_name ocamllibdep) + (modules ocamllibdep) + (package coq) + (libraries unix)) + +(ocamllex coqdep_lexer ocamllibdep) (executable (name coqwc) diff --git a/tools/ocamllibdep.mll b/tools/ocamllibdep.mll index 41a4e2a86a..2ecc20f1b0 100644 --- a/tools/ocamllibdep.mll +++ b/tools/ocamllibdep.mll @@ -195,6 +195,14 @@ let mllib_dependencies () = flush stdout) (List.rev !mllibAccu) +let coq_makefile_mode = ref false + +let print_for_pack modname d = + if !coq_makefile_mode then + printf "%s.cmx : FOR_PACK=-for-pack %s\n" d modname + else + printf "%s_FORPACK:= -for-pack %s\n" d modname + let mlpack_dependencies () = List.iter (fun (name,dirname) -> @@ -204,7 +212,7 @@ let mlpack_dependencies () = 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; + List.iter (print_for_pack modname) deps; printf "%s.cmo:$(addsuffix .cmo,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname; printf "%s.cmx:$(addsuffix .cmx,$(%s_MLPACK_DEPENDENCIES))\n" @@ -213,6 +221,7 @@ let mlpack_dependencies () = (List.rev !mlpackAccu) let rec parse = function + | "-c" :: r -> coq_makefile_mode := true; parse r | "-I" :: r :: ll -> (* To solve conflict (e.g. same filename in kernel and checker) we allow to state an explicit order *) |