Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Fetching contributors…

Cannot retrieve contributors at this time

983 lines (760 sloc) 31.89 kb
#######################################################################
# 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
SYSMOD:=str unix
SYSCMA:=$(addsuffix .cma,$(SYSMOD))
SYSCMXA:=$(addsuffix .cmxa,$(SYSMOD))
ifeq ($(CAMLP4),camlp5)
P4CMA:=gramlib.cma
else
P4CMA:=dynlink.cma camlp4lib.cma
endif
###########################################################################
# 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 -I $(MYCAMLP4LIB) $(MLINCLUDES)\
$(DOCMLIS) -t "Coq mlis documentation" \
-intro $(OCAMLDOCDIR)/docintro -o $@
mli-doc:: $(DOCMLIS:.mli=.cmi)
$(OCAMLDOC) -html -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) $(MLINCLUDES) $(ODOCDOTOPTS) -dot-types -o $@ $<
OCAMLDOC_MLLIBD = $(OCAMLDOC) $(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) $(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) $(P4CMA) $^ -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 $@
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 $@
# Specific rule for term.ml which uses -rectypes
# Since term.mli doesn't need -rectypes, this doesn't impact the other ml files
TERM:=kernel/term
$(TERM).cmo: $(TERM).ml | $(TERM).ml.d
$(SHOW)'OCAMLC -rectypes $<'
$(HIDE)$(OCAMLC) $(BYTEFLAGS) -rectypes -c $<
$(TERM).cmx: $(TERM).ml | $(TERM).ml.d
$(SHOW)'OCAMLOPT -rectypes $<'
$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -intf-suffix .cmi -rectypes -c $<
# 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:
Jump to Line
Something went wrong with that request. Please try again.