From c56ab637cb3052f48b07b9a6b0e0060bd163ae7a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Wed, 24 Jan 2024 15:44:37 +0100
Subject: [PATCH] Don't commit symlinks in the repository (test-suite
 library_attributes)

Fix #18548

No idea why that bug happens on coqide-server and not -core or -stdlib
but we have historically avoided symlinks in the git repo due to
similar issues.
---
 test-suite/Makefile                                  | 3 ---
 test-suite/output/library_attributes_require.out     | 2 +-
 test-suite/output/library_attributes_require.v       | 2 +-
 test-suite/prerequisite/deprecated_library.v         | 1 +
 test-suite/prerequisite/library_attributes.v         | 1 -
 test-suite/prerequisite/library_attributes_require.v | 1 -
 6 files changed, 3 insertions(+), 7 deletions(-)
 create mode 100644 test-suite/prerequisite/deprecated_library.v
 delete mode 120000 test-suite/prerequisite/library_attributes.v
 delete mode 120000 test-suite/prerequisite/library_attributes_require.v

diff --git a/test-suite/Makefile b/test-suite/Makefile
index f799c97c69928..0a9a5848f0aa3 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -346,9 +346,6 @@ 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.out b/test-suite/output/library_attributes_require.out
index 44e76fd8efd11..a184d91c5d6c9 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 b787ada26ef37..8079f33235875 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/prerequisite/deprecated_library.v b/test-suite/prerequisite/deprecated_library.v
new file mode 100644
index 0000000000000..fe3c18ed7117a
--- /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 17f197f80d2c7..0000000000000
--- 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 f4d6756780c8c..0000000000000
--- a/test-suite/prerequisite/library_attributes_require.v
+++ /dev/null
@@ -1 +0,0 @@
-../output/library_attributes_require.v
\ No newline at end of file