Merge PR #958: coq_makefile: build/use .cma for packed plugins too

2 files changed, 38 insertions, 24 deletions

diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 9f891afe5..f4d1118d0 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
@@ -151,7 +159,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:=
@@ -170,7 +178,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) $(OCAML_API_FLAGS)
 
 CAMLLIB:=$(shell "$(OCAMLFIND)" printconf stdlib)
 
@@ -440,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\
@@ -451,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
@@ -558,46 +567,51 @@ 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
+$(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmxa
 	$(SHOW)'CAMLOPT -shared -o $@'
-	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -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 $@'
-	$(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $^
+	$(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^
 
 $(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack
 	$(SHOW)'CAMLC -pack -o $@'
@@ -610,7 +624,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) -shared -o $@ $<
+	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
+		-shared -o $@ $<
 
 ifneq (,$(TIMING))
 TIMING_EXTRA = > $<.$(TIMING_EXT)
@@ -734,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), \
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 0f38d1938..de76bf98b 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;