From 9cdf9c3c0341a395249946d9e8f0bed7dd3c6d53 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 24 Dec 2008 14:38:55 +0000 Subject: - coq_makefile: target install now respects the original tree structure of the archive to install in coq user-contrib installation directory. - Relaxed the validity check on identifiers from an error to a warning. - Added a filtering option to Print LoadPath. - Support for empty root in option -R. - Better handling of redundant paths in ml loadpath. - Makefile's: Added target initplugins and added initplugins to coqbinaries. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11713 85f007b7-540e-0410-9357-904b9bb8a0f7 --- CHANGES | 1 + Makefile.build | 4 +- Makefile.common | 2 +- contrib/interface/xlate.ml | 3 +- doc/refman/RefMan-oth.tex | 5 + kernel/names.ml | 2 +- lib/system.ml | 28 ++++ lib/system.mli | 2 + lib/util.ml | 47 ++++--- lib/util.mli | 1 + library/libnames.ml | 12 +- library/library.ml | 42 ++---- library/library.mli | 3 + parsing/g_vernac.ml4 | 2 +- parsing/ppvernac.ml | 2 +- tools/coq_makefile.ml4 | 318 ++++++++++++++++++++++++++++----------------- toplevel/coqtop.ml | 16 ++- toplevel/mltop.ml4 | 12 +- toplevel/vernacentries.ml | 7 +- toplevel/vernacexpr.ml | 2 +- 20 files changed, 317 insertions(+), 194 deletions(-) diff --git a/CHANGES b/CHANGES index 395b4cf70..20b3131c4 100644 --- a/CHANGES +++ b/CHANGES @@ -82,6 +82,7 @@ Vernacular commands compiled in native code with a version of OCaml that supports native Dynlink (>= 3.11). - Specific sort constraints on Record now taken into account. +- "Print LoadPath" supports a path argument to filter the display. Libraries (DOC TO CHECK) diff --git a/Makefile.build b/Makefile.build index fefaf2cb7..6a0857ccd 100644 --- a/Makefile.build +++ b/Makefile.build @@ -165,13 +165,13 @@ kernel/copcodes.ml: kernel/byterun/coq_instruct.h # Main targets (coqmktop, coqtop.opt, coqtop.byte) ########################################################################### -coqbinaries:: ${COQBINARIES} ${CSDPCERT} +coqbinaries:: ${COQBINARIES} ${CSDPCERT} $(INITPLUGINSOPT) $(INITPLUGINS) coq: coqlib tools coqbinaries coqlib:: initplugins theories contrib -coqlight: initplugins theories-light tools coqbinaries +coqlight: theories-light tools coqbinaries states:: states/initial.coq diff --git a/Makefile.common b/Makefile.common index c2f3e305b..b5c81882f 100644 --- a/Makefile.common +++ b/Makefile.common @@ -911,7 +911,7 @@ STAGE2_TARGETS:=$(COQBINARIES) lib kernel byterun library proofs tactics \ interp parsing pretyping highparsing toplevel hightactics \ coqide-binaries coqide-byte coqide-opt $(COQIDEOPT) $(COQIDEBYTE) $(COQIDE) \ pcoq-binaries $(COQINTERFACE) $(CSDPCERT) coqbinaries pcoq $(TOOLS) tools \ - printers debug + printers debug initplugins VO_TARGETS:=logic arith bool narith zarith qarith lists strings sets \ fsets allfsets relations wellfounded ints reals allreals \ setoids sorting natural integer rational numbers noreal \ diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 6d6a0c065..02f36a8c8 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1886,7 +1886,8 @@ let rec xlate_vernac = | PrintHint id -> CT_print_hint (CT_coerce_ID_to_ID_OPT (loc_qualid_to_ct_ID id)) | PrintHintGoal -> CT_print_hint ctv_ID_OPT_NONE - | PrintLoadPath -> CT_print_loadpath + | PrintLoadPath None -> CT_print_loadpath + | PrintLoadPath _ -> xlate_error "TODO: Print LoadPath dir" | PrintMLLoadPath -> CT_ml_print_path | PrintMLModules -> CT_ml_print_modules | PrintGraph -> CT_print_graph diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 6db166762..3f1e517d6 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -629,6 +629,11 @@ This command removes the path {\str} from the current \Coq\ loadpath. \subsection[\tt Print LoadPath.]{\tt Print LoadPath.\comindex{Print LoadPath}} This command displays the current \Coq\ loadpath. +\begin{Variants} +\item {\tt Print LoadPath {\dirpath}.}\\ +Works as {\tt Print LoadPath} but displays only the paths that extend the {\dirpath} prefix. +\end{Variants} + \subsection[\tt Add ML Path {\str}.]{\tt Add ML Path {\str}.\comindex{Add ML Path}} This command adds the path {\str} to the current Objective Caml loadpath (see the command {\tt Declare ML Module} in the Section~\ref{compiled}). diff --git a/kernel/names.ml b/kernel/names.ml index e75900cfa..6ee96fddd 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -17,7 +17,7 @@ type identifier = string let id_ord = Pervasives.compare -let id_of_string s = check_ident s; String.copy s +let id_of_string s = check_ident_soft s; String.copy s let string_of_id id = String.copy id diff --git a/lib/system.ml b/lib/system.ml index 7ca62dcc8..00d6dec22 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -63,6 +63,34 @@ type load_path = physical_path list let physical_path_of_string s = s let string_of_physical_path p = p +(* Hints to partially detects if two paths refer to the same repertory *) +let rec remove_path_dot p = + let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *) + let n = String.length curdir in + if String.length p > n && String.sub p 0 n = curdir then + remove_path_dot (String.sub p n (String.length p - n)) + else + p + +let strip_path p = + let cwd = Filename.concat (Sys.getcwd ()) "" in (* Unix: "`pwd`/" *) + let n = String.length cwd in + if String.length p > n && String.sub p 0 n = cwd then + remove_path_dot (String.sub p n (String.length p - n)) + else + remove_path_dot p + +let canonical_path_name p = + let current = Sys.getcwd () in + try + Sys.chdir p; + let p' = Sys.getcwd () in + Sys.chdir current; + p' + with Sys_error _ -> + (* We give up to find a canonical name and just simplify it... *) + strip_path p + (* All subdirectories, recursively *) let exists_dir dir = diff --git a/lib/system.mli b/lib/system.mli index 6c607607f..48e02cb5d 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -16,6 +16,8 @@ type physical_path = string type load_path = physical_path list +val canonical_path_name : string -> string + val exclude_search_in_dirname : string -> unit val all_subdirs : unix_path:string -> (physical_path * string list) list diff --git a/lib/util.ml b/lib/util.ml index b0e66af05..3b04e2574 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -309,27 +309,40 @@ let next_utf8 s i = (* Check the well-formedness of an identifier *) -let check_ident s = +let check_initial handle j n s = + match classify_unicode n with + | UnicodeLetter -> () + | _ -> + let c = String.sub s 0 j in + handle ("Invalid character '"^c^"' at beginning of identifier \""^s^"\".") + +let check_trailing handle i j n s = + match classify_unicode n with + | UnicodeLetter | UnicodeIdentPart -> () + | _ -> + let c = String.sub s i j in + handle ("Invalid character '"^c^"' in identifier \""^s^"\".") + +let check_ident_gen handle s = let i = ref 0 in if s <> ".." then try let j, n = next_utf8 s 0 in - match classify_unicode n with - | UnicodeLetter -> - i := !i + j; - begin try - while true do - let j, n = next_utf8 s !i in - match classify_unicode n with - | UnicodeLetter | UnicodeIdentPart -> i := !i + j - | _ -> error - ("invalid character "^(String.sub s !i j)^" in identifier "^s) - done - with End_of_input -> () end - | _ -> error (s^": an identifier should start with a letter") + check_initial handle j n s; + i := !i + j; + try + while true do + let j, n = next_utf8 s !i in + check_trailing handle !i j n s; + i := !i + j + done + with End_of_input -> () with - | End_of_input -> error "The empty string is not an identifier" - | UnsupportedUtf8 -> error (s^": unsupported character in utf8 sequence") - | Invalid_argument _ -> error (s^": invalid utf8 sequence") + | End_of_input -> error "The empty string is not an identifier." + | UnsupportedUtf8 -> error (s^": unsupported character in utf8 sequence.") + | Invalid_argument _ -> error (s^": invalid utf8 sequence.") + +let check_ident_soft = check_ident_gen warning +let check_ident = check_ident_gen error let lowercase_unicode s unicode = match unicode land 0x1F000 with diff --git a/lib/util.mli b/lib/util.mli index 8b27e6158..dc6498b15 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -89,6 +89,7 @@ exception UnsupportedUtf8 val classify_unicode : int -> utf8_status val check_ident : string -> unit +val check_ident_soft : string -> unit val lowercase_first_char_utf8 : string -> string (*s Lists. *) diff --git a/library/libnames.ml b/library/libnames.ml index bf02efb03..b7b36afb3 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -123,21 +123,21 @@ let path_of_inductive env (sp,tyi) = let parse_dir s = let len = String.length s in let rec decoupe_dirs dirs n = - if n>=len then dirs else + if n = len && n > 0 then error (s ^ " is an invalid path."); + if n >= len then dirs else let pos = try String.index_from s n '.' with Not_found -> len in + if pos = n then error (s ^ " is an invalid path."); let dir = String.sub s n (pos-n) in - decoupe_dirs ((id_of_string dir)::dirs) (pos+1) + decoupe_dirs ((id_of_string dir)::dirs) (pos+1) in decoupe_dirs [] 0 -let dirpath_of_string s = - match parse_dir s with - [] -> invalid_arg "dirpath_of_string" - | dir -> make_dirpath dir +let dirpath_of_string s = + make_dirpath (if s = "" then [] else parse_dir s) module Dirset = Set.Make(struct type t = dir_path let compare = compare end) module Dirmap = Map.Make(struct type t = dir_path let compare = compare end) diff --git a/library/library.ml b/library/library.ml index fd9d93eb4..ff0e62064 100644 --- a/library/library.ml +++ b/library/library.ml @@ -28,43 +28,15 @@ let load_paths = ref ([] : (System.physical_path * logical_path * bool) list) let get_load_paths () = List.map pi1 !load_paths -(* Hints to partially detects if two paths refer to the same repertory *) -let rec remove_path_dot p = - let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *) - let n = String.length curdir in - if String.length p > n && String.sub p 0 n = curdir then - remove_path_dot (String.sub p n (String.length p - n)) - else - p - -let strip_path p = - let cwd = Filename.concat (Sys.getcwd ()) "" in (* Unix: "`pwd`/" *) - let n = String.length cwd in - if String.length p > n && String.sub p 0 n = cwd then - remove_path_dot (String.sub p n (String.length p - n)) - else - remove_path_dot p - -let canonical_path_name p = - let current = Sys.getcwd () in - try - Sys.chdir p; - let p' = Sys.getcwd () in - Sys.chdir current; - p' - with Sys_error _ -> - (* We give up to find a canonical name and just simplify it... *) - strip_path p - let find_logical_path phys_dir = - let phys_dir = canonical_path_name phys_dir in + let phys_dir = System.canonical_path_name phys_dir in match List.filter (fun (p,d,_) -> p = phys_dir) !load_paths with | [_,dir,_] -> dir | [] -> Nameops.default_root_prefix | l -> anomaly ("Two logical paths are associated to "^phys_dir) let is_in_load_paths phys_dir = - let dir = canonical_path_name phys_dir in + let dir = System.canonical_path_name phys_dir in let lp = get_load_paths () in let check_p = fun p -> (String.compare dir p) == 0 in List.exists check_p lp @@ -73,13 +45,13 @@ let remove_load_path dir = load_paths := List.filter (fun (p,d,_) -> p <> dir) !load_paths let add_load_path isroot (phys_path,coq_path) = - let phys_path = canonical_path_name phys_path in + let phys_path = System.canonical_path_name phys_path in match List.filter (fun (p,d,_) -> p = phys_path) !load_paths with | [_,dir,_] -> if coq_path <> dir (* If this is not the default -I . to coqtop *) && not - (phys_path = canonical_path_name Filename.current_dir_name + (phys_path = System.canonical_path_name Filename.current_dir_name && coq_path = Nameops.default_root_prefix) then begin @@ -627,9 +599,15 @@ let import_module export (loc,qid) = (************************************************************************) (*s Initializing the compilation of a library. *) +let check_coq_overwriting p = + let l = repr_dirpath p in + if not !Flags.boot && l <> [] && string_of_id (list_last l) = "Coq" then + errorlabstrm "" (strbrk ("Name "^string_of_dirpath p^" starts with prefix \"Coq\" which is reserved for the Coq library.")) + let start_library f = let _,longf = System.find_file_in_path (get_load_paths ()) (f^".v") in let ldir0 = find_logical_path (Filename.dirname longf) in + check_coq_overwriting ldir0; let id = id_of_string (Filename.basename f) in let ldir = extend_dirpath ldir0 id in Declaremods.start_library ldir; diff --git a/library/library.mli b/library/library.mli index c6bd8fe0b..2b7ecc664 100644 --- a/library/library.mli +++ b/library/library.mli @@ -79,5 +79,8 @@ val locate_qualified_library : bool -> qualid -> library_location * dir_path * System.physical_path val try_locate_qualified_library : qualid located -> dir_path * string +(* Reserve Coq prefix for the standard library *) +val check_coq_overwriting : dir_path -> unit + (*s Statistics: display the memory use of a library. *) val mem : dir_path -> Pp.std_ppcmds diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 4ffd53fe4..48a7a7a5a 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -675,7 +675,7 @@ GEXTEND Gram | IDENT "Grammar"; ent = IDENT -> (* This should be in "syntax" section but is here for factorization*) PrintGrammar ent - | IDENT "LoadPath" -> PrintLoadPath + | IDENT "LoadPath"; dir = OPT dirpath -> PrintLoadPath dir | IDENT "Modules" -> error "Print Modules is obsolete; use Print Libraries instead" | IDENT "Libraries" -> PrintModules diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 33c7654d2..a3eed62b7 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -878,7 +878,7 @@ let rec pr_vernac = function str"Print Section" ++ spc() ++ Libnames.pr_reference s | PrintGrammar ent -> str"Print Grammar" ++ spc() ++ str ent - | PrintLoadPath -> str"Print LoadPath" + | PrintLoadPath dir -> str"Print LoadPath" ++ pr_opt pr_dirpath dir | PrintModules -> str"Print Modules" | PrintMLLoadPath -> str"Print ML Path" | PrintMLModules -> str"Print ML Modules" diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4 index 77fdffb0d..dcb220ea2 100644 --- a/tools/coq_makefile.ml4 +++ b/tools/coq_makefile.ml4 @@ -29,6 +29,7 @@ let some_mlfile = ref false let opt = ref "-opt" let impredicative_set = ref false +let no_install = ref false let print x = output_string !output_channel x let printf x = Printf.fprintf !output_channel x @@ -38,6 +39,9 @@ let rec print_list sep = function | x :: l -> print x; print sep; print_list sep l | [] -> () +let list_iter_i f = + let rec aux i = function [] -> () | a::l -> f i a; aux (i+1) l in aux 1 + let best_ocamlc = if Coq_config.best = "opt" then "ocamlc.opt" else "ocamlc" let best_ocamlopt = @@ -63,10 +67,11 @@ let usage () = coq_makefile [subdirectory] .... [file.v] ... [file.ml] ... [-custom command dependencies file] ... [-I dir] ... [-R physicalpath logicalpath] - ... [VARIABLE = value] ... [-opt|-byte] [-f file] [-o file] [-h] [--help] + ... [VARIABLE = value] ... [-opt|-byte] [-impredicative-set] [-no-install] + [-f file] [-o file] [-h] [--help] [file.v]: Coq file to be compiled -[file.ml]: ML file to be compiled +[file.ml]: Objective Caml file to be compiled [subdirectory] : subdirectory that should be \"made\" [-custom command dependencies file]: add target \"file\" with command \"command\" and dependencies \"dependencies\" @@ -78,6 +83,7 @@ coq_makefile [subdirectory] .... [file.v] ... [file.ml] ... [-custom [-byte]: compile with byte-code version of coq [-opt]: compile with native-code version of coq [-impredicative-set]: compile with option -impredicative-set of coq +[-no-install]: build a makefile with no install target [-f file]: take the contents of file as arguments [-o file]: output should go in file file [-h]: print this usage summary @@ -88,24 +94,106 @@ let is_genrule r = let genrule = Str.regexp("%") in Str.string_match genrule r 0 -let standard sds sps = +let absolute_dir dir = + let current = Sys.getcwd () in + Sys.chdir dir; + let dir' = Sys.getcwd () in + Sys.chdir current; + dir' + +let is_prefix dir1 dir2 = + let l1 = String.length dir1 in + let l2 = String.length dir2 in + dir1 = dir2 or (l1 < l2 & String.sub dir2 0 l1 = dir1 & dir2.[l1] = '/') + +let canonize f = + let l = String.length f in + if l > 2 && f.[0] = '.' && f.[1] = '/' then + let n = let i = ref 2 in while !i < l && f.[!i] = '/' do incr i done; !i in + String.sub f n (l-n) + else f + +let is_absolute_prefix dir dir' = + is_prefix (absolute_dir dir) (absolute_dir dir') + +let is_included dir = function + | RInclude (dir',_) -> is_absolute_prefix dir' dir + | Include dir' -> absolute_dir dir = absolute_dir dir' + | _ -> false + +let has_top_file = function + | ML s | V s -> s = Filename.basename s + | _ -> false + +let physical_dir_of_logical_dir ldir = + let pdir = String.copy ldir in + for i = 0 to String.length ldir - 1 do + if pdir.[i] = '.' then pdir.[i] <- '/'; + done; + pdir + +let standard ()= print "byte:\n"; print "\t$(MAKE) all \"OPT:=-byte\"\n\n"; print "opt:\n"; if !opt = "" then print "\t@echo \"WARNING: opt is disabled\"\n"; - print "\t$(MAKE) all \"OPT:="; print !opt; print "\"\n\n"; + print "\t$(MAKE) all \"OPT:="; print !opt; print "\"\n\n" + +let is_prefix_of_file dir f = + is_prefix dir (absolute_dir (Filename.dirname f)) + +let classify_files_by_root var files (inc_i,inc_r) = + if not (List.exists (fun (pdir,_,_) -> pdir = ".") inc_r) then + begin + (* Files in the scope of a -R option (assuming they are disjoint) *) + list_iter_i (fun i (pdir,ldir,abspdir) -> + if List.exists (is_prefix_of_file abspdir) files then + printf "%s%d:=$(patsubst %s/%%,%%,$(filter %s/%%,$(%s)))\n" + var i pdir pdir var) + inc_r; + (* Files not in the scope of a -R option *) + let pat_of_dir (pdir,_,_) = pdir^"/%" in + let pdir_patterns = String.concat " " (List.map pat_of_dir inc_r) in + printf "%s0:=$(filter-out %s,$(%s))\n" var pdir_patterns var + end + +let install_include_by_root var files (_,inc_r) = + try + (* All files caught by a -R . option (assuming it is the only one) *) + let ldir = List.assoc "." (List.map (fun (p,l,_) -> (p,l)) inc_r) in + let pdir = physical_dir_of_logical_dir ldir in + printf "\t(for i in $(%s); do \\\n" var; + printf "\t install -D $$i $(COQLIB)/user-contrib/%s/$$i; \\\n" pdir; + printf "\t done)\n" + with Not_found -> + (* Files in the scope of a -R option (assuming they are disjoint) *) + list_iter_i (fun i (pdir,ldir,abspdir) -> + if List.exists (is_prefix_of_file abspdir) files then + begin + let pdir' = physical_dir_of_logical_dir ldir in + printf "\t(cd %s; for i in $(%s%d); do \\\n" pdir var i; + printf "\t install -D $$i $(COQLIB)/user-contrib/%s/$$i; \\\n" pdir'; + printf "\t done)\n" + end) inc_r; + (* Files not in the scope of a -R option *) + printf "\t(for i in $(%s0); do \\\n" var; + printf "\t install -D $$i $(COQLIB)/user-contrib/$(INSTALLDEFAULTROOT)/$$i; \\\n"; + printf "\t done)\n" + +let install (vfiles,mlfiles,_,sds) inc = print "install:\n"; print "\tmkdir -p $(COQLIB)/user-contrib\n"; - if !some_vfile then - print "\tcp -f $(VOFILES) $(COQLIB)/user-contrib\n"; - if !some_mlfile then - print "\tcp -f $(CMOFILES) $(COQLIB)/user-contrib\n"; + if !some_vfile then install_include_by_root "VOFILES" vfiles inc; + if !some_mlfile then install_include_by_root "CMOFILES" mlfiles inc; if Coq_config.has_natdynlink && !some_mlfile then - print "\tcp -f $(CMXSFILES) $(COQLIB)/user-contrib\n"; + install_include_by_root "CMXSFILES" mlfiles inc; List.iter - (fun x -> print "\t(cd "; print x; print " ; $(MAKE) install)\n") + (fun x -> + printf "\t(cd %s; $(MAKE) INSTALLDEFAULTROOT=$(INSTALLDEFAULTROOT)/%s install)\n" x x) sds; - print "\n"; + print "\n" + +let make_makefile sds = if !make_name <> "" then begin printf "%s: %s\n" !makefile_name !make_name; printf "\tmv -f %s %s.bak\n" !makefile_name !makefile_name; @@ -115,7 +203,9 @@ let standard sds sps = (fun x -> print "\t(cd "; print x; print " ; $(MAKE) Makefile)\n") sds; print "\n"; - end; + end + +let clean sds sps = print "clean:\n"; print "\trm -f $(CMOFILES) $(CMIFILES) $(CMXFILES) $(CMXSFILES) $(OFILES) $(VOFILES) $(VIFILES) $(GFILES) $(MLFILES:.ml=.cmo) $(MLFILES:.ml=.cmx) *~\n"; print "\trm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(HTMLFILES) \ @@ -171,12 +261,8 @@ let implicit () = if !some_mlfile then ml_rules (); if !some_vfile then v_rule () -let variables l = - let rec var_aux = function - | [] -> () - | Def(v,def) :: r -> print v; print "="; print def; print "\n"; var_aux r - | _ :: r -> var_aux r - in +let variables defs = + let var_aux (v,def) = print v; print "="; print def; print "\n" in section "Variables definitions."; print "ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)\n"; if !opt = "-byte" then @@ -200,33 +286,10 @@ let variables l = print "GRAMMARS:=grammar.cma\n"; print "CAMLP4EXTEND:=pa_extend.cmo pa_macro.cmo q_MLast.cmo\n"; print "CAMLP4OPTIONS:=\n"; - var_aux l; + List.iter var_aux defs; print "PP:=-pp \"$(CAMLP4BIN)$(CAMLP4)o -I . $(COQSRCLIBS) $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl\"\n"; print "\n" -let absolute_dir dir = - let current = Sys.getcwd () in - Sys.chdir dir; - let dir' = Sys.getcwd () in - Sys.chdir current; - dir' - -let is_prefix dir1 dir2 = - let l1 = String.length dir1 in - let l2 = String.length dir2 in - dir1 = dir2 or (l1 < l2 & String.sub dir2 0 l1 = dir1 & dir2.[l1] = '/') - -let is_included dir = function - | RInclude (dir',_) -> is_prefix (absolute_dir dir') (absolute_dir dir) - | Include dir' -> absolute_dir dir = absolute_dir dir' - | _ -> false - -let dir_of_target t = - match t with - | RInclude (dir,_) -> dir - | Include dir -> dir - | _ -> assert false - let parameters () = print "# \n"; print "# This Makefile may take 3 arguments passed as environment variables:\n"; @@ -237,33 +300,16 @@ let parameters () = print "ifndef CAMLP4BIN\n CAMLP4BIN:=$(CAMLBIN)\nendif\n\n"; print "CAMLP4LIB:=$(shell $(CAMLP4BIN)$(CAMLP4) -where)\n\n" -let include_dirs l = - let rec split_includes l = - match l with - | [] -> [], [] - | Include _ as i :: rem -> - let ri, rr = split_includes rem in - (i :: ri), rr - | RInclude _ as r :: rem -> - let ri, rr = split_includes rem in - ri, (r :: rr) - | _ :: rem -> split_includes rem - in - let rec parse_includes l = - match l with - | [] -> [] - | Include x :: rem -> ("-I " ^ x) :: parse_includes rem - | RInclude (p,l) :: rem -> - let l' = if l = "" then "\"\"" else l in - ("-R " ^ p ^ " " ^ l') :: parse_includes rem - | _ :: rem -> parse_includes rem - in - let l' = if List.exists (is_included ".") l then l else Include "." :: l in - let inc_i, inc_r = split_includes l' in - let inc_i' = List.filter (fun i -> not (List.exists (fun i' -> is_included (dir_of_target i) i') inc_r)) inc_i in +let include_dirs (inc_i,inc_r) = + let parse_includes l = List.map (fun (x,_) -> "-I " ^ x) l in + let parse_rec_includes l = + List.map (fun (p,l,_) -> + let l' = if l = "" then "\"\"" else l in "-R " ^ p ^ " " ^ l') + l in + let inc_i' = List.filter (fun (i,_) -> not (List.exists (fun (i',_,_) -> is_absolute_prefix i' i) inc_r)) inc_i in let str_i = parse_includes inc_i in let str_i' = parse_includes inc_i' in - let str_r = parse_includes inc_r in + let str_r = parse_rec_includes inc_r in section "Libraries definitions."; print "OCAMLLIBS:=-I $(CAMLP4LIB) "; print_list "\\\n " str_i; print "\n"; print "COQSRCLIBS:=-I $(COQLIB)/kernel -I $(COQLIB)/lib \\ @@ -295,15 +341,10 @@ let custom sps = if sps <> [] then section "Custom targets."; List.iter pr_sp sps -let subdirs l = - let rec subdirs_aux = function - | [] -> [] - | Subdir x :: r -> x :: (subdirs_aux r) - | _ :: r -> subdirs_aux r - and pr_subdir s = +let subdirs sds = + let pr_subdir s = print s; print ":\n\tcd "; print s; print " ; $(MAKE) all\n\n" in - let sds = subdirs_aux l in if sds <> [] then section "Subdirectories."; List.iter pr_subdir sds; section "Special targets."; @@ -311,34 +352,31 @@ let subdirs l = print_list " " ("all" :: "opt" :: "byte" :: "archclean" :: "clean" :: "install" :: "depend" :: "html" :: sds); - print "\n\n"; - sds - -let all_target l = - let rec parse_arguments l = - match l with - | ML n :: r -> let v,m,o = parse_arguments r in (v,n::m,o) - | Subdir n :: r -> let v,m,o = parse_arguments r in (v,m,n::o) - | V n :: r -> let v,m,o = parse_arguments r in (n::v,m,o) - | Special (n,_,_) :: r -> - let v,m,o = parse_arguments r in - if is_genrule n then - (v,m,o) - else - (v,m,n::o) - | Include _ :: r -> parse_arguments r - | RInclude _ :: r -> parse_arguments r - | Def _ :: r -> parse_arguments r - | [] -> [],[],[] - in - let - vfiles, mlfiles, other_targets = parse_arguments l - in - section "Definition of the \"all\" target."; + print "\n\n" + +let rec split_arguments = function + | V n :: r -> + let (v,m,o,s),i,d = split_arguments r in ((canonize n::v,m,o,s),i,d) + | ML n :: r -> + let (v,m,o,s),i,d = split_arguments r in ((v,canonize n::m,o,s),i,d) + | Special (n,dep,c) :: r -> + let (v,m,o,s),i,d = split_arguments r in ((v,m,(n,dep,c)::o,s),i,d) + | Subdir n :: r -> + let (v,m,o,s),i,d = split_arguments r in ((v,m,o,n::s),i,d) + | Include p :: r -> + let t,(i,r),d = split_arguments r in (t,((p,absolute_dir p)::i,r),d) + | RInclude (p,l) :: r -> + let t,(i,r),d = split_arguments r in (t,(i,(p,l,absolute_dir p)::r),d) + | Def (v,def) :: r -> + let t,i,d = split_arguments r in (t,i,(v,def)::d) + | [] -> ([],[],[],[]),([],[]),[] + +let main_targets vfiles mlfiles other_targets inc = if !some_vfile then begin print "VFILES:="; print_list "\\\n " vfiles; print "\n"; print "VOFILES:=$(VFILES:.v=.vo)\n"; + classify_files_by_root "VOFILES" vfiles inc; print "GLOBFILES:=$(VFILES:.v=.glob)\n"; print "VIFILES:=$(VFILES:.v=.vi)\n"; print "GFILES:=$(VFILES:.v=.g)\n"; @@ -349,9 +387,11 @@ let all_target l = begin print "MLFILES:="; print_list "\\\n " mlfiles; print "\n"; print "CMOFILES:=$(MLFILES:.ml=.cmo)\n"; + classify_files_by_root "CMOFILES" mlfiles inc; print "CMIFILES:=$(MLFILES:.ml=.cmi)\n"; print "CMXFILES:=$(MLFILES:.ml=.cmx)\n"; print "CMXSFILES:=$(MLFILES:.ml=.cmxs)\n"; + classify_files_by_root "CMXSFILES" mlfiles inc; print "OFILES:=$(MLFILES:.ml=.o)\n"; end; print "\nall: "; @@ -379,6 +419,14 @@ let all_target l = print "\t$(COQDOC) -toc -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n"; print "\n\n" end + +let all_target (vfiles, mlfiles, sps, sds) inc = + let special_targets = List.filter (fun (n,_,_) -> not (is_genrule n)) sps in + let other_targets = List.map (fun x,_,_ -> x) special_targets @ sds in + section "Definition of the \"all\" target."; + main_targets vfiles mlfiles other_targets inc; + custom sps; + subdirs sds let parse f = let rec string = parser @@ -415,6 +463,8 @@ let rec process_cmd_line = function opt := "-opt"; process_cmd_line r | "-impredicative-set" :: r -> impredicative_set := true; process_cmd_line r + | "-no-install" :: r -> + no_install := true; process_cmd_line r | "-custom" :: com :: dependencies :: file :: r -> let check_dep f = if Filename.check_suffix f ".v" then @@ -498,26 +548,61 @@ let directories_deps l = in iter ([],[]) l +let ensure_root_dir l = + if List.exists (is_included ".") l or not (List.exists has_top_file l) then + l + else + Include "." :: l + +let warn_install_at_root_directory (vfiles,mlfiles,_,_) (inc_i,inc_r) = + let inc_r_top = List.filter (fun (_,ldir,_) -> ldir = "") inc_r in + let inc_top = List.map (fun (p,_,a) -> (p,a)) inc_r_top @ inc_i in + let files = vfiles @ mlfiles in + if not !no_install && + List.exists (fun f -> List.mem_assoc (Filename.dirname f) inc_top) files + then + Printf.eprintf "Warning: install target will copy files at the first level of the coq contributions installation directory; option -R %sis recommended\n" + (if inc_r_top = [] then "" else "with non trivial logical root ") + +let check_overlapping_include (inc_i,inc_r) = + let pwd = Sys.getcwd () in + let rec aux = function + | [] -> () + | (pdir,_,abspdir)::l -> + if not (is_prefix pwd abspdir) then + Printf.eprintf "Warning: in option -R, %s is not a subdirectoty of the current directory\n" pdir; + List.iter (fun (pdir',_,abspdir') -> + if is_prefix abspdir abspdir' or is_prefix abspdir' abspdir then + Printf.eprintf "Warning: in options -R, %s and %s overlap\n" pdir pdir') l; + List.iter (fun (pdir',abspdir') -> + if is_prefix abspdir abspdir' or is_prefix abspdir' abspdir then + Printf.eprintf "Warning: in option -I, %s overlap with %s in option -R\n" pdir' pdir) inc_i + in aux inc_r + let do_makefile args = let l = process_cmd_line args in - banner (); - header_includes (); - warning (); - command_line args; - parameters (); - include_dirs l; - variables l; - all_target l; - let sps = special l in - custom sps; - let sds = subdirs l in - implicit (); - standard sds sps; - (* TEST directories_deps l; *) - footer_includes (); - warning (); - if not (!output_channel == stdout) then close_out !output_channel; - exit 0 + let l = ensure_root_dir l in + let (_,_,sps,sds as targets), inc, defs = split_arguments l in + warn_install_at_root_directory targets inc; + check_overlapping_include inc; + banner (); + header_includes (); + warning (); + command_line args; + parameters (); + include_dirs inc; + variables defs; + all_target targets inc; + implicit (); + standard (); + if not !no_install then install targets inc; + clean sds sps; + make_makefile sds; + (* TEST directories_deps l; *) + footer_includes (); + warning (); + if not (!output_channel == stdout) then close_out !output_channel; + exit 0 let main () = let args = @@ -527,4 +612,3 @@ let main () = do_makefile args let _ = Printexc.catch main () - diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index fec6b0740..9ada5bff2 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -51,7 +51,9 @@ let set_batch_mode () = batch_mode := true let toplevel_default_name = make_dirpath [id_of_string "Top"] let toplevel_name = ref (Some toplevel_default_name) -let set_toplevel_name dir = toplevel_name := Some dir +let set_toplevel_name dir = + if dir = empty_dirpath then error "Need a non empty toplevel module name"; + toplevel_name := Some dir let unset_toplevel_name () = toplevel_name := None let remove_top_ml () = Mltop.remove () @@ -68,16 +70,16 @@ let outputstate = ref "" let set_outputstate s = outputstate:=s let outputstate () = if !outputstate <> "" then extern_state !outputstate -let check_coq_overwriting p = - if string_of_id (list_last (repr_dirpath p)) = "Coq" then - error "The \"Coq\" logical root directory is reserved for the Coq library" - let set_default_include d = push_include (d,Nameops.default_root_prefix) let set_default_rec_include d = push_rec_include(d,Nameops.default_root_prefix) let set_include d p = - let p = dirpath_of_string p in check_coq_overwriting p; push_include (d,p) + let p = dirpath_of_string p in + Library.check_coq_overwriting p; + push_include (d,p) let set_rec_include d p = - let p = dirpath_of_string p in check_coq_overwriting p; push_rec_include(d,p) + let p = dirpath_of_string p in + Library.check_coq_overwriting p; + push_rec_include(d,p) let load_vernacular_list = ref ([] : (string * bool) list) let add_load_vernacular verb s = diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index dcdc46e8e..685eaba3f 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -47,8 +47,10 @@ open Vernacinterp (* This path is where we look for .cmo *) let coq_mlpath_copy = ref ["."] -let keep_copy_mlpath path = - coq_mlpath_copy := path :: !coq_mlpath_copy +let keep_copy_mlpath path = + let cpath = canonical_path_name path in + let filter path' = (cpath <> canonical_path_name path') in + coq_mlpath_copy := path :: List.filter filter !coq_mlpath_copy (* If there is a toplevel under Coq *) type toplevel = { @@ -106,7 +108,7 @@ let dir_ml_load s = * if this code section starts to use a module not used elsewhere * in this file, the Makefile dependency logic needs to be updated. *) - let _,gname = where_in_path true (list_uniquize !coq_mlpath_copy) s in + let _,gname = where_in_path true !coq_mlpath_copy s in try Dynlink.loadfile gname; with | Dynlink.Error a -> @@ -310,10 +312,10 @@ let cache_ml_module_object (_,{mnames=mnames}) = if_verbose msg (str"[Loading ML file " ++ str fname ++ str" ..."); load_object mname fname; - if_verbose msgnl (str"done]"); + if_verbose msgnl (str" done]"); add_loaded_module mname with e -> - if_verbose msgnl (str"failed]"); + if_verbose msgnl (str" failed]"); raise e else if_verbose diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index f5603535b..42a06308c 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -182,8 +182,11 @@ let show_match id = let print_path_entry (s,l) = (str (string_of_dirpath l) ++ str " " ++ tbrk (0,0) ++ str s) -let print_loadpath () = +let print_loadpath dir = let l = Library.get_full_load_paths () in + let l = match dir with + | None -> l + | Some dir -> List.filter (fun (s,l) -> is_dirpath_prefix_of dir l) l in msgnl (Pp.t (str "Logical Path: " ++ tab () ++ str "Physical path:" ++ fnl () ++ prlist_with_sep pr_fnl print_path_entry l)) @@ -1063,7 +1066,7 @@ let vernac_print = function | PrintSectionContext qid -> msg (print_sec_context_typ qid) | PrintInspect n -> msg (inspect n) | PrintGrammar ent -> Metasyntax.print_grammar ent - | PrintLoadPath -> (* For compatibility ? *) print_loadpath () + | PrintLoadPath dir -> (* For compatibility ? *) print_loadpath dir | PrintModules -> msg (print_modules ()) | PrintModule qid -> print_module qid | PrintModuleType qid -> print_modtype qid diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 8e797a883..d8084c966 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -38,7 +38,7 @@ type printable = | PrintSectionContext of reference | PrintInspect of int | PrintGrammar of string - | PrintLoadPath + | PrintLoadPath of dir_path option | PrintModules | PrintModule of reference | PrintModuleType of reference -- cgit v1.2.3