diff options
| -rw-r--r-- | CHANGES | 4 | ||||
| -rw-r--r-- | checker/check.ml | 4 | ||||
| -rw-r--r-- | checker/checker.ml | 35 | ||||
| -rw-r--r-- | doc/refman/RefMan-com.tex | 43 | ||||
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 157 | ||||
| -rw-r--r-- | doc/refman/RefMan-mod.tex | 2 | ||||
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 53 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 8 | ||||
| -rw-r--r-- | library/libnames.ml | 2 | ||||
| -rw-r--r-- | library/libnames.mli | 1 | ||||
| -rw-r--r-- | library/library.ml | 104 | ||||
| -rw-r--r-- | library/library.mli | 8 | ||||
| -rw-r--r-- | library/states.ml | 4 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 19 | ||||
| -rw-r--r-- | toplevel/mltop.ml4 | 23 | ||||
| -rw-r--r-- | toplevel/usage.ml | 8 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 25 |
17 files changed, 300 insertions, 200 deletions
@@ -58,6 +58,8 @@ Vernacular commands that should be expanded first. - New command "Print Assumptions" to display all variables, parameters or axioms a theorem or definition relies on. +- "Add Rec LoadPath" now provides references to libraries using partially + qualified names (this holds also for coqtop/coqc option -R). Libraries (DOC TO CHECK) @@ -411,6 +413,8 @@ CoqIDE Tools - New stand-alone .vo files verifier "coqchk". +- Extended -I coqtop/coqc option to specify a logical dir: "-I dir -as coqdir". +- New coqtop/coqc option -exclude-dir to exclude subdirs for option -R. Miscellaneous diff --git a/checker/check.ml b/checker/check.ml index f8844975a..bc36f2732 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -209,7 +209,7 @@ let locate_absolute_library dir = if loadpath = [] then raise LibUnmappedDir; try let name = string_of_id base^".vo" in - let _, file = System.where_in_path loadpath name in + let _, file = System.where_in_path false loadpath name in (dir, file) with Not_found -> (* Last chance, removed from the file system but still in memory *) @@ -229,7 +229,7 @@ let locate_qualified_library qid = in if loadpath = [] then raise LibUnmappedDir; let name = qid.basename^".vo" in - let path, file = System.where_in_path loadpath name in + let path, file = System.where_in_path true loadpath name in let dir = extend_dirpath (find_logical_path path) (id_of_string qid.basename) in (* Look if loaded *) diff --git a/checker/checker.ml b/checker/checker.ml index 1c7ace12f..7de258352 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -73,16 +73,14 @@ let convert_string d = failwith "caught" let add_rec_path ~unix_path:dir ~coq_root:coq_dirpath = - let dirs = all_subdirs dir in - let prefix = repr_dirpath coq_dirpath in - if dirs <> [] then + if exists_dir dir then + let dirs = all_subdirs dir in + let prefix = repr_dirpath coq_dirpath in let convert_dirs (lp,cp) = - (lp,Names.make_dirpath - ((List.map convert_string (List.rev cp))@prefix)) in + (lp,make_dirpath (List.map convert_string (List.rev cp)@prefix)) in let dirs = map_succeed convert_dirs dirs in - begin - List.iter Check.add_load_path dirs - end + List.iter Check.add_load_path dirs; + Check.add_load_path (dir,coq_dirpath) else msg_warning (str ("Cannot open " ^ dir)) @@ -101,6 +99,14 @@ let set_default_rec_include d = let p = Check.default_root_prefix in check_coq_overwriting p; push_rec_include (d, p) +let set_include d p = + let p = dirpath_of_string p in + 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) (* Initializes the LoadPath according to COQLIB and Coq_config *) let init_load_path () = @@ -174,9 +180,11 @@ let print_usage_channel co command = output_string co command; output_string co "Coq options are:\n"; output_string co -" -I dir add directory dir in the include path +" -I dir -as coqdir map physical dir to logical coqdir + -I dir map directory dir to the empty logical path -include dir (idem) - -R dir coqdir recursively map physical dir to logical coqdir + -R dir -as coqdir recursively map physical dir to logical coqdir + -R dir coqdir (idem) -admit module load module and dependencies without checking -norec module check module but admit dependencies without checking @@ -297,11 +305,14 @@ let parse_args() = | "-impredicative-set" :: rem -> set_engagement Declarations.ImpredicativeSet; parse rem + | ("-I"|"-include") :: d :: "-as" :: p :: rem -> set_include d p; parse rem + | ("-I"|"-include") :: d :: "-as" :: [] -> usage () | ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem | ("-I"|"-include") :: [] -> usage () - | "-R" :: d :: p :: rem -> - push_rec_include (d, dirpath_of_string p);parse rem + | "-R" :: d :: "-as" :: p :: rem -> set_rec_include d p;parse rem + | "-R" :: d :: "-as" :: [] -> usage () + | "-R" :: d :: p :: rem -> set_rec_include d p;parse rem | "-R" :: ([] | [_]) -> usage () | "-debug" :: rem -> set_debug (); parse rem diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index f74ace29f..1bd3d148e 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -84,7 +84,8 @@ only for developers that are writing their own tactics and are using you move the \Coq\ binaries and library after installation. \section[Options]{Options\index{Options of the command line} -\label{vmoption}} +\label{vmoption} +\label{coqoptions}} The following command-line options are recognized by the commands {\tt coqc} and {\tt coqtop}, unless stated otherwise: @@ -100,20 +101,48 @@ The following command-line options are recognized by the commands {\tt \item[{\tt -I} {\em directory}, {\tt -include} {\em directory}]\ - Add {\em directory} to the searched directories when looking for a - file. + Add physical path {\em directory} to the list of directories where to + look for a file and bind it to the empty logical directory. The + subdirectory structure of {\em directory} is recursively available + from {\Coq} using absolute names (see Section~\ref{LongNames}). -\item[{\tt -R} {\em directory} {\dirpath}]\ +\item[{\tt -I} {\em directory} {\tt -as} {\em dirpath}]\ - This maps the subdirectory structure of physical {\em directory} to - logical {\dirpath} and adds {\em directory} and its subdirectories - to the searched directories when looking for a file. + Add physical path {\em directory} to the list of directories where to + look for a file and bind it to the logical directory {\dirpath}. The + subdirectory structure of {\em directory} is recursively available + from {\Coq} using absolute names extending the {\dirpath} prefix. + + \SeeAlso {\tt Add LoadPath} in Section~\ref{AddLoadPath} and logical + paths in Section~\ref{Libraries}. + +\item[{\tt -R} {\em directory} {\dirpath}, {\tt -R} {\em directory} {\tt -as} {\dirpath}]\ + + Do as {\tt -I} {\em directory} {\tt -as} {\dirpath} but make the + subdirectory structure of {\em directory} recursively visible so + that the recursive contents of physical {\em directory} is available + from {\Coq} using short or partially qualified names. + + \SeeAlso {\tt Add Rec LoadPath} in Section~\ref{AddRecLoadPath} and logical + paths in Section~\ref{Libraries}. \item[{\tt -top} {\dirpath}]\ This sets the toplevel module name to {\dirpath} instead of {\tt Top}. Not valid for {\tt coqc}. +\item[{\tt -notop} {\dirpath}]\ + + This sets the toplevel module name to the empty logical dirpath. Not + valid for {\tt coqc}. + +\item[{\tt -exclude-dir} {\em subdirectory}]\ + + This tells to exclude any subdirectory named {\em subdirectory} + while processing option {\tt -R}. Without this option only the + conventional version control management subdirectories named {\tt + CVS} and {\tt \_darcs} are excluded. + \item[{\tt -is} {\em file}, {\tt -inputstate} {\em file}]\ Cause \Coq~to use the state put in the file {\em file} as its input diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 5baf84bec..1294ee7c0 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -851,106 +851,87 @@ section is closed. \subsection{Names of libraries and files \label{Libraries} \index{Libraries} +\index{Physical paths} \index{Logical paths}} \paragraph{Libraries} -The theories developed in {\Coq} are stored in {\em libraries}. A -library is characterized by a name called {\it root} of the -library. The standard library of {\Coq} has root name {\tt Coq} and is -known by default when a {\Coq} session starts. - -Libraries have a tree structure. E.g., the {\tt Coq} library -contains the sub-libraries {\tt Init}, {\tt Logic}, {\tt Arith}, {\tt -Lists}, ... The ``dot notation'' is used to separate the different -component of a library name. For instance, the {\tt Arith} library of -{\Coq} standard library is written ``{\tt Coq.Arith}''. - -\medskip -\Rem no blank is allowed between the dot and the identifier on its -right, otherwise the dot is interpreted as the full stop (period) of -the command! -\medskip - -\paragraph{Physical paths vs logical paths} - -Libraries and sub-libraries are denoted by {\em logical directory -paths} (written {\dirpath} and of which the syntax is the same as -{\qualid}, see \ref{qualid}). Logical directory -paths can be mapped to physical directories of the -operating system using the command (see \ref{AddLoadPath}) -\begin{quote} -{\tt Add LoadPath {\it physical\_path} as {\dirpath}}. -\end{quote} -A library can inherit the tree structure of a physical directory by -using the {\tt -R} option to {\tt coqtop} or the -command (see \ref{AddRecLoadPath}) -\begin{quote} -{\tt Add Rec LoadPath {\it physical\_path} as {\dirpath}}. -\end{quote} - -\Rem When used interactively with {\tt coqtop} command, {\Coq} opens a -library called {\tt Top}. - -\paragraph{The file level} - -At some point, (sub-)libraries contain {\it modules} which coincide -with files at the physical level. As for sublibraries, the dot -notation is used to denote a specific module of a library. Typically, -{\tt Coq.Init.Logic} is the logical path associated to the file {\tt - Logic.v} of {\Coq} standard library. Notice that compilation (see -\ref{Addoc-coqc}) is done at the level of files. - -If the physical directory where a file {\tt File.v} lies is mapped to -the empty logical directory path (which is the default when using the -simple form of {\tt Add LoadPath} or {\tt -I} option to coqtop), then -the name of the module it defines is {\tt File}. +The theories developed in {\Coq} are stored in {\em library files} +which are hierarchically classified into {\em libraries} and {\em +sublibraries}. To express this hierarchy, library names are +represented by qualified identifiers {\qualid}, i.e. as list of +identifiers separated by dots (see Section~\ref{qualid}). For +instance, the library file {\tt Mult} of the standard {\Coq} library +{\tt Arith} has name {\tt Coq.Arith.Mult}. The identifier +that starts the name of a library is called a {\em library root}. +All library files of the standard library of {\Coq} have reserved root +{\tt Coq} but library file names based on other roots can be obtained +by using {\tt coqc} options {\tt -I} or {\tt -R} (see +Section~\ref{coqoptions}). Also, when an interactive {\Coq} session +starts, a library of root {\tt Top} is started, unless option {\tt +-top} or {\tt -notop} is set (see Section~\ref{coqoptions}). + +As library files are stored on the file system of the underlying +operating system, a translation from file-system names to {\Coq} names +is needed. In this translation, names in the file system are called +{\em physical} paths while {\Coq} names are contrastingly called {\em +logical} names. Logical names are mapped to physical paths using the +commands {\tt Add LoadPath} or {\tt Add Rec LoadPath} (see +Sections~\ref{AddLoadPath} and~\ref{AddRecLoadPath}). \subsection{Qualified names \label{LongNames} \index{Qualified identifiers} \index{Absolute names}} -Modules contain constructions (sub-modules, axioms, parameters, -definitions, lemmas, theorems, remarks or facts). The (full) name of a -construction starts with the logical name of the module in which it is defined -followed by the (short) name of the construction. -Typically, the full name {\tt Coq.Init.Logic.eq} denotes Leibniz' equality -defined in the module {\tt Logic} in the sublibrary {\tt Init} of the -standard library of \Coq. - -\paragraph{Absolute, partially qualified and short names} - -The full name of a library, module, section, definition, theorem, -... is its {\it absolute name}. The last identifier ({\tt eq} in the -previous example) is its {\it short name} (or sometimes {\it base -name}). Any suffix of the absolute name is a {\em partially qualified -name} (e.g. {\tt Logic.eq} is a partially qualified name for {\tt -Coq.Init.Logic.eq}). Partially qualified names (shortly {\em -qualified name}) are also built from identifiers separated by dots. -They are written {\qualid} in the documentation. +Library files are modules which possibly contain submodules which +eventually contain constructions (axioms, parameters, definitions, +lemmas, theorems, remarks or facts). The {\em absolute name}, or {\em +full name}, of a construction in some library file is a qualified +identifier starting with the logical name of the library file, +followed by the sequence of submodules names encapsulating the +construction and ended by the proper name of the construction. +Typically, the absolute name {\tt Coq.Init.Logic.eq} denotes Leibniz' +equality defined in the module {\tt Logic} in the sublibrary {\tt +Init} of the standard library of \Coq. + +The proper name that ends the name of a construction is the {\it short +name} (or sometimes {\it base name}) of the construction (for +instance, the short name of {\tt Coq.Init.Logic.eq} is {\tt eq}). Any +partial suffix of the absolute name is a {\em partially qualified name} +(e.g. {\tt Logic.eq} is a partially qualified name for {\tt +Coq.Init.Logic.eq}). Especially, the short name of a construction is +its shortest partially qualified name. {\Coq} does not accept two constructions (definition, theorem, ...) with the same absolute name but different constructions can have the same short name (or even same partially qualified names as soon as the full names are different). -\paragraph{Visibility} +Notice that the notion of absolute, partially qualified and +short names also applies to library file names. -{\Coq} maintains a {\it name table} mapping qualified names to absolute -names. This table is modified by the commands {\tt Require} (see -\ref{Require}), {\tt Import} and {\tt Export} (see \ref{Import}) and -also each time a new declaration is added to the context. +\paragraph{Visibility} -An absolute name is called {\it visible} from a given short or -partially qualified name when this name suffices to denote it. This -means that the short or partially qualified name is mapped to the absolute -name in {\Coq} name table. +{\Coq} maintains a table called {\it name table} which maps partially +qualified names of constructions to absolute names. This table is +updated by the commands {\tt Require} (see \ref{Require}), {\tt +Import} and {\tt Export} (see \ref{Import}) and also each time a new +declaration is added to the context. An absolute name is called {\it +visible} from a given short or partially qualified name when this +latter name is enough to denote it. This means that the short or +partially qualified name is mapped to the absolute name in {\Coq} name +table. + +A similar table exists for library file names. It is updated by the +vernacular commands {\tt Add LoadPath} and {\tt Add Rec LoadPath} (or +their equivalent as options of the {\Coq} executables, {\tt -I} and +{\tt -R}). It may happen that a visible name is hidden by the short name or a qualified name of another construction. In this case, the name that has been hidden must be referred to using one more level of -qualification. Still, to ensure that a construction always remains +qualification. To ensure that a construction always remains accessible, absolute names can never be hidden. Examples: @@ -965,14 +946,8 @@ Check Datatypes.nat. Locate nat. \end{coq_example} -\Rem There is also a name table for sublibraries, modules and sections. - -\Rem In versions prior to {\Coq} 7.4, lemmas declared with {\tt -Remark} and {\tt Fact} kept in their full name the names of the -sections in which they were defined. Since {\Coq} 7.4, they strictly -behaves as {\tt Theorem} and {\tt Lemma} do. - -\SeeAlso Command {\tt Locate} in Section~\ref{Locate}. +\SeeAlso Command {\tt Locate} in Section~\ref{Locate} and {\tt Locate +Library} in Section~\ref{Locate Library}. %% \paragraph{The special case of remarks and facts} %% @@ -985,16 +960,6 @@ behaves as {\tt Theorem} and {\tt Lemma} do. %% a fact {\tt F} is defined in subsection {\tt S2} of section {\tt S1} %% in module {\tt M}, then its absolute name is {\tt M.S1.F}. - -\paragraph{Requiring a file} - -A module compiled in a ``.vo'' file comes with a logical names (e.g. -physical file \verb!theories/Init/Datatypes.vo! in the {\Coq} installation directory is bound to the logical module {\tt Coq.Init.Datatypes}). -When requiring the file, the mapping between physical directories and logical library should be consistent with the mapping used to compile the file (for modules of the standard library, this is automatic -- check it by typing {\tt Print LoadPath}). - -The command {\tt Add Rec LoadPath} is also available from {\tt coqtop} -and {\tt coqc} by using option~\verb=-R=. - \section{Implicit arguments \index{Implicit arguments} \label{Implicit Arguments}} diff --git a/doc/refman/RefMan-mod.tex b/doc/refman/RefMan-mod.tex index 12cfacbc4..2891ba2e9 100644 --- a/doc/refman/RefMan-mod.tex +++ b/doc/refman/RefMan-mod.tex @@ -386,7 +386,7 @@ Prints the module type and (optionally) the body of the module {\ident}. Prints the module type corresponding to {\ident}. -\subsection{\texttt{Locate Module {\qualid}} +\subsection{\tt Locate Module {\qualid} \comindex{Locate Module}} Prints the full name of the module {\qualid}. diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 76faac593..ec07dc079 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -427,12 +427,14 @@ replayed nor rechecked. To locate the file in the file system, {\qualid} is decomposed under the form {\dirpath}{\tt .}{\textsl{ident}} and the file {\ident}{\tt -.vo} is searched in the directory of the physical file system that is +.vo} is searched in the physical directory of the file system that is mapped in {\Coq} loadpath to the logical path {\dirpath} (see -Section~\ref{Loadpath}). +Section~\ref{loadpath}). The mapping between physical directories and +logical names at the time of requiring the file must be consistent +with the mapping used to compile the file. \begin{Variants} -\item {\tt Require Import {\qualid}.}\\ \comindex{Require} +\item {\tt Require Import {\qualid}.} \comindex{Require} This loads and declares the module {\qualid} and its dependencies then imports the contents of {\qualid} as described in @@ -493,6 +495,15 @@ Section~\ref{Loadpath}). The file {\tt{\ident}.vo} was found but either it is not a \Coq\ compiled module, or it was compiled with an older and incompatible version of \Coq. + +\item \errindex{The file {\ident}.vo contains library {\dirpath} and not + library {\dirpath'}} + + The library file {\dirpath'} is indirectly required by the {\tt + Require} command but it is bound in the current loadpath to the file + {\ident}.vo which was bound to a different library name {\dirpath} + at the time it was compiled. + \end{ErrMsgs} \SeeAlso Chapter~\ref{Addoc-coqc} @@ -546,10 +557,13 @@ which can be any valid path. \subsection[\tt Add LoadPath {\str} as {\dirpath}.]{\tt Add LoadPath {\str} as {\dirpath}.\comindex{Add LoadPath}\label{AddLoadPath}} -This command adds the path {\str} to the current {\Coq} loadpath and -maps it to the logical directory {\dirpath}, which means that every -file {\tt M.v} physically lying in directory {\str} becomes accessible -through logical name ``{\dirpath}{\tt{.M}}''. +This command adds the physical directory {\str} to the current {\Coq} +loadpath and maps it to the logical directory {\dirpath}, which means +that every file \textrm{\textsl{dirname}}/\textrm{\textsl{basename.v}} +physically lying in subdirectory {\str}/\textrm{\textsl{dirname}} +becomes accessible in {\Coq} through absolute logical name +{\dirpath}{\tt .}\textrm{\textsl{dirname}}{\tt +.}\textrm{\textsl{basename}}. \Rem {\tt Add LoadPath} also adds {\str} to the current ML loadpath. @@ -559,8 +573,27 @@ Performs as {\tt Add LoadPath {\str} as {\dirpath}} but for the empty directory \end{Variants} \subsection[\tt Add Rec LoadPath {\str} as {\dirpath}.]{\tt Add Rec LoadPath {\str} as {\dirpath}.\comindex{Add Rec LoadPath}\label{AddRecLoadPath}} -This command adds the directory {\str} and all its subdirectories -to the current \Coq\ loadpath. The top directory {\str} is mapped to the logical directory {\dirpath} while any subdirectory {\textsl{pdir}} is mapped to logical directory {\dirpath}{\tt{.pdir}} and so on. +This command adds the physical directory {\str} and all its subdirectories to +the current \Coq\ loadpath. The top directory {\str} is mapped to the +logical directory {\dirpath} and any subdirectory {\textsl{pdir}} of it is +mapped to logical name {\dirpath}{\tt .}\textsl{pdir} and +recursively. Subdirectories corresponding to invalid {\Coq} +identifiers are skipped, and, by convention, subdirectories named {\tt +CVS} or {\tt \_darcs} are skipped too. + +Otherwise, said, {\tt Add Rec LoadPath {\str} as {\dirpath}} behaves +as {\tt Add LoadPath {\str} as {\dirpath}} excepts that files lying in +validly named subdirectories of {\str} need not be qualified to be +found. + +In case of files with identical base name, files lying in most recently +declared {\dirpath} are found first and explicit qualification is +required to refer to the other files of same base name. + +If several files with identical base name are present in different +subdirectories of a recursive loadpath declared via a single instance of +{\tt Add Rec LoadPath}, which of these files is found first is +system-dependent and explicit qualification is recommended. \Rem {\tt Add Rec LoadPath} also recursively adds {\str} to the current ML loadpath. @@ -600,7 +633,7 @@ command {\tt Declare ML Module} in the section This command displays the location of file {\str} in the current loadpath. Typically, {\str} is a \texttt{.cmo} or \texttt{.vo} or \texttt{.v} file. -\subsection[\tt Locate Library {\dirpath}.]{\tt Locate Library {\dirpath}.\comindex{Locate Library}} +\subsection[\tt Locate Library {\dirpath}.]{\tt Locate Library {\dirpath}.\comindex{Locate Library}\label{Locate Library}} This command gives the status of the \Coq\ module {\dirpath}. It tells if the module is loaded and if not searches in the load path for a module of logical name {\dirpath}. diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 8539136a0..9f6fa8be1 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1543,7 +1543,7 @@ induction n. This syntax is used for selecting which occurrences of {\term} the induction has to be carried on. The {\tt in {\atoccurrences}} clause is an occurrence clause whose syntax and behavior is described in - Section~\ref{Occurrences clause}. + Section~\ref{Occurrences clauses}. When an occurrence clause is given, an equation between {\term} and the value it gets in each case of the induction is added to the @@ -2448,8 +2448,10 @@ the given bindings to instantiate parameters or hypotheses of {\term}. \item \texttt{discriminate} - This looks for a quantified or not quantified hypothesis {\ident} on - which {\tt discriminate {\ident}} is applicable. + This behaves like {\tt discriminate {\ident}} if {\ident} is the + name of an hypothesis to which {\tt discriminate} is applicable; if + the current goal is of the form {\term$_1$} {\tt <>} {\term$_2$}, + this behaves as {\tt intro {\ident}; injection {\ident}}. \begin{ErrMsgs} \item \errindex{No discriminable equalities} \\ diff --git a/library/libnames.ml b/library/libnames.ml index dfa0fb82d..04ab34baa 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -89,6 +89,8 @@ let drop_dirpath_prefix d1 d2 = let d = Util.list_drop_prefix (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2)) in make_dirpath (List.rev d) +let append_dirpath d1 d2 = make_dirpath (repr_dirpath d2 @ repr_dirpath d1) + (* To know how qualified a name should be to be understood in the current env*) let add_dirpath_prefix id d = make_dirpath (repr_dirpath d @ [id]) diff --git a/library/libnames.mli b/library/libnames.mli index fe5033d73..890a442e3 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -59,6 +59,7 @@ val chop_dirpath : int -> dir_path -> dir_path * dir_path val drop_dirpath_prefix : dir_path -> dir_path -> dir_path val extract_dirpath_prefix : int -> dir_path -> dir_path val is_dirpath_prefix_of : dir_path -> dir_path -> bool +val append_dirpath : dir_path -> dir_path -> dir_path module Dirset : Set.S with type elt = dir_path module Dirmap : Map.S with type key = dir_path diff --git a/library/library.ml b/library/library.ml index 272f01f7d..b17be690a 100644 --- a/library/library.ml +++ b/library/library.ml @@ -24,9 +24,9 @@ open Nametab type logical_path = dir_path -let load_paths = ref ([],[] : System.physical_path list * logical_path list) +let load_paths = ref ([] : (System.physical_path * logical_path * bool) list) -let get_load_paths () = fst !load_paths +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 = @@ -56,12 +56,12 @@ let canonical_path_name p = (* We give up to find a canonical name and just simplify it... *) strip_path p -let find_logical_path phys_dir = +let find_logical_path phys_dir = let phys_dir = canonical_path_name phys_dir in - match list_filter2 (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) + 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 @@ -70,12 +70,12 @@ let is_in_load_paths phys_dir = List.exists check_p lp let remove_load_path dir = - load_paths := list_filter2 (fun p d -> p <> dir) !load_paths + load_paths := List.filter (fun (p,d,_) -> p <> dir) !load_paths -let add_load_path (phys_path,coq_path) = +let add_load_path isroot (phys_path,coq_path) = let phys_path = canonical_path_name phys_path in - match list_filter2 (fun p d -> p = phys_path) !load_paths with - | _,[dir] -> + 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 @@ -90,18 +90,54 @@ let add_load_path (phys_path,coq_path) = pr_dirpath dir ++ strbrk "; it is remapped to " ++ pr_dirpath coq_path); remove_load_path phys_path; - load_paths := (phys_path::fst !load_paths, coq_path::snd !load_paths) + load_paths := (phys_path,coq_path,isroot) :: !load_paths; end - | _,[] -> - load_paths := (phys_path :: fst !load_paths, coq_path :: snd !load_paths) + | [] -> + load_paths := (phys_path,coq_path,isroot) :: !load_paths; | _ -> anomaly ("Two logical paths are associated to "^phys_path) let physical_paths (dp,lp) = dp -let load_paths_of_dir_path dir = - fst (list_filter2 (fun p d -> d = dir) !load_paths) - -let get_full_load_paths () = List.combine (fst !load_paths) (snd !load_paths) +let extend_path_with_dirpath p dir = + List.fold_left Filename.concat p + (List.map string_of_id (List.rev (repr_dirpath dir))) + +let root_paths_matching_dir_path dir = + let rec aux = function + | [] -> [] + | (p,d,true) :: l when is_dirpath_prefix_of d dir -> + let suffix = drop_dirpath_prefix d dir in + extend_path_with_dirpath p suffix :: aux l + | _ :: l -> aux l in + aux !load_paths + +(* Root p is bound to A.B.C.D and we require file C.D.E.F *) +(* We may mean A.B.C.D.E.F, or A.B.C.D.C.D.E.F *) + +(* Root p is bound to A.B.C.C and we require file C.C.E.F *) +(* We may mean A.B.C.C.E.F, or A.B.C.C.C.E.F, or A.B.C.C.C.C.E.F *) + +let intersections d1 d2 = + let rec aux d1 = + if d1 = empty_dirpath then [d2] else + let rest = aux (snd (chop_dirpath 1 d1)) in + if is_dirpath_prefix_of d1 d2 then drop_dirpath_prefix d1 d2 :: rest + else rest in + aux d1 + +let loadpaths_matching_dir_path dir = + let rec aux = function + | [] -> [] + | (p,d,true) :: l -> + let inters = intersections d dir in + List.map (fun tl -> (extend_path_with_dirpath p tl,append_dirpath d tl)) + inters @ + aux l + | (p,d,_) :: l -> + (extend_path_with_dirpath p dir,append_dirpath d dir) :: aux l in + aux !load_paths + +let get_full_load_paths () = List.map (fun (a,b,c) -> (a,b)) !load_paths (************************************************************************) (*s Modules on disk contain the following informations (after the magic @@ -196,6 +232,12 @@ let library_full_filename dir = try LibraryFilenameMap.find dir !libraries_filename_table with Not_found -> "<unavailable filename>" +let overwrite_library_filenames f = + let f = + if Filename.is_relative f then Filename.concat (Sys.getcwd ()) f else f in + LibraryMap.iter (fun dir _ -> register_library_filename dir f) + !libraries_table + let library_is_loaded dir = try let _ = find_library dir in true with Not_found -> false @@ -334,11 +376,11 @@ type library_location = LibLoaded | LibInPath let locate_absolute_library dir = (* Search in loadpath *) let pref, base = split_dirpath dir in - let loadpath = load_paths_of_dir_path pref in + let loadpath = root_paths_matching_dir_path pref in if loadpath = [] then raise LibUnmappedDir; try let name = (string_of_id base)^".vo" in - let _, file = System.where_in_path loadpath name in + let _, file = System.where_in_path false loadpath name in (dir, file) with Not_found -> (* Last chance, removed from the file system but still in memory *) @@ -347,20 +389,15 @@ let locate_absolute_library dir = else raise LibNotFound -let locate_qualified_library qid = +let locate_qualified_library warn qid = try (* Search library in loadpath *) - let dir, base = repr_qualid qid in - let loadpath = - if repr_dirpath dir = [] then get_load_paths () - else - (* we assume dir is an absolute dirpath *) - load_paths_of_dir_path dir - in + let dir, base = repr_qualid qid in + let loadpath = loadpaths_matching_dir_path dir in if loadpath = [] then raise LibUnmappedDir; - let name = (string_of_id base)^".vo" in - let path, file = System.where_in_path loadpath name in - let dir = extend_dirpath (find_logical_path path) base in + let name = string_of_id base ^ ".vo" in + let lpath, file = System.where_in_path warn (List.map fst loadpath) name in + let dir = extend_dirpath (List.assoc lpath loadpath) base in (* Look if loaded *) if library_is_loaded dir then (LibLoaded, dir, library_full_filename dir) (* Otherwise, look for it in the file system *) @@ -386,7 +423,7 @@ let try_locate_absolute_library dir = let try_locate_qualified_library (loc,qid) = try - let (_,dir,f) = locate_qualified_library qid in + let (_,dir,f) = locate_qualified_library true qid in dir,f with e -> explain_locate_library_error qid e @@ -586,8 +623,7 @@ let import_module export (loc,qid) = (*s Initializing the compilation of a library. *) let start_library f = - let _,longf = - System.find_file_in_path (get_load_paths ()) (f^".v") in + let _,longf = System.find_file_in_path (get_load_paths ()) (f^".v") in let ldir0 = find_logical_path (Filename.dirname longf) in let id = id_of_string (Filename.basename f) in let ldir = extend_dirpath ldir0 id in diff --git a/library/library.mli b/library/library.mli index 1e2197409..d7cef3243 100644 --- a/library/library.mli +++ b/library/library.mli @@ -52,6 +52,9 @@ val opened_libraries : unit -> dir_path list (* - Return the full filename of a loaded library. *) val library_full_filename : dir_path -> string + (* - Overwrite the filename of all libraries (used when restoring a state) *) +val overwrite_library_filenames : string -> unit + (*s Hook for the xml exportation of libraries *) val set_xml_require : (dir_path -> unit) -> unit @@ -61,11 +64,10 @@ val set_xml_require : (dir_path -> unit) -> unit val get_load_paths : unit -> System.physical_path list val get_full_load_paths : unit -> (System.physical_path * dir_path) list -val add_load_path : System.physical_path * dir_path -> unit +val add_load_path : bool -> System.physical_path * dir_path -> unit val remove_load_path : System.physical_path -> unit val find_logical_path : System.physical_path -> dir_path val is_in_load_paths : System.physical_path -> bool -val load_paths_of_dir_path : dir_path -> System.physical_path list (*s Locate a library in the load paths *) exception LibUnmappedDir @@ -73,7 +75,7 @@ exception LibNotFound type library_location = LibLoaded | LibInPath val locate_qualified_library : - qualid -> library_location * dir_path * System.physical_path + bool -> qualid -> library_location * dir_path * System.physical_path (*s Statistics: display the memory use of a library. *) val mem : dir_path -> Pp.std_ppcmds diff --git a/library/states.ml b/library/states.ml index dcb4111ed..7c3953151 100644 --- a/library/states.ml +++ b/library/states.ml @@ -24,7 +24,9 @@ let state_magic_number = 19764 let (extern_state,intern_state) = let (raw_extern, raw_intern) = extern_intern state_magic_number ".coq" in (fun s -> raw_extern s (freeze())), - (fun s -> unfreeze (raw_intern (Library.get_load_paths ()) s)) + (fun s -> + unfreeze (raw_intern (Library.get_load_paths ()) s); + Library.overwrite_library_filenames s) (* Rollback. *) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 83a4703a2..7e92b804c 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -72,10 +72,12 @@ 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_include d p = push_include (d,p) -let set_rec_include d p = check_coq_overwriting p; push_rec_include (d,p) -let set_default_include d = set_include d Nameops.default_root_prefix -let set_default_rec_include d = set_rec_include d Nameops.default_root_prefix +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 set_rec_include d p = + let p = dirpath_of_string p in check_coq_overwriting p; push_rec_include(d,p) let load_vernacular_list = ref ([] : (string * bool) list) let add_load_vernacular verb s = @@ -187,15 +189,22 @@ let parse_args is_ide = | "-impredicative-set" :: rem -> set_engagement Declarations.ImpredicativeSet; parse rem + | ("-I"|"-include") :: d :: "-as" :: p :: rem -> set_include d p; parse rem + | ("-I"|"-include") :: d :: "-as" :: [] -> usage () | ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem | ("-I"|"-include") :: [] -> usage () - | "-R" :: d :: p :: rem ->set_rec_include d (dirpath_of_string p);parse rem + | "-R" :: d :: "-as" :: p :: rem -> set_rec_include d p;parse rem + | "-R" :: d :: "-as" :: [] -> usage () + | "-R" :: d :: p :: rem -> set_rec_include d p;parse rem | "-R" :: ([] | [_]) -> usage () | "-top" :: d :: rem -> set_toplevel_name (dirpath_of_string d); parse rem | "-top" :: [] -> usage () + | "-exclude-dir" :: f :: rem -> exclude_search_in_dirname f; parse rem + | "-exclude-dir" :: [] -> usage () + | "-notop" :: rem -> unset_toplevel_name (); parse rem | "-q" :: rem -> no_load_rc (); parse rem diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index 71369f0ab..c64807db1 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -108,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 !coq_mlpath_copy s in + let _,gname = where_in_path true !coq_mlpath_copy s in try Dynlink.loadfile gname; Dynlink.add_interfaces @@ -145,7 +145,7 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath = if exists_dir dir then begin add_ml_dir dir; - Library.add_load_path (dir,coq_dirpath) + Library.add_load_path true (dir,coq_dirpath) end else msg_warning [< str ("Cannot open " ^ dir) >] @@ -159,19 +159,18 @@ let convert_string d = failwith "caught" let add_rec_path ~unix_path:dir ~coq_root:coq_dirpath = - let dirs = all_subdirs dir in - let prefix = Names.repr_dirpath coq_dirpath in - if dirs <> [] then + if exists_dir dir then + let dirs = all_subdirs dir in + let prefix = Names.repr_dirpath coq_dirpath in let convert_dirs (lp,cp) = - (lp,Names.make_dirpath - ((List.map convert_string (List.rev cp))@prefix)) in + (lp,Names.make_dirpath (List.map convert_string (List.rev cp)@prefix)) in let dirs = map_succeed convert_dirs dirs in - begin - List.iter (fun lpe -> add_ml_dir (fst lpe)) dirs; - List.iter Library.add_load_path dirs - end + List.iter (fun lpe -> add_ml_dir (fst lpe)) dirs; + add_ml_dir dir; + List.iter (Library.add_load_path false) dirs; + Library.add_load_path true (dir,coq_dirpath) else - msg_warning [< str ("Cannot open " ^ dir) >] + msg_warning (str ("Cannot open " ^ dir)) (* convertit un nom quelconque en nom de fichier ou de module *) let mod_of_name name = diff --git a/toplevel/usage.ml b/toplevel/usage.ml index e00f7808b..124ce0593 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -20,10 +20,14 @@ let print_usage_channel co command = output_string co command; output_string co "Coq options are:\n"; output_string co -" -I dir add directory dir in the include path +" -I dir -as coqdir map physical dir to logical coqdir + -I dir map directory dir to the empty logical path -include dir (idem) - -R dir coqdir recursively map physical dir to logical coqdir + -R dir -as coqdir recursively map physical dir to logical coqdir + -R dir coqdir (idem) -top coqdir set the toplevel name to be coqdir instead of Top + -notop r set the toplevel name to be the empty logical path + -exclude-dir f exclude subdirectories named f for option -R -inputstate f read state from file f.coq -is f (idem) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index d1003bd83..7ccfe526d 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -180,12 +180,12 @@ let show_match id = (* "Print" commands *) let print_path_entry (s,l) = - (str s ++ str " " ++ tbrk (0,2) ++ str (string_of_dirpath l)) + (str (string_of_dirpath l) ++ str " " ++ tbrk (0,0) ++ str s) let print_loadpath () = let l = Library.get_full_load_paths () in - msgnl (Pp.t (str "Physical path: " ++ - tab () ++ str "Logical Path:" ++ fnl () ++ + msgnl (Pp.t (str "Logical Path: " ++ + tab () ++ str "Physical path:" ++ fnl () ++ prlist_with_sep pr_fnl print_path_entry l)) let print_modules () = @@ -232,7 +232,7 @@ let dump_universes s = let locate_file f = try - let _,file = System.where_in_path (Library.get_load_paths ()) f in + let _,file = System.where_in_path false (Library.get_load_paths ()) f in msgnl (str file) with Not_found -> msgnl (hov 0 (str"Can't find file" ++ spc () ++ str f ++ spc () ++ @@ -240,24 +240,25 @@ let locate_file f = let msg_found_library = function | Library.LibLoaded, fulldir, file -> - msgnl(pr_dirpath fulldir ++ str " has been loaded from file" ++ fnl () ++ - str file) + msgnl (hov 0 + (pr_dirpath fulldir ++ strbrk " has been loaded from file " ++ + str file)) | Library.LibInPath, fulldir, file -> - msgnl(pr_dirpath fulldir ++ str " is bound to file " ++ str file) + msgnl (hov 0 + (pr_dirpath fulldir ++ strbrk " is bound to file " ++ str file)) let msg_notfound_library loc qid = function | Library.LibUnmappedDir -> let dir = fst (repr_qualid qid) in user_err_loc (loc,"locate_library", - str "Cannot find a physical path bound to logical path " ++ + strbrk "Cannot find a physical path bound to logical path " ++ pr_dirpath dir ++ fnl ()) | Library.LibNotFound -> - msgnl (hov 0 - (str"Unable to locate library" ++ spc () ++ pr_qualid qid)) + msgnl (hov 0 (strbrk "Unable to locate library " ++ pr_qualid qid)) | e -> assert false let print_located_library r = let (loc,qid) = qualid_of_reference r in - try msg_found_library (Library.locate_qualified_library qid) + try msg_found_library (Library.locate_qualified_library false qid) with e -> msg_notfound_library loc qid e let print_located_module r = @@ -570,7 +571,7 @@ let vernac_end_segment lid = let vernac_require import _ qidl = let qidl = List.map qualid_of_reference qidl in - let modrefl = List.map (fun (_, qid) -> let (_, dp, _) = (Library.locate_qualified_library qid) in dp) qidl in + let modrefl = List.map (fun (_, qid) -> let (_, dp, _) = (Library.locate_qualified_library false qid) in dp) qidl in List.iter2 (fun (loc, _) dp -> Dumpglob.dump_libref loc dp "lib") qidl modrefl; Library.require_library qidl import |