Merge PR #22292: Cleanups around kernel side of Require

Reviewed-by: ppedrot
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>

Author: coqbot-app[bot]

kernel/safe_typing.ml

@@ -1694,13 +1694,23 @@ let export ~output_native_objects senv dir =
   let vmlib = Vmlibrary.export @@ Environ.vm_library senv.env in
   mp, lib, vmlib, (ast, symbols)
 
-let import lib vmtab vodigest senv =
-  let senv = check_flags_for_library lib senv in
-  let required = check_required senv.required lib.comp_deps in
-  if DirPath.equal (ModPath.dp senv.modpath) lib.comp_name then
+let import_gen ~replaying lib vmtab vodigest senv =
+  let () = if DirPath.equal (ModPath.dp senv.modpath) lib.comp_name then
     CErrors.user_err
       Pp.(strbrk "Cannot load a library with the same name as the current one ("
-          ++ DirPath.print lib.comp_name ++ str").");
+          ++ DirPath.print lib.comp_name ++ str").")
+  in
+  let senv = check_flags_for_library lib senv in
+  let required = check_required senv.required lib.comp_deps in
+  let required =
+    if DirPath.Map.mem lib.comp_name required then
+      if replaying then
+        (* only happens in close_section, could probably be done in a saner way *)
+        required
+      else
+        CErrors.anomaly Pp.(str "Double kernel import of " ++ DirPath.print lib.comp_name ++ str ".")
+    else DirPath.Map.add lib.comp_name { req_root = true; req_digest = vodigest } required
+  in
   let mp = MPfile lib.comp_name in
   let mb = lib.comp_mod in
   let univs = lib.comp_univs in
@@ -1724,12 +1734,6 @@ let import lib vmtab vodigest senv =
         {custom with rev_reimport = (lib,vmtab,vodigest) :: custom.rev_reimport}))
       senv.sections
   in
-  let required =
-    if DirPath.Map.mem lib.comp_name required then
-      (* should probably be an error, we are requiring the same library twice *)
-      required
-    else DirPath.Map.add lib.comp_name { req_root = true; req_digest = vodigest } required
-  in
   mp,
   { senv with
     env;
@@ -1741,6 +1745,9 @@ let import lib vmtab vodigest senv =
     sections;
   }
 
+let import lib vmtab vodigest senv =
+  import_gen ~replaying:false lib vmtab vodigest senv
+
 (** {6 Interactive sections} *)
 
 let open_section senv =
@@ -1770,8 +1777,10 @@ let close_section senv =
         rev_reimport; rev_revstruct = revstruct; rev_paramresolver = paramresolver } = revert in
   let env = if Environ.rewrite_rules_allowed env0 then Environ.allow_rewrite_rules env else env in
   let senv = { senv with env; revstruct; sections; univ; qualities; elims; objlabels; paramresolver } in
-  (* Second phase: replay Requires *)
-  let senv = List.fold_left (fun senv (lib,vmtab,vodigest) -> snd (import lib vmtab vodigest senv))
+  (* Second phase: replay Requires
+     should probably be done in a saner way that doesn't need the [replaying] flag *)
+  let senv = List.fold_left (fun senv (lib,vmtab,vodigest) ->
+      snd (import_gen ~replaying:true lib vmtab vodigest senv))
       senv (List.rev rev_reimport)
   in
   (* Third phase: replay the discharged section contents *)

test-suite/coq-makefile/global-unchecked-univs/_CoqProject

@@ -0,0 +1,6 @@
+-R . Test22292
+
+file1.v
+file2.v
+file3.v
+file3bad.v

test-suite/coq-makefile/global-unchecked-univs/file1.v

@@ -0,0 +1 @@
+Global Unset Universe Checking.

test-suite/coq-makefile/global-unchecked-univs/file2.v

@@ -0,0 +1,2 @@
+Require file1.
+Universe u. Constraint u < u.

test-suite/coq-makefile/global-unchecked-univs/file3.v

@@ -0,0 +1 @@
+Require file2.

test-suite/coq-makefile/global-unchecked-univs/file3bad.v

@@ -0,0 +1,3 @@
+Require file1.
+Set Universe Checking.
+Fail Require file2.

test-suite/coq-makefile/global-unchecked-univs/run.sh

@@ -0,0 +1,13 @@
+#!/usr/bin/env bash
+
+. ../template/path-init.sh
+
+rm -rf _test
+mkdir _test
+find . -maxdepth 1 -not -name . -not -name _test -exec cp -r '{}' -t _test ';'
+cd _test
+
+rocq makefile -f _CoqProject -o Makefile
+
+export COQEXTRAFLAGS='-native-compiler no' # loading flags not supported by separate native compiler
+make

vernac/declaremods.ml

@@ -1641,22 +1641,9 @@ let declare_include me_asts =
     user_err Pp.(str "Include is not allowed inside sections.");
   RawIncludeOps.Interp.declare_include me_asts
 
-let register_library dir cenv (objs:library_objects) digest vmtab =
+let register_library dir (objs:library_objects) =
   let mp = MPfile dir in
   let sp = path_of_file dir in
-  let () =
-    try
-      (* If the library was loaded inside a module or section, the
-         end_segment will replay the library object for non-kernel
-         effects but the kernel did not forget the library. *)
-      ignore(Global.lookup_module mp);
-    with Not_found ->
-      begin
-      let mp' = Global.import cenv vmtab digest in
-      if not (ModPath.equal mp mp') then
-        anomaly (Pp.str "Unexpected disk module name.")
-      end
-  in
   let sobjs,keepobjs,escapeobjs = objs in
   InterpVisitor.load_module 1 sp mp ([],Objs sobjs);
   InterpVisitor.load_escape 1 sp mp escapeobjs;

vernac/declaremods.mli

@@ -131,11 +131,7 @@ val start_modtype :
 
 val end_modtype : unit -> ModPath.t
 
-val register_library :
-  library_name ->
-  Safe_typing.compiled_library -> library_objects -> Safe_typing.vodigest ->
-  Vmlibrary.on_disk ->
-  unit
+val register_library : library_name -> library_objects -> unit
 
 (** [import_module export mp] imports the module [mp].
    It modifies Nametab and performs the [open_object] function for

vernac/library.ml

@@ -370,11 +370,7 @@ let register_library m =
   let l = m.library_data in
   Declaremods.Interp.register_library
     m.library_name
-    l.md_compiled
-    l.md_objects
-    m.library_digests
-    m.library_vm
-  ;
+    l.md_objects;
   register_native_library m.library_name
 
 let register_library_syntax (root, m) =
@@ -389,7 +385,7 @@ let register_library_syntax (root, m) =
      the module or module type
    - not called from a library (i.e. a module identified with a file) *)
 let load_require _ needed =
-  List.iter register_library needed
+  register_library needed
 
   (* [needed] is the ordered list of libraries not already loaded *)
 let cache_require o =
@@ -399,7 +395,7 @@ let discharge_require o = Some o
 
 (* open_function is never called from here because an Anticipate object *)
 
-type require_obj = library_t list
+type require_obj = library_t
 
 let in_require : require_obj -> obj =
   declare_object
@@ -411,7 +407,7 @@ let in_require : require_obj -> obj =
      classify_function = (fun o -> Anticipate) }
 
 let load_require_syntax _ needed =
-  List.iter register_library_syntax needed
+  register_library_syntax needed
 
 let cache_require_syntax o =
   load_require_syntax 1 o
@@ -420,8 +416,7 @@ let discharge_require_syntax o = Some o
 
 (* open_function is never called from here because an Anticipate object *)
 
-type require_obj_syntax = (bool * library_t) list
-
+type require_obj_syntax = bool * library_t
 let in_require_syntax : require_obj_syntax -> obj =
   declare_object
     {(default_object "REQUIRE-SYNTAX") with
@@ -440,14 +435,29 @@ let warn_require_in_module =
     (fun () -> strbrk "Use of “Require” inside a module is fragile." ++ spc() ++
                strbrk "It is not recommended to use this functionality in finished proof scripts.")
 
+let kernel_load_require m =
+  let l = m.library_data in
+  let mp' = Global.import l.md_compiled m.library_vm m.library_digests in
+  if not (ModPath.equal (MPfile m.library_name) mp') then
+    anomaly (Pp.str "Unexpected disk module name.")
+
 let require_library_from_dirpath needed =
   if Lib.is_module_or_modtype () then warn_require_in_module ();
-  Lib.add_leaf (in_require needed)
+  (* Note that putting the list in the libobject would need to split the iter
+     (ie do [List.iter kernel_load_require needed; List.iter add_leaf needed])
+     which changes behaviour because libobjects can change kernel flags
+     (eg Global Unset Universe Checking).
+     TBH I'm not sure how much we care about preserving such behaviours
+     if it ever becomes inconvenient though. *)
+  List.iter (fun m ->
+      kernel_load_require m;
+      Lib.add_leaf (in_require m))
+    needed
 
 let require_library_syntax_from_dirpath ~intern modrefl =
   let needed, contents = List.fold_left (rec_intern_library ~intern) ([], DirPath.Map.empty) modrefl in
   let needed = List.rev_map (fun (root, dir) -> root, DirPath.Map.find dir contents) needed in
-  Lib.add_leaf (in_require_syntax needed);
+  List.iter (fun m -> Lib.add_leaf (in_require_syntax m)) needed;
   List.map snd needed
 
 (************************************************************************)