From e7bc719df55907b00b04f9fa2d45dba2da838360 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 28 Jun 2017 01:04:41 -0400 Subject: Quote $(OCAMLFIND) in CoqMakefile.in for Windows This, I hope, will fix [bug #5620](https://coq.inria.fr/bugs/show_bug.cgi?id=5620)--- tools/CoqMakefile.in | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 7b01c1b663..29e2a89e38 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -73,11 +73,11 @@ COQDOC ?= "$(COQBIN)coqdoc" COQMKTOP ?= "$(COQBIN)coqmktop" # OCaml binaries -CAMLC ?= $(OCAMLFIND) ocamlc -c -rectypes -thread -CAMLOPTC ?= $(OCAMLFIND) opt -c -rectypes -thread -CAMLLINK ?= $(OCAMLFIND) ocamlc -rectypes -thread -CAMLOPTLINK ?= $(OCAMLFIND) opt -rectypes -thread -CAMLDEP ?= $(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack +CAMLC ?= "$(OCAMLFIND)" ocamlc -c -rectypes -thread +CAMLOPTC ?= "$(OCAMLFIND)" opt -c -rectypes -thread +CAMLLINK ?= "$(OCAMLFIND)" ocamlc -rectypes -thread +CAMLOPTLINK ?= "$(OCAMLFIND)" opt -rectypes -thread +CAMLDEP ?= "$(OCAMLFIND)" ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack # DESTDIR is prepended to all installation paths DESTDIR ?= @@ -139,7 +139,7 @@ COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)") CAMLFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB) -CAMLLIB:=$(shell $(OCAMLFIND) printconf stdlib) +CAMLLIB:=$(shell "$(OCAMLFIND)" printconf stdlib) # FIXME This should be generated by Coq GRAMMARS:=grammar.cma @@ -308,12 +308,12 @@ html: $(GLOBFILES) $(VFILES) mlihtml: $(MLIFILES:.mli=.cmi) $(SHOW)'OCAMLDOC -d $@' $(HIDE)mkdir $@ || rm -rf $@/* - $(HIDE)$(OCAMLFIND) ocamldoc -html -rectypes \ + $(HIDE)"$(OCAMLFIND)" ocamldoc -html -rectypes \ -d $@ -m A $(CAMLDEBUG) $(CAMLFLAGS) $(MLIFILES) all-mli.tex: $(MLIFILES:.mli=.cmi) $(SHOW)'OCAMLDOC -latex $@' - $(OCAMLFIND) ocamldoc -latex -rectypes \ + "$(OCAMLFIND)" ocamldoc -latex -rectypes \ -o $@ -m A $(CAMLDEBUG) $(CAMLFLAGS) $(MLIFILES) gallina: $(GFILES) -- cgit v1.2.3 From 05db464aefe90ff69ea69d5ce7c4775c6a7f218f Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 28 Jun 2017 12:20:47 -0400 Subject: Create a variable for CAMLDOC in CoqMakefile.in --- tools/CoqMakefile.in | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 29e2a89e38..4f967e6336 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -77,6 +77,7 @@ CAMLC ?= "$(OCAMLFIND)" ocamlc -c -rectypes -thread CAMLOPTC ?= "$(OCAMLFIND)" opt -c -rectypes -thread CAMLLINK ?= "$(OCAMLFIND)" ocamlc -rectypes -thread CAMLOPTLINK ?= "$(OCAMLFIND)" opt -rectypes -thread +CAMLDOC ?= "$(OCAMLFIND)" ocamldoc -rectypes CAMLDEP ?= "$(OCAMLFIND)" ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack # DESTDIR is prepended to all installation paths @@ -306,14 +307,14 @@ html: $(GLOBFILES) $(VFILES) -toc $(COQDOCFLAGS) -html $(GAL) $(COQDOCLIBS) -d html $(VFILES) mlihtml: $(MLIFILES:.mli=.cmi) - $(SHOW)'OCAMLDOC -d $@' + $(SHOW)'CAMLDOC -d $@' $(HIDE)mkdir $@ || rm -rf $@/* - $(HIDE)"$(OCAMLFIND)" ocamldoc -html -rectypes \ + $(HIDE)$(CAMLDOC) -html \ -d $@ -m A $(CAMLDEBUG) $(CAMLFLAGS) $(MLIFILES) all-mli.tex: $(MLIFILES:.mli=.cmi) - $(SHOW)'OCAMLDOC -latex $@' - "$(OCAMLFIND)" ocamldoc -latex -rectypes \ + $(SHOW)'CAMLDOC -latex $@' + $(HIDE)$(CAMLDOC) -latex \ -o $@ -m A $(CAMLDEBUG) $(CAMLFLAGS) $(MLIFILES) gallina: $(GFILES) -- cgit v1.2.3 From 2a95acfe2892d982cda1fcd7c7a921c8e25f16d4 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 28 Jun 2017 12:26:40 -0400 Subject: Also quote $(COQLIB)/grammar In case COQLIB has backslashes, as it does on Windows, or spaces--- tools/CoqMakefile.in | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 4f967e6336..3027bf92d2 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -150,7 +150,7 @@ else CAMLP4EXTEND= endif -PP:=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(COQLIB)/grammar compat5.cmo $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl' +PP:=-pp '$(CAMLP4O) -I $(CAMLLIB) -I "$(COQLIB)/grammar" compat5.cmo $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl' COQLIBINSTALL = $(COQLIB)user-contrib COQDOCINSTALL = $(DOCDIR)user-contrib -- cgit v1.2.3 From b55d44168ee39b0d9da8364238e716526ffcf920 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 28 Jun 2017 12:31:41 -0400 Subject: Fix more potential quoting issues: COQBIN , COQLIB --- tools/CoqMakefile.in | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 3027bf92d2..c4afc930a7 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -66,6 +66,7 @@ STDTIME?=/usr/bin/time -f "$* (user: %U mem: %M ko)" # Coq binaries COQC ?= "$(COQBIN)coqc" +COQTOP ?= "$(COQBIN)coqtop" COQCHK ?= "$(COQBIN)coqchk" COQDEP ?= "$(COQBIN)coqdep" GALLINA ?= "$(COQBIN)gallina" @@ -177,7 +178,7 @@ ALLSRCFILES := \ # helpers vo_to_obj = $(addsuffix .o,\ $(filter-out Warning: Error:,\ - $(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(1)))) + $(shell $(COQTOP) -q -noinit -batch -quiet -print-mod-uid $(1)))) strip_dotslash = $(patsubst ./%,%,$(1)) VO = vo @@ -632,14 +633,14 @@ printenv:: .merlin: $(SHOW)'FILL .merlin' $(HIDE)echo 'FLG -rectypes' > .merlin - $(HIDE)echo "B $(COQLIB)" >> .merlin - $(HIDE)echo "S $(COQLIB)" >> .merlin + $(HIDE)echo 'B $(COQLIB)' >> .merlin + $(HIDE)echo 'S $(COQLIB)' >> .merlin $(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \ - echo "B $(COQLIB)$(d)" >> .merlin;) + echo 'B $(COQLIB)$(d)' >> .merlin;) $(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \ - echo "S $(COQLIB)$(d)" >> .merlin;) - $(HIDE)$(foreach d,$(SRC_SUBDIRS), echo "B $(d)" >> .merlin;) - $(HIDE)$(foreach d,$(SRC_SUBDIRS), echo "S $(d)" >> .merlin;) + echo 'S $(COQLIB)$(d)' >> .merlin;) + $(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'B $(d)' >> .merlin;) + $(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'S $(d)' >> .merlin;) $(HIDE)$(MAKE) merlin-hook -f "$(SELF)" .PHONY: merlin -- cgit v1.2.3