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

-include config/Makefile

###########################################################################
# The SHOW and HIDE variables control whether make will echo complete commands
# or only abbreviated versions.
# Quiet mode is ON by default except if VERBOSE=1 option is given to make

SHOW := $(if $(VERBOSE),@true "",@echo "")
HIDE := $(if $(VERBOSE),,@)

###########################################################################
# Basic build directories
###########################################################################
BCONTEXT=_build/default
CONTEXT=_build/install/default
CBIN=_build/install/default/bin
CSHARE=_build/install/default/share/coq

_DBUILD_DEPS:=

# FLOCK
ifeq (,$(shell command -v flock 2>/dev/null))
FLOCK:=_build/default/tools/flock/coq_flock.exe
_DBUILD_DEPS+=$(FLOCK)

$(FLOCK): tools/flock/coq_flock.ml tools/flock/flock.c
	$(SHOW)'DUNE      $@'
	$(HIDE)dune build $@
else
FLOCK:=flock
endif

# Standard DESTDIR variable as used in Debian and coq_makefile, will
# have make install prefixing all install targets with DESTDIR
DESTDIR ?=

###########################################################################
# VO build directory
###########################################################################

# slash at the end allows us to define this variable as empty, be
# careful, the slash is mandatory.
#
# Note, we can use this as _build/default , but unfortunately dune
# will remove the .vos files as they are not recognized as targets
BUILD_OUT_DIR=_build_vo/default/
VO_OUT_DIR=$(BUILD_OUT_DIR)/lib/coq/

LEGACY_BIN_DIR=bin

$(BUILD_OUT_DIR) $(VO_OUT_DIR):
	$(SHOW)'MKDIR     BUILD_OUT'
	$(HIDE)mkdir -p $(BUILD_OUT_DIR)
	$(HIDE)mkdir -p $(BUILD_OUT_DIR)/lib/coq
	$(HIDE)mkdir -p $(BUILD_OUT_DIR)/lib/coq-core
	$(HIDE)ln -s $(shell pwd)/_build/install/default/bin/ $(LEGACY_BIN_DIR)
	$(HIDE)ln -s $(shell pwd)/_build/install/default/bin/ $(BUILD_OUT_DIR)/bin
	$(HIDE)ln -s $(shell pwd)/_build/default/plugins/ $(BUILD_OUT_DIR)/lib/coq-core
	$(HIDE)ln -s $(shell pwd)/_build/default/tools/ $(BUILD_OUT_DIR)/lib/coq-core
	$(HIDE)ln -s $(shell pwd)/_build/default/kernel/ $(BUILD_OUT_DIR)/lib/coq-core

###########################################################################
# Executables
###########################################################################

ifeq ($(BEST),byte)
  COQC:=$(CBIN)/coqc.byte$(EXE)
  export CAML_LD_LIBRARY_PATH:=$(shell echo $(CONTEXT)/lib/stublibs:$$CAML_LD_LIBRARY_PATH)
else
  COQC:=$(CBIN)/coqc$(EXE)
endif

COQTOPEXE:=$(CBIN)/coqtop$(EXE)
TOPBINOPT:=$(addsuffix .opt$(EXE), $(addprefix $(CBIN)/, coqproofworker coqtacticworker coqqueryworker)) $(COQTOPEXE)
COQDEP:=$(CBIN)/coqdep$(EXE)
DOC_GRAM:=_build/default/doc/tools/docgram/doc_grammar.exe
COQMAKEFILE:=$(CBIN)/coq_makefile$(EXE)
COQMAKEFILEIN:=$(BCONTEXT)/tools/CoqMakefile.in
COQTEX:=$(CBIN)/coq-tex$(EXE)
COQWC:=$(CBIN)/coqwc$(EXE)
COQDOC:=$(CBIN)/coqdoc$(EXE)
COQNATIVE:=$(CBIN)/coqnative$(EXE)
COQDOCSTY:=$(CONTEXT)/lib/coq-core/tools/coqdoc/coqdoc.sty
COQDOCCSS:=$(CONTEXT)/lib/coq-core/tools/coqdoc/coqdoc.css
COQWORKMGR:=$(CBIN)/coqworkmgr$(EXE)
COQMAKE_ONE_TIME_FILE:=tools/make-one-time-file.py
COQTIME_FILE_MAKER:=tools/TimeFileMaker.py
COQMAKE_BOTH_TIME_FILES:=tools/make-both-time-files.py
COQMAKE_BOTH_SINGLE_TIMING_FILES:=tools/make-both-single-timing-files.py
VOTOUR:=$(CBIN)/votour$(EXE)
OCAMLLIBDEP:=$(CBIN)/ocamllibdep$(EXE)
USERCONTRIBDIRS:=Ltac2
CHICKEN:=$(CBIN)/coqchk$(EXE)
TOOLS:=$(VOTOUR) $(COQDOC) $(COQDOCSTY) $(COQDOCCSS) $(COQWC) $(COQMAKEFILE) $(COQMAKEFILEIN) $(COQNATIVE)
CSDPCERT:=$(CBIN)/csdpcert$(EXE)

ifeq ($(origin COQ_SRC_DIR),undefined)
COQ_SRC_DIR=.
endif

COQ_CM_LIBS=coqpp lib clib kernel library engine pretyping gramlib interp printing parsing proofs tactics vernac stm toplevel topbin tools
ML_SOURCE_DIRS=$(addprefix $(COQ_SRC_DIR)/,$(COQ_CM_LIBS))
ALL_ML_SOURCE_FILES=$(shell find $(ML_SOURCE_DIRS) -name '*.ml' -or -name '*.mli' -or -name '*.c' -or -name '*.h')
DOCGRAM_SOURCE_FILES=$(shell find $(addprefix $(COQ_SRC_DIR)/, doc/tools/docgram) -name '*.ml' -or -name '*.mlg')

# Override for developer build [to get warn-as-error for example]
_DDISPLAY?=quiet
_DPROFILE?=$(CONFIGURE_DPROFILE)
_DOPT:=--display=$(_DDISPLAY) $(_DPROFILE)
_DBUILD:=$(FLOCK) .dune.lock dune build $(_DOPT)

# We rerun dune when any of the source files have changed

# touch is needed for all targets in `_build` as make won't track
# symlink's date correctly [and dune won't update the mtime as it
# doesn't use it as the main criteria], so if we didn't touch an
# updated mtime in a source file may not trigger a dune rebuild it it
# didn't change hash, thus the mtime of the target would confuse make.

$(CBIN)/%: $(ALL_ML_SOURCE_FILES) $(_DBUILD_DEPS)
	$(SHOW)'DUNE      $@'
	$(HIDE)$(_DBUILD) $@
	$(HIDE)touch $@

$(CSHARE)/%: $(_DBUILD_DEPS)
	$(SHOW)'DUNE      $@'
	$(HIDE)$(_DBUILD) $@
	$(HIDE)touch $@

ALL_PLUGIN_SOURCE_FILES=$(shell find $(COQ_SRC_DIR)/plugins -name '*.ml' -or -name '*.mli' -or -name '*.mlg') $(ALL_ML_SOURCE_FILES)

_build/default/plugins/%.cmxs: $(ALL_PLUGIN_SOURCE_FILES) $(_DBUILD_DEPS)
	$(SHOW)'DUNE      $@'
	$(HIDE)$(_DBUILD) $@
	$(HIDE)touch $@

_build/default/plugins/%.cma: $(ALL_PLUGIN_SOURCE_FILES) $(_DBUILD_DEPS)
	$(SHOW)'DUNE      $@'
	$(HIDE)$(_DBUILD) $@
	$(HIDE)touch $@

# Only used for the test-suite in local mode
_build/default/tools/%: $(ALL_ML_SOURCE_FILES) $(_DBUILD_DEPS)
	$(SHOW)'DUNE      $@'
	$(HIDE)$(_DBUILD) $@
	$(HIDE)touch $@

_build/install/default/lib/coq-core/plugins/%.cmxs: $(ALL_PLUGIN_SOURCE_FILES) $(_DBUILD_DEPS)
	$(SHOW)'DUNE      $@'
	$(HIDE)$(_DBUILD) $@
	$(HIDE)touch $@

_build/install/default/lib/stublibs/%.so: $(ALL_ML_SOURCE_FILES) $(_DBUILD_DEPS)
	$(SHOW)'DUNE      $@'
	$(HIDE)$(_DBUILD) $@
	$(HIDE)touch $@

_build/install/default/lib/coq/%.cmi: $(ALL_ML_SOURCE_FILES) $(_DBUILD_DEPS)
	$(SHOW)'DUNE      $@'
	$(HIDE)$(_DBUILD) $@
	$(HIDE)touch $@

_build/install/default/lib/coq-core/tools/coqdoc/coqdoc.sty: $(_DBUILD_DEPS)
	$(SHOW)'DUNE      $@'
	$(HIDE)$(_DBUILD) $@
	$(HIDE)touch $@

_build/install/default/lib/coq-core/tools/coqdoc/coqdoc.css: $(_DBUILD_DEPS)
	$(SHOW)'DUNE      $@'
	$(HIDE)$(_DBUILD) $@
	$(HIDE)touch $@

_build/default/%.install: $(_DBUILD_DEPS)
	$(SHOW)'DUNE      $@'
	$(HIDE)$(_DBUILD) $@

ALL_CONTRIB_SOURCE_FILES=$(shell find $(COQ_SRC_DIR)/user-contrib -name '*.ml' -or -name '*.mli' -or -name '*.mlg') $(ALL_PLUGIN_SOURCE_FILES)
_build/default/user-contrib/%.cmxs: $(ALL_CONTRIB_SOURCE_FILES) $(_DBUILD_DEPS)
	$(SHOW)'DUNE      $@'
	$(HIDE)$(_DBUILD) $@
	$(HIDE)touch $@

_build/default/user-contrib/%.cma: $(ALL_CONTRIB_SOURCE_FILES) $(_DBUILD_DEPS)
	$(SHOW)'DUNE      $@'
	$(HIDE)$(_DBUILD) $@
	$(HIDE)touch $@

.PHONY: all-src

ALL_SOURCE_FILES=$(ALL_CONTRIB_SOURCE_FILES) $(ALL_PLUGIN_SOURCE_FILES) $(ALL_ML_SOURCE_FILES)
all-src: $(ALL_SOURCE_FILES) $(_DBUILD_DEPS)
	$(SHOW)'DUNE      sources'
	$(HIDE)$(_DBUILD) @all-src

# For docgram
_build/default/doc/tools/%: $(ALL_ML_SOURCE_FILES) $(DOCGRAM_SOURCE_FILES) $(_DBUILD_DEPS)
	$(SHOW)'DUNE      $@'
	$(HIDE)$(_DBUILD) $@
	$(HIDE)touch $@

PLUGINTUTO := doc/plugin_tutorial

revision: $(_DBUILD_DEPS)
	$(SHOW)'DUNE      $@'
	$(HIDE)$(_DBUILD) $@
	$(HIDE)touch $@

# For emacs:
# Local Variables:
# mode: makefile
# End: