diff --git a/test-suite/Makefile b/test-suite/Makefile index f799c97c6992..0a4dbbf84559 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -346,8 +346,7 @@ 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 +prerequisite/requires_deprecated_library.v.log: prerequisite/deprecated_library.v.log $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" diff --git a/test-suite/output/library_attributes_require.out b/test-suite/output/library_attributes_require.out index 44e76fd8efd1..a184d91c5d6c 100644 --- a/test-suite/output/library_attributes_require.out +++ b/test-suite/output/library_attributes_require.out @@ -1,4 +1,4 @@ File "./output/library_attributes_require.v", line 1, characters 0-37: -Warning: Library File TestSuite.library_attributes is deprecated since XX YY. +Warning: Library File TestSuite.deprecated_library 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.v b/test-suite/output/library_attributes_require.v index b787ada26ef3..8079f3323587 100644 --- a/test-suite/output/library_attributes_require.v +++ b/test-suite/output/library_attributes_require.v @@ -1 +1 @@ -Require TestSuite.library_attributes. +Require TestSuite.deprecated_library. diff --git a/test-suite/output/library_attributes_require_transitive.out b/test-suite/output/library_attributes_require_transitive.out index 9434e9c8e141..a9644e1630b4 100644 --- a/test-suite/output/library_attributes_require_transitive.out +++ b/test-suite/output/library_attributes_require_transitive.out @@ -1,8 +1,8 @@ File "./output/library_attributes_require_transitive.v", line 5, characters 0-37: -Warning: Library File TestSuite.library_attributes is deprecated since XX YY. +Warning: Library File TestSuite.deprecated_library is deprecated since XX YY. This library is useless. [deprecated-library-file-since-XX-YY,deprecated-since-XX-YY,deprecated-library-file,deprecated,default] -File "./output/library_attributes_require_transitive.v", line 11, characters 0-45: -Warning: Library File (transitively required) TestSuite.library_attributes is +File "./output/library_attributes_require_transitive.v", line 11, characters 0-46: +Warning: Library File (transitively required) TestSuite.deprecated_library is deprecated since XX YY. This library is useless. [deprecated-transitive-library-file-since-XX-YY,deprecated-since-XX-YY,deprecated-transitive-library-file,deprecated] diff --git a/test-suite/output/library_attributes_require_transitive.v b/test-suite/output/library_attributes_require_transitive.v index c5e30750241c..c3ed1037b682 100644 --- a/test-suite/output/library_attributes_require_transitive.v +++ b/test-suite/output/library_attributes_require_transitive.v @@ -1,11 +1,11 @@ (* check that file deprecations are only printed on direct requirement *) -Require TestSuite.library_attributes_require. +Require TestSuite.requires_deprecated_library. (* but still printed on direct requirement even if the Require doesn't actually do anything (because file is already loaded) *) -Require TestSuite.library_attributes. +Require TestSuite.deprecated_library. (* We have the second warning "deprecated-transitive-library-file" that always triggers (even on transitive requires) *) Reset Initial. Set Warnings "deprecated-transitive-library-file". -Require TestSuite.library_attributes_require. +Require TestSuite.requires_deprecated_library. diff --git a/test-suite/prerequisite/deprecated_library.v b/test-suite/prerequisite/deprecated_library.v new file mode 100644 index 000000000000..fe3c18ed7117 --- /dev/null +++ b/test-suite/prerequisite/deprecated_library.v @@ -0,0 +1 @@ +Attributes deprecated(note="This library is useless.", since="XX YY"). diff --git a/test-suite/prerequisite/library_attributes.v b/test-suite/prerequisite/library_attributes.v deleted file mode 120000 index 17f197f80d2c..000000000000 --- a/test-suite/prerequisite/library_attributes.v +++ /dev/null @@ -1 +0,0 @@ -../output/library_attributes.v \ No newline at end of file diff --git a/test-suite/prerequisite/library_attributes_require.v b/test-suite/prerequisite/library_attributes_require.v deleted file mode 120000 index f4d6756780c8..000000000000 --- a/test-suite/prerequisite/library_attributes_require.v +++ /dev/null @@ -1 +0,0 @@ -../output/library_attributes_require.v \ No newline at end of file diff --git a/test-suite/prerequisite/requires_deprecated_library.v b/test-suite/prerequisite/requires_deprecated_library.v new file mode 100644 index 000000000000..8079f3323587 --- /dev/null +++ b/test-suite/prerequisite/requires_deprecated_library.v @@ -0,0 +1 @@ +Require TestSuite.deprecated_library.