path: root/Makefile.build

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

# $Id: Makefile.build 13477 2010-09-30 16:50:00Z vgross $ 


# Makefile for Coq
#
# To be used with GNU Make.
#
# This is the only Makefile. You won't find Makefiles in sub-directories
# and this is done on purpose. If you are not yet convinced of the advantages
# of a single Makefile, please read
#    http://www.pcug.org.au/~millerp/rmch/recu-make-cons-harm.html
# before complaining.
# 
# When you are working in a subdir, you can compile without moving to the
# upper directory using "make -C ..", and the output is still understood
# by Emacs' next-error.
###########################################################################

include Makefile.common
ifndef COQ_CONFIGURED
 $(error Please run ./configure first)
endif

.PHONY: NOARG

NOARG: world

# build and install the three subsystems: coq, coqide
world: revision coq coqide
install: install-coq install-coqide

ifeq ($(WITHDOC),all)
world: doc
install: install-doc
endif

#install-manpages: install-coq-manpages

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

# 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

ifdef VERBOSE
 SHOW = @true ""
 HIDE = 
else 
 SHOW = @echo ""
 HIDE = @
endif

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

OCAMLC += $(CAMLFLAGS)
OCAMLOPT += $(CAMLFLAGS)

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

CAMLP4EXTENDFLAGS=-I $(CAMLLIB) -I . #grammar dependencies are now in camlp4use statements
CAMLP4DEPS=sed -n -e 's@^(\*.*camlp4deps: "\(.*\)".*\*)@\1@p'
CAMLP4USE=sed -n -e 's/pa_macro.cmo/pa_macro.cmo -D$(CAMLVERSION)/' -e 's@^(\*.*camlp4use: "\(.*\)".*\*)@\1@p'

COQ_XML=	# is "-xml" when building XML library
VM=		# is "-no-vm" to not use the vm"
UNBOXEDVALUES=	# is "-unboxed-values" to use unboxed values
COQOPTS=$(COQ_XML) $(VM) $(UNBOXEDVALUES)
TIMECMD=	# is "'time -p'" to get compilation time of .v

# NB: variable TIME, if set, is the formatting string for unix command 'time'.
# For instance:
# TIME="%C (%U user, %S sys, %e total, %M maxres)"

BOOTCOQTOP:=$(TIMECMD) $(BESTCOQTOP) -boot $(COQOPTS)

###########################################################################
# 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 := $(BESTCOQTOP)
ifdef COQ_XML
 VO_TOOLS_DEP += $(COQDOC)
endif
ifdef VALIDATE
 VO_TOOLS_DEP += $(BESTCHICKEN)
endif
ifdef NO_RECOMPILE_LIB
 VO_TOOLS_ORDER_ONLY:=$(VO_TOOLS_DEP)
 VO_TOOLS_STRICT:=
else
 VO_TOOLS_ORDER_ONLY:=
 VO_TOOLS_STRICT:=$(VO_TOOLS_DEP)
endif

ifdef NO_RECALC_DEPS
  D_DEPEND_BEFORE_SRC:=|
  D_DEPEND_AFTER_SRC:=
else
  D_DEPEND_BEFORE_SRC:=
  D_DEPEND_AFTER_SRC:=|
endif

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

CINCLUDES= -I $(CAMLHLIB)

# libcoqrun.a, dllcoqrun.so

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

#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' kernel/byterun/coq_instruct.h > \
                          kernel/byterun/coq_jumptbl.h \
	  || ( RV=$$?; rm -f "$@"; exit $${RV} )

kernel/copcodes.ml: kernel/byterun/coq_instruct.h
	sed -n -e '/^enum/p' -e 's/,//g' -e '/^  /p' \
	kernel/byterun/coq_instruct.h | \
	awk -f kernel/make-opcodes > kernel/copcodes.ml \
	|| ( RV=$$?; rm -f "$@"; exit $${RV} )


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

coqbinaries:: ${COQBINARIES} ${CSDPCERT}

coq: coqlib tools coqbinaries

coqlib:: theories plugins

coqlight: theories-light tools coqbinaries

states:: states/initial.coq

$(COQTOPOPT): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN)
	$(SHOW)'COQMKTOP -o $@'	
	$(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) -o $@
	$(STRIP) $@

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

$(COQTOPEXE): $(ORDER_ONLY_SEP) $(BESTCOQTOP)
	cd bin; ln -sf coqtop.$(BEST)$(EXE) coqtop$(EXE)

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

$(CHICKENOPT): checker/check.cmxa checker/main.ml
	$(SHOW)'OCAMLOPT -o $@'
	$(HIDE)$(OCAMLOPT) $(CHKOPTFLAGS) -o $@ str.cmxa unix.cmxa gramlib.cmxa $^
	$(STRIP) $@

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

$(CHICKEN): $(ORDER_ONLY_SEP) $(BESTCHICKEN)
	cd bin && ln -sf coqchk.$(BEST)$(EXE) coqchk$(EXE)

# coqmktop 

$(COQMKTOPBYTE): $(COQMKTOPCMO)
	$(SHOW)'OCAMLC -o $@'	
	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma gramlib.cma\
          $^ $(OSDEPLIBS)

$(COQMKTOPOPT): $(COQMKTOPCMX)
	$(SHOW)'OCAMLOPT -o $@'	
	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ str.cmxa unix.cmxa gramlib.cmxa\
          $^ $(OSDEPLIBS)
	$(STRIP) $@

$(COQMKTOP): $(ORDER_ONLY_SEP) $(BESTCOQMKTOP)
	cd bin; ln -sf coqmktop.$(BEST)$(EXE) coqmktop$(EXE)

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)"\"" >> $@
	$(HIDE)echo "let ide = \""$(IDEMOD)"\"" >> $@

# coqc

$(COQCBYTE): $(COQCCMO) $(COQTOPBYTE) $(BESTCOQTOP)
	$(SHOW)'OCAMLC -o $@'
	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma gramlib.cma $(COQCCMO) $(OSDEPLIBS)

$(COQCOPT): $(COQCCMX) $(COQTOPOPT) $(BESTCOQTOP)
	$(SHOW)'OCAMLOPT -o $@'
	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ str.cmxa unix.cmxa gramlib.cmxa $(COQCCMX) $(OSDEPLIBS)
	$(STRIP) $@

$(COQC): $(ORDER_ONLY_SEP) $(BESTCOQC)
	cd bin; ln -sf coqc.$(BEST)$(EXE) coqc$(EXE)

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

ifeq ($(BEST),opt)
plugins/micromega/csdpcert$(EXE): $(CSDPCERTCMX)
	$(SHOW)'OCAMLOPT -o $@'
	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) nums.cmxa unix.cmxa -o $@ $^
	$(STRIP) $@
else
plugins/micromega/csdpcert$(EXE): $(CSDPCERTCMO)
	$(SHOW)'OCAMLC -o $@'
	$(HIDE)$(OCAMLC) $(BYTEFLAGS) nums.cma unix.cma -o $@ $^
endif

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

# target to build CoqIde
coqide:: coqide-files coqide-binaries states

COQIDEFLAGS=-thread $(COQIDEINCLUDES)

.SUFFIXES:.vo

IDEFILES=ide/coq.png ide/.coqide-gtk2rc

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

$(COQIDEOPT): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) ide/ide.cmxa
	$(SHOW)'COQMKTOP -o $@'	
	$(HIDE)$(COQMKTOP) -boot -ide -opt $(OPTFLAGS) -o $@
	$(STRIP) $@

$(COQIDEBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) ide/ide.cma
	$(SHOW)'COQMKTOP -o $@'	
	$(HIDE)$(COQMKTOP) -boot -g -ide -top $(BYTEFLAGS) -o $@

$(COQIDE):
	cd bin; ln -sf coqide.$(HASCOQIDE)$(EXE) coqide$(EXE)

ide/%.cmo: ide/%.ml | ide/%.ml.d 
	$(SHOW)'OCAMLC    $<'	
	$(HIDE)$(OCAMLC) -g $(COQIDEFLAGS) $(BYTEFLAGS) -c $<

ide/%.cmi: ide/%.mli | ide/%.mli.d
	$(SHOW)'OCAMLC    $<'	
	$(HIDE)$(OCAMLC) -g $(COQIDEFLAGS) $(BYTEFLAGS) -c $<

ide/%.cmx: ide/%.ml | ide/%.ml.d
	$(SHOW)'OCAMLOPT  $<'	
	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -c $<

# install targets

FULLIDELIB=$(FULLCOQLIB)/ide

install-coqide:: install-ide-$(HASCOQIDE) install-ide-files install-ide-info

install-ide-no:

install-ide-byte: 
	$(MKDIR) $(FULLBINDIR)
	$(INSTALLBIN) $(COQIDEBYTE) $(FULLBINDIR)
	$(INSTALLSH) $(FULLCOQLIB) $(IDECMA) \
	  `cat $(IDECMA:.cma=.mllib.d) | tr ' ' '\n' | sed -n -e "/\.cmo/s/\.cmo/\.cmi/p"`
	cd $(FULLBINDIR); ln -sf coqide.byte$(EXE) coqide$(EXE)

install-ide-opt:
	$(MKDIR) $(FULLBINDIR)
	$(INSTALLBIN) $(COQIDEBYTE) $(COQIDEOPT) $(FULLBINDIR)
	$(INSTALLSH) $(FULLCOQLIB) $(IDECMA) $(IDECMA:.cma=.cmxa) $(IDECMA:.cma=.a) \
	  `cat $(IDECMA:.cma=.mllib.d) | tr ' ' '\n' | sed -n -e "/\.cmo/s/\.cmo/\.cmi/p"`
	cd $(FULLBINDIR); ln -sf coqide.opt$(EXE) coqide$(EXE)

install-ide-files:
	$(MKDIR) $(FULLIDELIB)
	$(INSTALLLIB) $(IDEFILES) $(FULLIDELIB)

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

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

VALIDOPTS=-silent -o -m

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

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

check:: validate test-suite

test-suite: world
	$(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
##################################################################

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

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)

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

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

plugins: $(PLUGINSVO)
omega: $(OMEGAVO) $(OMEGACMA) $(ROMEGAVO) $(ROMEGACMA)
micromega: $(MICROMEGAVO) $(MICROMEGACMA) $(CSDPCERT)
ring: $(RINGVO) $(RINGCMA)
setoid_ring: $(NEWRINGVO) $(NEWRINGCMA)
nsatz: $(NSATZVO) $(NSATZCMA)
dp: $(DPCMA)
xml: $(XMLVO) $(XMLCMA)
extraction: $(EXTRACTIONCMA)
field: $(FIELDVO) $(FIELDCMA)
fourier: $(FOURIERVO) $(FOURIERCMA)
funind: $(FUNINDCMA) $(FUNINDVO)
cc: $(CCVO) $(CCCMA)
subtac: $(SUBTACCMA)
rtauto: $(RTAUTOVO) $(RTAUTOCMA)

###########################################################################
# rules to make theories, plugins and states
###########################################################################

states/initial.coq: states/MakeInitial.v $(INITVO) $(VO_TOOLS_STRICT) | states/MakeInitial.v.d $(VO_TOOLS_ORDER_ONLY)
	$(SHOW)'BUILD     $@'
	$(HIDE)$(BOOTCOQTOP) -batch -notop -silent -nois -load-vernac-source states/MakeInitial.v -outputstate states/initial.coq

theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_STRICT) | theories/Init/%.v.d $(VO_TOOLS_ORDER_ONLY)
	$(SHOW)'COQC -nois $<'
	$(HIDE)rm -f theories/Init/$*.glob
	$(HIDE)$(BOOTCOQTOP) -nois -compile theories/Init/$*

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

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

printers: $(DEBUGPRINTERS)

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

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

$(COQDEPBOOT): $(COQDEPBOOTML)
ifeq ($(BEST),opt)
	$(SHOW)'OCAMLOPT -o $@'
	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ -I tools unix.cmxa $^
	$(STRIP) $@
else
	$(SHOW)'OCAMLC -o $@'
	$(HIDE)$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ -I tools unix.cma $^
endif

# the full coqdep

ifeq ($(BEST),opt)
$(COQDEP): $(COQDEPCMX)
	$(SHOW)'OCAMLOPT -o $@'
	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ str.cmxa unix.cmxa gramlib.cmxa $^ $(OSDEPLIBS)
	$(STRIP) $@
else
$(COQDEP): $(COQDEPCMO)
	$(SHOW)'OCAMLC -o $@'
	$(HIDE)$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ str.cma unix.cma gramlib.cma $^ $(OSDEPLIBS)
endif

ifeq ($(BEST),opt)
$(GALLINA): $(GALLINACMX)
	$(SHOW)'OCAMLOPT -o $@'
	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ $(GALLINACMX)
	$(STRIP) $@
else
$(GALLINA): $(GALLINACMO)
	$(SHOW)'OCAMLC -o $@'
	$(HIDE)$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ $^
endif

ifeq ($(BEST),opt)
$(COQMAKEFILE): tools/coq_makefile.cmx config/coq_config.cmx
	$(SHOW)'OCAMLOPT -o $@'
	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ str.cmxa config/coq_config.cmx tools/coq_makefile.cmx
	$(STRIP) $@
else
$(COQMAKEFILE): config/coq_config.cmo tools/coq_makefile.cmo
	$(SHOW)'OCAMLC -o $@'
	$(HIDE)$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ str.cma $^
endif

ifeq ($(BEST),opt)
$(COQTEX): tools/coq_tex.cmx
	$(SHOW)'OCAMLOPT -o $@'
	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ str.cmxa $^
	$(STRIP) $@
else
$(COQTEX): tools/coq_tex.cmo
	$(SHOW)'OCAMLC -o $@'
	$(HIDE)$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ str.cma $^
endif

ifeq ($(BEST),opt)
$(COQWC): tools/coqwc.cmx
	$(SHOW)'OCAMLOPT -o $@'
	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ tools/coqwc.cmx
	$(STRIP) $@
else
$(COQWC): tools/coqwc.cmo
	$(SHOW)'OCAMLC -o $@'
	$(HIDE)$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ $^
endif

ifeq ($(BEST),opt)
$(COQDOC): $(COQDOCCMX)
	$(SHOW)'OCAMLOPT -o $@'
	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ str.cmxa unix.cmxa $(COQDOCCMX)
	$(STRIP) $@
else
$(COQDOC): $(COQDOCCMO)
	$(SHOW)'OCAMLC -o $@'
	$(HIDE)$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ str.cma unix.cma $^
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)%)
FULLMANDIR=$(MANDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
FULLEMACSLIB=$(EMACSLIB:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
FULLCOQDOCDIR=$(COQDOCDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
FULLDOCDIR=$(DOCDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
else
FULLBINDIR=$(BINDIR)
FULLCOQLIB=$(COQLIBINSTALL)
FULLMANDIR=$(MANDIR)
FULLEMACSLIB=$(EMACSLIB)
FULLCOQDOCDIR=$(COQDOCDIR)
FULLDOCDIR=$(DOCDIR)
endif

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

install-binaries:: install-$(BEST)  install-tools

install-byte::
	$(MKDIR) $(FULLBINDIR)
	$(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(CHICKEN) $(FULLBINDIR)
	cd $(FULLBINDIR); ln -sf coqtop.byte$(EXE) coqtop$(EXE); ln -sf coqchk.byte$(EXE) coqchk$(EXE)

install-opt::
	$(MKDIR) $(FULLBINDIR)
	$(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(COQTOPOPT) $(CHICKEN) $(CHICKENOPT) $(FULLBINDIR)
	cd $(FULLBINDIR); ln -sf coqtop.opt$(EXE) coqtop$(EXE); ln -sf coqchk.opt$(EXE) coqchk$(EXE)

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)

install-library:
	$(MKDIR) $(FULLCOQLIB)
	$(INSTALLSH) $(FULLCOQLIB) $(LIBFILES) $(PLUGINS) $(PLUGINSOPT)
	$(MKDIR) $(FULLCOQLIB)/states
	$(INSTALLLIB) states/*.coq $(FULLCOQLIB)/states
	$(MKDIR) $(FULLCOQLIB)/user-contrib
	$(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB)
	$(INSTALLSH)  $(FULLCOQLIB) $(CONFIG) $(LINKCMO) $(GRAMMARCMA)
	# reconstitute the list of core .cmi
	$(INSTALLSH)  $(FULLCOQLIB) $(CONFIG:.cmo=.cmi) \
          `cat $(CORECMA:.cma=.mllib.d) $(PLUGINSCMA:.cma=.mllib.d) | tr ' ' '\n' | sed -n -e "/\.cmo/s/\.cmo/\.cmi/p"`
ifeq ($(BEST),opt)
	$(INSTALLLIB) $(LIBCOQRUN) $(FULLCOQLIB)
	$(INSTALLSH)  $(FULLCOQLIB) $(CONFIG:.cmo=.cmx) $(CONFIG:.cmo=.o) $(LINKCMO:.cma=.cmxa) $(LINKCMO:.cma=.a)
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
	-$(INSTALLLIB) revision $(FULLCOQLIB)

install-library-light:
	$(MKDIR) $(FULLCOQLIB)
	$(INSTALLSH) $(FULLCOQLIB) $(LIBFILESLIGHT) $(INITPLUGINS) $(INITPLUGINSOPT)
	$(MKDIR) $(FULLCOQLIB)/states
	$(INSTALLLIB) states/*.coq $(FULLCOQLIB)/states
	-$(INSTALLLIB) revision $(FULLCOQLIB)

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

source-doc:
	if !(test -d $(SOURCEDOCDIR)); then mkdir $(SOURCEDOCDIR); fi
	$(OCAMLDOC) -html -rectypes $(LOCALINCLUDES) -d $(SOURCEDOCDIR) $(MLFILES)


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

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

parsing/grammar.cma: | parsing/grammar.mllib.d
	$(SHOW)'Testing $@'
	@touch test.ml4
	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) $^ -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)

toplevel/mltop.cmo: toplevel/mltop.byteml | toplevel/mltop.ml4.ml.d toplevel/mltop.ml4.d
	$(SHOW)'OCAMLC    $<'	
	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -c -impl $< -o $@

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

## This works dependency-wise because the dependencies of the
## .{opt,byte}ml files are those we deduce from the .ml4 file.
## In other words, the Byte-only code doesn't import a new module.
toplevel/mltop.byteml: toplevel/mltop.ml4 config/Makefile # no camlp4deps here
	$(SHOW)'CAMLP4O   $<'	
	$(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` \
	  -DByte -DHasDynlink -impl $< > $@ \
	  || ( RV=$$?; rm -f "$@"; exit $${RV} )

toplevel/mltop.optml: toplevel/mltop.ml4 config/Makefile # no camlp4deps here 
	$(SHOW)'CAMLP4O   $<'	
	$(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` \
	  $(NATDYNLINKDEF) -impl $< > $@ \
	  || ( RV=$$?; rm -f "$@"; exit $${RV} )

# 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 -f); \
	  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
###########################################################################

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

checker/%.cmx: checker/%.ml | checker/%.ml.d
	$(SHOW)'OCAMLOPT  $<'
	$(HIDE)$(OCAMLOPT) -c $(CHKOPTFLAGS) $<

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

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

ifdef KEEP_ML4_PREPROCESSED
.PRECIOUS: %.ml4-preprocessed
%.cmo: %.ml4-preprocessed | %.ml4.ml.d
	$(SHOW)'OCAMLC    $<'
	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -c -impl $<

%.cmx: %.ml4-preprocessed | %.ml4.ml.d
	$(SHOW)'OCAMLOPT  $<'
	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -c -impl $<
else
%.cmo: %.ml4 | %.ml4.ml.d %.ml4.d
	$(SHOW)'OCAMLC4   $<'
	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4USE) $<` `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl" -c -impl $<

%.cmx: %.ml4 | %.ml4.ml.d %.ml4.d
	$(SHOW)'OCAMLOPT4 $<'
	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4USE) $<` `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl" -c -impl $<
endif

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

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

%.cmx: %.ml | %.ml.d
	$(SHOW)'OCAMLOPT  $<'
	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -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 $*)\"" >> $@

.SECONDARY: $(filter plugins/%,$(MLLIBFILES:%.mllib=%_mod.ml))

%.ml4-preprocessed: %.ml4 | %.ml4.d
	$(SHOW)'CAMLP4O   $<'
	$(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $@ \
	  || ( RV=$$?; rm -f "$@"; exit $${RV} )

%.vo %.glob: %.v states/initial.coq $(INITPLUGINSBEST) $(VO_TOOLS_STRICT) | %.v.d  $(VO_TOOLS_ORDER_ONLY)
	$(SHOW)'COQC      $<'
	$(HIDE)rm -f $*.glob 
	$(HIDE)$(BOOTCOQTOP) -compile $*
ifdef VALIDATE
	$(SHOW)'COQCHK    $(call vo_to_mod,$@)'
	$(HIDE)$(BESTCHICKEN) -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.
ifdef NO_RECOMPILE_ML4
  SEP:=$(ORDER_ONLY_SEP)
else
  SEP:=
endif
%.ml4.d: $(D_DEPEND_BEFORE_SRC) %.ml4
	$(SHOW)'CAMLP4DEPS $<'
	$(HIDE)( printf "%s" '$*.cmo $*.cmx $*.ml4.ml.d $*.ml4-preprocessed: $(SEP)' && $(CAMLP4DEPS) "$<" ) > "$@" \
	  || ( RV=$$?; rm -f "$@"; exit $${RV} )

%.ml4.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml4 $(D_DEPEND_AFTER_SRC) $(GENFILES) $(ML4FILESML) %.ml4.d
#Critical section:
# Nobody (in a make -j) should touch the .ml file here.
	$(SHOW)'OCAMLDEP4 $<'
	$(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< -o $*.ml \
	  || ( RV=$$?; rm -f "$*.ml"; exit $${RV} )
	$(HIDE)$(OCAMLDEP) $(DEPFLAGS) $*.ml | sed '' > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
	$(HIDE)echo "let keep_ocamldep_happy Do_not_compile_me = assert false" > $*.ml
#End critical section

checker/%.ml.d: $(D_DEPEND_BEFORE_SRC) checker/%.ml $(D_DEPEND_AFTER_SRC)
	$(SHOW)'OCAMLDEP  $<'
	$(HIDE)$(OCAMLDEP) -slash $(LOCALCHKLIBS) "$<" | sed '' > "$@"

checker/%.mli.d: $(D_DEPEND_BEFORE_SRC) checker/%.mli $(D_DEPEND_AFTER_SRC)
	$(SHOW)'OCAMLDEP  $<'
	$(HIDE)$(OCAMLDEP) -slash $(LOCALCHKLIBS) "$<" | sed '' > "$@"

%.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml $(D_DEPEND_AFTER_SRC) $(GENFILES) $(ML4FILESML)
	$(SHOW)'OCAMLDEP  $<'
	$(HIDE)$(OCAMLDEP) $(DEPFLAGS) "$<" | sed '' > "$@"

%.mli.d: $(D_DEPEND_BEFORE_SRC) %.mli $(D_DEPEND_AFTER_SRC) $(GENFILES) $(ML4FILESML)
	$(SHOW)'OCAMLDEP  $<'
	$(HIDE)$(OCAMLDEP) $(DEPFLAGS) "$<" | sed '' > "$@"

checker/%.mllib.d: $(D_DEPEND_BEFORE_SRC) checker/%.mllib $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT)
	$(SHOW)'COQDEP  $<'
	$(HIDE)$(COQDEPBOOT) -slash -boot -I checker -c "$<" > "$@" \
	  || ( RV=$$?; rm -f "$@"; exit $${RV} )

%.mllib.d: $(D_DEPEND_BEFORE_SRC) %.mllib $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT)
	$(SHOW)'COQDEP  $<'
	$(HIDE)$(COQDEPBOOT) -slash -boot -I kernel -I tools/coqdoc -c "$<" > "$@" \
	  || ( RV=$$?; rm -f "$@"; exit $${RV} )

## Veerry nasty hack to keep ocamldep happy
%.ml: | %.ml4
	$(SHOW)'TOUCH     $@'
	$(HIDE)echo "let keep_ocamldep_happy Do_not_compile_me = assert false" > $@ \
	  || ( RV=$$?; rm -f "$@"; exit $${RV} )

%.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENVFILES)
	$(SHOW)'COQDEP    $<'
	$(HIDE)$(COQDEPBOOT) $(DEPNATDYN) -slash -boot "$<" > "$@" \
	  || ( RV=$$?; rm -f "$@"; exit $${RV} )

%.c.d: $(D_DEPEND_BEFORE_SRC) %.c $(D_DEPEND_AFTER_SRC) $(GENHFILES)
	$(SHOW)'CCDEP     $<'
	$(HIDE)$(CC) -MM -MQ "$@" -MQ "$(<:.c=.o)" $(CFLAGS) -isystem $(CAMLHLIB) $< > $@ \
	  || ( RV=$$?; rm -f "$@"; exit $${RV} )

.SECONDARY: $(GENFILES)

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

.PHONY: devel
devel: $(DEBUGPRINTERS)

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


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

%.dep.ps: %.dot
	$(DOT) $(DOTOPTS) -o $@ $<

OCAMLDOC_MLLIBD = $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ \
  `cat $| | tr ' ' '\n' | sed -n -e "/\.cmo/s/\.cmo/\.ml/p"`

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

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

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

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


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