Skip to content

Commit

Permalink
Fix coq#18193 don't trigger file deprecation transitively
Browse files Browse the repository at this point in the history
Following coq#18193 we had the following behavior:

in A.v
  Attributes deprecated(note="A deprecated").

in B.v
  Require Import A.
  (* warning as expected *)

in C.v
  Require Import B.
  (* also a warning *)

Whereas we don't want the warning in the last case. This triggers the
warnings only when directly requiring a file.

(cherry picked from commit 3cbcc49)
  • Loading branch information
proux01 authored and SkySkimmer committed Dec 13, 2023
1 parent 237ec57 commit 082261b
Show file tree
Hide file tree
Showing 5 changed files with 25 additions and 6 deletions.
3 changes: 3 additions & 0 deletions test-suite/Makefile
Expand Up @@ -308,6 +308,9 @@ unit-tests/%.ml.log: unit-tests/%.ml unit-tests/src/$(UNIT_LINK)
# Other generic tests
#######################################################################

# There is a dependency between those two files
prerequisite/library_attributes_require.v.log: prerequisite/library_attributes.v.log

$(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v
@echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
$(HIDE){ \
Expand Down
4 changes: 4 additions & 0 deletions test-suite/output/library_attributes_require_transitive.out
@@ -0,0 +1,4 @@
File "./output/library_attributes_require_transitive.v", line 5, characters 0-37:
Warning: Library File TestSuite.library_attributes is deprecated since XX YY.
This library is useless.
[deprecated-library-file-since-XX-YY,deprecated-since-XX-YY,deprecated-library-file,deprecated,default]
5 changes: 5 additions & 0 deletions test-suite/output/library_attributes_require_transitive.v
@@ -0,0 +1,5 @@
(* check that file deprecations are only printed on direct requirement *)
Require TestSuite.library_attributes_require.
(* but still printed on direct requirement even if the Require doesn't actually
do anything (because file is already loaded) *)
Require TestSuite.library_attributes.
1 change: 1 addition & 0 deletions test-suite/prerequisite/library_attributes_require.v
18 changes: 12 additions & 6 deletions vernac/library.ml
Expand Up @@ -102,11 +102,13 @@ type library_t = {
library_deps : (compilation_unit_name * Safe_typing.vodigest) array;
library_digests : Safe_typing.vodigest;
library_extra_univs : Univ.ContextSet.t;
library_info : Library_info.t list;
}

type library_summary = {
libsum_name : compilation_unit_name;
libsum_digests : Safe_typing.vodigest;
libsum_info : Library_info.t list;
}

(* This is a map from names to loaded libraries *)
Expand Down Expand Up @@ -238,11 +240,13 @@ let mk_library sd md digests univs =
library_deps = sd.md_deps;
library_digests = digests;
library_extra_univs = univs;
library_info = sd.md_info;
}

let mk_summary m = {
libsum_name = m.library_name;
libsum_digests = m.library_digests;
libsum_info = m.library_info;
}

let mk_intern_library sum lib digest_lib univs digest_univs proofs =
Expand Down Expand Up @@ -281,19 +285,18 @@ let intern_from_file lib_resolver dir =
DirPath.print lsd.md_name ++ spc () ++ str "and not library" ++
spc() ++ DirPath.print dir ++ str ".");
Feedback.feedback (Feedback.FileLoaded(DirPath.to_string dir, f));
List.iter (fun info -> Library_info.warn_library_info (lsd.md_name,info)) lsd.md_info;
lsd, lmd, digest_lmd, univs, digest_u, del_opaque

let rec intern_library ~intern (needed, contents as acc) dir =
(* Look if in the current logical environment *)
try (find_library dir).libsum_digests, acc
try find_library dir, acc
with Not_found ->
(* Look if already listed and consequently its dependencies too *)
try (DPmap.find dir contents).library_digests, acc
try mk_summary (DPmap.find dir contents), acc
with Not_found ->
let lsd, lmd, digest_lmd, univs, digest_u, del_opaque = intern dir in
let m = mk_intern_library lsd lmd digest_lmd univs digest_u del_opaque in
m.library_digests, intern_library_deps ~intern acc dir m
mk_summary m, intern_library_deps ~intern acc dir m

and intern_library_deps ~intern libs dir m =
let needed, contents =
Expand All @@ -302,7 +305,8 @@ and intern_library_deps ~intern libs dir m =
(dir :: needed, DPmap.add dir m contents )

and intern_mandatory_library ~intern caller libs (dir,d) =
let digest, libs = intern_library ~intern libs dir in
let m, libs = intern_library ~intern libs dir in
let digest = m.libsum_digests in
let () = if not (Safe_typing.digest_match ~actual:digest ~required:d) then
let from = library_full_filename caller in
user_err
Expand All @@ -315,7 +319,9 @@ and intern_mandatory_library ~intern caller libs (dir,d) =

let rec_intern_library ~lib_resolver libs dir =
let intern dir = intern_from_file lib_resolver dir in
let _, libs = intern_library ~intern libs dir in
let m, libs = intern_library ~intern libs dir in
List.iter (fun info -> Library_info.warn_library_info (m.libsum_name,info))
m.libsum_info;
libs

let native_name_from_filename f =
Expand Down

0 comments on commit 082261b

Please sign in to comment.