Merge PR #12076: [coqchk] Fix #5030 (coqchk reports names from opaque modules as axioms)

Reviewed-by: herbelin
Reviewed-by: ppedrot

13 files changed, 160 insertions, 51 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 6d307b3c5e..1ff1425dea 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -119,11 +119,12 @@ let check_one_lib admit senv (dir,m) =
     if LibrarySet.mem dir admit then
       (Flags.if_verbose Feedback.msg_notice
          (str "Admitting library: " ++ pr_dirpath dir);
-       Safe_checking.unsafe_import senv md m.library_extra_univs dig)
+       Safe_checking.unsafe_import (fst senv) md m.library_extra_univs dig),
+      (snd senv)
     else
       (Flags.if_verbose Feedback.msg_notice
          (str "Checking library: " ++ pr_dirpath dir);
-       Safe_checking.import senv md m.library_extra_univs dig)
+       Safe_checking.import (fst senv) (snd senv) md m.library_extra_univs dig)
   in
     register_loaded_library m; senv
 
@@ -435,6 +436,6 @@ let recheck_library senv ~norec ~admit ~check =
   Flags.if_verbose Feedback.msg_notice (fnl()++hv 2 (str "Ordered list:" ++ fnl() ++
     prlist
     (fun (dir,_) -> pr_dirpath dir ++ fnl()) needed));
-  let senv = List.fold_left (check_one_lib nochk) senv needed in
+  let senv = List.fold_left (check_one_lib nochk) (senv, Cmap.empty) needed in
   Flags.if_verbose Feedback.msg_notice (str"Modules were successfully checked");
   senv
diff --git a/checker/check.mli b/checker/check.mli
index bb19f09d2e..93274204a3 100644
--- a/checker/check.mli
+++ b/checker/check.mli
@@ -30,4 +30,4 @@ val add_load_path : physical_path * logical_path -> unit
 val recheck_library : safe_environment ->
   norec:object_file list ->
   admit:object_file list ->
-  check:object_file list -> safe_environment
+  check:object_file list -> safe_environment * Cset.t Cmap.t
diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index ee7170df48..0a2da7435c 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -38,8 +38,14 @@ let pr_assumptions ass axs =
   else
     hv 2 (str ass ++ str ":" ++ fnl() ++ prlist_with_sep fnl str axs)
 
-let pr_axioms env =
-  let csts = fold_constants (fun c cb acc -> if not (Declareops.constant_has_body cb) then Constant.to_string c :: acc else acc) env [] in
+let pr_axioms env opac =
+  let add c cb acc =
+    if Declareops.constant_has_body cb then acc else
+      match Cmap.find_opt c opac with
+      | None -> Cset.add c acc
+      | Some s -> Cset.union s acc in
+  let csts = fold_constants add env Cset.empty in
+  let csts = Cset.fold (fun c acc -> Constant.to_string c :: acc) csts [] in
   pr_assumptions "Axioms" csts
 
 let pr_type_in_type env =
@@ -56,20 +62,20 @@ let pr_nonpositive env =
   let inds = fold_inductives (fun c cb acc -> if not cb.mind_typing_flags.check_positive then MutInd.to_string c :: acc else acc) env [] in
   pr_assumptions "Inductives whose positivity is assumed" inds
 
-let print_context env =
+let print_context env opac =
   if !output_context then begin
     Feedback.msg_notice
       (hov 0
       (fnl() ++ str"CONTEXT SUMMARY" ++ fnl() ++
       str"===============" ++ fnl() ++ fnl() ++
       str "* " ++ hov 0 (pr_engagement env ++ fnl()) ++ fnl() ++
-      str "* " ++ hov 0 (pr_axioms env ++ fnl()) ++ fnl() ++
+      str "* " ++ hov 0 (pr_axioms env opac ++ fnl()) ++ fnl() ++
       str "* " ++ hov 0 (pr_type_in_type env ++ fnl()) ++ fnl() ++
       str "* " ++ hov 0 (pr_unguarded env ++ fnl()) ++ fnl() ++
       str "* " ++ hov 0 (pr_nonpositive env ++ fnl()))
       )
   end
 
-let stats env =
-  print_context env;
+let stats env opac =
+  print_context env opac;
   print_memory_stat ()
diff --git a/checker/check_stat.mli b/checker/check_stat.mli
index 8796bcda76..987d50b469 100644
--- a/checker/check_stat.mli
+++ b/checker/check_stat.mli
@@ -10,4 +10,4 @@
 val memory_stat : bool ref
 val output_context : bool ref
 
-val stats : Environ.env -> unit
+val stats : Environ.env -> Names.Cset.t Names.Cmap.t -> unit
diff --git a/checker/checker.ml b/checker/checker.ml
index 0522d43417..086acc482c 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -407,6 +407,6 @@ let run senv =
 
 let start () =
   let senv = init() in
-  let senv = run senv in
-  Check_stat.stats (Safe_typing.env_of_safe_env senv);
+  let senv, opac = run senv in
+  Check_stat.stats (Safe_typing.env_of_safe_env senv) opac;
   exit 0
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 2f795ff8d9..999f44bf1d 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -15,7 +15,25 @@ let indirect_accessor = ref {
 
 let set_indirect_accessor f = indirect_accessor := f
 
-let check_constant_declaration env kn cb =
+let register_opacified_constant env opac kn cb =
+  let rec gather_consts s c =
+    match Constr.kind c with
+    | Constr.Const (c, _) -> Cset.add c s
+    | _ -> Constr.fold gather_consts s c
+  in
+  let wo_body =
+    Cset.fold
+      (fun kn s ->
+        if Declareops.constant_has_body (lookup_constant kn env) then s else
+          match Cmap.find_opt kn opac with
+          | None -> Cset.add kn s
+          | Some s' -> Cset.union s' s)
+      (gather_consts Cset.empty cb)
+      Cset.empty
+  in
+  Cmap.add kn wo_body opac
+
+let check_constant_declaration env opac kn cb opacify =
   Flags.if_verbose Feedback.msg_notice (str "  checking cst:" ++ Constant.print kn);
   let env = CheckFlags.set_local_flags cb.const_typing_flags env in
   let poly, env =
@@ -54,11 +72,13 @@ let check_constant_declaration env kn cb =
        with NotConvertible -> Type_errors.error_actual_type env j ty)
     | None -> ()
   in
-  ()
+  match body with
+  | Some body when opacify -> register_opacified_constant env opac kn body
+  | Some _ | None -> opac
 
-let check_constant_declaration env kn cb =
-  let () = check_constant_declaration env kn cb in
-  Environ.add_constant kn cb env
+let check_constant_declaration env opac kn cb opacify =
+  let opac = check_constant_declaration env opac kn cb opacify in
+  Environ.add_constant kn cb env, opac
 
 (** {6 Checking modules } *)
 
@@ -80,18 +100,32 @@ let mk_mtb mp sign delta =
     mod_delta = delta;
     mod_retroknowledge = ModTypeRK; }
 
-let rec check_module env mp mb =
+let collect_constants_without_body sign mp =
+  let collect_sf s lab = function
+  | SFBconst cb ->
+     let c = Constant.make2 mp lab in
+     if Declareops.constant_has_body cb then s else Cset.add c s
+  | SFBmind _ | SFBmodule _ | SFBmodtype _ -> s in
+  match sign with
+  | MoreFunctor _ -> Cset.empty  (* currently ignored *)
+  | NoFunctor struc ->
+     List.fold_left (fun s (lab,mb) -> collect_sf s lab mb) Cset.empty struc
+
+let rec check_module env opac mp mb =
   Flags.if_verbose Feedback.msg_notice (str "  checking module: " ++ str (ModPath.to_string mp));
   let env = Modops.add_retroknowledge mb.mod_retroknowledge env in
-  let (_:module_signature) =
-    check_signature env mb.mod_type mb.mod_mp mb.mod_delta
+  let sign, opac =
+    check_signature env opac mb.mod_type mb.mod_mp mb.mod_delta Cset.empty
   in
-  let optsign = match mb.mod_expr with
-    |Struct sign -> Some (check_signature env sign mb.mod_mp mb.mod_delta, mb.mod_delta)
-    |Algebraic me -> Some (check_mexpression env me mb.mod_mp mb.mod_delta)
-    |Abstract|FullStruct -> None
+  let optsign, opac = match mb.mod_expr with
+    |Struct sign_struct ->
+      let opacify = collect_constants_without_body sign mb.mod_mp in
+      let sign, opac = check_signature env opac sign_struct mb.mod_mp mb.mod_delta opacify in
+      Some (sign, mb.mod_delta), opac
+    |Algebraic me -> Some (check_mexpression env opac me mb.mod_mp mb.mod_delta), opac
+    |Abstract|FullStruct -> None, opac
   in
-  match optsign with
+  let () = match optsign with
   |None -> ()
   |Some (sign,delta) ->
     let mtb1 = mk_mtb mp sign delta
@@ -100,35 +134,37 @@ let rec check_module env mp mb =
     let cu = Subtyping.check_subtypes env mtb1 mtb2 in
     if not (Environ.check_constraints cu env) then
       CErrors.user_err Pp.(str "Incorrect universe constraints for module subtyping");
+  in
+  opac
 
 and check_module_type env mty =
   Flags.if_verbose Feedback.msg_notice (str "  checking module type: " ++ str (ModPath.to_string mty.mod_mp));
-  let (_:module_signature) =
-    check_signature env mty.mod_type mty.mod_mp mty.mod_delta in
+  let (_:module_signature), _ =
+    check_signature env Cmap.empty mty.mod_type mty.mod_mp mty.mod_delta Cset.empty in
   ()
 
-and check_structure_field env mp lab res = function
+and check_structure_field env opac mp lab res opacify = function
   | SFBconst cb ->
       let c = Constant.make2 mp lab in
-      check_constant_declaration env c cb
+      check_constant_declaration env opac c cb (Cset.mem c opacify)
   | SFBmind mib ->
       let kn = KerName.make mp lab in
       let kn = Mod_subst.mind_of_delta_kn res kn in
-      CheckInductive.check_inductive env kn mib
+      CheckInductive.check_inductive env kn mib, opac
   | SFBmodule msb ->
-      let () = check_module env (MPdot(mp,lab)) msb in
-      Modops.add_module msb env
+      let opac = check_module env opac (MPdot(mp,lab)) msb in
+      Modops.add_module msb env, opac
   | SFBmodtype mty ->
       check_module_type env mty;
-      add_modtype mty env
+      add_modtype mty env, opac
 
-and check_mexpr env mse mp_mse res = match mse with
+and check_mexpr env opac mse mp_mse res = match mse with
   | MEident mp ->
       let mb = lookup_module mp env in
       let mb = Modops.strengthen_and_subst_mb mb mp_mse false in
       mb.mod_type, mb.mod_delta
   | MEapply (f,mp) ->
-      let sign, delta = check_mexpr env f mp_mse res in
+      let sign, delta = check_mexpr env opac f mp_mse res in
       let farg_id, farg_b, fbody_b = Modops.destr_functor sign in
       let mtb = Modops.module_type_of_module (lookup_module mp env) in
       let cu = Subtyping.check_subtypes env mtb farg_b in
@@ -139,22 +175,22 @@ and check_mexpr env mse mp_mse res = match mse with
   | MEwith _ -> CErrors.user_err Pp.(str "Unsupported 'with' constraint in module implementation")
 
 
-and check_mexpression env sign mp_mse res = match sign with
+and check_mexpression env opac sign mp_mse res = match sign with
   | MoreFunctor (arg_id, mtb, body) ->
       check_module_type env mtb;
       let env' = Modops.add_module_type (MPbound arg_id) mtb env in
-      let body, delta = check_mexpression env' body mp_mse res in
+      let body, delta = check_mexpression env' opac body mp_mse res in
       MoreFunctor(arg_id,mtb,body), delta
-  | NoFunctor me -> check_mexpr env me mp_mse res
+  | NoFunctor me -> check_mexpr env opac me mp_mse res
 
-and check_signature env sign mp_mse res = match sign with
+and check_signature env opac sign mp_mse res opacify = match sign with
   | MoreFunctor (arg_id, mtb, body) ->
       check_module_type env mtb;
       let env' = Modops.add_module_type (MPbound arg_id) mtb env in
-      let body = check_signature env' body mp_mse res in
-      MoreFunctor(arg_id,mtb,body)
+      let body, opac = check_signature env' opac body mp_mse res Cset.empty in
+      MoreFunctor(arg_id,mtb,body), opac
   | NoFunctor struc ->
-      let (_:env) = List.fold_left (fun env (lab,mb) ->
-        check_structure_field env mp_mse lab res mb) env struc
+      let (_:env), opac = List.fold_left (fun (env, opac) (lab,mb) ->
+        check_structure_field env opac mp_mse lab res opacify mb) (env, opac) struc
       in
-      NoFunctor struc
+      NoFunctor struc, opac
diff --git a/checker/mod_checking.mli b/checker/mod_checking.mli
index 58eb135b50..194f6c6e16 100644
--- a/checker/mod_checking.mli
+++ b/checker/mod_checking.mli
@@ -10,4 +10,4 @@
 
 val set_indirect_accessor : Opaqueproof.indirect_accessor -> unit
 
-val check_module : Environ.env -> Names.ModPath.t -> Declarations.module_body -> unit
+val check_module : Environ.env -> Names.Cset.t Names.Cmap.t -> Names.ModPath.t -> Declarations.module_body -> Names.Cset.t Names.Cmap.t
diff --git a/checker/safe_checking.ml b/checker/safe_checking.ml
index b5beab532e..55bfa36ce5 100644
--- a/checker/safe_checking.ml
+++ b/checker/safe_checking.ml
@@ -11,14 +11,14 @@
 open Declarations
 open Environ
 
-let import senv clib univs digest =
+let import senv opac clib univs digest =
   let mb = Safe_typing.module_of_library clib in
   let env = Safe_typing.env_of_safe_env senv in
   let env = push_context_set ~strict:true (Safe_typing.univs_of_library clib) env in
   let env = push_context_set ~strict:true univs env in
   let env = Modops.add_retroknowledge mb.mod_retroknowledge env in
-  Mod_checking.check_module env mb.mod_mp mb;
-  let (_,senv) = Safe_typing.import clib univs digest senv in senv
+  let opac = Mod_checking.check_module env opac mb.mod_mp mb in
+  let (_,senv) = Safe_typing.import clib univs digest senv in senv, opac
 
 let unsafe_import senv clib univs digest =
   let (_,senv) = Safe_typing.import clib univs digest senv in senv
diff --git a/checker/safe_checking.mli b/checker/safe_checking.mli
index 21566555d4..b4abc52a74 100644
--- a/checker/safe_checking.mli
+++ b/checker/safe_checking.mli
@@ -12,5 +12,5 @@
 open Safe_typing
 (*i*)
 
-val import : safe_environment -> compiled_library -> Univ.ContextSet.t -> vodigest -> safe_environment
+val import : safe_environment -> Names.Cset.t Names.Cmap.t -> compiled_library -> Univ.ContextSet.t -> vodigest -> safe_environment * Names.Cset.t Names.Cmap.t
 val unsafe_import : safe_environment -> compiled_library -> Univ.ContextSet.t -> vodigest -> safe_environment
diff --git a/doc/changelog/08-tools/12076-fix-5030.rst b/doc/changelog/08-tools/12076-fix-5030.rst
new file mode 100644
index 0000000000..afb59b1cde
--- /dev/null
+++ b/doc/changelog/08-tools/12076-fix-5030.rst
@@ -0,0 +1,4 @@
+- **Fixed:**
+  Fix #5030 (coqchk reports names from opaque modules as axioms)
+  (`#12076 <https://github.com/coq/coq/pull/12076>`_,
+  by Pierre Roux).
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 5dd4f42af3..d4ad438d61 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -115,7 +115,7 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output output-coqtop \
   coqdoc ssr primitive/uint63 primitive/float ltac2
 
 # All subsystems
-SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile tools $(UNIT_TESTS)
+SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk output-coqchk coqwc coq-makefile tools $(UNIT_TESTS)
 
 .csdp.cache: .csdp.cache.test-suite
 	cp $< $@
@@ -192,6 +192,7 @@ summary:
 	  $(call summary_dir, "IDE tests", ide); \
 	  $(call summary_dir, "VI tests", vio); \
 	  $(call summary_dir, "Coqchk tests", coqchk); \
+	  $(call summary_dir, "Output tests with coqchk", output-coqchk); \
 	  $(call summary_dir, "Coqwc tests", coqwc); \
 	  $(call summary_dir, "Coq makefile", coq-makefile); \
 	  $(call summary_dir, "Coqdoc tests", coqdoc); \
@@ -462,6 +463,43 @@ $(addsuffix .log,$(wildcard output-coqtop/*.v)): %.v.log: %.v %.out $(PREREQUISI
 	  fi; \
 	} > "$@"
 
+output-coqchk: $(addsuffix .log,$(wildcard output-coqchk/*.v))
+$(addsuffix .log,$(wildcard output-coqchk/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG)
+	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
+	$(HIDE){ \
+	  opts="$(if $(findstring modules/,$<),-R modules Mods)"; \
+	  echo $(call log_intro,$<); \
+	  $(coqc) "$<" $(call get_coq_prog_args,"$<") $$opts 2>&1; R=$$?; times; \
+	  if [ $$R = 0 ]; then \
+	    echo $(log_success); \
+	    echo "    $<...Ok"; \
+	  else \
+	    echo $(log_failure); \
+	    echo "    $<...Error! (should be accepted)"; \
+	    $(FAIL); \
+	  fi; \
+	} > "$@"
+	@if ! grep -q -F "Error!" $@; then echo "CHECK     $<"; fi
+	$(HIDE)if ! grep -q -F "Error!" $@; then { \
+	  echo $(call log_intro,$<); \
+	  output=$*.out.real; \
+	  export LC_CTYPE=C; \
+	  export LANG=C; \
+	  $(coqchk) -o -silent $(call get_set_impredicativity,$<) $(if $(findstring modules/,$<),-R modules Mods -norec Mods.$(shell basename $< .v),-Q $(shell dirname $<) "" -norec $(shell basename $< .v)) 2>&1 \
+	    | sed 's/File "[^"]*"/File "stdin"/' \
+	    > $$output; \
+	  diff -a -u --strip-trailing-cr $*.out $$output 2>&1; R=$$?; times; \
+	  if [ $$R = 0 ]; then \
+	    echo $(log_success); \
+	    echo "    $<...Ok"; \
+	    rm $$output; \
+	  else \
+	    echo $(log_failure); \
+	    echo "    $<...Error! (unexpected output)"; \
+	    $(FAIL); \
+	  fi; \
+	} > "$(shell dirname $<)/$(shell basename $< .v).chk.log"; fi
+
 .PHONY: approve-output
 approve-output: output output-coqtop
 	$(HIDE)for f in output/*.out.real; do \
diff --git a/test-suite/output-coqchk/bug_5030.out b/test-suite/output-coqchk/bug_5030.out
new file mode 100644
index 0000000000..bef45bf2f6
--- /dev/null
+++ b/test-suite/output-coqchk/bug_5030.out
@@ -0,0 +1,14 @@
+
+CONTEXT SUMMARY
+===============
+
+* Theory: Set is predicative
+  
+* Axioms: <none>
+  
+* Constants/Inductives relying on type-in-type: <none>
+  
+* Constants/Inductives relying on unsafe (co)fixpoints: <none>
+  
+* Inductives whose positivity is assumed: <none>
+  
diff --git a/test-suite/output-coqchk/bug_5030.v b/test-suite/output-coqchk/bug_5030.v
new file mode 100644
index 0000000000..543784e3c9
--- /dev/null
+++ b/test-suite/output-coqchk/bug_5030.v
@@ -0,0 +1,10 @@
+Module Type testt.
+Parameter proof : True.
+End testt.
+
+Module Export test : testt.
+Definition proof := I.
+End test.
+
+Lemma true : True.
+Proof. apply proof. Qed.