aboutsummaryrefslogtreecommitdiffstats
path: root/src/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'src/Makefile')
-rw-r--r--src/Makefile38
1 files changed, 21 insertions, 17 deletions
diff --git a/src/Makefile b/src/Makefile
index 5653389..3efcfc3 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -7,7 +7,7 @@
## # GNU Lesser General Public License Version 2.1 ##
## # (see LICENSE file for the text of the license) ##
##########################################################################
-## GNUMakefile for Coq 8.12.2
+## GNUMakefile for Coq 8.13.2
# For debugging purposes (must stay here, don't move below)
INITIAL_VARS := $(.VARIABLES)
@@ -104,7 +104,7 @@ BEFORE ?=
AFTER ?=
# FIXME this should be generated by Coq (modules already linked by Coq)
-CAMLDONTLINK=num,str,unix,dynlink,threads
+CAMLDONTLINK=str,unix,dynlink,threads,zarith
# OCaml binaries
CAMLC ?= "$(OCAMLFIND)" ocamlc -c
@@ -146,6 +146,21 @@ TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line
TGTS ?=
+# Retro compatibility (DESTDIR is standard on Unix, DSTROOT is not)
+ifdef DSTROOT
+DESTDIR := $(DSTROOT)
+endif
+
+# Substitution of the path by appending $(DESTDIR) if needed.
+# The variable $(COQMF_WINDRIVE) can be needed for Cygwin environments.
+windrive_path = $(if $(COQMF_WINDRIVE),$(subst $(COQMF_WINDRIVE),/,$(1)),$(1))
+destination_path = $(if $(DESTDIR),$(DESTDIR)/$(call windrive_path,$(1)),$(1))
+
+# Installation paths of libraries and documentation.
+COQLIBINSTALL ?= $(call destination_path,$(COQLIB)/user-contrib)
+COQDOCINSTALL ?= $(call destination_path,$(DOCDIR)/user-contrib)
+COQTOPINSTALL ?= $(call destination_path,$(COQLIB)/toploop) # FIXME: Unused variable?
+
########## End of parameters ##################################################
# What follows may be relevant to you only if you need to
# extend this Makefile. If so, look for 'Extension point' here and
@@ -203,7 +218,7 @@ COQDOCLIBS?=$(COQLIBS_NOML)
# The version of Coq being run and the version of coq_makefile that
# generated this makefile
COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1)
-COQMAKEFILE_VERSION:=8.12.2
+COQMAKEFILE_VERSION:=8.13.2
COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)/$(d)")
@@ -227,17 +242,6 @@ else
TIMING_ARG=
endif
-# Retro compatibility (DESTDIR is standard on Unix, DSTROOT is not)
-ifdef DSTROOT
-DESTDIR := $(DSTROOT)
-endif
-
-concat_path = $(if $(1),$(1)/$(if $(COQMF_WINDRIVE),$(subst $(COQMF_WINDRIVE),/,$(2)),$(2)),$(2))
-
-COQLIBINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)/user-contrib)
-COQDOCINSTALL = $(call concat_path,$(DESTDIR),$(DOCDIR)/user-contrib)
-COQTOPINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)/toploop)
-
# Files #######################################################################
#
# We here define a bunch of variables about the files being part of the
@@ -463,7 +467,7 @@ vok: $(VOFILES:%.vo=%.vok)
.PHONY: vok
validate: $(VOFILES)
- $(TIMER) $(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $^
+ $(TIMER) $(COQCHK) $(COQCHKFLAGS) $(COQLIBS_NOML) $^
.PHONY: validate
only: $(TGTS)
@@ -577,7 +581,7 @@ uninstall::
instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\
rm -f "$$instf" &&\
echo RM "$$instf" &&\
- (rmdir "$(call concat_path,,$(COQLIBINSTALL)/$$df/)" 2>/dev/null || true); \
+ (rmdir "$(COQLIBINSTALL)/$$df/" 2>/dev/null || true); \
done
.PHONY: uninstall
@@ -797,7 +801,7 @@ $(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack
# projects. Note that extra options might be on the command line.
VDFILE_FLAGS:=$(if _CoqProject,-f _CoqProject,) $(CMDLINE_COQLIBS) $(CMDLINE_VFILES)
-$(VDFILE): $(VFILES)
+$(VDFILE): _CoqProject $(VFILES)
$(SHOW)'COQDEP VFILES'
$(HIDE)$(COQDEP) -vos -dyndep var $(VDFILE_FLAGS) $(redir_if_ok)