From 02b40f6cdb7ec56f34c6b773b1d7768b4b135fd9 Mon Sep 17 00:00:00 2001
From: Ike Mulder
Date: Fri, 26 Apr 2019 16:16:47 +0200
Subject: Fixed some escaping problems with arguments containing spaces in
 IDE's Compile buffer, and with building from a path containing spaces.

Updated CHANGES.md

Now using Filename.quote instead of enclosing in single quotes.

Fixed rebasing problems.
---
 configure.ml        |  2 +-
 ide/coqide.ml       |  4 ++--
 test-suite/Makefile | 14 +++++++-------
 3 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/configure.ml b/configure.ml
index 6e15cdbe4e..55d71f6c2e 100644
--- a/configure.ml
+++ b/configure.ml
@@ -975,7 +975,7 @@ let config_runtime () =
   | Some flags -> string_split ',' flags
   | _ when use_custom -> [custom_flag]
   | _ when !prefs.local ->
-    ["-dllib";"-lcoqrun";"-dllpath";coqtop/"kernel/byterun"]
+    ["-dllib";"-lcoqrun";"-dllpath";("\"" ^ coqtop ^ "/kernel/byterun\"")]
   | _ ->
     let ld="CAML_LD_LIBRARY_PATH" in
     build_loadpath := sprintf "export %s:='%s/kernel/byterun':$(%s)" ld coqtop ld;
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 143a12deeb..61e95c21b1 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -460,7 +460,7 @@ let compile sn =
     |Some f ->
       let args = Coq.get_arguments sn.coqtop in
       let cmd = cmd_coqc#get
-        ^ " " ^ String.concat " " args
+        ^ " " ^ String.concat " " (List.map Filename.quote args)
         ^ " " ^ (Filename.quote f) ^ " 2>&1"
       in
       let buf = Buffer.create 1024 in
@@ -474,7 +474,7 @@ let compile sn =
           flash_info (f ^ " successfully compiled")
         else begin
           flash_info (f ^ " failed to compile");
-          sn.messages#default_route#set (Pp.str "Compilation output:\n");
+          sn.messages#default_route#set (Pp.str ("Compilation output:\n" ^ cmd ^ "\n"));
           sn.messages#default_route#add (Pp.str (Buffer.contents buf));
         end
       in
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 265c2eafa7..6a6b729578 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -33,10 +33,10 @@ include ../Makefile.common
 #######################################################################
 
 ifneq ($(wildcard ../_build),)
-BIN:=$(shell cd ..; pwd)/_build/install/default/bin/
-COQLIB:=$(shell cd ..; pwd)/_build/install/default/lib/coq
+BIN:='$(shell cd ..; pwd)'/_build/install/default/bin/
+COQLIB:='$(shell cd ..; pwd)'/_build/install/default/lib/coq
 else
-BIN := $(shell cd ..; pwd)/bin/
+BIN := '$(shell cd ..; pwd)'/bin/
 
 COQLIB?=
 ifeq ($(COQLIB),)
@@ -602,10 +602,10 @@ $(patsubst %.sh,%.log,$(wildcard misc/*.sh)): %.log: %.sh $(PREREQUISITELOG)
 	@echo "TEST      $<"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
-	  export BIN="$(BIN)"; \
-	  export coqc="$(coqc)"; \
-	  export coqtop="$(coqc)"; \
-	  export coqdep="$(coqdep)"; \
+	  export BIN=$(BIN); \
+	  export coqc="eval $(coqc)"; \
+	  export coqtop="eval $(coqc)"; \
+	  export coqdep="eval $(coqdep)"; \
 	  "$<" 2>&1; R=$$?; times; \
 	  if [ $$R = 0 ]; then \
 	    echo $(log_success); \
-- 
cgit v1.2.3


From a4d8c9414e65271fc97347ae04b0b431206d33f8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 25 Feb 2020 13:53:03 +0100
Subject: Makefile in test-suite: More separation of concerns as suggested by
 Enrico.

See "https://github.com/coq/coq/pull/10008#discussion_r382899607".
---
 test-suite/Makefile | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 6a6b729578..1681150f7b 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -32,11 +32,15 @@ include ../Makefile.common
 # Variables
 #######################################################################
 
+# Using quotes to anticipate the possibility of spaces in the directory name
+# Note that this will later need an eval in shell to interpret the quotes
+ROOT='$(shell cd ..; pwd)'
+
 ifneq ($(wildcard ../_build),)
-BIN:='$(shell cd ..; pwd)'/_build/install/default/bin/
-COQLIB:='$(shell cd ..; pwd)'/_build/install/default/lib/coq
+BIN:=$(ROOT)/_build/install/default/bin/
+COQLIB:=$(ROOT)/_build/install/default/lib/coq
 else
-BIN := '$(shell cd ..; pwd)'/bin/
+BIN := $(ROOT)/bin/
 
 COQLIB?=
 ifeq ($(COQLIB),)
-- 
cgit v1.2.3


From 7462ca3189ceff514bdb919ae7f2908d0f0c0518 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 28 Feb 2020 01:27:14 +0100
Subject: Adding change log

---
 doc/changelog/09-coqide/10008-snyke7+escape_spaces.rst | 4 ++++
 1 file changed, 4 insertions(+)
 create mode 100644 doc/changelog/09-coqide/10008-snyke7+escape_spaces.rst

diff --git a/doc/changelog/09-coqide/10008-snyke7+escape_spaces.rst b/doc/changelog/09-coqide/10008-snyke7+escape_spaces.rst
new file mode 100644
index 0000000000..99b1592fb3
--- /dev/null
+++ b/doc/changelog/09-coqide/10008-snyke7+escape_spaces.rst
@@ -0,0 +1,4 @@
+- **Fixed:**
+  Fix file paths containing spaces when compiling
+  (`#10008 <https://github.com/coq/coq/pull/10008>`_,
+  by snyke7, fixing `#11595 <https://github.com/coq/coq/pull/11595>`_).
-- 
cgit v1.2.3