From 082261bacf6e31e44cad4d63345de7f9408f38c2 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 23 Nov 2023 13:54:36 +0100 Subject: [PATCH] Fix #18193 don't trigger file deprecation transitively Following https://github.com/coq/coq/pull/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 3cbcc49bb6e59a899a781ace268714576534cced) --- test-suite/Makefile | 3 +++ .../library_attributes_require_transitive.out | 4 ++++ .../library_attributes_require_transitive.v | 5 +++++ .../prerequisite/library_attributes_require.v | 1 + vernac/library.ml | 18 ++++++++++++------ 5 files changed, 25 insertions(+), 6 deletions(-) create mode 100644 test-suite/output/library_attributes_require_transitive.out create mode 100644 test-suite/output/library_attributes_require_transitive.v create mode 120000 test-suite/prerequisite/library_attributes_require.v diff --git a/test-suite/Makefile b/test-suite/Makefile index 28748802ae912..3abe4b1cb70d4 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -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){ \ diff --git a/test-suite/output/library_attributes_require_transitive.out b/test-suite/output/library_attributes_require_transitive.out new file mode 100644 index 0000000000000..06a86f4267ba5 --- /dev/null +++ b/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] diff --git a/test-suite/output/library_attributes_require_transitive.v b/test-suite/output/library_attributes_require_transitive.v new file mode 100644 index 0000000000000..cc4252ea9c4c4 --- /dev/null +++ b/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. diff --git a/test-suite/prerequisite/library_attributes_require.v b/test-suite/prerequisite/library_attributes_require.v new file mode 120000 index 0000000000000..f4d6756780c8c --- /dev/null +++ b/test-suite/prerequisite/library_attributes_require.v @@ -0,0 +1 @@ +../output/library_attributes_require.v \ No newline at end of file diff --git a/vernac/library.ml b/vernac/library.ml index 5ddd8345de44b..2ad12c9b2efc3 100644 --- a/vernac/library.ml +++ b/vernac/library.ml @@ -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 *) @@ -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 = @@ -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 = @@ -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 @@ -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 =