########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## ## v # INRIA, CNRS and contributors - Copyright 1999-2018 ## ## $@ ############ # revision ############ # display the revision number when compiling a checked out source tree 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 .PHONY: revision ################### # Partial builds ################### # The following partial targets are normally not necessary # for a complete build of coq, see instead 'make world' for that. # But these partial targets could be quite handy for quick builds # of specific components of Coq. ########################################################################### # OCaml dev files ########################################################################### camldevfiles: $(MERLINFILES) META.coq .merlin: .merlin.in cp -a "$<" "$@" %/.merlin: %/.merlin.in cp -a "$<" "$@" META.coq: META.coq.in cp -a "$<" "$@" ############################### ### 1) general-purpose targets ############################### coqlight: theories-light tools coqbinaries states: camldevfiles theories/Init/Prelude.vo miniopt: $(COQTOPEXE) pluginsopt minibyte: $(COQTOPBYTE) pluginsbyte pluginsopt: $(PLUGINSOPT) pluginsbyte: $(PLUGINS) # This should build all the ocaml code but not (most of) the .v files coqocaml: tools coqbinaries $(PLUGINSCMO:.cmo=$(DYNOBJ)) coqide printers bin/votour .PHONY: coqlight states miniopt minibyte pluginsopt pluginsbyte coqocaml ########################## ### 2) core ML components ########################## lib: lib/clib.cma lib/lib.cma kernel: kernel/kernel.cma byterun: $(BYTERUN) library: library/library.cma engine: engine/engine.cma proofs: proofs/proofs.cma tactics: tactics/tactics.cma interp: interp/interp.cma parsing: parsing/parsing.cma pretyping: pretyping/pretyping.cma stm: stm/stm.cma toplevel: toplevel/toplevel.cma .PHONY: lib kernel byterun library proofs tactics interp parsing pretyping .PHONY: engine stm toplevel ###################### ### 3) theories files ###################### init: $(filter theories/Init/%, $(THEORIESVO)) logic: $(filter theories/Logic/%, $(THEORIESVO)) arith: $(filter theories/Arith/%, $(THEORIESVO)) bool: $(filter theories/Bool/%, $(THEORIESVO)) parith: $(filter theories/PArith/%, $(THEORIESVO)) narith: $(filter theories/NArith/%, $(THEORIESVO)) zarith: $(filter theories/ZArith/%, $(THEORIESVO)) qarith: $(filter theories/QArith/%, $(THEORIESVO)) lists: $(filter theories/Lists/%, $(THEORIESVO)) strings: $(filter theories/Strings/%, $(THEORIESVO)) sets: $(filter theories/Sets/%, $(THEORIESVO)) fsets: $(filter theories/FSets/%, $(THEORIESVO)) relations: $(filter theories/Relations/%, $(THEORIESVO)) wellfounded: $(filter theories/Wellfounded/%, $(THEORIESVO)) reals: $(filter theories/Reals/%, $(THEORIESVO)) setoids: $(filter theories/Setoids/%, $(THEORIESVO)) sorting: $(filter theories/Sorting/%, $(THEORIESVO)) numbers: $(filter theories/Numbers/%, $(THEORIESVO)) unicode: $(filter theories/Unicode/%, $(THEORIESVO)) classes: $(filter theories/Classes/%, $(THEORIESVO)) program: $(filter theories/Program/%, $(THEORIESVO)) structures: $(filter theories/Structures/%, $(THEORIESVO)) vectors: $(filter theories/Vectors/%, $(THEORIESVO)) msets: $(filter theories/MSets/%, $(THEORIESVO)) compat: $(filter theories/Compat/%, $(THEORIESVO)) theories-light: $(THEORIESLIGHTVO) noreal: unicode logic arith bool zarith qarith lists sets fsets \ relations wellfounded setoids sorting .PHONY: init theories-light noreal .PHONY: logic arith bool narith zarith qarith lists strings sets .PHONY: fsets relations wellfounded reals setoids sorting numbers .PHONY: msets mmaps compat parith classes program unicode structures vectors ################ ### 4) plugins ################ OMEGAVO:=$(filter plugins/omega/%, $(PLUGINSVO)) ROMEGAVO:=$(filter plugins/romega/%, $(PLUGINSVO)) MICROMEGAVO:=$(filter plugins/micromega/%, $(PLUGINSVO)) QUOTEVO:=$(filter plugins/quote/%, $(PLUGINSVO)) RINGVO:=$(filter plugins/setoid_ring/%, $(PLUGINSVO)) NSATZVO:=$(filter plugins/nsatz/%, $(PLUGINSVO)) FUNINDVO:=$(filter plugins/funind/%, $(PLUGINSVO)) BTAUTOVO:=$(filter plugins/btauto/%, $(PLUGINSVO)) RTAUTOVO:=$(filter plugins/rtauto/%, $(PLUGINSVO)) EXTRACTIONVO:=$(filter plugins/extraction/%, $(PLUGINSVO)) CCVO:= DERIVEVO:=$(filter plugins/derive/%, $(PLUGINSVO)) LTACVO:=$(filter plugins/ltac/%, $(PLUGINSVO)) omega: $(OMEGAVO) $(OMEGACMO) $(ROMEGAVO) $(ROMEGACMO) micromega: $(MICROMEGAVO) $(MICROMEGACMO) $(CSDPCERT) setoid_ring: $(RINGVO) $(RINGCMO) nsatz: $(NSATZVO) $(NSATZCMO) extraction: $(EXTRACTIONCMO) $(EXTRACTIONVO) funind: $(FUNINDCMO) $(FUNINDVO) cc: $(CCVO) $(CCCMO) rtauto: $(RTAUTOVO) $(RTAUTOCMO) btauto: $(BTAUTOVO) $(BTAUTOCMO) ltac: $(LTACVO) $(LTACCMO) .PHONY: omega micromega setoid_ring nsatz extraction .PHONY: funind cc rtauto btauto ltac # For emacs: # Local Variables: # mode: makefile # End: