diff options
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 358 |
1 files changed, 2 insertions, 356 deletions
@@ -8,359 +8,5 @@ ## # (see LICENSE file for the text of the license) ## ########################################################################## - -# Makefile for Coq -# -# To be used with GNU Make >= 3.81. -# -# This Makefile is now separated into Makefile.{common,build,doc}. -# 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://aegis.sourceforge.net/auug97.pdf -# 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. -# -# Specific command-line options to this Makefile: -# -# make VERBOSE=1 # restore the raw echoing of commands -# make NO_RECALC_DEPS=1 # avoid recomputing dependencies -# -# Nota: the 1 above can be replaced by any non-empty value -# -# ---------------------------------------------------------------------- -# See dev/doc/build-system*.txt for more details/FAQ about this Makefile -# ---------------------------------------------------------------------- - - -########################################################################### -# File lists -########################################################################### - -# NB: due to limitations in Win32, please refrain using 'export' too much -# to communicate between make sub-calls (in Win32, 8kb max per env variable, -# 32kb total) - -# !! Before using FIND_SKIP_DIRS, please read how you should in the !! -# !! FIND_SKIP_DIRS section of dev/doc/build-system.dev.txt !! -FIND_SKIP_DIRS:='(' \ - -name '{arch}' -o \ - -name '.svn' -o \ - -name '_darcs' -o \ - -name '.git' -o \ - -name '.bzr' -o \ - -name 'debian' -o \ - -name "$${GIT_DIR}" -o \ - -name '_build' -o \ - -name '_build_ci' -o \ - -name '_install_ci' -o \ - -name 'gramlib' -o \ - -name 'user-contrib' -o \ - -name 'test-suite' -o \ - -name '.opamcache' -o \ - -name '.coq-native' -o \ - -name 'plugin_tutorial' \ -')' -prune -o - -define find - $(shell find . user-contrib/Ltac2 $(FIND_SKIP_DIRS) '(' -name $(1) ')' -print | sed 's|^\./||') -endef - -define findindir - $(shell find $(1) $(FIND_SKIP_DIRS) '(' -name $(2) ')' -print | sed 's|^\./||') -endef - -## Files in the source tree - -# instead of using "export FOO" do "COQ_EXPORTED += FOO" -# this makes it possible to clean up the environment in the subcall -COQ_EXPORTED := COQ_EXPORTED - -LEXFILES := $(call find, '*.mll') -YACCFILES := $(call find, '*.mly') -MLLIBFILES := $(call find, '*.mllib') -MLPACKFILES := $(call find, '*.mlpack') -MLGFILES := $(call find, '*.mlg') -CFILES := $(call findindir, 'kernel/byterun', '*.c') -COQ_EXPORTED +=MLLIBFILES MLPACKFILES MLGFILES CFILES - -# NB our find wrapper ignores the test suite -MERLININFILES := $(call find, '.merlin.in') test-suite/unit-tests/.merlin.in -MERLINFILES := $(MERLININFILES:.in=) -COQ_EXPORTED += MERLINFILES - -# NB: The lists of currently existing .ml and .mli files will change -# before and after a build or a make clean. Hence we do not export -# these variables, but cleaned-up versions (see below MLFILES and co) - -EXISTINGML := $(call find, '*.ml') -EXISTINGMLI := $(call find, '*.mli') - -## Files that will be generated - -# GRAMFILES must be in linking order -GRAMFILES=$(addprefix gramlib/.pack/gramlib__,Ploc Plexing Gramext Grammar) -GRAMMLFILES := $(addsuffix .ml, $(GRAMFILES)) -GRAMMLIFILES := $(addsuffix .mli, $(GRAMFILES)) -GENGRAMMLFILES := $(GRAMMLFILES) gramlib/.pack/gramlib.ml # why is gramlib.ml not in GRAMMLFILES? - -GENMLGFILES:= $(MLGFILES:.mlg=.ml) -GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) $(GENGRAMMLFILES) ide/coqide_os_specific.ml kernel/copcodes.ml kernel/uint63.ml -GENMLIFILES:=$(GRAMMLIFILES) -GENHFILES:=kernel/byterun/coq_instruct.h kernel/byterun/coq_jumptbl.h -GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) kernel/genOpcodeFiles.exe -COQ_EXPORTED += GRAMFILES GRAMMLFILES GRAMMLIFILES GENMLFILES GENHFILES GENFILES - -## More complex file lists - -MLSTATICFILES := $(filter-out $(GENMLFILES), $(EXISTINGML)) -MLIFILES := $(sort $(GENMLIFILES) $(EXISTINGMLI)) -COQ_EXPORTED += MLSTATICFILES MLIFILES - -export $(COQ_EXPORTED) - -include Makefile.common - -########################################################################### -# Starting rules -########################################################################### - -NOARG: world - -.PHONY: NOARG help noconfig submake camldevfiles - -help: - @echo "Please use either:" - @echo " ./configure" - @echo " make world" - @echo " make install" - @echo " make clean" - @echo "or make archclean" - @echo "For make to be verbose, add VERBOSE=1" - @echo - @echo "Bytecode compilation is now a separate target:" - @echo " make byte" - @echo " make install-byte" - @echo "Please do not mix bytecode and native targets in the same make -j" - -UNSAVED_FILES:=$(shell find . -name '.\#*v' -o -name '.\#*.ml' -o -name '.\#*.ml?') -ifdef UNSAVED_FILES -$(error You have unsaved changes in your editor (emacs?) [$(UNSAVED_FILES)]; \ -cancel them or save before proceeding. Or your editor crashed. \ -Then, you may want to consider whether you want to restore the autosaves) -#If you try to simply remove this explicit test, the compilation may -#fail later. In particular, if a .#*.v file exists, coqdep fails to -#run. -endif - -# Apart from clean and a few misc files, everything will be done in a -# sub-call to make on Makefile.build. This way, we avoid doing here -# the -include of .d : since they trigger some compilations, we do not -# want them for a mere clean. Moreover, we regroup this sub-call in a -# common target named 'submake'. This way, multiple user-given goals -# (cf the MAKECMDGOALS variable) won't trigger multiple (possibly -# parallel) make sub-calls - -ifdef COQ_CONFIGURED -%:: submake ; -else -%:: noconfig ; -endif - -MAKE_OPTS := --warn-undefined-variable --no-builtin-rules - -bin: - mkdir bin - -submake: alienclean camldevfiles | bin - $(MAKE) $(MAKE_OPTS) -f Makefile.build $(MAKECMDGOALS) - -noconfig: - @echo "Please run ./configure first" >&2; exit 1 - -# To speed-up things a bit, let's dissuade make to attempt rebuilding makefiles - -Makefile $(wildcard Makefile.*) config/Makefile : ; - -########################################################################### -# OCaml dev files -########################################################################### -camldevfiles: $(MERLINFILES) META.coq - -# prevent submake dependency -META.coq.in $(MERLININFILES): ; - -.merlin: .merlin.in - cp -a "$<" "$@" - -%/.merlin: %/.merlin.in - cp -a "$<" "$@" - -META.coq: META.coq.in - cp -a "$<" "$@" - -########################################################################### -# Cleaning -########################################################################### - -.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean plugin-tutorialclean clean-ide mlgclean depclean cleanconfig distclean voclean timingclean alienclean - -clean: objclean cruftclean depclean docclean camldevfilesclean gramlibclean - -cleankeepvo: indepclean clean-ide optclean cruftclean depclean docclean - -objclean: archclean indepclean - -.PHONY: gramlibclean -gramlibclean: - rm -rf gramlib/.pack/ - -cruftclean: mlgclean - find . \( -name '*~' -o -name '*.annot' \) -exec rm -f {} + - rm -f gmon.out core - -camldevfilesclean: - rm -f $(MERLINFILES) META.coq - -indepclean: - rm -f $(GENFILES) - rm -f $(COQTOPBYTE) $(CHICKENBYTE) $(TOPBYTE) - find . \( -name '*~' -o -name '*.cm[ioat]' -o -name '*.cmti' \) -exec rm -f {} + - rm -f */*.pp[iox] plugins/*/*.pp[iox] - rm -rf $(SOURCEDOCDIR) - rm -f toplevel/mltop.byteml toplevel/mltop.optml - rm -f glob.dump - rm -f config/revision.ml revision - rm -f plugins/micromega/.micromega.ml.generated - $(MAKE) -C test-suite clean - -docclean: - rm -f doc/*/*.dvi doc/*/*.aux doc/*/*.log doc/*/*.bbl doc/*/*.blg doc/*/*.toc \ - doc/*/*.idx doc/*/*~ doc/*/*.ilg doc/*/*.ind doc/*/*.dvi.gz doc/*/*.ps.gz doc/*/*.pdf.gz\ - doc/*/*.???idx doc/*/*.???ind doc/*/*.v.tex doc/*/*.atoc doc/*/*.lof\ - doc/*/*.hatoc doc/*/*.haux doc/*/*.hcomind doc/*/*.herrind doc/*/*.hidx doc/*/*.hind \ - doc/*/*.htacind doc/*/*.htoc doc/*/*.v.html - rm -f doc/stdlib/index-list.html doc/stdlib/index-body.html \ - doc/stdlib/*Library.coqdoc.tex doc/stdlib/library.files \ - doc/stdlib/library.files.ls doc/stdlib/FullLibrary.tex - rm -f doc/*/*.ps doc/*/*.pdf doc/*/*.eps doc/*/*.pdf_t doc/*/*.eps_t - rm -rf doc/stdlib/html doc/tutorial/tutorial.v.html - rm -f doc/common/version.tex - rm -f doc/coq.tex - rm -rf doc/sphinx/_build - -archclean: clean-ide optclean voclean plugin-tutorialclean - rm -rf _build - rm -f $(ALLSTDLIB).* - -optclean: - rm -f $(COQTOPEXE) $(CHICKEN) $(TOPBINOPT) - rm -f $(TOOLS) $(PRIVATEBINARIES) $(CSDPCERT) - find . \( -name '*.cmx' -o -name '*.cmx[as]' -o -name '*.[soa]' -o -name '*.so' \) -exec rm -f {} + - -clean-ide: - rm -f $(COQIDECMO) $(COQIDECMX) $(COQIDECMO:.cmo=.cmi) $(COQIDEBYTE) $(COQIDE) - rm -f ide/input_method_lexer.ml - rm -f ide/highlight.ml ide/config_lexer.ml ide/config_parser.mli ide/config_parser.ml - rm -f ide/utf8_convert.ml - rm -f ide/default.bindings ide/default_bindings_src.exe - rm -rf $(COQIDEAPP) - -mlgclean: - rm -f $(GENMLGFILES) - -depclean: - find . $(FIND_SKIP_DIRS) '(' -name '*.d' ')' -exec rm -f {} + - -cacheclean: - find theories plugins test-suite -name '.*.aux' -exec rm -f {} + - -cleanconfig: - rm -f config/Makefile config/coq_config.ml dev/ocamldebug-coq config/Info-*.plist - -distclean: clean cleanconfig cacheclean timingclean - -voclean: - find theories plugins test-suite \( -name '*.vo' -o -name '*.vio' -o -name '*.vos' -o -name '*.vok' -o -name '*.glob' -o -name "*.cmxs" \ - -o -name "*.native" -o -name "*.cmx" -o -name "*.cmi" -o -name "*.o" \) -exec rm -f {} + - find theories plugins test-suite -name .coq-native -empty -exec rm -rf {} + - -timingclean: - find theories plugins test-suite \( -name '*.v.timing' -o -name '*.v.before-timing' \ - -o -name "*.v.after-timing" -o -name "*.v.timing.diff" -o -name "time-of-build.log" \ - -o -name "time-of-build-before.log" -o -name "time-of-build-after.log" \ - -o -name "time-of-build-pretty.log" -o -name "time-of-build-both.log" \) -exec rm -f {} + - -plugin-tutorialclean: - +$(MAKE) -C $(PLUGINTUTO) clean - -# Ensure that every compiled file around has a known source file. -# This should help preventing weird compilation failures caused by leftover -# compiled files after deleting or moving some source files. - -EXISTINGVO:=$(call find, '*.vo') -KNOWNVO:=$(patsubst %.v,%.vo,$(call find, '*.v')) -ALIENVO:=$(filter-out $(KNOWNVO),$(EXISTINGVO)) - -EXISTINGOBJS:=$(call find, '*.cm[oxia]' -o -name '*.cmxa') -KNOWNML:=$(EXISTINGML) $(GENMLFILES) $(MLPACKFILES:.mlpack=.ml) \ - $(patsubst %.mlp,%.ml,$(wildcard grammar/*.mlp)) -KNOWNOBJS:=$(KNOWNML:.ml=.cmo) $(KNOWNML:.ml=.cmx) $(KNOWNML:.ml=.cmi) \ - $(MLIFILES:.mli=.cmi) \ - gramlib/.pack/gramlib.cma gramlib/.pack/gramlib.cmxa $(MLLIBFILES:.mllib=.cma) $(MLLIBFILES:.mllib=.cmxa) grammar/grammar.cma -ALIENOBJS:=$(filter-out $(KNOWNOBJS),$(EXISTINGOBJS)) - -alienclean: - rm -f $(ALIENOBJS) $(ALIENVO) - -########################################################################### -# Continuous Intregration Tests -########################################################################### -include Makefile.ci - -########################################################################### -# Emacs tags -########################################################################### - -.PHONY: tags printenv - -tags: - echo $(filter-out checker/%, $(MLIFILES)) $(filter-out checker/%, $(MLSTATICFILES)) $(MLGFILES) | sort -r | xargs \ - etags --language=none\ - "--regex=/let[ \t]+\([^ \t]+\)/\1/" \ - "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \ - "--regex=/and[ \t]+\([^ \t]+\)/\1/" \ - "--regex=/type[ \t]+\([^ \t]+\)/\1/" \ - "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \ - "--regex=/val[ \t]+\([^ \t]+\)/\1/" \ - "--regex=/module[ \t]+\([^ \t]+\)/\1/" - echo $(MLGFILES) | sort -r | xargs \ - etags --append --language=none\ - "--regex=/[ \t]*\([^: \t]+\)[ \t]*:/\1/" - -checker-tags: - echo $(filter-out kernel/%, $(MLIFILES)) $(filter-out kernel/%, $(MLSTATICFILES)) $(MLGFILES) | sort -r | xargs \ - etags --language=none\ - "--regex=/let[ \t]+\([^ \t]+\)/\1/" \ - "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \ - "--regex=/and[ \t]+\([^ \t]+\)/\1/" \ - "--regex=/type[ \t]+\([^ \t]+\)/\1/" \ - "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \ - "--regex=/val[ \t]+\([^ \t]+\)/\1/" \ - "--regex=/module[ \t]+\([^ \t]+\)/\1/" - echo $(MLGFILES) | sort -r | xargs \ - etags --append --language=none\ - "--regex=/[ \t]*\([^: \t]+\)[ \t]*:/\1/" - -# Useful to check that the exported variables are within the win32 limits - -printenv: - @env - @echo - @echo -n "Maxsize (win32 limit is 8k) : " - @env | wc -L - @echo -n "Total (win32 limit is 32k) : " - @env | wc -m +# The default build system is make-based one. +include Makefile.make |