Makefile.build

##########################################################################
##         #   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
include Makefile.dev

###########################################################################
# 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: