diff options
| author | Hugo Herbelin | 2020-02-28 23:08:05 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-28 23:08:05 +0100 |
| commit | 7c1d1a58697486f4f52ac7f45b932d03a7e77e5c (patch) | |
| tree | ce4a5f8cbd17e9dcaed5202b43d946b8a6e1e52d | |
| parent | c2d7fbe834031a45e3be4c5cdf93694e109131e9 (diff) | |
| parent | 7462ca3189ceff514bdb919ae7f2908d0f0c0518 (diff) | |
Merge PR #10008: CoqIDE: Fix not escaping coqtop arguments when compiling
Ack-by: ejgallego
Ack-by: gares
Ack-by: herbelin
| -rw-r--r-- | configure.ml | 2 | ||||
| -rw-r--r-- | doc/changelog/09-coqide/10008-snyke7+escape_spaces.rst | 4 | ||||
| -rw-r--r-- | ide/coqide.ml | 4 | ||||
| -rw-r--r-- | test-suite/Makefile | 18 |
4 files changed, 18 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/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>`_). 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..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),) @@ -602,10 +606,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); \ |