From 534b8afafc763b382fb3fa747bb95a9a57676d4c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 9 Aug 2017 14:43:48 +0200 Subject: coq_makefile: build/use .cma for packed plugins The build chain is always ml -> cmo -> cma ml -> cmx -> cmxa -> cmxs If we are packing, then it becomes ml -> cmo \ ml -> cmo --> cmo -> cma ml -> cmo / ml -> cmxo \ ml -> cmxo --> cmxo -> cmxa -> cmxs ml -> cmxo / The interest of always having a .cma or .cmxa is that such file can carry linking flags, that in findlib terms means which -package was use to build the plugin. --- tools/CoqMakefile.in | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tools') diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 9f891afe53..f6fe6ddeb1 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -151,7 +151,7 @@ OPT?= # The DYNOBJ and DYNLIB variables are used by "coqdep -dyndep var" in .v.d ifeq '$(OPT)' '-byte' USEBYTE:=true -DYNOBJ:=.cmo +DYNOBJ:=.cma DYNLIB:=.cma else USEBYTE:= -- cgit v1.2.3 From 2f335733853a062d0a0e21fa0842750b7b897b28 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 20 Aug 2017 15:24:53 +0200 Subject: coq_makefile: use dedicated variable for extra packages CAMLPKGS is now used to hold extra findlib -packages The previous solution was to use CAMLFLAGS but since 4.05 an invocation of `ocamlopt -pack useless.cmxa foo.cmx -o packedfoo.cmx` fails saying that `useless.cmxa` is not a compilation unit description. CAMLPKGS is used in all `ocamlopt` invocations but for the one performing the packing. --- tools/CoqMakefile.in | 24 +++++++++++++----------- 1 file changed, 13 insertions(+), 11 deletions(-) (limited to 'tools') diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index f6fe6ddeb1..9713b8eb57 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -171,6 +171,8 @@ COQMAKEFILE_VERSION:=@COQ_VERSION@ COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)") CAMLFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB) $(OCAML_API_FLAGS) +CAMLFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB) +CAMLPKGS?= CAMLLIB:=$(shell "$(OCAMLFIND)" printconf stdlib) @@ -558,46 +560,46 @@ archclean:: $(MLIFILES:.mli=.cmi): %.cmi: %.mli $(SHOW)'CAMLC -c $<' - $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $< + $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $< $(ML4FILES:.ml4=.cmo): %.cmo: %.ml4 $(SHOW)'CAMLC -pp -c $<' - $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(PP) -impl $< + $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(PP) -impl $< $(ML4FILES:.ml4=.cmx): %.cmx: %.ml4 $(SHOW)'CAMLOPT -pp -c $(FOR_PACK) $<' - $(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(PP) $(FOR_PACK) -impl $< + $(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(PP) $(FOR_PACK) -impl $< $(MLFILES:.ml=.cmo): %.cmo: %.ml $(SHOW)'CAMLC -c $<' - $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $< + $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $< $(MLFILES:.ml=.cmx): %.cmx: %.ml $(SHOW)'CAMLOPT -c $(FOR_PACK) $<' - $(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(FOR_PACK) $< + $(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(FOR_PACK) $< $(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa $(SHOW)'CAMLOPT -shared -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) \ + $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ -linkall -shared -o $@ $< $(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib $(SHOW)'CAMLC -a -o $@' - $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $^ + $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^ $(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib $(SHOW)'CAMLOPT -a -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $^ + $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^ $(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmx $(SHOW)'CAMLOPT -shared -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -shared -o $@ $< + $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -shared -o $@ $< $(MLPACKFILES:.mlpack=.cma): %.cma: %.cmo | %.mlpack $(SHOW)'CAMLC -a -o $@' - $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $^ + $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^ $(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack $(SHOW)'CAMLC -pack -o $@' @@ -610,7 +612,7 @@ $(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack # This rule is for _CoqProject with no .mllib nor .mlpack $(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs)): %.cmxs: %.cmx $(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -shared -o $@ $< + $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -shared -o $@ $< ifneq (,$(TIMING)) TIMING_EXTRA = > $<.$(TIMING_EXT) -- cgit v1.2.3 From ddced9fa0c3e96925aac9efda39d3fb29e8bdfcd Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 29 Aug 2017 13:56:37 +0200 Subject: coq_makefile: do not overwrite CAMLFLAGS --- tools/CoqMakefile.in | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'tools') diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 9713b8eb57..fc8c450ec8 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -170,8 +170,7 @@ COQMAKEFILE_VERSION:=@COQ_VERSION@ COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)") -CAMLFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB) $(OCAML_API_FLAGS) -CAMLFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB) +CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB) $(OCAML_API_FLAGS) CAMLPKGS?= CAMLLIB:=$(shell "$(OCAMLFIND)" printconf stdlib) -- cgit v1.2.3 From 6e07e3a53e56882043b9db49f03fdf1470a16c46 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 29 Aug 2017 14:56:31 +0200 Subject: coq_makefile(pack): ml -> cmx --pack-> cmx -> cmxa -> cmxs --- tools/CoqMakefile.in | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) (limited to 'tools') diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index fc8c450ec8..e919db4a98 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -592,9 +592,14 @@ $(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^ -$(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmx +$(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmxa $(SHOW)'CAMLOPT -shared -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -shared -o $@ $< + $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ + -shared -linkall -o $@ $< + +$(MLPACKFILES:.mlpack=.cmxa): %.cmxa: %.cmx + $(SHOW)'CAMLOPT -a -o $@' + $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $< $(MLPACKFILES:.mlpack=.cma): %.cma: %.cmo | %.mlpack $(SHOW)'CAMLC -a -o $@' @@ -611,7 +616,8 @@ $(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack # This rule is for _CoqProject with no .mllib nor .mlpack $(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs)): %.cmxs: %.cmx $(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -shared -o $@ $< + $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ + -shared -o $@ $< ifneq (,$(TIMING)) TIMING_EXTRA = > $<.$(TIMING_EXT) -- cgit v1.2.3 From a93279fb7fe5917ab859e7b3dfb6f89522161419 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 29 Aug 2017 13:54:46 +0200 Subject: coq_makefile: print error message when coqlib is not set properly --- tools/coq_makefile.ml | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) (limited to 'tools') diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 0f38d19386..de76bf98bc 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -114,13 +114,12 @@ let read_whole_file s = close_in ic; Buffer.contents b -let makefile_template = - let template = "/tools/CoqMakefile.in" in - Coq_config.coqlib ^ template - let quote s = if String.contains s ' ' then "'" ^ s ^ "'" else s let generate_makefile oc conf_file local_file args project = + let makefile_template = + let template = "/tools/CoqMakefile.in" in + Envars.coqlib () ^ template in let s = read_whole_file makefile_template in let s = List.fold_left (fun s (k,v) -> Str.global_replace (Str.regexp_string k) v s) s @@ -424,7 +423,7 @@ let _ = check_overlapping_include project; - Envars.set_coqlib ~fail:(fun x -> x); + Envars.set_coqlib ~fail:(fun x -> Printf.eprintf "Error: %s\n" x; exit 1); let ocm = Option.cata open_out stdout project.makefile in generate_makefile ocm conf_file local_file (prog :: args) project; -- cgit v1.2.3 From ba64f7c64ad3da70d4c939b33384099ad8df7124 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 29 Aug 2017 14:07:16 +0200 Subject: coq_makefile: improve documentation --- tools/CoqMakefile.in | 18 +++++++++++++----- 1 file changed, 13 insertions(+), 5 deletions(-) (limited to 'tools') diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index e919db4a98..19b1d8cbda 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -52,7 +52,7 @@ HASNATDYNLINK := $(COQMF_HASNATDYNLINK) # # Parameters are make variable assignments. # They can be passed to (each call to) make on the command line. -# They can also be put in @LOCAL_FILE@ once an forall. +# They can also be put in @LOCAL_FILE@ once an for all. # For retro-compatibility reasons they can be put in the _CoqProject, but this # practice is discouraged since _CoqProject better not contain make specific # code (be nice to user interfaces). @@ -96,11 +96,14 @@ COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQLIB)/tools/make-both-single-timing-fil BEFORE ?= AFTER ?= +# FIXME this should be generated by Coq (modules already linked by Coq) +CAMLDONTLINK=camlp5.gramlib,unix,str + # OCaml binaries CAMLC ?= "$(OCAMLFIND)" ocamlc -c -rectypes -thread CAMLOPTC ?= "$(OCAMLFIND)" opt -c -rectypes -thread -CAMLLINK ?= "$(OCAMLFIND)" ocamlc -rectypes -thread -CAMLOPTLINK ?= "$(OCAMLFIND)" opt -rectypes -thread +CAMLLINK ?= "$(OCAMLFIND)" ocamlc -rectypes -thread -linkpkg -dontlink $(CAMLDONTLINK) +CAMLOPTLINK ?= "$(OCAMLFIND)" opt -rectypes -thread -linkpkg -dontlink $(CAMLDONTLINK) CAMLDOC ?= "$(OCAMLFIND)" ocamldoc -rectypes CAMLDEP ?= "$(OCAMLFIND)" ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack @@ -111,6 +114,11 @@ DESTDIR ?= CAMLDEBUG ?= COQDEBUG ?= +# Extra flags to the OCaml compiler +CAMLFLAGS ?= +# Extra packages to be linked in (as in findlib -package) +CAMLPKGS ?= + # Option for making timing files TIMING?= # Output file names for timed builds @@ -171,7 +179,6 @@ COQMAKEFILE_VERSION:=@COQ_VERSION@ COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)") CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB) $(OCAML_API_FLAGS) -CAMLPKGS?= CAMLLIB:=$(shell "$(OCAMLFIND)" printconf stdlib) @@ -441,7 +448,7 @@ beautify: $(BEAUTYFILES) # There rules can be extended in @LOCAL_FILE@ # Extensions can't assume when they run. -install: install-extra +install: $(HIDE)for f in $(FILESTOINSTALL); do\ df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\ if [ "$$?" != "0" -o -z "$$df" ]; then\ @@ -452,6 +459,7 @@ install: install-extra echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\ fi;\ done + $(HIDE)$(MAKE) install-extra -f "$(SELF)" install-extra:: @# Extension point .PHONY: install install-extra -- cgit v1.2.3 From 5cba636c873a93367cd3f26fd0efc919e68ddc5a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 29 Aug 2017 17:30:26 +0200 Subject: coq_makefile: fix .merlin generation (FLG -thread) --- tools/CoqMakefile.in | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tools') diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 19b1d8cbda..f4d1118d0f 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -749,7 +749,7 @@ printenv:: # file you can extend the merlin-hook target in @LOCAL_FILE@ .merlin: $(SHOW)'FILL .merlin' - $(HIDE)echo 'FLG -rectypes' > .merlin + $(HIDE)echo 'FLG -rectypes -thread' > .merlin $(HIDE)echo 'B $(COQLIB)' >> .merlin $(HIDE)echo 'S $(COQLIB)' >> .merlin $(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \ -- cgit v1.2.3