aboutsummaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/declaremods.ml2
-rw-r--r--library/global.ml17
-rw-r--r--library/global.mli8
-rw-r--r--library/lib.ml3
-rw-r--r--library/lib.mli1
-rw-r--r--library/libnames.ml3
-rw-r--r--library/libnames.mli3
-rw-r--r--library/library.ml179
-rw-r--r--library/library.mli37
-rw-r--r--library/library.mllib1
-rw-r--r--library/loadpath.ml119
-rw-r--r--library/loadpath.mli57
-rw-r--r--library/nametab.mli2
-rw-r--r--library/summary.mli2
14 files changed, 81 insertions, 353 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 5fd11e187a..d74bdd484c 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -51,7 +51,7 @@ let inl2intopt = function
- Then comes either the object segment itself (for interactive
modules), or a compact way to store derived objects (path to
- a earlier module + subtitution).
+ a earlier module + substitution).
*)
type algebraic_objects =
diff --git a/library/global.ml b/library/global.ml
index 58e2380440..d5ffae7716 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -132,9 +132,20 @@ let exists_objlabel id = Safe_typing.exists_objlabel id (safe_env ())
let opaque_tables () = Environ.opaque_tables (env ())
-let body_of_constant_body ce = body_of_constant_body (env ()) ce
-
-let body_of_constant cst = body_of_constant_body (lookup_constant cst)
+let body_of_constant_body access env cb =
+ let open Declarations in
+ let otab = Environ.opaque_tables env in
+ match cb.const_body with
+ | Undef _ | Primitive _ ->
+ None
+ | Def c ->
+ Some (Mod_subst.force_constr c, Declareops.constant_polymorphic_context cb)
+ | OpaqueDef o ->
+ Some (Opaqueproof.force_proof access otab o, Declareops.constant_polymorphic_context cb)
+
+let body_of_constant_body access ce = body_of_constant_body access (env ()) ce
+
+let body_of_constant access cst = body_of_constant_body access (lookup_constant cst)
(** Operations on kernel names *)
diff --git a/library/global.mli b/library/global.mli
index 984d8c666c..eaa76c3117 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -42,8 +42,8 @@ val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set
val push_named_def : (Id.t * Entries.section_def_entry) -> unit
val export_private_constants : in_section:bool ->
- Safe_typing.private_constants Entries.definition_entry ->
- unit Entries.definition_entry * Safe_typing.exported_private_constant list
+ Safe_typing.private_constants Entries.proof_output ->
+ Constr.constr Univ.in_universe_context_set * Safe_typing.exported_private_constant list
val add_constant :
?role:Entries.side_effect_role -> in_section:bool -> Id.t -> Safe_typing.global_declaration -> Constant.t * Safe_typing.private_constants
@@ -100,13 +100,13 @@ val mind_of_delta_kn : KerName.t -> MutInd.t
val opaque_tables : unit -> Opaqueproof.opaquetab
-val body_of_constant : Constant.t -> (Constr.constr * Univ.AUContext.t) option
+val body_of_constant : Opaqueproof.indirect_accessor -> Constant.t -> (Constr.constr * Univ.AUContext.t) option
(** Returns the body of the constant if it has any, and the polymorphic context
it lives in. For monomorphic constant, the latter is empty, and for
polymorphic constants, the term contains De Bruijn universe variables that
need to be instantiated. *)
-val body_of_constant_body : Opaqueproof.opaque Declarations.constant_body -> (Constr.constr * Univ.AUContext.t) option
+val body_of_constant_body : Opaqueproof.indirect_accessor -> Opaqueproof.opaque Declarations.constant_body -> (Constr.constr * Univ.AUContext.t) option
(** Same as {!body_of_constant} but on {!Declarations.constant_body}. *)
(** {6 Compiled libraries } *)
diff --git a/library/lib.ml b/library/lib.ml
index 4be288ed20..daa41eca65 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -474,9 +474,6 @@ let extract_hyps (secs,ohyps) =
let instance_from_variable_context =
List.map fst %> List.filter is_local_assum %> List.map NamedDecl.get_id %> Array.of_list
-let named_of_variable_context =
- List.map fst
-
let name_instance inst =
(* FIXME: this should probably be done at an upper level, by storing the
name information in the section data structure. *)
diff --git a/library/lib.mli b/library/lib.mli
index 5da76961a6..c19c3bf7fa 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -168,7 +168,6 @@ type abstr_info = private {
}
val instance_from_variable_context : variable_context -> Id.t array
-val named_of_variable_context : variable_context -> Constr.named_context
val section_segment_of_constant : Constant.t -> abstr_info
val section_segment_of_mutual_inductive: MutInd.t -> abstr_info
diff --git a/library/libnames.ml b/library/libnames.ml
index 87c4de42e8..41b38e0378 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -162,6 +162,9 @@ let qualid_basename qid =
let qualid_path qid =
qid.CAst.v.dirpath
+let idset_mem_qualid qid s =
+ qualid_is_ident qid && Id.Set.mem (qualid_basename qid) s
+
(* Default paths *)
let default_library = Names.DirPath.initial (* = ["Top"] *)
diff --git a/library/libnames.mli b/library/libnames.mli
index bbb4d2a058..7d77d95991 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -88,6 +88,9 @@ val qualid_is_ident : qualid -> bool
val qualid_path : qualid -> DirPath.t
val qualid_basename : qualid -> Id.t
+val idset_mem_qualid : qualid -> Id.Set.t -> bool
+(** false when the qualid is not an ident *)
+
(** {6 ... } *)
(** some preset paths *)
diff --git a/library/library.ml b/library/library.ml
index 500e77f89b..1ac75d2fdc 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -208,7 +208,7 @@ let register_open_library export m =
let open_library export explicit_libs m =
if
(* Only libraries indirectly to open are not reopen *)
- (* Libraries explicitly mentionned by the user are always reopen *)
+ (* Libraries explicitly mentioned by the user are always reopen *)
List.exists (fun m' -> DirPath.equal m m') explicit_libs
|| not (library_is_opened m)
then begin
@@ -264,90 +264,11 @@ let in_import_library : DirPath.t list * bool -> obj =
subst_function = subst_import_library;
classify_function = classify_import_library }
-
-(************************************************************************)
-(*s Locate absolute or partially qualified library names in the path *)
-
-exception LibUnmappedDir
-exception LibNotFound
-type library_location = LibLoaded | LibInPath
-
-let warn_several_object_files =
- CWarnings.create ~name:"several-object-files" ~category:"require"
- (fun (vi, vo) -> str"Loading" ++ spc () ++ str vi ++
- strbrk " instead of " ++ str vo ++
- strbrk " because it is more recent")
-
-let locate_absolute_library dir =
- (* Search in loadpath *)
- let pref, base = split_dirpath dir in
- let loadpath = Loadpath.filter_path (fun dir -> DirPath.equal dir pref) in
- let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in
- let loadpath = List.map fst loadpath in
- let find ext =
- try
- let name = Id.to_string base ^ ext in
- let _, file = System.where_in_path ~warn:false loadpath name in
- Some file
- with Not_found -> None in
- match find ".vo", find ".vio" with
- | None, None -> raise LibNotFound
- | Some file, None | None, Some file -> file
- | Some vo, Some vi when Unix.((stat vo).st_mtime < (stat vi).st_mtime) ->
- warn_several_object_files (vi, vo);
- vi
- | Some vo, Some _ -> vo
-
-let locate_qualified_library ?root ?(warn = true) qid =
- (* Search library in loadpath *)
- let dir, base = repr_qualid qid in
- let loadpath = Loadpath.expand_path ?root dir in
- let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in
- let find ext =
- try
- let name = Id.to_string base ^ ext in
- let lpath, file =
- System.where_in_path ~warn (List.map fst loadpath) name in
- Some (lpath, file)
- with Not_found -> None in
- let lpath, file =
- match find ".vo", find ".vio" with
- | None, None -> raise LibNotFound
- | Some res, None | None, Some res -> res
- | Some (_, vo), Some (_, vi as resvi)
- when Unix.((stat vo).st_mtime < (stat vi).st_mtime) ->
- warn_several_object_files (vi, vo);
- resvi
- | Some resvo, Some _ -> resvo
- in
- let dir = add_dirpath_suffix (String.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 *)
- else (LibInPath, dir, file)
-
-let error_unmapped_dir qid =
- let prefix, _ = repr_qualid qid in
- user_err ~hdr:"load_absolute_library_from"
- (str "Cannot load " ++ pr_qualid qid ++ str ":" ++ spc () ++
- str "no physical path bound to" ++ spc () ++ DirPath.print prefix ++ fnl ())
-
-let error_lib_not_found qid =
- user_err ~hdr:"load_absolute_library_from"
- (str"Cannot find library " ++ pr_qualid qid ++ str" in loadpath")
-
-let try_locate_absolute_library dir =
- try
- locate_absolute_library dir
- with
- | LibUnmappedDir -> error_unmapped_dir (qualid_of_dirpath dir)
- | LibNotFound -> error_lib_not_found (qualid_of_dirpath dir)
-
(************************************************************************)
(** {6 Tables of opaque proof terms} *)
(** We now store opaque proof terms apart from the rest of the environment.
- See the [Indirect] contructor in [Lazyconstr.lazy_constr]. This way,
+ See the [Indirect] constructor in [Lazyconstr.lazy_constr]. This way,
we can quickly load a first half of a .vo file without these opaque
terms, and access them only when a specific command (e.g. Print or
Print Assumptions) needs it. *)
@@ -355,18 +276,14 @@ let try_locate_absolute_library dir =
(** Delayed / available tables of opaque terms *)
type 'a table_status =
- | ToFetch of 'a Future.computation array delayed
- | Fetched of 'a Future.computation array
+ | ToFetch of 'a array delayed
+ | Fetched of 'a array
let opaque_tables =
- ref (LibraryMap.empty : (Constr.constr table_status) LibraryMap.t)
-let univ_tables =
- ref (LibraryMap.empty : (Univ.ContextSet.t table_status) LibraryMap.t)
+ ref (LibraryMap.empty : ((Opaqueproof.cooking_info list * int * Constr.constr option) table_status) LibraryMap.t)
let add_opaque_table dp st =
opaque_tables := LibraryMap.add dp st !opaque_tables
-let add_univ_table dp st =
- univ_tables := LibraryMap.add dp st !univ_tables
let access_table what tables dp i =
let t = match LibraryMap.find dp !tables with
@@ -389,17 +306,15 @@ let access_table what tables dp i =
let access_opaque_table dp i =
let what = "opaque proofs" in
- access_table what opaque_tables dp i
-
-let access_univ_table dp i =
- try
- let what = "universe contexts of opaque proofs" in
- Some (access_table what univ_tables dp i)
- with Not_found -> None
-
-let () =
- Opaqueproof.set_indirect_opaque_accessor access_opaque_table;
- Opaqueproof.set_indirect_univ_accessor access_univ_table
+ let (info, n, c) = access_table what opaque_tables dp i in
+ match c with
+ | None -> None
+ | Some c -> Some (Cooking.cook_constr info n c)
+
+let indirect_accessor = {
+ Opaqueproof.access_proof = access_opaque_table;
+ Opaqueproof.access_discharge = Cooking.cook_constr;
+}
(************************************************************************)
(* Internalise libraries *)
@@ -407,9 +322,8 @@ let () =
type seg_sum = summary_disk
type seg_lib = library_disk
type seg_univ = (* true = vivo, false = vi *)
- Univ.ContextSet.t Future.computation array * Univ.ContextSet.t * bool
-type seg_discharge = Opaqueproof.cooking_info list array
-type seg_proofs = Constr.constr Future.computation array
+ Univ.ContextSet.t * bool
+type seg_proofs = (Opaqueproof.cooking_info list * int * Constr.t option) array
let mk_library sd md digests univs =
{
@@ -433,7 +347,6 @@ let intern_from_file f =
let ((lmd : seg_lib delayed), digest_lmd) = in_delayed f ch in
let (univs : seg_univ option), _, digest_u = System.marshal_in_segment f ch in
let _ = System.skip_in_segment f ch in
- let _ = System.skip_in_segment f ch in
let ((del_opaque : seg_proofs delayed),_) = in_delayed f ch in
close_in ch;
register_library_filename lsd.md_name f;
@@ -441,16 +354,14 @@ let intern_from_file f =
let open Safe_typing in
match univs with
| None -> mk_library lsd lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty
- | Some (utab,uall,true) ->
- add_univ_table lsd.md_name (Fetched utab);
+ | Some (uall,true) ->
mk_library lsd lmd (Dvivo (digest_lmd,digest_u)) uall
- | Some (utab,_,false) ->
- add_univ_table lsd.md_name (Fetched utab);
+ | Some (_,false) ->
mk_library lsd lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty
module DPMap = Map.Make(DirPath)
-let rec intern_library (needed, contents) (dir, f) from =
+let rec intern_library ~lib_resolver (needed, contents) (dir, f) from =
(* Look if in the current logical environment *)
try (find_library dir).libsum_digests, (needed, contents)
with Not_found ->
@@ -459,7 +370,7 @@ let rec intern_library (needed, contents) (dir, f) from =
with Not_found ->
Feedback.feedback(Feedback.FileDependency (from, DirPath.to_string dir));
(* [dir] is an absolute name which matches [f] which must be in loadpath *)
- let f = match f with Some f -> f | None -> try_locate_absolute_library dir in
+ let f = match f with Some f -> f | None -> lib_resolver dir in
let m = intern_from_file f in
if not (DirPath.equal dir m.library_name) then
user_err ~hdr:"load_physical_library"
@@ -467,22 +378,24 @@ let rec intern_library (needed, contents) (dir, f) from =
DirPath.print m.library_name ++ spc () ++ str "and not library" ++
spc() ++ DirPath.print dir);
Feedback.feedback (Feedback.FileLoaded(DirPath.to_string dir, f));
- m.library_digests, intern_library_deps (needed, contents) dir m f
+ m.library_digests, intern_library_deps ~lib_resolver (needed, contents) dir m f
-and intern_library_deps libs dir m from =
- let needed, contents = Array.fold_left (intern_mandatory_library dir from) libs m.library_deps in
+and intern_library_deps ~lib_resolver libs dir m from =
+ let needed, contents =
+ Array.fold_left (intern_mandatory_library ~lib_resolver dir from)
+ libs m.library_deps in
(dir :: needed, DPMap.add dir m contents )
-and intern_mandatory_library caller from libs (dir,d) =
- let digest, libs = intern_library libs (dir, None) (Some from) in
+and intern_mandatory_library ~lib_resolver caller from libs (dir,d) =
+ let digest, libs = intern_library ~lib_resolver libs (dir, None) (Some from) in
if not (Safe_typing.digest_match ~actual:digest ~required:d) then
user_err (str "Compiled library " ++ DirPath.print caller ++
str " (in file " ++ str from ++ str ") makes inconsistent assumptions \
over library " ++ DirPath.print dir);
libs
-let rec_intern_library libs (dir, f) =
- let _, libs = intern_library libs (dir, Some f) None in
+let rec_intern_library ~lib_resolver libs (dir, f) =
+ let _, libs = intern_library ~lib_resolver libs (dir, Some f) None in
libs
let native_name_from_filename f =
@@ -557,8 +470,8 @@ let warn_require_in_module =
strbrk "You can Require a module at toplevel " ++
strbrk "and optionally Import it inside another one.")
-let require_library_from_dirpath modrefl export =
- let needed, contents = List.fold_left rec_intern_library ([], DPMap.empty) modrefl in
+let require_library_from_dirpath ~lib_resolver modrefl export =
+ let needed, contents = List.fold_left (rec_intern_library ~lib_resolver) ([], DPMap.empty) modrefl in
let needed = List.rev_map (fun dir -> DPMap.find dir contents) needed in
let modrefl = List.map fst modrefl in
if Lib.is_module_or_modtype () then
@@ -616,15 +529,13 @@ let load_library_todo f =
let (s0 : seg_sum), _, _ = System.marshal_in_segment f ch in
let (s1 : seg_lib), _, _ = System.marshal_in_segment f ch in
let (s2 : seg_univ option), _, _ = System.marshal_in_segment f ch in
- let (s3 : seg_discharge option), _, _ = System.marshal_in_segment f ch in
let tasks, _, _ = System.marshal_in_segment f ch in
- let (s5 : seg_proofs), _, _ = System.marshal_in_segment f ch in
+ let (s4 : seg_proofs), _, _ = System.marshal_in_segment f ch in
close_in ch;
if tasks = None then user_err ~hdr:"restart" (str"not a .vio file");
if s2 = None then user_err ~hdr:"restart" (str"not a .vio file");
- if s3 = None then user_err ~hdr:"restart" (str"not a .vio file");
- if pi3 (Option.get s2) then user_err ~hdr:"restart" (str"not a .vio file");
- s0, s1, Option.get s2, Option.get s3, Option.get tasks, s5
+ if snd (Option.get s2) then user_err ~hdr:"restart" (str"not a .vio file");
+ s0, s1, Option.get s2, Option.get tasks, s4
(************************************************************************)
(*s [save_library dir] ends library [dir] and save it to the disk. *)
@@ -667,10 +578,10 @@ let save_library_to ?todo ~output_native_objects dir f otab =
List.fold_left (fun e (r,_) -> Future.UUIDSet.add r.Stateid.uuid e)
Future.UUIDSet.empty l in
let cenv, seg, ast = Declaremods.end_library ~output_native_objects ~except dir in
- let opaque_table, univ_table, disch_table, f2t_map = Opaqueproof.dump otab in
- let tasks, utab, dtab =
+ let opaque_table, f2t_map = Opaqueproof.dump ~except otab in
+ let tasks, utab =
match todo with
- | None -> None, None, None
+ | None -> None, None
| Some (tasks, rcbackup) ->
let tasks =
List.map Stateid.(fun (r,b) ->
@@ -678,18 +589,8 @@ let save_library_to ?todo ~output_native_objects dir f otab =
with Not_found -> assert b; { r with uuid = -1 }, b)
tasks in
Some (tasks,rcbackup),
- Some (univ_table,Univ.ContextSet.empty,false),
- Some disch_table in
- let except =
- Future.UUIDSet.fold (fun uuid acc ->
- try Int.Set.add (Future.UUIDMap.find uuid f2t_map) acc
- with Not_found -> acc)
- except Int.Set.empty in
- let is_done_or_todo i x = Future.is_val x || Int.Set.mem i except in
- Array.iteri (fun i x ->
- if not(is_done_or_todo i x) then CErrors.user_err ~hdr:"library"
- Pp.(str"Proof object "++int i++str" is not checked nor to be checked"))
- opaque_table;
+ Some (Univ.ContextSet.empty,false)
+ in
let sd = {
md_name = dir;
md_deps = Array.of_list (current_deps ());
@@ -709,7 +610,6 @@ let save_library_to ?todo ~output_native_objects dir f otab =
System.marshal_out_segment f' ch (sd : seg_sum);
System.marshal_out_segment f' ch (md : seg_lib);
System.marshal_out_segment f' ch (utab : seg_univ option);
- System.marshal_out_segment f' ch (dtab : seg_discharge option);
System.marshal_out_segment f' ch (tasks : 'tasks option);
System.marshal_out_segment f' ch (opaque_table : seg_proofs);
close_out ch;
@@ -729,7 +629,6 @@ let save_library_raw f sum lib univs proofs =
System.marshal_out_segment f ch (sum : seg_sum);
System.marshal_out_segment f ch (lib : seg_lib);
System.marshal_out_segment f ch (Some univs : seg_univ option);
- System.marshal_out_segment f ch (None : seg_discharge option);
System.marshal_out_segment f ch (None : 'tasks option);
System.marshal_out_segment f ch (proofs : seg_proofs);
close_out ch
diff --git a/library/library.mli b/library/library.mli
index 390299bf56..727eca10cf 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -22,17 +22,20 @@ open Libnames
(** {6 ... }
Require = load in the environment + open (if the optional boolean
is not [None]); mark also for export if the boolean is [Some true] *)
-val require_library_from_dirpath : (DirPath.t * string) list -> bool option -> unit
+val require_library_from_dirpath
+ : lib_resolver:(DirPath.t -> CUnix.physical_path)
+ -> (DirPath.t * string) list
+ -> bool option
+ -> unit
(** {6 Start the compilation of a library } *)
(** Segments of a library *)
type seg_sum
type seg_lib
-type seg_univ = (* cst, all_cst, finished? *)
- Univ.ContextSet.t Future.computation array * Univ.ContextSet.t * bool
-type seg_discharge = Opaqueproof.cooking_info list array
-type seg_proofs = Constr.constr Future.computation array
+type seg_univ = (* all_cst, finished? *)
+ Univ.ContextSet.t * bool
+type seg_proofs = (Opaqueproof.cooking_info list * int * Constr.t option) array
(** Open a module (or a library); if the boolean is true then it's also
an export otherwise just a simple import *)
@@ -45,8 +48,10 @@ val save_library_to :
output_native_objects:bool ->
DirPath.t -> string -> Opaqueproof.opaquetab -> unit
-val load_library_todo :
- string -> seg_sum * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs
+val load_library_todo
+ : CUnix.physical_path
+ -> seg_sum * seg_lib * seg_univ * 'tasks * seg_proofs
+
val save_library_raw : string -> seg_sum -> seg_lib -> seg_univ -> seg_proofs -> unit
(** {6 Interrogate the status of libraries } *)
@@ -65,20 +70,8 @@ val library_full_filename : DirPath.t -> string
(** - Overwrite the filename of all libraries (used when restoring a state) *)
val overwrite_library_filenames : string -> unit
-(** {6 Locate a library in the load paths } *)
-exception LibUnmappedDir
-exception LibNotFound
-type library_location = LibLoaded | LibInPath
-
-val locate_qualified_library :
- ?root:DirPath.t -> ?warn:bool -> qualid ->
- library_location * DirPath.t * CUnix.physical_path
-(** Locates a library by implicit name.
-
- @raise LibUnmappedDir if the library is not in the path
- @raise LibNotFound if there is no corresponding file in the path
-
-*)
-
(** {6 Native compiler. } *)
val native_name_from_filename : string -> string
+
+(** {6 Opaque accessors} *)
+val indirect_accessor : Opaqueproof.indirect_accessor
diff --git a/library/library.mllib b/library/library.mllib
index 8f694f4a31..ef53471377 100644
--- a/library/library.mllib
+++ b/library/library.mllib
@@ -7,7 +7,6 @@ Global
Decl_kinds
Lib
Declaremods
-Loadpath
Library
States
Kindops
diff --git a/library/loadpath.ml b/library/loadpath.ml
deleted file mode 100644
index fc13c864d0..0000000000
--- a/library/loadpath.ml
+++ /dev/null
@@ -1,119 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-open Pp
-open Util
-open CErrors
-open Names
-open Libnames
-
-(** Load paths. Mapping from physical to logical paths. *)
-
-type t = {
- path_physical : CUnix.physical_path;
- path_logical : DirPath.t;
- path_implicit : bool;
-}
-
-let load_paths = Summary.ref ([] : t list) ~name:"LOADPATHS"
-
-let logical p = p.path_logical
-
-let physical p = p.path_physical
-
-let get_load_paths () = !load_paths
-
-let anomaly_too_many_paths path =
- anomaly (str "Several logical paths are associated to" ++ spc () ++ str path ++ str ".")
-
-let find_load_path phys_dir =
- let phys_dir = CUnix.canonical_path_name phys_dir in
- let filter p = String.equal p.path_physical phys_dir in
- let paths = List.filter filter !load_paths in
- match paths with
- | [] -> raise Not_found
- | [p] -> p
- | _ -> anomaly_too_many_paths phys_dir
-
-let is_in_load_paths phys_dir =
- let dir = CUnix.canonical_path_name phys_dir in
- let lp = get_load_paths () in
- let check_p p = String.equal dir p.path_physical in
- List.exists check_p lp
-
-let remove_load_path dir =
- let filter p = not (String.equal p.path_physical dir) in
- load_paths := List.filter filter !load_paths
-
-let warn_overriding_logical_loadpath =
- CWarnings.create ~name:"overriding-logical-loadpath" ~category:"loadpath"
- (fun (phys_path, old_path, coq_path) ->
- str phys_path ++ strbrk " was previously bound to " ++
- DirPath.print old_path ++ strbrk "; it is remapped to " ++
- DirPath.print coq_path)
-
-let add_load_path phys_path coq_path ~implicit =
- let phys_path = CUnix.canonical_path_name phys_path in
- let filter p = String.equal p.path_physical phys_path in
- let binding = {
- path_logical = coq_path;
- path_physical = phys_path;
- path_implicit = implicit;
- } in
- match List.filter filter !load_paths with
- | [] ->
- load_paths := binding :: !load_paths
- | [{ path_logical = old_path; path_implicit = old_implicit }] ->
- let replace =
- if DirPath.equal coq_path old_path then
- implicit <> old_implicit
- else
- let () =
- (* Do not warn when overriding the default "-I ." path *)
- if not (DirPath.equal old_path Libnames.default_root_prefix) then
- warn_overriding_logical_loadpath (phys_path, old_path, coq_path)
- in
- true in
- if replace then
- begin
- remove_load_path phys_path;
- load_paths := binding :: !load_paths;
- end
- | _ -> anomaly_too_many_paths phys_path
-
-let filter_path f =
- let rec aux = function
- | [] -> []
- | p :: l ->
- if f p.path_logical then (p.path_physical, p.path_logical) :: aux l
- else aux l
- in
- aux !load_paths
-
-let expand_path ?root dir =
- let rec aux = function
- | [] -> []
- | { path_physical = ph; path_logical = lg; path_implicit = implicit } :: l ->
- let success =
- match root with
- | None ->
- if implicit then is_dirpath_suffix_of dir lg
- else DirPath.equal dir lg
- | Some root ->
- is_dirpath_prefix_of root lg &&
- is_dirpath_suffix_of dir (drop_dirpath_prefix root lg) in
- if success then (ph, lg) :: aux l else aux l in
- aux !load_paths
-
-let locate_file fname =
- let paths = List.map physical !load_paths in
- let _,longfname =
- System.find_file_in_path ~warn:(not !Flags.quiet) paths fname in
- longfname
diff --git a/library/loadpath.mli b/library/loadpath.mli
deleted file mode 100644
index 4044ca1127..0000000000
--- a/library/loadpath.mli
+++ /dev/null
@@ -1,57 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-open Names
-
-(** * Load paths.
-
- A load path is a physical path in the file system; to each load path is
- associated a Coq [DirPath.t] (the "logical" path of the physical path).
-
-*)
-
-type t
-(** Type of loadpath bindings. *)
-
-val physical : t -> CUnix.physical_path
-(** Get the physical path (filesystem location) of a loadpath. *)
-
-val logical : t -> DirPath.t
-(** Get the logical path (Coq module hierarchy) of a loadpath. *)
-
-val get_load_paths : unit -> t list
-(** Get the current loadpath association. *)
-
-val add_load_path : CUnix.physical_path -> DirPath.t -> implicit:bool -> unit
-(** [add_load_path phys log type] adds the binding [phys := log] to the current
- loadpaths. *)
-
-val remove_load_path : CUnix.physical_path -> unit
-(** Remove the current logical path binding associated to a given physical path,
- if any. *)
-
-val find_load_path : CUnix.physical_path -> t
-(** Get the binding associated to a physical path. Raises [Not_found] if there
- is none. *)
-
-val is_in_load_paths : CUnix.physical_path -> bool
-(** Whether a physical path is currently bound. *)
-
-val expand_path : ?root:DirPath.t -> DirPath.t -> (CUnix.physical_path * DirPath.t) list
-(** Given a relative logical path, associate the list of absolute physical and
- logical paths which are possible matches of it. *)
-
-val filter_path : (DirPath.t -> bool) -> (CUnix.physical_path * DirPath.t) list
-(** As {!expand_path} but uses a filter function instead, and ignores the
- implicit status of loadpaths. *)
-
-val locate_file : string -> string
-(** Locate a file among the registered paths. Do not use this function, as
- it does not respect the visibility of paths. *)
diff --git a/library/nametab.mli b/library/nametab.mli
index a4f177aad0..33cb4faf99 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -38,7 +38,7 @@ open Globnames
}
{- [exists : full_user_name -> bool]
- Is the [full_user_name] already atributed as an absolute user name
+ Is the [full_user_name] already attributed as an absolute user name
of some object?
}
{- [locate : qualid -> object_reference]
diff --git a/library/summary.mli b/library/summary.mli
index 0d77d725ac..3875bcfe9e 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -28,7 +28,7 @@ type 'a summary_declaration = {
Beware: for tables registered dynamically after the initialization
of Coq, their init functions may not be run immediately. It is hence
- the responsability of plugins to initialize themselves properly.
+ the responsibility of plugins to initialize themselves properly.
*)
val declare_summary : string -> 'a summary_declaration -> unit
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 13:09:50 +0000