coq · coqbot-app · Feb 5, 2024 · Jan 24, 2024
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
diff --git a/test-suite/prerequisite/library_attributes_require.v b/test-suite/prerequisite/library_attributes_require.v
diff --git a/test-suite/prerequisite/requires_deprecated_library.v b/test-suite/prerequisite/requires_deprecated_library.v
@@ -0,0 +1 @@
+Require TestSuite.deprecated_library.