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

# Extra targets for developers :
# debug printers, revision, partial targets ...

#########################
# Debug printers in dev/
#########################

.PHONY: devel printers

DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo

devel: printers
printers: $(CORECMA) $(DEBUGPRINTERS)

###################
# Partial builds
###################

# The following partial targets are normally not necessary
# for a complete build of coq, see instead 'make world' for that.
# But these partial targets could be quite handy for quick builds
# of specific components of Coq.

###############################
### 1) general-purpose targets
###############################

coqlight: theories-light tools coqbinaries

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

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

# This should build all the ocaml code but not (most of) the .v files
coqocaml: tools coqbinaries $(PLUGINSCMO:.cmo=$(DYNOBJ)) coqide printers bin/votour

.PHONY: coqlight states miniopt minibyte pluginsopt pluginsbyte coqocaml

######################
### 3) theories files
######################

init: $(filter theories/Init/%, $(THEORIESVO))
logic: $(filter theories/Logic/%, $(THEORIESVO))
arith: $(filter theories/Arith/%, $(THEORIESVO))
bool: $(filter theories/Bool/%, $(THEORIESVO))
parith: $(filter theories/PArith/%, $(THEORIESVO))
narith: $(filter theories/NArith/%, $(THEORIESVO))
zarith: $(filter theories/ZArith/%, $(THEORIESVO))
qarith: $(filter theories/QArith/%, $(THEORIESVO))
lists: $(filter theories/Lists/%, $(THEORIESVO))
strings: $(filter theories/Strings/%, $(THEORIESVO))
sets: $(filter theories/Sets/%, $(THEORIESVO))
fsets: $(filter theories/FSets/%, $(THEORIESVO))
relations: $(filter theories/Relations/%, $(THEORIESVO))
wellfounded: $(filter theories/Wellfounded/%, $(THEORIESVO))
reals: $(filter theories/Reals/%, $(THEORIESVO))
setoids: $(filter theories/Setoids/%, $(THEORIESVO))
sorting: $(filter theories/Sorting/%, $(THEORIESVO))
numbers: $(filter theories/Numbers/%, $(THEORIESVO))
unicode: $(filter theories/Unicode/%, $(THEORIESVO))
classes: $(filter theories/Classes/%, $(THEORIESVO))
program: $(filter theories/Program/%, $(THEORIESVO))
structures: $(filter theories/Structures/%, $(THEORIESVO))
vectors: $(filter theories/Vectors/%, $(THEORIESVO))
msets: $(filter theories/MSets/%, $(THEORIESVO))
compat: $(filter theories/Compat/%, $(THEORIESVO))

theories-light: $(THEORIESLIGHTVO)

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

.PHONY: init theories-light noreal
.PHONY: logic arith bool narith zarith qarith lists strings sets
.PHONY: fsets relations wellfounded reals setoids sorting numbers
.PHONY: msets mmaps compat parith classes program unicode structures vectors

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