##########################################################################
## # The Coq Proof Assistant / The Coq Development Team ##
## v # Copyright INRIA, CNRS and contributors ##
## <O___,, # (see version control and CREDITS file for authors & dates) ##
## \VV/ ###############################################################
## // # This file is distributed under the terms of the ##
## # GNU Lesser General Public License Version 2.1 ##
## # (see LICENSE file for the text of the license) ##
##########################################################################
# This makefile is normally called by the main Makefile after setting
# some variables.
###########################################################################
# User-customizable variables
###########################################################################
# The following variables could be modified via the command-line of make,
# either with the syntax 'make XYZ=1' or 'XYZ=1 make'
# To see the actual commands launched by make instead of shortened versions,
# set this variable to 1 (or any non-empty value):
VERBOSE ?=
# When non-empty, a time command is performed at each .v compilation.
# To collect compilation timings of .v and import them in a spreadsheet,
# you could hence consider: make TIMED=1 2> timings.csv
TIMED ?=
# When $(TIMED) is set, the time command used by default is $(STDTIME)
# (see below), unless the following variable is non-empty. For instance,
# it could be set to "'/usr/bin/env time -p'".
TIMECMD ?=
# When non-empty, -time is passed to coqc and the output is recorded
# in a timing file for each .v file. If set to "before" or "after",
# the file name for foo.v is foo.v.$(TIMING)-timing; otherwise, it is
# foo.v.timing
TIMING ?=
# Non-empty runs the checker on all produced .vo files:
VALIDATE ?=
# When non-empty, passed as extra arguments to coqtop/coqc:
COQUSERFLAGS ?=
# Option for changing sorting of timing output file
TIMING_SORT_BY ?= auto
# Option for changing the fuzz parameter on the output file
TIMING_FUZZ ?= 0
# Option for changing whether to use real or user time for timing tables
TIMING_REAL?=
# Option for including the memory column(s)
TIMING_INCLUDE_MEM?=
# Option for sorting by the memory column
TIMING_SORT_BY_MEM?=
# Output file names for timed builds
TIME_OF_BUILD_FILE ?= time-of-build.log
TIME_OF_BUILD_BEFORE_FILE ?= time-of-build-before.log
TIME_OF_BUILD_AFTER_FILE ?= time-of-build-after.log
TIME_OF_PRETTY_BUILD_FILE ?= time-of-build-pretty.log
TIME_OF_PRETTY_BOTH_BUILD_FILE ?= time-of-build-both.log
TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line
BEFORE ?=
AFTER ?=
# Number of parallel jobs for -schedule-vio2vo
NJOBS ?= 2
###########################################################################
# Includes
###########################################################################
.PHONY: NOARG
NOARG: world byte
include Makefile.common
include Makefile.vofiles
include Makefile.doc ## provides the 'documentation' rule
include Makefile.ide ## provides the 'coqide' rule
include Makefile.install
###########################################################################
# Default starting rule
###########################################################################
.PHONY: world byte coq world.timing.diff coq.timing.diff states
world: coq coqide documentation revision
byte: world
coq: coqlib coqbinaries tools $(BCONTEXT)/coq-core.install $(BCONTEXT)/coqide-server.install
world.timing.diff: coq.timing.diff
coq.timing.diff: coqlib.timing.diff
states: $(VO_OUT_DIR)theories/Init/Prelude.$(VO)
.PHONY: coqbinaries tools
coqbinaries: $(TOPBINOPT) $(COQC) $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(COQNATIVE)
tools: $(TOOLS) $(OCAMLLIBDEP) $(COQDEP) $(DOC_GRAM)
###########################################################################
# Timing targets
###########################################################################
ifeq (0,$(TIMING_REAL))
TIMING_REAL_ARG :=
TIMING_USER_ARG := --user
else
ifeq (1,$(TIMING_REAL))
TIMING_REAL_ARG := --real
TIMING_USER_ARG :=
else
TIMING_REAL_ARG :=
TIMING_USER_ARG :=
endif
endif
ifeq (0,$(TIMING_INCLUDE_MEM))
TIMING_INCLUDE_MEM_ARG := --no-include-mem
else
TIMING_INCLUDE_MEM_ARG :=
endif
ifeq (1,$(TIMING_SORT_BY_MEM))
TIMING_SORT_BY_MEM_ARG := --sort-by-mem
else
TIMING_SORT_BY_MEM_ARG :=
endif
make-pretty-timed-before:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_BEFORE_FILE)
make-pretty-timed-after:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_AFTER_FILE)
make-pretty-timed make-pretty-timed-before make-pretty-timed-after::
$(HIDE)rm -f pretty-timed-success.ok
$(HIDE)($(MAKE) --no-print-directory $(TGTS) TIMED=1 2>&1 && touch pretty-timed-success.ok) | tee -a $(TIME_OF_BUILD_FILE)
$(HIDE)rm pretty-timed-success.ok # must not be -f; must fail if the touch failed
print-pretty-timed::
$(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIMING_INCLUDE_MEM_ARG) $(TIMING_SORT_BY_MEM_ARG) $(TIMING_REAL_ARG) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
print-pretty-timed-diff::
$(HIDE)$(COQMAKE_BOTH_TIME_FILES) --sort-by=$(TIMING_SORT_BY) $(TIMING_INCLUDE_MEM_ARG) $(TIMING_SORT_BY_MEM_ARG) $(TIMING_REAL_ARG) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
ifeq (,$(BEFORE))
print-pretty-single-time-diff::
@echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing'
$(HIDE)false
else
ifeq (,$(AFTER))
print-pretty-single-time-diff::
@echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing'
$(HIDE)false
else
print-pretty-single-time-diff::
$(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) --fuzz=$(TIMING_FUZZ) --sort-by=$(TIMING_SORT_BY) $(TIMING_USER_ARG) $(AFTER) $(BEFORE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
endif
endif
pretty-timed:
$(HIDE)$(MAKE) --no-print-directory make-pretty-timed
$(HIDE)$(MAKE) --no-print-directory print-pretty-timed
.PHONY: pretty-timed make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff
ifneq (,$(TIMING))
TIMING_ARG=-time
ifeq (after,$(TIMING))
TIMING_EXT=after-timing
else
ifeq (before,$(TIMING))
TIMING_EXT=before-timing
else
TIMING_EXT=timing
endif
endif
else
TIMING_ARG=
endif
###########################################################################
# Build the .v deps
VFILED=.vfiles.d
-include $(VFILED)
# All dependency includes must be declared secondary, otherwise make will
# delete them if it decided to build them by dependency instead of because
# of include, and they will then be automatically deleted, leading to an
# infinite loop.
.SECONDARY: $(VFILED)
###########################################################################
# Compilation options
###########################################################################
# Default timing command
# Use /usr/bin/env time on linux, gtime on Mac OS
TIMEFMT?="$@ (real: %e, user: %U, sys: %S, mem: %M ko)"
ifneq (,$(TIMED))
ifeq (0,$(shell /usr/bin/env time -f "" true >/dev/null 2>/dev/null; echo $$?))
STDTIME?=/usr/bin/env time -f $(TIMEFMT)
else
ifeq (0,$(shell gtime -f "" true >/dev/null 2>/dev/null; echo $$?))
STDTIME?=gtime -f $(TIMEFMT)
else
STDTIME?=time
endif
endif
else
STDTIME?=/usr/bin/env time -f $(TIMEFMT)
endif
TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
# NB: do not use a variable named TIME, since this variable controls
# the output format of the unix command time. For instance:
# TIME="%C (%U user, %S sys, %e total, %M maxres)"
PLUGININCLUDES=$(addprefix -I _build/default/, $(wildcard plugins/*))
DUNEPLUGININCLUDES=$(addprefix -I _build/default/, $(wildcard plugins/*))
NATIVEINCLUDES=$(addprefix -nI _build/default/, kernel/.kernel.objs/byte)
USERCONTRIBINCLUDES=$(addprefix -I _build/default/user-contrib/,$(USERCONTRIBDIRS))
ifdef NATIVECOMPUTE
COQOPTS += -w -deprecated-native-compiler-option -native-compiler ondemand
endif
COQOPTS += $(COQWARNERROR) $(COQUSERFLAGS)
# Beware this depends on the makefile being in a particular dir, we
# should pass an absolute path here but windows is tricky
# c.f. https://github.com/coq/coq/pull/9560
BOOTCOQC=$(TIMER) $(COQC) -coqlib $(VO_OUT_DIR) -q $(COQOPTS) $(DUNEPLUGININCLUDES) $(USERCONTRIBINCLUDES)
###########################################################################
# Infrastructure for the rest of the Makefile
###########################################################################
VO_TOOLS_DEP = $(COQC)
ifeq ($(BEST),byte)
VO_TOOLS_DEP += $(CONTEXT)/lib/stublibs/dllcoqrun_stubs.so
endif
ifdef NATIVECOMPUTE
VO_TOOLS_DEP += $(COQNATIVE)
endif
ifdef VALIDATE
VO_TOOLS_DEP += $(CHICKEN)
endif
## When a rule redirects stdout of a command to the target file : cmd > $@
## then the target file will be created even if cmd has failed.
## Hence relaunching make will go further, as make thinks the target has been
## done ok. To avoid this, we use the following special variable:
.DELETE_ON_ERROR:
###########################################################################
# tests
###########################################################################
.PHONY: validate check test-suite
VALIDOPTS=$(if $(VERBOSE),,-silent) -o -m -coqlib $(VO_OUT_DIR)
validate: $(CHICKEN) | $(ALLVO:.$(VO)=.vo)
$(SHOW)'COQCHK <theories & plugins>'
$(HIDE)$(CHICKEN) $(VALIDOPTS) $(ALLVO)
MAKE_TSOPTS=-C test-suite -s VERBOSE=$(VERBOSE)
check: validate test-suite
test-suite: world
$(MAKE) $(MAKE_TSOPTS) clean
$(MAKE) $(MAKE_TSOPTS) all
###########################################################################
# Compilation of .v files
###########################################################################
# NB: for make world, no need to mention explicitly the .cmxs of the plugins,
# since they are all mentioned in at least one Declare ML Module in some .v
coqlib: stdlib-vo contrib-vo contrib-vo-fixup
ifdef QUICK
$(SHOW)'COQC -schedule-vio2vo $(NJOBS) theories/**.vio'
$(HIDE)$(BOOTCOQC) -schedule-vio2vo $(NJOBS) $(THEORIESVO) $(CONTRIBVO)
endif
coqlib.timing.diff: stdlib.timing.diff
stdlib-vo: $(THEORIESVO)
contrib-vo: $(CONTRIBVO)
# This is needed to make $(VO_OUT_DIR) compliant w.r.t. what is expected in Coqlib
$(VO_OUT_DIR)user-contrib/Ltac2/ltac2_plugin.cmxs: $(BCONTEXT)/user-contrib/Ltac2/ltac2_plugin.cmxs
$(HIDE)cp -a $(BCONTEXT)/user-contrib/Ltac2/ltac2_plugin.cmxs $(VO_OUT_DIR)/user-contrib/Ltac2
$(HIDE)chmod u+w $(VO_OUT_DIR)/user-contrib/Ltac2/ltac2_plugin.cmxs
$(VO_OUT_DIR)user-contrib/Ltac2/ltac2_plugin.cma: $(BCONTEXT)/user-contrib/Ltac2/ltac2_plugin.cma
$(HIDE)cp -a $(BCONTEXT)/user-contrib/Ltac2/ltac2_plugin.cma $(VO_OUT_DIR)/user-contrib/Ltac2
$(HIDE)chmod u+w $(VO_OUT_DIR)/user-contrib/Ltac2/ltac2_plugin.cma
$(VO_OUT_DIR)user-contrib/Ltac2/ltac2_plugin.mllib: user-contrib/Ltac2/ltac2_plugin.mllib
$(HIDE)mkdir -p $(VO_OUT_DIR)$(shell dirname $<)
$(HIDE)cp -a $< $@
contrib-vo-fixup: contrib-vo $(BCONTEXT)/user-contrib/Ltac2/ltac2_plugin.cmxs
stdlib.timing.diff: $(ALLVO:.$(VO)=.v.timing.diff)
.PHONY: coqlib stdlib-vo contrib-vo contrib-vo-fixup coqlib.timing.diff stdlib.timing.diff
# The .vo files in Init are built with the -noinit option
ifneq (,$(TIMING))
TIMING_EXTRA = > $<.$(TIMING_EXT)
else
TIMING_EXTRA =
endif
# Rules for sources; it is standard to copy them to build dir so we
# work in a "sandbox".
$(VO_OUT_DIR)theories/%.v: theories/%.v | $(VO_OUT_DIR)
$(HIDE)mkdir -p $(VO_OUT_DIR)$(shell dirname $<)
$(HIDE)cp -a $< $@
$(VO_OUT_DIR)user-contrib/%.v: user-contrib/%.v | $(VO_OUT_DIR)
$(HIDE)mkdir -p $(VO_OUT_DIR)$(shell dirname $<)
$(HIDE)cp -a $< $@
$(VO_OUT_DIR)theories/Init/%.vo $(VO_OUT_DIR)theories/Init/%.glob: $(VO_OUT_DIR)theories/Init/%.v $(VO_TOOLS_DEP) | $(VO_OUT_DIR)
$(SHOW)'COQCBOOT theories/Init/$*.v'
$(HIDE)rm -f $(VO_OUT_DIR)theories/Init/$*.glob
$(HIDE)mkdir -p $(shell dirname $<)
$(HIDE)$(BOOTCOQC) $< -o $@ -noinit -R $(VO_OUT_DIR)theories Coq $(TIMING_ARG) $(TIMING_EXTRA)
ifdef NATIVECOMPUTE
$(SHOW)'COQNATIVE $*.vo'
$(HIDE)$(COQNATIVE) $(NATIVEINCLUDES) -coqlib $(VO_OUT_DIR) -R $(VO_OUT_DIR)theories Coq $(VO_OUT_DIR)theories/Init/$*.vo
endif
$(VO_OUT_DIR)theories/Init/%.vio: theories/Init/%.v $(VO_TOOLS_DEP) | $(VO_OUT_DIR)
$(SHOW)'COQC -quick -noinit $<'
$(HIDE)mkdir -p $(VO_OUT_DIR)$(shell dirname $<)
$(HIDE)$(BOOTCOQC) $< -o $@ -noinit -R $(VO_OUT_DIR)theories Coq -vio -noglob
# The general rule for building .vo files :
$(VO_OUT_DIR)%.vo $(VO_OUT_DIR)%.glob: $(VO_OUT_DIR)%.v $(VO_OUT_DIR)theories/Init/Prelude.vo $(VO_TOOLS_DEP) | $(VO_OUT_DIR)
$(SHOW)'COQC $*.v'
$(HIDE)rm -f $*.glob
$(HIDE)mkdir -p $(shell dirname $<)
$(HIDE)$(BOOTCOQC) $< -o $@ $(TIMING_ARG) $(TIMING_EXTRA)
ifdef NATIVECOMPUTE
$(SHOW)'COQNATIVE $*.vo'
$(HIDE)$(COQNATIVE) $(NATIVEINCLUDES) -coqlib $(VO_OUT_DIR) -R $(VO_OUT_DIR)theories Coq $(VO_OUT_DIR)$*.vo
endif
ifdef VALIDATE
$(SHOW)'COQCHK $(call vo_to_mod,$@)'
$(HIDE)$(CHICKEN) $(VALIDOPTS) -norec $(call vo_to_mod,$@) \
|| ( RV=$$?; rm -f "$@"; exit $${RV} )
endif
$(VO_OUT_DIR)%.vio: %.v $(VO_OUT_DIR)theories/Init/Prelude.vio $(VO_TOOLS_DEP)
$(SHOW)'COQC -vio $<'
$(HIDE)mkdir -p $(shell dirname $<)
$(HIDE)$(BOOTCOQC) $< -vio -noglob -o $@
$(VO_OUT_DIR)%.v.timing.diff: %.v.before-timing %.v.after-timing
$(SHOW)'PYTHON TIMING-DIFF $*.v.{before,after}-timing'
$(HIDE)$(MAKE) --no-print-directory print-pretty-single-time-diff BEFORE=$*.v.before-timing AFTER=$*.v.after-timing TIME_OF_PRETTY_BUILD_FILE="$@"
# Dependencies of .v files
ifeq ($(BEST),byte)
DYNDEP=-dyndep byte
else
DYNDEP=-dyndep opt
endif
# can easily produce too long command line with many .v files prefixed by build_vo
# so we use find + xargs to split coqdep invocation if necessary
# OSX sed doesn't support -null-data so can't use -print0
$(VFILED): $(BUILD_VFILES) $(BUILD_MLFILES) $(COQDEP) | all-src
$(SHOW)'COQDEP VFILES'
$(HIDE)find theories $(addprefix user-contrib/, $(USERCONTRIBDIRS)) -type f -name '*.v' | \
sed 's|^|$(VO_OUT_DIR)|' | \
xargs $(COQDEP) -boot $(DYNDEP) -R $(VO_OUT_DIR)theories Coq -Q $(VO_OUT_DIR)user-contrib "" $(PLUGININCLUDES) $(USERCONTRIBINCLUDES) > "$@"
# To speed-up things a bit, let's dissuade make to attempt rebuilding makefiles
Makefile $(wildcard Makefile.*) config/Makefile : ;
# Final catch-all rule.
# Usually, 'make' would display such an error itself.
# But if the target has some declared dependencies (e.g. in a .d)
# but no building rule, 'make' succeeds silently (see bug #4812).
%:
@echo "Error: no rule to make target $@ (or missing .PHONY)" && false
# For emacs:
# Local Variables:
# mode: makefile-gmake
# End: