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

1120 lines (874 sloc) 37.775 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 documentation
.PHONY: world
###########################################################################
# Includes
###########################################################################
include Makefile.common
include Makefile.doc
# In a first phase, we restrict to the basic .ml4 (the ones without grammar.cma)
ifdef BUILDGRAMMAR
MLFILES := $(MLSTATICFILES) $(GENMLFILES) $(ML4BASEFILES:.ml4=.ml)
CURFILES := $(MLFILES) $(MLIFILES) $(ML4BASEFILES) grammar/grammar.mllib
else
MLFILES := $(MLSTATICFILES) $(GENMLFILES) $(ML4FILES:.ml4=.ml)
CURFILES := $(MLFILES) $(MLIFILES) $(ML4FILES) $(MLLIBFILES) $(CFILES) $(VFILES)
endif
CURDEPS:=$(addsuffix .d, $(CURFILES))
# 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.
.SECONDARY: $(CURDEPS) $(GENFILES) $(ML4FILES:.ml4=.ml)
# This include below will lauch the build of all concerned .d.
# The - at front is for disabling warnings about currently missing ones.
-include $(CURDEPS)
###########################################################################
# Compilation options
###########################################################################
# Variables meant to be modifiable via the command-line of make
VERBOSE=
NO_RECOMPILE_ML4=
NO_RECALC_DEPS=
READABLE_ML4=true # 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)
OCAMLC := $(OCAMLC) $(CAMLFLAGS)
OCAMLOPT := $(OCAMLOPT) $(CAMLFLAGS)
BYTEFLAGS=-thread $(CAMLDEBUG) $(USERFLAGS)
OPTFLAGS=-thread $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS)
DEPFLAGS= $(LOCALINCLUDES) -I ide -I ide/utils
ifeq ($(ARCH),Darwin)
LINKMETADATA=-ccopt "-sectcreate __TEXT __info_plist config/Info-$(notdir $@).plist"
CODESIGN=codesign -s -
else
LINKMETADATA=
CODESIGN=true
endif
define bestocaml
$(if $(OPT),\
$(if $(findstring $@,$(PRIVATEBINARIES)),\
$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -o $@ $(1) $(addsuffix .cmxa,$(2)) $^ && $(STRIP) $@,\
$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) $(LINKMETADATA) -o $@ $(1) $(addsuffix .cmxa,$(2)) $^ && $(STRIP) $@ && $(CODESIGN) $@),\
$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(CUSTOM) -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
CAMLP4FLAGS=-I $(CAMLLIB) -I $(CAMLLIB)/threads -I $(MYCAMLP4LIB) unix.cma threads.cma
PR_O := $(if $(READABLE_ML4),pr_o.cmo,pr_dump.cmo) # works also with new camlp4
SYSMOD:=str unix dynlink threads
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) $(TOPLOOPCMA:.cma=.cmxs)
$(SHOW)'COQMKTOP -o $@'
$(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) $(LINKMETADATA) -thread -o $@
$(STRIP) $@
$(CODESIGN) $@
else
$(COQTOPEXE): $(COQTOPBYTE)
cp $< $@
endif
$(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA)
$(SHOW)'COQMKTOP -o $@'
$(HIDE)$(COQMKTOP) -boot -top $(BYTEFLAGS) -thread -o $@
LOCALCHKLIBS:=$(addprefix -I , $(CHKSRCDIRS) )
CHKLIBS:=$(LOCALCHKLIBS) -I $(MYCAMLP4LIB)
ifeq ($(BEST),opt)
$(CHICKEN): checker/check.cmxa checker/main.ml
$(SHOW)'OCAMLOPT -o $@'
$(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) $(LINKMETADATA) -thread -o $@ $(SYSCMXA) $^
$(STRIP) $@
$(CODESIGN) $@
else
$(CHICKEN): $(CHICKENBYTE)
cp $< $@
endif
$(CHICKENBYTE): checker/check.cma checker/main.ml
$(SHOW)'OCAMLC -o $@'
$(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) $(CUSTOM) -thread -o $@ $(SYSCMA) $^
# coqmktop
$(COQMKTOP): $(patsubst %.cma,%$(BESTLIB),$(COQMKTOPCMO:.cmo=$(BESTOBJ)))
$(SHOW)'OCAMLBEST -o $@'
$(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD))
tools/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) $(MLINCLUDES) $(BYTEFLAGS) -a -o $@ $^
%.cmxa: | %.mllib.d
$(SHOW)'OCAMLOPT -a -o $@'
$(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -a -o $@ $^
# For the checker, different flags may be used
checker/check.cma: | checker/check.mllib.d
$(SHOW)'OCAMLC -a -o $@'
$(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) -a -o $@ $^
checker/check.cmxa: | checker/check.mllib.d
$(SHOW)'OCAMLOPT -a -o $@'
$(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) -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=$(addprefix -I , $(IDESRCDIRS)) $(COQIDEINCLUDES)
.SUFFIXES:.vo
IDEFILES=$(wildcard ide/*.lang) ide/coq_style.xml ide/coq.png ide/MacOS/default_accel_map
coqide-binaries: coqide-$(HASCOQIDE) ide-toploop
coqide-no:
coqide-byte: $(COQIDEBYTE) $(COQIDE)
coqide-opt: $(COQIDEBYTE) $(COQIDE)
coqide-files: $(IDEFILES)
ifeq ($(BEST),opt)
ide-toploop: $(IDETOPLOOPCMA) $(IDETOPLOOPCMA:.cma=.cmxs)
else
ide-toploop: $(IDETOPLOOPCMA)
endif
ifeq ($(HASCOQIDE),opt)
$(COQIDE): $(LINKIDEOPT)
$(SHOW)'OCAMLOPT -o $@'
$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ unix.cmxa threads.cmxa lablgtk.cmxa \
lablgtksourceview2.cmxa str.cmxa $(IDEFLAGS:.cma=.cmxa) $^
$(STRIP) $@
else
$(COQIDE): $(COQIDEBYTE)
cp $< $@
endif
$(COQIDEBYTE): $(LINKIDE)
$(SHOW)'OCAMLC -o $@'
$(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ unix.cma threads.cma lablgtk.cma \
lablgtksourceview2.cma str.cma $(IDEFLAGS) $(IDECDEPSFLAGS) $^
# install targets
.PHONY: install-coqide install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles
ifeq ($(HASCOQIDE),no)
install-coqide: install-ide-toploop
else
install-coqide: install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles
endif
install-ide-bin:
$(MKDIR) $(FULLBINDIR)
$(INSTALLBIN) $(COQIDE) $(FULLBINDIR)
install-ide-toploop:
$(MKDIR) $(FULLCOQLIB)/toploop
$(INSTALLBIN) $(IDETOPLOOPCMA) $(FULLCOQLIB)/toploop/
ifeq ($(BEST),opt)
$(INSTALLBIN) $(IDETOPLOOPCMA:.cma=.cmxs) $(FULLCOQLIB)/toploop/
endif
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: #Please update $(COQIDEAPP)/Contents/Resources/ at the same time
$(MKDIR) $(FULLDATADIR)
$(INSTALLLIB) ide/coq.png ide/*.lang ide/coq_style.xml $(FULLDATADIR)
$(MKDIR) $(FULLCONFIGDIR)
if [ $(IDEINT) = QUARTZ ] ; then $(INSTALLLIB) ide/mac_default_accel_map $(FULLCONFIGDIR)/coqide.keys ; fi
install-ide-info:
$(MKDIR) $(FULLDOCDIR)
$(INSTALLLIB) ide/FAQ $(FULLDOCDIR)/FAQ-CoqIde
###########################################################################
# CoqIde MacOS special targets
###########################################################################
.PHONY: $(COQIDEAPP)/Contents
$(COQIDEAPP)/Contents:
rm -rdf $@
$(MKDIR) $@
sed -e "s/VERSION/$(VERSION)/g" ide/MacOS/Info.plist.template > $@/Info.plist
$(MKDIR) "$@/MacOS"
$(COQIDEINAPP): ide/macos_prehook.cmx $(LINKIDEOPT) | $(COQIDEAPP)/Contents
$(SHOW)'OCAMLOPT -o $@'
$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ \
unix.cmxa lablgtk.cmxa lablgtksourceview2.cmxa str.cmxa \
threads.cmxa $(IDEFLAGS:.cma=.cmxa) $^
$(STRIP) $@
$(COQIDEAPP)/Contents/Resources/share: $(COQIDEAPP)/Contents
$(MKDIR) $@/coq/
$(INSTALLLIB) ide/coq.png ide/*.lang ide/coq_style.xml $@/coq/
$(MKDIR) $@/gtksourceview-2.0/{language-specs,styles}
$(INSTALLLIB) "$(GTKSHARE)/"gtksourceview-2.0/language-specs/{def.lang,language2.rng} $@/gtksourceview-2.0/language-specs/
$(INSTALLLIB) "$(GTKSHARE)/"gtksourceview-2.0/styles/{styles.rng,classic.xml} $@/gtksourceview-2.0/styles/
cp -R "$(GTKSHARE)/"locale $@
cp -R "$(GTKSHARE)/"icons $@
cp -R "$(GTKSHARE)/"themes $@
$(COQIDEAPP)/Contents/Resources/loaders: $(COQIDEAPP)/Contents
$(MKDIR) $@
$(INSTALLLIB) $$("$(GTKBIN)/gdk-pixbuf-query-loaders" | sed -n -e '5 s!.*= \(.*\)$$!\1!p')/libpixbufloader-png.so $@
$(COQIDEAPP)/Contents/Resources/immodules: $(COQIDEAPP)/Contents
$(MKDIR) $@
$(INSTALLLIB) "$(GTKLIBS)/gtk-2.0/2.10.0/immodules/"*.so $@
$(COQIDEAPP)/Contents/Resources/etc: $(COQIDEAPP)/Contents/Resources/lib
$(MKDIR) $@/xdg/coq
$(INSTALLLIB) ide/MacOS/default_accel_map $@/xdg/coq/coqide.keys
$(MKDIR) $@/gtk-2.0
{ "$(GTKBIN)/gdk-pixbuf-query-loaders" $@/../loaders/*.so |\
sed -e "s!/.*\(/loaders/.*.so\)!@executable_path/../Resources/\1!"; } \
> $@/gtk-2.0/gdk-pixbuf.loaders
{ "$(GTKBIN)/gtk-query-immodules-2.0" $@/../immodules/*.so |\
sed -e "s!/.*\(/immodules/.*.so\)!@executable_path/../Resources/\1!" |\
sed -e "s!/.*\(/share/locale\)!@executable_path/../Resources/\1!"; } \
> $@/gtk-2.0/gtk-immodules.loaders
$(MKDIR) $@/pango
echo "[Pango]" > $@/pango/pangorc
$(COQIDEAPP)/Contents/Resources/lib: $(COQIDEAPP)/Contents/Resources/immodules $(COQIDEAPP)/Contents/Resources/loaders $(COQIDEAPP)/Contents $(COQIDEINAPP)
$(MKDIR) $@
$(INSTALLLIB) $(GTKLIBS)/charset.alias $@/
$(MKDIR) $@/pango/1.8.0/modules
$(INSTALLLIB) "$(GTKLIBS)/pango/1.8.0/modules/"*.so $@/pango/1.8.0/modules/
{ "$(GTKBIN)/pango-querymodules" $@/pango/1.8.0/modules/*.so |\
sed -e "s!/.*\(/pango/1.8.0/modules/.*.so\)!@executable_path/../Resources/lib\1!"; } \
> $@/pango/1.8.0/modules.cache
for i in $$(otool -L $(COQIDEINAPP) |sed -n -e "\@$(GTKLIBS)@ s/[^/]*\(\/[^ ]*\) .*$$/\1/p"); \
do cp $$i $@/; \
ide/MacOS/relatify_with-respect-to_.sh $@/$$(basename $$i) $(GTKLIBS) $@; \
done
for i in $@/../loaders/*.so $@/../immodules/*.so $@/pango/1.8.0/modules/*.so; \
do \
for j in $$(otool -L $$i | sed -n -e "\@$(GTKLIBS)@ s/[^/]*\(\/[^ ]*\) .*$$/\1/p"); \
do cp $$j $@/; ide/MacOS/relatify_with-respect-to_.sh $@/$$(basename $$j) $(GTKLIBS) $@; done; \
ide/MacOS/relatify_with-respect-to_.sh $$i $(GTKLIBS) $@; \
done
EXTRAWORK=1; \
while [ $${EXTRAWORK} -eq 1 ]; \
do EXTRAWORK=0; \
for i in $@/*.dylib; \
do for j in $$(otool -L $$i | sed -n -e "\@$(GTKLIBS)@ s/[^/]*\(\/[^ ]*\) .*$$/\1/p"); \
do EXTRAWORK=1; cp $$j $@/; ide/MacOS/relatify_with-respect-to_.sh $@/$$(basename $$j) $(GTKLIBS) $@; done; \
done; \
done
ide/MacOS/relatify_with-respect-to_.sh $(COQIDEINAPP) $(GTKLIBS) $@
$(COQIDEAPP)/Contents/Resources:$(COQIDEAPP)/Contents/Resources/etc $(COQIDEAPP)/Contents/Resources/share
$(INSTALLLIB) ide/MacOS/*.icns $@
$(COQIDEAPP):$(COQIDEAPP)/Contents/Resources
$(CODESIGN) $@
###########################################################################
# tests
###########################################################################
.PHONY: validate check test-suite $(ALLSTDLIB).v md5chk
md5chk:
$(SHOW)'MD5SUM cic.mli'
$(HIDE)if grep -q `$(MD5SUM) checker/cic.mli` checker/values.ml; \
then true; else echo "Error: outdated checker/values.ml"; false; fi
VALIDOPTS=$(if $(VERBOSE),,-silent) -o -m
validate: $(CHICKEN) md5chk | $(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 stm 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
stm: stm/stm.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 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)
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 -R theories Coq
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 threads)
$(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)
$(COQWORKMGR): $(addsuffix $(BESTOBJ), stm/coqworkmgrApi tools/coqworkmgr) \
$(addsuffix $(BESTLIB), lib/clib)
$(SHOW)'OCAMLBEST -o $@'
$(HIDE)$(call bestocaml,, $(SYSMOD) clib)
# fake_ide : for debugging or test-suite purpose, a fake ide simulating
# a connection to coqtop -ideslave
$(FAKEIDE): lib/clib$(BESTLIB) lib/xml_lexer$(BESTOBJ) lib/xml_parser$(BESTOBJ) lib/xml_printer$(BESTOBJ) lib/errors$(BESTOBJ) lib/spawn$(BESTOBJ) ide/document$(BESTOBJ) ide/xmlprotocol$(BESTOBJ) tools/fake_ide$(BESTOBJ) | $(IDETOPLOOPCMA:.cma=$(BESTDYN))
$(SHOW)'OCAMLBEST -o $@'
$(HIDE)$(call bestocaml,-I ide,str unix threads)
# votour: a small vo explorer (based on the checker)
bin/votour: lib/cObj$(BESTOBJ) checker/values$(BESTOBJ) checker/votour.ml
$(SHOW)'OCAMLBEST -o $@'
$(HIDE)$(call bestocaml, -I checker,)
# 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) $(CAMLP4FLAGS) -impl' -impl $<
tools/compat5b.cmo: tools/compat5b.mlp
$(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) $(CAMLP4FLAGS) -impl' -impl $<
else
tools/compat5.cmo: tools/compat5.ml
$(OCAMLC) -c $<
tools/compat5b.cmo: tools/compat5b.ml
$(OCAMLC) -c $<
endif
###########################################################################
# Documentation : cf Makefile.doc
###########################################################################
documentation: doc-$(WITHDOC)
doc-all: doc
doc-no:
.PHONY: documentation doc-all doc-no
###########################################################################
# Installation
###########################################################################
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:
.PHONY: install install-doc-all install-doc-no
#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)
$(MKDIR) $(FULLCOQLIB)/toploop
$(INSTALLBIN) $(TOPLOOPCMA) $(FULLCOQLIB)/toploop/
ifeq ($(BEST),opt)
$(INSTALLBIN) $(TOPLOOPCMA:.cma=.cmxs) $(FULLCOQLIB)/toploop/
endif
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 \
$(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) $(CORECMA:.cma=.a) $(STATICPLUGINS:.cma=.a)
endif
install-library:
$(MKDIR) $(FULLCOQLIB)
$(INSTALLSH) $(FULLCOQLIB) $(LIBFILES) $(PLUGINS)
$(MKDIR) $(FULLCOQLIB)/user-contrib
ifndef CUSTOM
$(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB)
endif
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)
ifndef CUSTOM
$(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB)
endif
ifeq ($(BEST),opt)
$(INSTALLLIB) $(LIBCOQRUN) $(FULLCOQLIB)
$(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/gallina-db.el tools/coq-font-lock.el tools/gallina-syntax.el tools/gallina.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 +threads -I $(MYCAMLP4LIB) $(MLINCLUDES) \
$(DOCMLIS) -d $(OCAMLDOCDIR)/html -colorize-code \
-t "Coq mlis documentation" -intro $(OCAMLDOCDIR)/docintro \
-css-style style.css
ml-dot: $(MLFILES)
$(OCAMLDOC) -dot -dot-reduce -rectypes -I +threads -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 -I +threads $(MLINCLUDES) $(COQIDEFLAGS) -d $(OCAMLDOCDIR) $(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) $(MLINCLUDES) $(BYTEFLAGS) -thread $(SYSCMA) $(P4CMA) $^ -o test-printer
@rm -f test-printer
$(SHOW)'OCAMLC -a $@'
$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -thread $(SYSCMA) $^ -linkall -a -o $@
grammar/grammar.cma: | grammar/grammar.mllib.d
$(SHOW)'Testing $@'
@touch test.ml4
$(HIDE)$(CAMLP4O) $(CAMLP4FLAGS) $^ -impl test.ml4 -o test.ml
$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) test.ml -o test-grammar
@rm -f test-grammar test.*
$(SHOW)'OCAMLC -a $@'
$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $^ -linkall -a -o $@
ide/coqide_main.ml: ide/coqide_main.ml4 config/Makefile # no camlp4deps here
$(SHOW)'CAMLP4O $<'
$(HIDE)$(CAMLP4O) $(CAMLP4FLAGS) $(PR_O) $(CAMLP4USE) -D$(IDEINT) -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/%,$<), $(CHKLIBS) -thread, \
$(if $(filter ide/%,$<), $(COQIDEFLAGS), \
$(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide,) $(MLINCLUDES) -thread)) $(BYTEFLAGS)
COND_OPTFLAGS= \
$(if $(filter checker/%,$<), $(CHKLIBS) -thread, \
$(if $(filter ide/%,$<), $(COQIDEFLAGS), \
$(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide,) $(MLINCLUDES) -thread)) $(OPTFLAGS)
%.o: %.c
$(SHOW)'OCAMLC $<'
$(HIDE)cd $(dir $<) && $(OCAMLC) -ccopt "$(CFLAGS)" -c $(notdir $<)
%.o: %.rc
$(SHOW)'WINDRES $<'
$(HIDE)i686-w64-mingw32-windres -i $< -o $@
%.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)$(CAMLP4O) $(CAMLP4FLAGS) $(PR_O) tools/compat5.cmo \
$(call CAMLP4DEPS,$<) $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< -o $@
%.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)
# Since OCaml 3.12.1, we could use again ocamldep directly, thanks to
# the option -ml-synonym
OCAMLDEP_NG = $(OCAMLDEP) -slash -ml-synonym .ml4
checker/%.ml.d: $(D_DEPEND_BEFORE_SRC) checker/%.ml $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES)
$(SHOW)'OCAMLDEP $<'
$(HIDE)$(OCAMLDEP_NG) $(LOCALCHKLIBS) "$<" $(TOTARGET)
checker/%.mli.d: $(D_DEPEND_BEFORE_SRC) checker/%.mli $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES)
$(SHOW)'OCAMLDEP $<'
$(HIDE)$(OCAMLDEP_NG) $(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) -I checker -c "$<" $(TOTARGET)
%.mllib.d: $(D_DEPEND_BEFORE_SRC) %.mllib $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES)
$(SHOW)'COQDEP $<'
$(HIDE)$(COQDEPBOOT) -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) "$<" $(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)
###########################################################################
# To speed-up things a bit, let's dissuade make to attempt rebuilding makefiles
Makefile Makefile.build Makefile.common config/Makefile : ;
# For emacs:
# Local Variables:
# mode: makefile
# End:
Jump to Line
Something went wrong with that request. Please try again.