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

16 files changed, 150 insertions, 43 deletions

diff --git a/Makefile.build b/Makefile.build
index 92eaf7232..26a40c6cc 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -534,7 +534,7 @@ MAKE_TSOPTS=-C test-suite -s VERBOSE=$(VERBOSE)
 
 check: validate test-suite
 
-test-suite: world $(ALLSTDLIB).v
+test-suite: world byte $(ALLSTDLIB).v
 	$(MAKE) $(MAKE_TSOPTS) clean
 	$(MAKE) $(MAKE_TSOPTS) all
 
diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex
index 768d0df76..f6371f8e5 100644
--- a/doc/refman/RefMan-uti.tex
+++ b/doc/refman/RefMan-uti.tex
@@ -51,6 +51,8 @@ arguments. In other cases, the debugger is simply called without additional
 arguments. Such a wrapper can be found in the \texttt{dev/}
 subdirectory of the sources.
 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
 \section[Building a \Coq\ project with {\tt coq\_makefile}]
 {Building a \Coq\ project with {\tt coq\_makefile}
 \label{Makefile}
@@ -95,7 +97,7 @@ Such command generates the following files:
 	\item[{\tt CoqMakefile.conf}] contains make variables assignments that reflect the contents of the {\tt \_CoqProject} file as well as the path relevant to \Coq{}.
 \end{description}
 
-An optional file {\bf {\tt CoqMakefile.local}} can be provided by the user in order to extend {\tt CoqMakefile}.  In particular one can declare custom actions to be performed before or after the build process. Similarly one can customize the install target or even provide new targets.  Extension points are documented in the {\tt CoqMakefile} file.
+An optional file {\bf {\tt CoqMakefile.local}} can be provided by the user in order to extend {\tt CoqMakefile}.  In particular one can declare custom actions to be performed before or after the build process. Similarly one can customize the install target or even provide new targets.  Extension points are documented in paragraph \ref{coqmakefile:local}.
 
 The extensions of the files listed in {\tt \_CoqProject} is
 used in order to decide how to build them.  In particular:
@@ -114,7 +116,52 @@ the plugin's ``name space'' ({\tt Qux\_plugin}).
 This reduces the chances of begin unable to load two distinct plugins
 because of a clash in their auxiliary module names.
 
-\paragraph{Timing targets and performance testing}
+\paragraph{CoqMakefile.local} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\label{coqmakefile:local}
+
+The optional file {\tt CoqMakefile.local} is included by the generated file
+{\tt CoqMakefile}.  Such can contain two kinds of directives.
+
+\begin{description}
+  \item[Variable assignment] to the variables listed in the {\tt Parameters}
+	  section of the generated makefile.  Here we describe only few of them.
+  \begin{description}
+  \item[CAMLPKGS] can be used to specify third party findlib packages, and is
+	  passed to the OCaml compiler on building or linking of modules.
+          Eg: {\tt -package yojson}.
+  \item[CAMLFLAGS] can be used to specify additional flags to the OCaml
+	  compiler, like {\tt -bin-annot} or {\tt -w...}.
+  \item[COQC, COQDEP, COQDOC] can be set in order to use alternative 
+	  binaries (e.g. wrappers)
+  \end{description}
+\item[Rule extension]
+  The following makefile rules can be extended. For example
+\begin{verbatim}
+pre-all::
+        echo "This line is print before making the all target"
+install-extra::
+        cp ThisExtraFile /there/it/goes
+\end{verbatim}
+  \begin{description}
+  \item[pre-all::] run before the {\tt all} target.  One can use this
+	  to configure the project, or initialize sub modules or check
+	  dependencies are met.
+  \item[post-all::] run after the {\tt all} target.  One can use this
+	  to run a test suite, or compile extracted code.
+  \item[install-extra::] run after {\tt install}.  One can use this
+	  to install extra files.
+  \item[install-doc::]  One can use this to install extra doc.
+  \item[uninstall::] 
+  \item[uninstall-doc::]
+  \item[clean::]
+  \item[cleanall::]
+  \item[archclean::]
+  \item[merlin-hook::] One can append lines to the generated {\tt .merlin}
+	  file extending this target.
+  \end{description}
+\end{description}
+
+\paragraph{Timing targets and performance testing} %%%%%%%%%%%%%%%%%%%%%%%%%%%
 The generated \texttt{Makefile} supports the generation of two kinds
 of timing data: per-file build-times, and per-line times for an
 individual file.
@@ -273,9 +320,10 @@ After     | Code                                                | Before    || C
   \texttt{Note}: This target requires \texttt{python} to build the table.
 \end{itemize}
 
-\paragraph{Notes about including the generated Makefile}
+\paragraph{Reusing/extending the generated Makefile} %%%%%%%%%%%%%%%%%%%%%%%%%
 
-This practice is discouraged. The contents of this file, including variable names
+Including the generated makefile with an {\tt include} directive is discouraged.
+The contents of this file, including variable names
 and status of rules shall change in the future.  Users are advised to
 include {\tt Makefile.conf} or call a target of the generated Makefile
 as in {\tt make -f Makefile target} from another Makefile.
@@ -303,21 +351,23 @@ invoke-coqmakefile: CoqMakefile
 .PHONY: invoke-coqmakefile $(KNOWNFILES)
 
 ####################################################################
-####################################################################
-####################################################################
-####################################################################
 ##                      Your targets here                         ##
 ####################################################################
-####################################################################
-####################################################################
-####################################################################
 
 # This should be the last rule, to handle any targets not declared above
 %: invoke-coqmakefile
 	@true
 \end{verbatim}
 
-\paragraph{Notes for users of {\tt coq\_makefile} with version $<$ 8.7}
+\paragraph{Building a subset of the targets with -j} %%%%%%%%%%%%%%%%%%%%%%%%%
+
+To build, say, two targets \texttt{foo.vo} and \texttt{bar.vo}
+in parallel one can use \texttt{make only TGTS="foo.vo bar.vo" -j}.
+
+Note that \texttt{make foo.vo bar.vo -j} has a different meaning for
+the make utility, in particular it may build a shared prerequisite twice.
+
+\paragraph{Notes for users of {\tt coq\_makefile} with version $<$ 8.7} %%%%%%
 
 \begin{itemize}
 \item Support for ``sub-directory'' is deprecated.  To perform actions before
@@ -328,13 +378,7 @@ invoke-coqmakefile: CoqMakefile
 	{\tt CoqMakefile.local}
 \end{itemize}
 
-\paragraph{Note: building a subset of the targets with -j}
-
-To build, say, two targets \texttt{foo.vo} and \texttt{bar.vo}
-in parallel one can use \texttt{make only TGTS="foo.vo bar.vo" -j}.
-
-Note that \texttt{make foo.vo bar.vo -j} has a different meaning for
-the make utility, in particular it may build a shared prerequisite twice.
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \section[Modules dependencies]{Modules dependencies\label{Dependencies}\index{Dependencies}
   \ttindex{coqdep}}
diff --git a/test-suite/coq-makefile/coqdoc1/run.sh b/test-suite/coq-makefile/coqdoc1/run.sh
index 1feff7479..dc5a500db 100755
--- a/test-suite/coq-makefile/coqdoc1/run.sh
+++ b/test-suite/coq-makefile/coqdoc1/run.sh
@@ -15,6 +15,7 @@ sort -u > desired <<EOT
 ./test
 ./test/test_plugin.cmi
 ./test/test_plugin.cmx
+./test/test_plugin.cmxa
 ./test/test_plugin.cmxs
 ./test/test.glob
 ./test/test.v
diff --git a/test-suite/coq-makefile/coqdoc2/run.sh b/test-suite/coq-makefile/coqdoc2/run.sh
index 1feff7479..dc5a500db 100755
--- a/test-suite/coq-makefile/coqdoc2/run.sh
+++ b/test-suite/coq-makefile/coqdoc2/run.sh
@@ -15,6 +15,7 @@ sort -u > desired <<EOT
 ./test
 ./test/test_plugin.cmi
 ./test/test_plugin.cmx
+./test/test_plugin.cmxa
 ./test/test_plugin.cmxs
 ./test/test.glob
 ./test/test.v
diff --git a/test-suite/coq-makefile/findlib-package/Makefile.local b/test-suite/coq-makefile/findlib-package/Makefile.local
new file mode 100644
index 000000000..0f4a7d995
--- /dev/null
+++ b/test-suite/coq-makefile/findlib-package/Makefile.local
@@ -0,0 +1 @@
+CAMLPKGS   += -package foo
diff --git a/test-suite/coq-makefile/findlib-package/_CoqProject b/test-suite/coq-makefile/findlib-package/_CoqProject
new file mode 100644
index 000000000..69f47302e
--- /dev/null
+++ b/test-suite/coq-makefile/findlib-package/_CoqProject
@@ -0,0 +1,10 @@
+-R src test
+-R theories test
+-I src
+
+src/test_plugin.mlpack
+src/test.ml4
+src/test.mli
+src/test_aux.ml
+src/test_aux.mli
+theories/test.v
diff --git a/test-suite/coq-makefile/findlib-package/findlib/foo/META b/test-suite/coq-makefile/findlib-package/findlib/foo/META
new file mode 100644
index 000000000..ff5f1c7c9
--- /dev/null
+++ b/test-suite/coq-makefile/findlib-package/findlib/foo/META
@@ -0,0 +1,4 @@
+archive(byte)="foo.cma"
+archive(native)="foo.cmxa"
+linkopts="-linkall"
+requires="str"
diff --git a/test-suite/coq-makefile/findlib-package/findlib/foo/Makefile b/test-suite/coq-makefile/findlib-package/findlib/foo/Makefile
new file mode 100644
index 000000000..31cf11665
--- /dev/null
+++ b/test-suite/coq-makefile/findlib-package/findlib/foo/Makefile
@@ -0,0 +1,14 @@
+-include ../../Makefile.conf
+
+CO=$(COQMF_OCAMLFIND) opt
+CB=$(COQMF_OCAMLFIND) ocamlc
+
+all:
+	$(CO) -c foolib.ml
+	$(CO) -a foolib.cmx -o foo.cmxa
+	$(CB) -c foolib.ml
+	$(CB) -a foolib.cmo -o foo.cma
+	$(CB) -c foo.mli # empty .mli file, to be understood
+
+clean:
+	rm -f *.cmo *.cma *.cmx *.cmxa *.cmi *.o *.a
diff --git a/test-suite/coq-makefile/findlib-package/findlib/foo/foo.mli b/test-suite/coq-makefile/findlib-package/findlib/foo/foo.mli
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test-suite/coq-makefile/findlib-package/findlib/foo/foo.mli
diff --git a/test-suite/coq-makefile/findlib-package/findlib/foo/foolib.ml b/test-suite/coq-makefile/findlib-package/findlib/foo/foolib.ml
new file mode 100644
index 000000000..81306fb89
--- /dev/null
+++ b/test-suite/coq-makefile/findlib-package/findlib/foo/foolib.ml
@@ -0,0 +1,2 @@
+let foo () =
+  assert(Str.search_forward (Str.regexp "foo") "barfoobar" 0 = 3)
diff --git a/test-suite/coq-makefile/findlib-package/run.sh b/test-suite/coq-makefile/findlib-package/run.sh
new file mode 100755
index 000000000..a0d8a7fea
--- /dev/null
+++ b/test-suite/coq-makefile/findlib-package/run.sh
@@ -0,0 +1,13 @@
+#!/usr/bin/env bash
+
+. ../template/init.sh
+
+echo "let () = Foolib.foo ();;" >> src/test_aux.ml
+export OCAMLPATH=$OCAMLPATH:$PWD/findlib
+make -C findlib/foo clean
+coq_makefile -f _CoqProject -o Makefile
+cat Makefile.conf
+cat Makefile.local
+make -C findlib/foo
+make
+make byte
diff --git a/test-suite/coq-makefile/mlpack1/run.sh b/test-suite/coq-makefile/mlpack1/run.sh
index 51669f28f..03df9cf05 100755
--- a/test-suite/coq-makefile/mlpack1/run.sh
+++ b/test-suite/coq-makefile/mlpack1/run.sh
@@ -15,6 +15,7 @@ sort > desired <<EOT
 ./test/test.glob
 ./test/test_plugin.cmi
 ./test/test_plugin.cmx
+./test/test_plugin.cmxa
 ./test/test_plugin.cmxs
 ./test/test.v
 ./test/test.vo
diff --git a/test-suite/coq-makefile/mlpack2/run.sh b/test-suite/coq-makefile/mlpack2/run.sh
index 51669f28f..03df9cf05 100755
--- a/test-suite/coq-makefile/mlpack2/run.sh
+++ b/test-suite/coq-makefile/mlpack2/run.sh
@@ -15,6 +15,7 @@ sort > desired <<EOT
 ./test/test.glob
 ./test/test_plugin.cmi
 ./test/test_plugin.cmx
+./test/test_plugin.cmxa
 ./test/test_plugin.cmxs
 ./test/test.v
 ./test/test.vo
diff --git a/test-suite/coq-makefile/native1/run.sh b/test-suite/coq-makefile/native1/run.sh
index 3bec11cb7..89bafe9ad 100755
--- a/test-suite/coq-makefile/native1/run.sh
+++ b/test-suite/coq-makefile/native1/run.sh
@@ -18,6 +18,7 @@ sort > desired <<EOT
 ./test/test.glob
 ./test/test_plugin.cmi
 ./test/test_plugin.cmx
+./test/test_plugin.cmxa
 ./test/test_plugin.cmxs
 ./test/test.v
 ./test/test.vo
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;