aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/declare.ml47
-rw-r--r--library/declaremods.ml6
-rw-r--r--library/declaremods.mli3
-rw-r--r--library/goptions.ml15
-rw-r--r--library/libobject.ml2
-rw-r--r--library/library.ml26
-rw-r--r--library/loadpath.ml2
-rw-r--r--library/nametab.ml6
-rw-r--r--library/universes.ml3
-rw-r--r--library/universes.mli2
10 files changed, 73 insertions, 39 deletions
diff --git a/library/declare.ml b/library/declare.ml
index c59d190a0..84284fd18 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -398,7 +398,7 @@ let declare_mind mie =
let pr_rank i = pr_nth (i+1)
let fixpoint_message indexes l =
- Flags.if_verbose msg_info (match l with
+ Flags.if_verbose Feedback.msg_info (match l with
| [] -> anomaly (Pp.str "no recursive definition")
| [id] -> pr_id id ++ str " is recursively defined" ++
(match indexes with
@@ -413,7 +413,7 @@ let fixpoint_message indexes l =
| None -> mt ()))
let cofixpoint_message l =
- Flags.if_verbose msg_info (match l with
+ Flags.if_verbose Feedback.msg_info (match l with
| [] -> anomaly (Pp.str "No corecursive definition.")
| [id] -> pr_id id ++ str " is corecursively defined"
| l -> hov 0 (prlist_with_sep pr_comma pr_id l ++
@@ -423,13 +423,13 @@ let recursive_message isfix i l =
(if isfix then fixpoint_message i else cofixpoint_message) l
let definition_message id =
- Flags.if_verbose msg_info (pr_id id ++ str " is defined")
+ Flags.if_verbose Feedback.msg_info (pr_id id ++ str " is defined")
let assumption_message id =
(* Changing "assumed" to "declared", "assuming" referring more to
the type of the object than to the name of the object (see
discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *)
- Flags.if_verbose msg_info (pr_id id ++ str " is declared")
+ Flags.if_verbose Feedback.msg_info (pr_id id ++ str " is declared")
(** Global universe names, in a different summary *)
@@ -440,8 +440,9 @@ let cache_universes (p, l) =
let glob = Universes.global_universe_names () in
let glob', ctx =
List.fold_left (fun ((idl,lid),ctx) (id, lev) ->
- ((Idmap.add id lev idl, Univ.LMap.add lev id lid),
- Univ.ContextSet.add_universe lev ctx))
+ ((Idmap.add id (p, lev) idl,
+ Univ.LMap.add lev id lid),
+ Univ.ContextSet.add_universe lev ctx))
(glob, Univ.ContextSet.empty) l
in
Global.push_context_set p ctx;
@@ -457,6 +458,12 @@ let input_universes : universe_decl -> Libobject.obj =
classify_function = (fun a -> Keep a) }
let do_universe poly l =
+ let in_section = Lib.sections_are_opened () in
+ let () =
+ if poly && not in_section then
+ user_err_loc (Loc.ghost, "Constraint",
+ str"Cannot declare polymorphic universes outside sections")
+ in
let l =
List.map (fun (l, id) ->
let lev = Universes.new_univ_level (Global.current_dirpath ()) in
@@ -485,14 +492,30 @@ let input_constraints : constraint_decl -> Libobject.obj =
let do_constraint poly l =
let u_of_id =
let names, _ = Universes.global_universe_names () in
- fun (loc, id) ->
- try Idmap.find id names
- with Not_found ->
- user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id)
+ fun (loc, id) ->
+ try Idmap.find id names
+ with Not_found ->
+ user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id)
+ in
+ let in_section = Lib.sections_are_opened () in
+ let () =
+ if poly && not in_section then
+ user_err_loc (Loc.ghost, "Constraint",
+ str"Cannot declare polymorphic constraints outside sections")
+ in
+ let check_poly loc p loc' p' =
+ if poly then ()
+ else if p || p' then
+ let loc = if p then loc else loc' in
+ user_err_loc (loc, "Constraint",
+ str "Cannot declare a global constraint on " ++
+ str "a polymorphic universe, use "
+ ++ str "Polymorphic Constraint instead")
in
let constraints = List.fold_left (fun acc (l, d, r) ->
- let lu = u_of_id l and ru = u_of_id r in
- Univ.Constraint.add (lu, d, ru) acc)
+ let p, lu = u_of_id l and p', ru = u_of_id r in
+ check_poly (fst l) p (fst r) p';
+ Univ.Constraint.add (lu, d, ru) acc)
Univ.Constraint.empty l
in
Lib.add_anonymous_leaf (input_constraints (poly, constraints))
diff --git a/library/declaremods.ml b/library/declaremods.ml
index f3f734aa0..dcd63c769 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -897,7 +897,13 @@ let start_library dir =
Lib.start_compilation dir mp;
Lib.add_frozen_state ()
+let end_library_hook = ref ignore
+let append_end_library_hook f =
+ let old_f = !end_library_hook in
+ end_library_hook := fun () -> old_f(); f ()
+
let end_library ?except dir =
+ !end_library_hook();
let oname = Lib.end_compilation_checks dir in
let mp,cenv,ast = Global.export ?except dir in
let prefix, lib_stack = Lib.end_compilation oname in
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 2b440c087..3917fe8d6 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -90,6 +90,9 @@ val end_library :
?except:Future.UUIDSet.t -> library_name ->
Safe_typing.compiled_library * library_objects * Safe_typing.native_library
+(** append a function to be executed at end_library *)
+val append_end_library_hook : (unit -> unit) -> unit
+
(** [really_import_module mp] opens the module [mp] (in a Caml sense).
It modifies Nametab and performs the [open_object] function for
every object of the module. Raises [Not_found] when [mp] is unknown
diff --git a/library/goptions.ml b/library/goptions.ml
index 5f6512e11..4aa3a2a21 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -108,7 +108,8 @@ module MakeTable =
(fun c -> t := MySet.remove c !t))
let print_table table_name printer table =
- pp (str table_name ++
+ Feedback.msg_notice
+ (str table_name ++
(hov 0
(if MySet.is_empty table then str " None" ++ fnl ()
else MySet.fold
@@ -122,7 +123,7 @@ module MakeTable =
method mem x =
let y = A.encode x in
let answer = MySet.mem y !t in
- msg_info (A.member_message y answer)
+ Feedback.msg_info (A.member_message y answer)
method print = print_table A.title A.printer !t
end
@@ -271,7 +272,7 @@ let declare_option cast uncast
in
let warn () =
if depr then
- msg_warning (str "Option " ++ str (nickname key) ++ str " is deprecated")
+ Feedback.msg_warning (str "Option " ++ str (nickname key) ++ str " is deprecated")
in
let cread () = cast (read ()) in
let cwrite v = warn (); write (uncast v) in
@@ -346,12 +347,12 @@ let set_int_option_value_gen locality =
set_option_value locality check_int_value
let set_bool_option_value_gen locality key v =
try set_option_value locality check_bool_value key v
- with UserError (_,s) -> msg_warning s
+ with UserError (_,s) -> Feedback.msg_warning s
let set_string_option_value_gen locality =
set_option_value locality check_string_value
let unset_option_value_gen locality key =
try set_option_value locality check_unset_value key ()
- with UserError (_,s) -> msg_warning s
+ with UserError (_,s) -> Feedback.msg_warning s
let set_int_option_value = set_int_option_value_gen None
let set_bool_option_value = set_bool_option_value_gen None
@@ -375,9 +376,9 @@ let print_option_value key =
let s = read () in
match s with
| BoolValue b ->
- msg_info (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off"))
+ Feedback.msg_info (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off"))
| _ ->
- msg_info (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s))
+ Feedback.msg_info (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s))
let get_tables () =
let tables = !value_tab in
diff --git a/library/libobject.ml b/library/libobject.ml
index c566840e4..b12d2038a 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -133,7 +133,7 @@ let apply_dyn_fun deflt f lobj =
Failure "local to_apply_dyn_fun" ->
if not (!relax_flag || Hashtbl.mem missing_tab tag) then
begin
- Pp.msg_warning
+ Feedback.msg_warning
(Pp.str ("Cannot find library functions for an object with tag "
^ tag ^ " (a plugin may be missing)"));
Hashtbl.add missing_tab tag ()
diff --git a/library/library.ml b/library/library.ml
index 34dbdfeba..bc7723f48 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -35,7 +35,7 @@ module Delayed :
sig
type 'a delayed
-val in_delayed : string -> in_channel -> 'a delayed
+val in_delayed : string -> in_channel -> 'a delayed * Digest.t
val fetch_delayed : 'a delayed -> 'a
end =
@@ -50,7 +50,7 @@ type 'a delayed = {
let in_delayed f ch =
let pos = pos_in ch in
let _, digest = System.skip_in_segment f ch in
- { del_file = f; del_digest = digest; del_off = pos; }
+ ({ del_file = f; del_digest = digest; del_off = pos; }, digest)
(** Fetching a table of opaque terms at position [pos] in file [f],
expecting to find first a copy of [digest]. *)
@@ -287,7 +287,7 @@ let locate_absolute_library dir =
| [] -> raise LibNotFound
| [file] -> file
| [vo;vi] when Unix.((stat vo).st_mtime < (stat vi).st_mtime) ->
- msg_warning (str"Loading " ++ str vi ++ str " instead of " ++
+ Feedback.msg_warning (str"Loading " ++ str vi ++ str " instead of " ++
str vo ++ str " because it is more recent");
vi
| [vo;vi] -> vo
@@ -311,7 +311,7 @@ let locate_qualified_library ?root ?(warn = true) qid =
| [lpath, file] -> lpath, file
| [lpath_vo, vo; lpath_vi, vi]
when Unix.((stat vo).st_mtime < (stat vi).st_mtime) ->
- msg_warning (str"Loading " ++ str vi ++ str " instead of " ++
+ Feedback.msg_warning (str"Loading " ++ str vi ++ str " instead of " ++
str vo ++ str " because it is more recent");
lpath_vi, vi
| [lpath_vo, vo; _ ] -> lpath_vo, vo
@@ -370,7 +370,7 @@ let access_table what tables dp i =
| Fetched t -> t
| ToFetch f ->
let dir_path = Names.DirPath.to_string dp in
- Flags.if_verbose msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path);
+ Flags.if_verbose Feedback.msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path);
let t =
try fetch_delayed f
with Faulty f ->
@@ -427,28 +427,28 @@ let mk_summary m = {
let intern_from_file f =
let ch = raw_intern_library f in
let (lsd : seg_sum), _, digest_lsd = System.marshal_in_segment f ch in
- let (lmd : seg_lib delayed) = in_delayed f ch in
+ 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
+ let ((del_opaque : seg_proofs delayed),_) = in_delayed f ch in
close_in ch;
register_library_filename lsd.md_name f;
add_opaque_table lsd.md_name (ToFetch del_opaque);
let open Safe_typing in
match univs with
- | None -> mk_library lsd lmd (Dvo_or_vi digest_lsd) Univ.ContextSet.empty
+ | 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);
- mk_library lsd lmd (Dvivo (digest_lsd,digest_u)) uall
+ mk_library lsd lmd (Dvivo (digest_lmd,digest_u)) uall
| Some (utab,_,false) ->
add_univ_table lsd.md_name (Fetched utab);
- mk_library lsd lmd (Dvo_or_vi digest_lsd) Univ.ContextSet.empty
+ 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 =
- Pp.feedback(Feedback.FileDependency (from, DirPath.to_string dir));
+ Feedback.feedback(Feedback.FileDependency (from, DirPath.to_string dir));
(* Look if in the current logical environment *)
try (find_library dir).libsum_digests, (needed, contents)
with Not_found ->
@@ -463,7 +463,7 @@ let rec intern_library (needed, contents) (dir, f) from =
(str "The file " ++ str f ++ str " contains library" ++ spc () ++
pr_dirpath m.library_name ++ spc () ++ str "and not library" ++
spc() ++ pr_dirpath dir);
- Pp.feedback(Feedback.FileLoaded(DirPath.to_string dir, f));
+ Feedback.feedback (Feedback.FileLoaded(DirPath.to_string dir, f));
m.library_digests, intern_library_deps (needed, contents) dir m (Some f)
and intern_library_deps libs dir m from =
@@ -753,7 +753,7 @@ let save_library_to ?todo dir f otab =
error "Could not compile the library to native code."
with reraise ->
let reraise = Errors.push reraise in
- let () = msg_warning (str "Removed file " ++ str f') in
+ let () = Feedback.msg_warning (str "Removed file " ++ str f') in
let () = close_out ch in
let () = Sys.remove f' in
iraise reraise
diff --git a/library/loadpath.ml b/library/loadpath.ml
index f8169576d..33c0f41e1 100644
--- a/library/loadpath.ml
+++ b/library/loadpath.ml
@@ -72,7 +72,7 @@ let add_load_path phys_path coq_path ~implicit =
let () =
(* Do not warn when overriding the default "-I ." path *)
if not (DirPath.equal old_path Nameops.default_root_prefix) then
- msg_warning
+ Feedback.msg_warning
(str phys_path ++ strbrk " was previously bound to " ++
pr_dirpath old_path ++ strbrk "; it is remapped to " ++
pr_dirpath coq_path) in
diff --git a/library/nametab.ml b/library/nametab.ml
index bbae98fc0..db902d625 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -119,7 +119,7 @@ struct
| Absolute (n,_) ->
(* This is an absolute name, we must keep it
otherwise it may become unaccessible forever *)
- msg_warning (str ("Trying to mask the absolute name \""
+ Feedback.msg_warning (str ("Trying to mask the absolute name \""
^ U.to_string n ^ "\"!"));
tree.path
| Nothing
@@ -155,7 +155,7 @@ let rec push_exactly uname o level tree = function
| Absolute (n,_) ->
(* This is an absolute name, we must keep it
otherwise it may become unaccessible forever *)
- msg_warning (str ("Trying to mask the absolute name \""
+ Feedback.msg_warning (str ("Trying to mask the absolute name \""
^ U.to_string n ^ "\"!"));
tree.path
| Nothing
@@ -525,7 +525,7 @@ let shortest_qualid_of_tactic kn =
let pr_global_env env ref =
try pr_qualid (shortest_qualid_of_global env ref)
with Not_found as e ->
- if !Flags.debug then Pp.msg_debug (Pp.str "pr_global_env not found"); raise e
+ if !Flags.debug then Feedback.msg_debug (Pp.str "pr_global_env not found"); raise e
let global_inductive r =
match global r with
diff --git a/library/universes.ml b/library/universes.ml
index c4eb2afcb..75cbd5604 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -13,10 +13,11 @@ open Term
open Environ
open Univ
open Globnames
+open Decl_kinds
(** Global universe names *)
type universe_names =
- Univ.universe_level Idmap.t * Id.t Univ.LMap.t
+ (polymorphic * Univ.universe_level) Idmap.t * Id.t Univ.LMap.t
let global_universes =
Summary.ref ~name:"Global universe names"
diff --git a/library/universes.mli b/library/universes.mli
index 53cf5f384..a5740ec49 100644
--- a/library/universes.mli
+++ b/library/universes.mli
@@ -19,7 +19,7 @@ val is_set_minimization : unit -> bool
(** Global universe name <-> level mapping *)
type universe_names =
- Univ.universe_level Idmap.t * Id.t Univ.LMap.t
+ (Decl_kinds.polymorphic * Univ.universe_level) Idmap.t * Id.t Univ.LMap.t
val global_universe_names : unit -> universe_names
val set_global_universe_names : universe_names -> unit
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 11:19:37 +0000