#######################################################################
#  v      #   The Coq Proof Assistant  /  The Coq Development Team    #
# <O___,, #        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              #
#   \VV/  #############################################################
#    //   #      This file is distributed under the terms of the      #
#         #       GNU Lesser General Public License Version 2.1       #
#######################################################################

# This makefile is normally called by the main Makefile after setting
# some variables.

###########################################################################
# Starting rule
###########################################################################

# build the different subsystems: coq, coqide
world: revision coq coqide

###########################################################################
# Includes
###########################################################################

include Makefile.common
include Makefile.doc

ifeq ($(LOCAL),true)
install:
	@echo "Nothing to install in a local build!"
else
install: install-coq install-coqide install-doc-$(WITHDOC)
endif

install-doc-all: install-doc
install-doc-no:

world: doc-$(WITHDOC)
doc-all: doc
doc-no:

.PHONY: world install install-doc-all install-doc-no doc-all doc-no

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

MLFILES:=$(MLSTATICFILES) $(MLEXTRAFILES)

ALLDEPS:=$(addsuffix .d, \
  $(ML4FILES) $(MLFILES) $(MLIFILES) $(CFILES) $(MLLIBFILES) $(VFILES))

.SECONDARY: $(ALLDEPS) $(GENFILES) $(ML4FILES:.ml4=.ml)

# NOTA: the -include below will lauch the build of all .d. Some of them
# will _fail_ at first, this is to be expected (no grammar.cma initially).
# These errors (see below "not ready yet") do not discourage make to
# try again and finally succeed.

-include $(ALLDEPS)


###########################################################################
# Compilation options
###########################################################################

# Variables meant to be modifiable via the command-line of make

VERBOSE=
NO_RECOMPILE_ML4=
NO_RECALC_DEPS=
READABLE_ML4=	# non-empty means .ml of .ml4 will be ascii instead of binary
VALIDATE=
COQ_XML=	# is "-xml" when building XML library
VM=		# is "-no-vm" to not use the vm"

TIMED=          # non-empty will activate a default time command
                # when compiling .v (see $(STDTIME) below)

TIMECMD=	# if you prefer a specific time command instead of $(STDTIME)
                # e.g. "'time -p'"

# NB: if you want to collect compilation timings of .v and import them
# in a spreadsheet, I suggest something like:
#   make TIMED=1 2> timings.csv

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

STDTIME=/usr/bin/time -f "$* (user: %U mem: %M ko)"
TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))

COQOPTS=$(COQ_XML) $(VM)
BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile

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

LOCALINCLUDES=$(addprefix -I , $(SRCDIRS) )
MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
COREMLINCLUDES=$(addprefix -I , $(CORESRCDIRS)) -I $(MYCAMLP4LIB)

OCAMLC := $(TYPEREX) $(OCAMLC) $(CAMLFLAGS)
OCAMLOPT := $(TYPEREX) $(OCAMLOPT) $(CAMLFLAGS)

BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG) $(USERFLAGS)
OPTFLAGS=$(MLINCLUDES) $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS)
COREBYTEFLAGS=$(COREMLINCLUDES) $(CAMLDEBUG) $(USERFLAGS)
COREOPTFLAGS=$(COREMLINCLUDES) $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS)
DEPFLAGS= -slash $(LOCALINCLUDES)

define bestocaml
$(if $(OPT),\
$(OCAMLOPT) $(OPTFLAGS) -o $@ $(1) $(addsuffix .cmxa,$(2)) $^ && $(STRIP) $@,\
$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ $(1) $(addsuffix .cma,$(2)) $^)
endef

CAMLP4DEPS=$(shell LC_ALL=C sed -n -e 's@^(\*.*camlp4deps: "\(.*\)".*@\1@p' $(1) \#))
ifeq ($(CAMLP4),camlp5)
CAMLP4USE=pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION)
else
CAMLP4USE=-D$(CAMLVERSION)
endif

PR_O := $(if $(READABLE_ML4),pr_o.cmo,pr_dump.cmo) # works also with new camlp4

ifeq ($(CAMLP4),camlp5)
SYSMOD:=str unix gramlib
else
SYSMOD:=str unix dynlink camlp4lib
endif

SYSCMA:=$(addsuffix .cma,$(SYSMOD))
SYSCMXA:=$(addsuffix .cmxa,$(SYSMOD))


###########################################################################
# Infrastructure for the rest of the Makefile
###########################################################################

define order-only-template
 ifeq "order-only" "$(1)"
   ORDER_ONLY_SEP:=|
 endif
endef

$(foreach f,$(.FEATURES),$(eval $(call order-only-template,$(f))))

ifndef ORDER_ONLY_SEP
$(error This Makefile needs GNU Make 3.81 or later (that is a version that supports the order-only dependency feature without major bugs.))
endif

VO_TOOLS_DEP := $(COQTOPEXE)
ifdef COQ_XML
 VO_TOOLS_DEP += $(COQDOC)
endif
ifdef VALIDATE
 VO_TOOLS_DEP += $(CHICKEN)
endif

ifdef NO_RECALC_DEPS
  D_DEPEND_BEFORE_SRC:=|
  D_DEPEND_AFTER_SRC:=
else
  D_DEPEND_BEFORE_SRC:=
  D_DEPEND_AFTER_SRC:=|
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 macro:

TOTARGET = > "$@" || (RV=$$?; rm -f "$@"; exit $${RV})

###########################################################################
# Compilation option for .c files 
###########################################################################

CINCLUDES= -I $(CAMLHLIB)

# libcoqrun.a, dllcoqrun.so

# NB: We used to do a ranlib after ocamlmklib, but it seems that
# ocamlmklib is already doing it

$(LIBCOQRUN): kernel/byterun/coq_jumptbl.h $(BYTERUN) 
	cd $(dir $(LIBCOQRUN)) && \
	$(OCAMLMKLIB) -oc $(COQRUN) $(foreach u,$(BYTERUN),$(notdir $(u)))

#coq_jumptbl.h is required only if you have GCC 2.0 or later
kernel/byterun/coq_jumptbl.h : kernel/byterun/coq_instruct.h
	sed -n -e '/^  /s/ \([A-Z]\)/ \&\&coq_lbl_\1/gp' \
               -e '/^}/q' $< $(TOTARGET)

kernel/copcodes.ml: kernel/byterun/coq_instruct.h
	sed -n -e '/^enum/p' -e 's/,//g' -e '/^  /p' $< | \
	awk -f kernel/make-opcodes $(TOTARGET)

###########################################################################
# Main targets (coqmktop, coqtop.opt, coqtop.byte)
###########################################################################

.PHONY: coqbinaries coq coqlib coqlight states

coqbinaries:: ${COQBINARIES} ${CSDPCERT} ${FAKEIDE}

coq: coqlib tools coqbinaries

coqlib:: theories plugins

coqlight: theories-light tools coqbinaries

states: theories/Init/Prelude.vo

miniopt: $(COQTOPEXE) pluginsopt
minibyte: $(COQTOPBYTE) pluginsbyte

ifeq ($(BEST),opt)
$(COQTOPEXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN)
	$(SHOW)'COQMKTOP -o $@'	
	$(HIDE)$(COQMKTOP) -boot -opt $(COREOPTFLAGS) -o $@
	$(STRIP) $@
else
$(COQTOPEXE): $(COQTOPBYTE)
	cp $< $@
endif

$(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN)
	$(SHOW)'COQMKTOP -o $@'	
	$(HIDE)$(COQMKTOP) -boot -top $(COREBYTEFLAGS) -o $@

LOCALCHKLIBS:=$(addprefix -I , $(CHKSRCDIRS) )
CHKLIBS:=$(LOCALCHKLIBS) -I $(MYCAMLP4LIB)
CHKBYTEFLAGS:=$(CHKLIBS) $(CAMLDEBUG) $(USERFLAGS)
CHKOPTFLAGS:=$(CHKLIBS) $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS)

ifeq ($(BEST),opt)
$(CHICKEN): checker/check.cmxa checker/main.ml
	$(SHOW)'OCAMLOPT -o $@'
	$(HIDE)$(OCAMLOPT) $(CHKOPTFLAGS) -o $@ $(SYSCMXA) $^
	$(STRIP) $@
else
$(CHICKEN): $(CHICKENBYTE)
	cp $< $@
endif

$(CHICKENBYTE): checker/check.cma checker/main.ml
	$(SHOW)'OCAMLC -o $@'
	$(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ $(SYSCMA) $^

# coqmktop
$(COQMKTOP): $(patsubst %.cma,%$(BESTLIB),$(COQMKTOPCMO:.cmo=$(BESTOBJ)))
	$(SHOW)'OCAMLBEST -o $@'
	$(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD))

scripts/tolink.ml: Makefile.build Makefile.common
	$(SHOW)"ECHO... >" $@
	$(HIDE)echo "let copts = \"-cclib -lcoqrun\"" > $@
	$(HIDE)echo "let core_libs = \""$(LINKCMO)"\"" >> $@
	$(HIDE)echo "let core_objs = \""$(OBJSMOD)"\"" >> $@

# coqc
$(COQC):  $(patsubst %.cma,%$(BESTLIB),$(COQCCMO:.cmo=$(BESTOBJ)))
	$(SHOW)'OCAMLBEST -o $@'
	$(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD))

# target for libraries

%.cma: | %.mllib.d
	$(SHOW)'OCAMLC -a -o $@'
	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $^

%.cmxa: | %.mllib.d
	$(SHOW)'OCAMLOPT -a -o $@'
	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $^

# For the checker, different flags may be used

checker/check.cma: | checker/check.mllib.d
	$(SHOW)'OCAMLC -a -o $@'
	$(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) -a -o $@ $^

checker/check.cmxa: | checker/check.mllib.d
	$(SHOW)'OCAMLOPT -a -o $@'
	$(HIDE)$(OCAMLOPT) $(CHKOPTFLAGS) -a -o $@ $^

###########################################################################
# Csdp to micromega special targets
###########################################################################

plugins/micromega/csdpcert$(EXE): $(CSDPCERTCMO:.cmo=$(BESTOBJ))
	$(SHOW)'OCAMLBEST -o $@'
	$(HIDE)$(call bestocaml,,nums unix)

###########################################################################
# CoqIde special targets
###########################################################################

.PHONY: coqide coqide-binaries coqide-no coqide-byte coqide-opt coqide-files

# target to build CoqIde
coqide:: coqide-files coqide-binaries theories/Init/Prelude.vo

COQIDEFLAGS=-thread $(COQIDEINCLUDES)

.SUFFIXES:.vo

IDEFILES=ide/coq.lang ide/coq_style.xml ide/coq.png ide/mac_default_accel_map

coqide-binaries: coqide-$(HASCOQIDE)
coqide-no:
coqide-byte: $(COQIDEBYTE) $(COQIDE)
coqide-opt:  $(COQIDEBYTE) $(COQIDE)
coqide-files: $(IDEFILES)

ifeq ($(HASCOQIDE),opt)
$(COQIDE): $(LINKIDEOPT) | $(COQTOPEXE)
	$(SHOW)'OCAMLOPT -o $@'
	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ unix.cmxa threads.cmxa \
		lablgtk.cmxa lablgtksourceview2.cmxa $(IDEOPTFLAGS) gtkThread.cmx \
		str.cmxa $(LINKIDEOPT)
	$(STRIP) $@
else
$(COQIDE): $(COQIDEBYTE)
	cp $< $@
endif

$(COQIDEBYTE): $(LINKIDE) | $(COQTOPBYTE)
	$(SHOW)'OCAMLC -o $@'
	$(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ unix.cma threads.cma lablgtk.cma\
	        lablgtksourceview2.cma gtkThread.cmo str.cma $(COQRUNBYTEFLAGS) $(LINKIDE)

# install targets

.PHONY: install-coqide install-ide-no install-ide-byte install-ide-opt
.PHONY: install-ide-files install-ide-info install-im install-ide-devfiles

ifeq ($(HASCOQIDE),no)
install-coqide:
else
install-coqide: install-ide-bin install-ide-files install-ide-info install-ide-devfiles
endif

install-ide-bin:
	$(MKDIR) $(FULLBINDIR)
	$(INSTALLBIN) $(COQIDE) $(FULLBINDIR)

install-ide-devfiles:
	$(MKDIR) $(FULLCOQLIB)
	$(INSTALLSH) $(FULLCOQLIB) $(IDECMA) \
	  $(foreach lib,$(IDECMA:.cma=_MLLIB_DEPENDENCIES),$(addsuffix .cmi,$($(lib))))
ifeq ($(BEST),opt)
	$(INSTALLSH) $(FULLCOQLIB) $(IDECMA:.cma=.cmxa) $(IDECMA:.cma=.a)
endif

install-ide-files:
	$(MKDIR) $(FULLDATADIR)
	$(INSTALLLIB) ide/coq.png ide/coq.lang ide/coq_style.xml $(FULLDATADIR)
	$(MKDIR) $(FULLCONFIGDIR)
	if [ $(IDEOPTINT) = QUARTZ ] ; then $(INSTALLLIB) ide/mac_default_accel_map $(FULLCONFIGDIR)/coqide.keys ; fi

install-ide-info:
	$(MKDIR) $(FULLDOCDIR)
	$(INSTALLLIB) ide/FAQ $(FULLDOCDIR)/FAQ-CoqIde

###########################################################################
# tests
###########################################################################

.PHONY: validate check test-suite $(ALLSTDLIB).v

VALIDOPTS=-silent -o -m

validate:: $(CHICKEN) $(ALLVO)
	$(SHOW)'COQCHK <theories & plugins>'
	$(HIDE)$(CHICKEN) -boot $(VALIDOPTS) $(ALLMODS)

$(ALLSTDLIB).v:
	$(SHOW)'MAKE $(notdir $@)'
	$(HIDE)echo "Require $(ALLMODS)." > $@

MAKE_TSOPTS=-C test-suite -s VERBOSE=$(VERBOSE)

check:: validate test-suite

test-suite: world $(ALLSTDLIB).v
	$(MAKE) $(MAKE_TSOPTS) clean
	$(MAKE) $(MAKE_TSOPTS) all
	$(HIDE)if grep -F 'Error!' test-suite/summary.log ; then false; fi

##################################################################
# partial targets: 1) core ML parts
##################################################################

.PHONY: lib kernel byterun library proofs tactics interp parsing pretyping
.PHONY: highparsing toplevel hightactics

lib: lib/clib.cma lib/lib.cma
kernel: kernel/kernel.cma
byterun: $(BYTERUN)
library: library/library.cma
proofs: proofs/proofs.cma
tactics: tactics/tactics.cma
interp: interp/interp.cma
parsing: parsing/parsing.cma
pretyping: pretyping/pretyping.cma
highparsing: parsing/highparsing.cma
toplevel: toplevel/toplevel.cma
hightactics: tactics/hightactics.cma

###########################################################################
# 2) theories and plugins files
###########################################################################

.PHONY: init theories theories-light
.PHONY: logic arith bool narith zarith qarith lists strings sets
.PHONY: fsets relations wellfounded reals setoids sorting numbers noreal

init: $(INITVO)

theories: $(THEORIESVO)
theories-light: $(THEORIESLIGHTVO)

logic: $(LOGICVO)
arith: $(ARITHVO)
bool: $(BOOLVO)
narith: $(NARITHVO)
zarith: $(ZARITHVO)
qarith: $(QARITHVO)
lists: $(LISTSVO)
strings: $(STRINGSVO)
sets: $(SETSVO)
fsets: $(FSETSVO)
relations: $(RELATIONSVO)
wellfounded: $(WELLFOUNDEDVO)
reals: $(REALSVO)
setoids: $(SETOIDSVO)
sorting: $(SORTINGVO)
numbers: $(NUMBERSVO)
unicode: $(UNICODEVO)
classes: $(CLASSESVO)
program: $(PROGRAMVO)
structures: $(STRUCTURESVO)
vectors: $(VECTORSVO)

noreal: unicode logic arith bool zarith qarith lists sets fsets \
	relations wellfounded setoids sorting

###########################################################################
# 3) plugins
###########################################################################

.PHONY: plugins omega micromega setoid_ring nsatz xml extraction
.PHONY: fourier funind cc rtauto btauto pluginsopt pluginsbyte

plugins: $(PLUGINSVO)
omega: $(OMEGAVO) $(OMEGACMA) $(ROMEGAVO) $(ROMEGACMA)
micromega: $(MICROMEGAVO) $(MICROMEGACMA) $(CSDPCERT)
setoid_ring: $(RINGVO) $(RINGCMA)
nsatz: $(NSATZVO) $(NSATZCMA)
xml: $(XMLVO) $(XMLCMA)
extraction: $(EXTRACTIONCMA)
fourier: $(FOURIERVO) $(FOURIERCMA)
funind: $(FUNINDCMA) $(FUNINDVO)
cc: $(CCVO) $(CCCMA)
rtauto: $(RTAUTOVO) $(RTAUTOCMA)
btauto: $(BTAUTOVO) $(BTAUTOCMA)

pluginsopt: $(PLUGINSOPT)
pluginsbyte: $(PLUGINS)

###########################################################################
# rules to make theories and plugins
###########################################################################

theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_DEP) | theories/Init/%.v.d
	$(SHOW)'COQC -noinit $<'
	$(HIDE)rm -f theories/Init/$*.glob
	$(HIDE)$(BOOTCOQC) theories/Init/$* -noinit

theories/Numbers/Natural/BigN/NMake_gen.v: theories/Numbers/Natural/BigN/NMake_gen.ml
	$(OCAML) $< $(TOTARGET)

###########################################################################
# tools
###########################################################################

.PHONY: printers tools

printers: $(DEBUGPRINTERS)

tools:: $(TOOLS) $(DEBUGPRINTERS) $(COQDEPBOOT)

# coqdep_boot : a basic version of coqdep, with almost no dependencies.

# Here it is important to mention .ml files instead of .cmo in order
# to avoid using implicit rules and hence .ml.d files that would need
# coqdep_boot.

COQDEPBOOTSRC:= \
  tools/coqdep_lexer.mli tools/coqdep_lexer.ml \
  tools/coqdep_common.mli tools/coqdep_common.ml \
  tools/coqdep_boot.ml

$(COQDEPBOOT): $(COQDEPBOOTSRC)
	$(SHOW)'OCAMLBEST -o $@'
	$(HIDE)$(call bestocaml, -I tools, unix)

# the full coqdep

$(COQDEP): $(patsubst %.cma,%$(BESTLIB),$(COQDEPCMO:.cmo=$(BESTOBJ)))
	$(SHOW)'OCAMLBEST -o $@'
	$(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD))

$(GALLINA): $(addsuffix $(BESTOBJ), tools/gallina_lexer tools/gallina)
	$(SHOW)'OCAMLBEST -o $@'
	$(HIDE)$(call bestocaml,,)

$(COQMAKEFILE):  $(patsubst %.cma,%$(BESTLIB),$(COQMAKEFILECMO:.cmo=$(BESTOBJ)))
	$(SHOW)'OCAMLBEST -o $@'
	$(HIDE)$(call bestocaml,,str unix)

$(COQTEX): tools/coq_tex$(BESTOBJ)
	$(SHOW)'OCAMLBEST -o $@'
	$(HIDE)$(call bestocaml,,str)

$(COQWC): tools/coqwc$(BESTOBJ)
	$(SHOW)'OCAMLBEST -o $@'
	$(HIDE)$(call bestocaml,,)

$(COQDOC): $(patsubst %.cma,%$(BESTLIB),$(COQDOCCMO:.cmo=$(BESTOBJ)))
	$(SHOW)'OCAMLBEST -o $@'
	$(HIDE)$(call bestocaml,,str unix)

# fake_ide : for debugging or test-suite purpose, a fake ide simulating
# a connection to coqtop -ideslave

$(FAKEIDE): lib/xml_lexer$(BESTOBJ) lib/xml_parser$(BESTOBJ) lib/xml_utils$(BESTOBJ) lib/serialize$(BESTOBJ) tools/fake_ide$(BESTOBJ)
	$(SHOW)'OCAMLBEST -o $@'
	$(HIDE)$(call bestocaml,,unix)

# Special rule for the compatibility-with-camlp5 extension for camlp4

ifeq ($(CAMLP4),camlp4)
tools/compat5.cmo: tools/compat5.mlp
	$(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) -impl' -impl $<
tools/compat5b.cmo: tools/compat5b.mlp
	$(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) -impl' -impl $<
else
tools/compat5.cmo: tools/compat5.ml
	$(OCAMLC) -c $<
tools/compat5b.cmo: tools/compat5b.ml
	$(OCAMLC) -c $<
endif

###########################################################################
# Installation
###########################################################################

#These variables are intended to be set by the caller to make
#COQINSTALLPREFIX=
#OLDROOT=

  # Can be changed for a local installation (to make packages).
  # You must NOT put a "/" at the end (Cygnus for win32 does not like "//").

ifdef COQINSTALLPREFIX
FULLBINDIR=$(BINDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
FULLCOQLIB=$(COQLIBINSTALL:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
FULLCONFIGDIR=$(CONFIGDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
FULLDATADIR=$(DATADIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
FULLMANDIR=$(MANDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
FULLEMACSLIB=$(EMACSLIB:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
FULLCOQDOCDIR=$(COQDOCDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
FULLDOCDIR=$(DOCDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
else
FULLBINDIR=$(BINDIR)
FULLCOQLIB=$(COQLIBINSTALL)
FULLCONFIGDIR=$(CONFIGDIR)
FULLDATADIR=$(DATADIR)
FULLMANDIR=$(MANDIR)
FULLEMACSLIB=$(EMACSLIB)
FULLCOQDOCDIR=$(COQDOCDIR)
FULLDOCDIR=$(DOCDIR)
endif

.PHONY: install-coq install-coqlight install-binaries install-byte install-opt
.PHONY: install-tools install-library install-library-light install-devfiles
.PHONY: install-coq-info install-coq-manpages install-emacs install-latex

install-coq: install-binaries install-library install-coq-info install-devfiles
install-coqlight: install-binaries install-library-light

install-binaries: install-tools
	$(MKDIR) $(FULLBINDIR)
	$(INSTALLBIN) $(COQC) $(COQTOPBYTE) $(COQTOPEXE) $(CHICKEN) $(FULLBINDIR)

install-tools::
	$(MKDIR) $(FULLBINDIR)
	# recopie des fichiers de style pour coqide
	$(MKDIR) $(FULLCOQLIB)/tools/coqdoc
	touch $(FULLCOQLIB)/tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc/coqdoc.css # to have the mode according to umask (bug #1715)
	$(INSTALLLIB) tools/coqdoc/coqdoc.css tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc
	$(INSTALLBIN) $(TOOLS) $(FULLBINDIR)

# The list of .cmi to install, including the ones obtained
# from .mli without .ml, and the ones obtained from .ml without .mli

INSTALLCMI = $(sort \
	$(CONFIG:.cmo=.cmi) \
	$(filter-out checker/% ide/% tools/%, $(MLIFILES:.mli=.cmi)) \
	$(foreach lib,$(CORECMA) $(PLUGINSCMA), $(addsuffix .cmi,$($(lib:.cma=_MLLIB_DEPENDENCIES)))))

install-devfiles:
	$(MKDIR) $(FULLBINDIR)
	$(INSTALLBIN) $(COQMKTOP) $(FULLBINDIR)
	$(MKDIR) $(FULLCOQLIB)
	$(INSTALLSH)  $(FULLCOQLIB) $(LINKCMO) $(GRAMMARCMA)
	$(INSTALLSH)  $(FULLCOQLIB) $(INSTALLCMI)
ifeq ($(BEST),opt)
	$(INSTALLSH)  $(FULLCOQLIB) $(LINKCMX) $(CONFIG:.cmo=.o) $(CORECMA:.cma=.a) $(STATICPLUGINS:.cma=.a)
endif

install-library:
	$(MKDIR) $(FULLCOQLIB)
	$(INSTALLSH) $(FULLCOQLIB) $(LIBFILES) $(PLUGINS)
	$(MKDIR) $(FULLCOQLIB)/user-contrib
	$(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB)
ifeq ($(BEST),opt)
	$(INSTALLLIB) $(LIBCOQRUN) $(FULLCOQLIB)
	$(INSTALLSH) $(FULLCOQLIB) $(PLUGINSOPT)
endif
# csdpcert is not meant to be directly called by the user; we install
# it with libraries
	-$(MKDIR) $(FULLCOQLIB)/plugins/micromega
	$(INSTALLBIN) $(CSDPCERT) $(FULLCOQLIB)/plugins/micromega
	rm -f $(FULLCOQLIB)/revision
	-$(INSTALLLIB) revision $(FULLCOQLIB)

install-library-light:
	$(MKDIR) $(FULLCOQLIB)
	$(INSTALLSH) $(FULLCOQLIB) $(LIBFILESLIGHT) $(INITPLUGINS)
	rm -f $(FULLCOQLIB)/revision
	-$(INSTALLLIB) revision $(FULLCOQLIB)
ifeq ($(BEST),opt)
	$(INSTALLSH)  $(FULLCOQLIB) $(INITPLUGINSOPT)
endif

install-coq-info: install-coq-manpages install-emacs install-latex

install-coq-manpages:
	$(MKDIR) $(FULLMANDIR)/man1
	$(INSTALLLIB) $(MANPAGES) $(FULLMANDIR)/man1

install-emacs:
	$(MKDIR) $(FULLEMACSLIB)
	$(INSTALLLIB) tools/coq-db.el tools/coq-font-lock.el tools/coq-syntax.el tools/coq.el tools/coq-inferior.el $(FULLEMACSLIB)

# command to update TeX' kpathsea database
#UPDATETEX = $(MKTEXLSR) /usr/share/texmf /var/spool/texmf $(BASETEXDIR) > /dev/null

install-latex:
	$(MKDIR) $(FULLCOQDOCDIR)
	$(INSTALLLIB) tools/coqdoc/coqdoc.sty $(FULLCOQDOCDIR)	
#	-$(UPDATETEX)

###########################################################################
# Documentation of the source code (using ocamldoc)
###########################################################################

.PHONY: source-doc mli-doc ml-doc

source-doc: mli-doc $(OCAMLDOCDIR)/coq.pdf

$(OCAMLDOCDIR)/coq.tex:: $(DOCMLIS:.mli=.cmi)
	$(OCAMLDOC) -latex -rectypes -I $(MYCAMLP4LIB) $(MLINCLUDES)\
	$(DOCMLIS) -t "Coq mlis documentation" \
	-intro $(OCAMLDOCDIR)/docintro -o $@

mli-doc:: $(DOCMLIS:.mli=.cmi)
	$(OCAMLDOC) -html -rectypes -I $(MYCAMLP4LIB) $(MLINCLUDES)\
	$(DOCMLIS) -d $(OCAMLDOCDIR)/html -colorize-code \
	-t "Coq mlis documentation" -intro $(OCAMLDOCDIR)/docintro \
	-css-style style.css

ml-dot:: $(MLEXTRAFILES)
	$(OCAMLDOC) -dot -dot-reduce -rectypes -I $(CAMLLIB) -I $(MYCAMLP4LIB) $(MLINCLUDES)\
	$(filter $(addsuffix /%.ml,$(CORESRCDIRS)),$(MLFILES)) -o $(OCAMLDOCDIR)/coq.dot

%_dep.png: %.dot
	$(DOT) -Tpng $< -o $@

%_types.dot: %.mli
	$(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -dot-types -o $@ $< 

OCAMLDOC_MLLIBD = $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ \
  $(foreach lib,$(|:.mllib.d=_MLLIB_DEPENDENCIES),$(addsuffix .ml,$($(lib))))

%.dot: | %.mllib.d
	$(OCAMLDOC_MLLIBD)

ml-doc:
	$(OCAMLDOC) -html -rectypes $(LOCALINCLUDES) -d $(SOURCEDOCDIR) $(MLSTATICFILES)

parsing/parsing.dot : | parsing/parsing.mllib.d parsing/highparsing.mllib.d
	$(OCAMLDOC_MLLIBD)

grammar/grammar.dot : | grammar/grammar.mllib.d
	$(OCAMLDOC_MLLIBD)

tactics/tactics.dot: | tactics/tactics.mllib.d tactics/hightactics.mllib.d
	$(OCAMLDOC_MLLIBD)

%.dot: %.mli
	$(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $< 

$(OCAMLDOCDIR)/%.pdf: $(OCAMLDOCDIR)/%.tex
	(cd $(OCAMLDOCDIR) ; pdflatex $*.tex && pdflatex $*.tex)

###########################################################################
### Special rules
###########################################################################

dev/printers.cma: | dev/printers.mllib.d
	$(SHOW)'Testing $@'
	$(HIDE)$(OCAMLC) $(BYTEFLAGS) $(SYSCMA) $^ -o test-printer
	@rm -f test-printer
	$(SHOW)'OCAMLC -a $@'   
	$(HIDE)$(OCAMLC) $(BYTEFLAGS) $^ -linkall -a -o $@

grammar/grammar.cma: | grammar/grammar.mllib.d
	$(SHOW)'Testing $@'
	@touch test.ml4
	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp '$(CAMLP4O) -I $(CAMLLIB) $^ -impl' -impl test.ml4 -o test-grammar
	@rm -f test-grammar test.*
	$(SHOW)'OCAMLC -a $@'   
	$(HIDE)$(OCAMLC) $(BYTEFLAGS) $^ -linkall -a -o $@

# toplevel/mltop.ml4 (ifdef Byte)

## NB: mltop.ml correspond to the byte version (and hence need no special rules)
## while the opt version is in mltop.optml. Since mltop.optml uses mltop.ml.d
## as dependency file, be sure to import the same modules in the different sections
## of the ml4

toplevel/mltop.cmx: toplevel/mltop.optml | toplevel/mltop.ml.d toplevel/mltop.ml4.d
	$(SHOW)'OCAMLOPT  $<'
	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -c -impl $< -o $@

toplevel/mltop.ml: toplevel/mltop.ml4 config/Makefile # no camlp4deps here
	$(SHOW)'CAMLP4O   $<'
	$(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) -DByte -DHasDynlink -impl $< -o $@

toplevel/mltop.optml: toplevel/mltop.ml4 config/Makefile # no camlp4deps here
	$(SHOW)'CAMLP4O   $<'
	$(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) $(NATDYNLINKDEF) -impl $< -o $@

ide/coqide_main.ml: ide/coqide_main.ml4
	$(SHOW)'CAMLP4O   $<'
	$(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) -impl $< -o $@

ide/coqide_main_opt.ml: ide/coqide_main.ml4 config/Makefile # no camlp4deps here
	$(SHOW)'CAMLP4O   $<'
	$(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) -D$(IDEOPTINT) -impl $< -o $@


# pretty printing of the revision number when compiling a checked out
# source tree
.PHONY: revision

revision:
	$(SHOW)'CHECK revision'
	$(HIDE)rm -f revision.new
ifeq ($(CHECKEDOUT),svn)
	$(HIDE)set -e; \
        if test -x "`which svn`"; then \
	  export LC_ALL=C;\
	  svn info . | sed -ne '/URL/s/.*\/\([^\/]\{1,\}\)/\1/p' > revision.new; \
	  svn info . | sed -ne '/Revision/s/Revision: \([0-9]\{1,\}\)/\1/p'>> revision.new; \
	fi
endif
ifeq ($(CHECKEDOUT),gnuarch)
	$(HIDE)set -e; \
        if test -x "`which tla`"; then \
	  LANG=C; export LANG; \
	  tla tree-version  >  revision.new ; \
	  tla tree-revision | sed -ne 's|.*--||p' >> revision.new ; \
	fi
endif
ifeq ($(CHECKEDOUT),git)
	$(HIDE)set -e; \
	if test -x "`which git`"; then \
	  LANG=C; export LANG; \
	  GIT_BRANCH=$$(git branch -a | sed -ne '/^\* /s/^\* \(.*\)/\1/p'); \
	  GIT_HOST=$$(hostname); \
	  GIT_PATH=$$(pwd); \
	  (echo "$${GIT_HOST}:$${GIT_PATH},$${GIT_BRANCH}") > revision.new; \
	  (echo "$$(git log -1 --pretty='format:%H')") >> revision.new; \
	fi
endif
	$(HIDE)set -e; \
	if test -e revision.new; then \
          if test -e revision; then \
	    if test "`cat revision`" = "`cat revision.new`" ; then \
	       rm -f revision.new; \
            else \
               mv -f revision.new revision; \
            fi; \
          else \
            mv -f revision.new revision; \
          fi \
	fi

###########################################################################
# Default rules
###########################################################################

## Three flavor of flags: checker/* ide/* and normal files

COND_BYTEFLAGS= \
 $(if $(filter checker/%,$<), $(CHKBYTEFLAGS), \
   $(if $(filter ide/%,$<),$(COQIDEFLAGS),) $(BYTEFLAGS))

COND_OPTFLAGS= \
 $(if $(filter checker/%,$<), $(CHKOPTFLAGS), \
   $(if $(filter ide/%,$<),$(COQIDEFLAGS),) $(OPTFLAGS))

%.o: %.c
	$(SHOW)'OCAMLC    $<'
	$(HIDE)cd $(dir $<) && $(OCAMLC) -ccopt "$(CFLAGS)" -c $(notdir $<)

%.cmi: %.mli | %.mli.d
	$(SHOW)'OCAMLC    $<'
	$(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -c $<

%.cmo: %.ml | %.ml.d
	$(SHOW)'OCAMLC    $<'
	$(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -c $<

## NB: for the moment ocamlopt erases and recreates .cmi if there's no .mli around.
## This can lead to nasty things with make -j. To avoid that:
##  1) We make .cmx always depend on .cmi
##  2) This .cmi will be created from the .mli, or trigger the compilation of the
##    .cmo if there's no .mli (see rule below about MLWITHOUTMLI)
##  3) We tell ocamlopt to use the .cmi as the interface source file. With this
##     hack, everything goes as if there is a .mli, and the .cmi is preserved
##     and the .cmx is checked with respect to this .cmi

HACKMLI = $(if $(wildcard $<i),,-intf-suffix .cmi)

define diff
 $(strip $(foreach f, $(1), $(if $(filter $(f),$(2)),,$f)))
endef

MLWITHOUTMLI := $(call diff, $(MLFILES), $(MLIFILES:.mli=.ml))

$(MLWITHOUTMLI:.ml=.cmx): %.cmx: %.cmi  # for .ml with .mli this is already the case

$(MLWITHOUTMLI:.ml=.cmi): %.cmi: %.cmo

%.cmx: %.ml | %.ml.d
	$(SHOW)'OCAMLOPT  $<'
	$(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) -c $<

%.cmxs: %.cmxa
	$(SHOW)'OCAMLOPT -shared -o $@'
ifeq ($(HASNATDYNLINK),os5fixme)
	$(HIDE)dev/ocamlopt_shared_os5fix.sh "$(OCAMLOPT)" $@
else
	$(HIDE)$(OCAMLOPT) -linkall -shared -o $@ $<
endif

%.cmxs: %.cmx
	$(SHOW)'OCAMLOPT -shared -o $@'
	$(HIDE)$(OCAMLOPT) -shared -o $@ $<

%.ml: %.mll
	$(SHOW)'OCAMLLEX  $<'
	$(HIDE)$(OCAMLLEX) -o $@ "$*.mll"

%.ml %.mli: %.mly
	$(SHOW)'OCAMLYACC $<'
	$(HIDE)$(OCAMLYACC) $<

plugins/%_mod.ml: plugins/%.mllib
	$(SHOW)'ECHO... > $@'
	$(HIDE)sed -e "s/\([^ ]\{1,\}\)/let _=Mltop.add_known_module\"\1\" /g" $< > $@
	$(HIDE)echo "let _=Mltop.add_known_module\"$(notdir $*)\"" >> $@

# NB: compatibility modules for camlp4: 
# - tools/compat5.cmo changes GEXTEND into EXTEND. Safe, always loaded
# - tools/compat5b.cmo changes EXTEND into EXTEND Gram. Interact badly with
#    syntax such that VERNAC EXTEND, we only load it for a few files via camlp4deps

%.ml: %.ml4 | %.ml4.d tools/compat5.cmo tools/compat5b.cmo
	$(SHOW)'CAMLP4O   $<'
	$(HIDE)\
	DEPS="$(call CAMLP4DEPS,$<)"; \
	if ls $${DEPS} > /dev/null 2>&1; then \
	$(CAMLP4O) $(PR_O) -I $(CAMLLIB) tools/compat5.cmo $${DEPS} $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< -o $@; \
	else echo $< : Dependency $${DEPS} not ready yet; false; fi

%.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP) | %.v.d
	$(SHOW)'COQC      $<'
	$(HIDE)rm -f $*.glob 
	$(HIDE)$(BOOTCOQC) $*
ifdef VALIDATE
	$(SHOW)'COQCHK    $(call vo_to_mod,$@)'
	$(HIDE)$(CHICKEN) -boot -silent -norec $(call vo_to_mod,$@) \
	  || ( RV=$$?; rm -f "$@"; exit $${RV} )
endif

###########################################################################
# Dependencies
###########################################################################

# .ml4.d contains the dependencies to generate the .ml from the .ml4
# NOT to generate object code.

%.ml4.d: $(D_DEPEND_BEFORE_SRC) %.ml4
	$(SHOW)'CAMLP4DEPS $<'
	$(HIDE)echo "$*.ml: $(if $(NO_RECOMPILE_ML4),$(ORDER_ONLY_SEP)) $(call CAMLP4DEPS,$<)" $(TOTARGET)

# We now use coqdep_boot to wrap around ocamldep -modules, since it is aware
# of .ml4 files

OCAMLDEP_NG = $(COQDEPBOOT) -mldep $(OCAMLDEP)

checker/%.ml.d: $(D_DEPEND_BEFORE_SRC) checker/%.ml $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES)
	$(SHOW)'OCAMLDEP  $<'
	$(HIDE)$(OCAMLDEP_NG) -slash $(LOCALCHKLIBS) "$<" $(TOTARGET)

checker/%.mli.d: $(D_DEPEND_BEFORE_SRC) checker/%.mli $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES)
	$(SHOW)'OCAMLDEP  $<'
	$(HIDE)$(OCAMLDEP_NG) -slash $(LOCALCHKLIBS) "$<" $(TOTARGET)

%.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES)
	$(SHOW)'OCAMLDEP  $<'
	$(HIDE)$(OCAMLDEP_NG) $(DEPFLAGS) "$<" $(TOTARGET)

%.mli.d: $(D_DEPEND_BEFORE_SRC) %.mli $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES)
	$(SHOW)'OCAMLDEP  $<'
	$(HIDE)$(OCAMLDEP_NG) $(DEPFLAGS) "$<" $(TOTARGET)

checker/%.mllib.d: $(D_DEPEND_BEFORE_SRC) checker/%.mllib $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES)
	$(SHOW)'COQDEP  $<'
	$(HIDE)$(COQDEPBOOT) -slash -I checker -c "$<" $(TOTARGET)

%.mllib.d: $(D_DEPEND_BEFORE_SRC) %.mllib $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES)
	$(SHOW)'COQDEP  $<'
	$(HIDE)$(COQDEPBOOT) -slash -I kernel -I tools/coqdoc -c "$<" $(TOTARGET)

%.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENVFILES)
	$(SHOW)'COQDEP    $<'
	$(HIDE)$(COQDEPBOOT) $(DEPNATDYN) -slash "$<" $(TOTARGET)

%_stubs.c.d: $(D_DEPEND_BEFORE_SRC) %_stubs.c $(D_DEPEND_AFTER_SRC)
	$(SHOW)'CCDEP	$<'
	$(HIDE)echo "$@ $(@:.c.d=.o): $(@:.c.d=.c)" > $@

%.c.d: $(D_DEPEND_BEFORE_SRC) %.c $(D_DEPEND_AFTER_SRC) $(GENHFILES)
	$(SHOW)'CCDEP     $<'
	$(HIDE)$(OCAMLC) -ccopt "-MM -MQ $@ -MQ $(<:.c=.o) -isystem $(CAMLHLIB)" $< $(TOTARGET)

###########################################################################
# this sets up developper supporting stuff
###########################################################################

.PHONY: devel otags
devel: $(DEBUGPRINTERS)

otags:
	otags $(MLIFILES) $(MLSTATICFILES) \
	$(foreach i,$(ML4FILES),-pc -pa tools/compat5.cmo -pa op -pa g -pa m -pa rq $(patsubst %,-pa %,$(call CAMLP4DEPS,$i)) -impl $i)


###########################################################################


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