From 17de81c8c006e89088b2173d1aeaae24b4c09cfa Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 18 May 2020 17:34:27 +0200
Subject: [test-suite] Ensure copies of files are writable

This is needed for the case the sources are set to read-only mode, for
example when using Dune >= 2.5 [needed for the global cache support]

Fixes #12264

Co-authored-by: Ignat Insarov <kindaro@gmail.com>
---
 test-suite/.csdp.cache                   | Bin 329899 -> 0 bytes
 test-suite/.csdp.cache.test-suite        | Bin 0 -> 329899 bytes
 test-suite/Makefile                      |   7 ++++++-
 test-suite/coq-makefile/template/init.sh |  22 +++++++++++++++-------
 4 files changed, 21 insertions(+), 8 deletions(-)
 delete mode 100644 test-suite/.csdp.cache
 create mode 100644 test-suite/.csdp.cache.test-suite

diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache
deleted file mode 100644
index 046cb067c5..0000000000
Binary files a/test-suite/.csdp.cache and /dev/null differ
diff --git a/test-suite/.csdp.cache.test-suite b/test-suite/.csdp.cache.test-suite
new file mode 100644
index 0000000000..046cb067c5
Binary files /dev/null and b/test-suite/.csdp.cache.test-suite differ
diff --git a/test-suite/Makefile b/test-suite/Makefile
index bbd31486fe..afc6080627 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -117,7 +117,11 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output output-coqtop \
 # All subsystems
 SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile tools $(UNIT_TESTS)
 
-PREREQUISITELOG = $(addsuffix .log,$(wildcard prerequisite/*.v))
+.csdp.cache: .csdp.cache.test-suite
+	cp $< $@
+	chmod u+w $@
+
+PREREQUISITELOG = $(addsuffix .log,$(wildcard prerequisite/*.v)) .csdp.cache
 
 #######################################################################
 # Phony targets
@@ -475,6 +479,7 @@ approve-output: output output-coqtop
 output/MExtraction.out: ../plugins/micromega/micromega.ml
 	$(SHOW) GEN $@
 	$(HIDE) cp $< $@
+	$(HIDE) chmod u+w $@
 	$(HIDE) echo >> $@
 
 $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out
diff --git a/test-suite/coq-makefile/template/init.sh b/test-suite/coq-makefile/template/init.sh
index 30be5e6456..ab89e12592 100755
--- a/test-suite/coq-makefile/template/init.sh
+++ b/test-suite/coq-makefile/template/init.sh
@@ -9,10 +9,18 @@ cd _test || exit 1
 mkdir -p src
 mkdir -p theories/sub
 
-cp ../../template/theories/sub/testsub.v theories/sub
-cp ../../template/theories/test.v theories
-cp ../../template/src/test.mlg src
-cp ../../template/src/test_aux.mli src
-cp ../../template/src/test.mli src
-cp ../../template/src/test_plugin.mlpack src
-cp ../../template/src/test_aux.ml src
+cp_file() {
+  local _TARGET=$1
+  cp ../../template/$_TARGET $_TARGET
+  chmod u+w $_TARGET
+}
+
+# We chmod +w as to fix the case where the sources are read-only, as
+# for example when using Dune's cache.
+cp_file theories/sub/testsub.v
+cp_file theories/test.v
+cp_file src/test.mlg
+cp_file src/test_aux.mli
+cp_file src/test.mli
+cp_file src/test_plugin.mlpack
+cp_file src/test_aux.ml
-- 
cgit v1.2.3