From 2f6eda3e8d255f3617ee2bfc6e343151a0445e3b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 9 Aug 2017 14:01:27 +0200 Subject: test-suite: depend on byte compilation too coq-makefile's tests do depend on this --- Makefile.build | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile.build b/Makefile.build index 3d4b475dcd..2d8b37163c 100644 --- a/Makefile.build +++ b/Makefile.build @@ -540,7 +540,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 -- cgit v1.2.3 From 10a3ad4074fbc85ca146d44449c1fe433515e3db Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 9 Aug 2017 14:01:22 +0200 Subject: coq_makefile: test using findlib's package --- test-suite/coq-makefile/findlib-package/Makefile.local | 3 +++ test-suite/coq-makefile/findlib-package/_CoqProject | 10 ++++++++++ test-suite/coq-makefile/findlib-package/findlib/foo/META | 4 ++++ .../coq-makefile/findlib-package/findlib/foo/Makefile | 14 ++++++++++++++ .../coq-makefile/findlib-package/findlib/foo/foo.mli | 0 .../coq-makefile/findlib-package/findlib/foo/foolib.ml | 2 ++ test-suite/coq-makefile/findlib-package/run.sh | 13 +++++++++++++ 7 files changed, 46 insertions(+) create mode 100644 test-suite/coq-makefile/findlib-package/Makefile.local create mode 100644 test-suite/coq-makefile/findlib-package/_CoqProject create mode 100644 test-suite/coq-makefile/findlib-package/findlib/foo/META create mode 100644 test-suite/coq-makefile/findlib-package/findlib/foo/Makefile create mode 100644 test-suite/coq-makefile/findlib-package/findlib/foo/foo.mli create mode 100644 test-suite/coq-makefile/findlib-package/findlib/foo/foolib.ml create mode 100755 test-suite/coq-makefile/findlib-package/run.sh 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 0000000000..e9c4305567 --- /dev/null +++ b/test-suite/coq-makefile/findlib-package/Makefile.local @@ -0,0 +1,3 @@ +OCAMLLIBS += -package foo +CAMLLINK := "$(OCAMLFIND)" ocamlc -rectypes -thread -linkpkg -dontlink str +CAMLOPTLINK := "$(OCAMLFIND)" ocamlopt -rectypes -thread -linkpkg -dontlink str diff --git a/test-suite/coq-makefile/findlib-package/_CoqProject b/test-suite/coq-makefile/findlib-package/_CoqProject new file mode 100644 index 0000000000..69f47302e1 --- /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 0000000000..ff5f1c7c96 --- /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 0000000000..31cf116652 --- /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 0000000000..e69de29bb2 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 0000000000..81306fb89b --- /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 0000000000..a0d8a7fea7 --- /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 -- cgit v1.2.3 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(-) 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. --- .../coq-makefile/findlib-package/Makefile.local | 2 +- tools/CoqMakefile.in | 24 ++++++++++++---------- 2 files changed, 14 insertions(+), 12 deletions(-) diff --git a/test-suite/coq-makefile/findlib-package/Makefile.local b/test-suite/coq-makefile/findlib-package/Makefile.local index e9c4305567..5373b0219f 100644 --- a/test-suite/coq-makefile/findlib-package/Makefile.local +++ b/test-suite/coq-makefile/findlib-package/Makefile.local @@ -1,3 +1,3 @@ -OCAMLLIBS += -package foo +CAMLPKGS += -package foo CAMLLINK := "$(OCAMLFIND)" ocamlc -rectypes -thread -linkpkg -dontlink str CAMLOPTLINK := "$(OCAMLFIND)" ocamlopt -rectypes -thread -linkpkg -dontlink str 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(-) 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 --- test-suite/coq-makefile/coqdoc1/run.sh | 1 + test-suite/coq-makefile/coqdoc2/run.sh | 1 + test-suite/coq-makefile/findlib-package/Makefile.local | 2 -- test-suite/coq-makefile/mlpack1/run.sh | 1 + test-suite/coq-makefile/mlpack2/run.sh | 1 + test-suite/coq-makefile/native1/run.sh | 1 + tools/CoqMakefile.in | 12 +++++++++--- 7 files changed, 14 insertions(+), 5 deletions(-) diff --git a/test-suite/coq-makefile/coqdoc1/run.sh b/test-suite/coq-makefile/coqdoc1/run.sh index 1feff7479b..dc5a500db8 100755 --- a/test-suite/coq-makefile/coqdoc1/run.sh +++ b/test-suite/coq-makefile/coqdoc1/run.sh @@ -15,6 +15,7 @@ sort -u > desired < desired < desired < desired < desired < $<.$(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(-) 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 --- doc/refman/RefMan-uti.tex | 80 ++++++++++++++++++++++++++++++++++++----------- tools/CoqMakefile.in | 18 ++++++++--- 2 files changed, 75 insertions(+), 23 deletions(-) diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex index 768d0df763..f6371f8e5c 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. @@ -302,22 +350,24 @@ 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/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(-) 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