Warning: Targets for subdirectories are very fragile. For example, nothing is done to handle dependencies with them. ############################################################################# ## v # The Coq Proof Assistant ## ## <O___,, # INRIA - CNRS - LIX - LRI - PPS ## ## \VV/ # ## ## // # Makefile automagically generated by coq_makefile V8.6 ## ############################################################################# # WARNING # # This Makefile has been automagically generated # Edit at your own risks ! # # END OF WARNING # # This Makefile was generated by the command line : # coq_makefile --version # .DEFAULT_GOAL := all # This Makefile may take arguments passed as environment variables: # COQBIN to specify the directory where Coq binaries resides; # TIMECMD set a command to log .v compilation time; # TIMED if non empty, use the default time command as TIMECMD; # ZDEBUG/COQDEBUG to specify debug flags for ocamlc&ocamlopt/coqc; # DSTROOT to specify a prefix to install path. # VERBOSE to disable the short display of compilation rules. VERBOSE?= SHOW := $(if $(VERBOSE),@true "",@echo "") HIDE := $(if $(VERBOSE),,@) # Here is a hack to make $(eval $(shell works: define donewline endef includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr -d '\r' | tr '\n' '@'; }))) $(call includecmdwithout@,$(COQBIN)coqtop -config) TIMED?= TIMECMD?= STDTIME?=/usr/bin/time -f "$* (user: %U mem: %M ko)" TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) vo_to_obj = $(addsuffix .o,\ $(filter-out Warning: Error:,\ $(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(1)))) ########################## # # # Libraries definitions. # # # ########################## ########################## # # # Variables definitions. # # # ########################## OPT?= ################## # # # Install Paths. # # # ################## ifdef USERINSTALL XDG_DATA_HOME?="$(HOME)/.local/share" COQLIBINSTALL=$(XDG_DATA_HOME)/coq COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq else COQLIBINSTALL="${COQLIB}user-contrib" COQDOCINSTALL="${DOCDIR}user-contrib" COQTOPINSTALL="${COQLIB}toploop" endif ###################### # # # Files dispatching. # # # ###################### ifeq '$(HASNATDYNLINK)' 'true' HASNATDYNLINK_OR_EMPTY := yes else HASNATDYNLINK_OR_EMPTY := endif ####################################### # # # Definition of the toplevel targets. # # # ####################################### all: ./--version .PHONY: all archclean beautify byte clean cleanall gallina gallinahtml html install install-doc install-natdynlink install-toploop opt printenv quick uninstall userinstall validate vio2vo ./--version ################### # # # Subdirectories. # # # ################### ./--version: +cd "./--version" && $(MAKE) all #################### # # # Special targets. # # # #################### byte: $(MAKE) all "OPT:=-byte" opt: $(MAKE) all "OPT:=-opt" userinstall: +$(MAKE) USERINSTALL=true install install: +cd ./--version && $(MAKE) DSTROOT="$(DSTROOT)" INSTALLDEFAULTROOT="$(INSTALLDEFAULTROOT)/./--version" install install-doc: uninstall_me.sh: Makefile echo '#!/bin/sh' > $@ printf 'cd "$${DSTROOT}"$(COQLIBINSTALL)/$(INSTALLDEFAULTROOT) && find . -type d -and -empty -delete\ncd "$${DSTROOT}"$(COQLIBINSTALL) && find "$(INSTALLDEFAULTROOT)" -maxdepth 0 -and -empty -exec rmdir -p \{\} \;\n' >> "$@" chmod +x $@ uninstall: uninstall_me.sh sh $< .merlin: @echo 'FLG -rectypes' > .merlin @echo "B $(COQLIB)kernel" >> .merlin @echo "B $(COQLIB)lib" >> .merlin @echo "B $(COQLIB)library" >> .merlin @echo "B $(COQLIB)parsing" >> .merlin @echo "B $(COQLIB)pretyping" >> .merlin @echo "B $(COQLIB)interp" >> .merlin @echo "B $(COQLIB)printing" >> .merlin @echo "B $(COQLIB)intf" >> .merlin @echo "B $(COQLIB)proofs" >> .merlin @echo "B $(COQLIB)tactics" >> .merlin @echo "B $(COQLIB)tools" >> .merlin @echo "B $(COQLIB)ltacprof" >> .merlin @echo "B $(COQLIB)toplevel" >> .merlin @echo "B $(COQLIB)stm" >> .merlin @echo "B $(COQLIB)grammar" >> .merlin @echo "B $(COQLIB)config" >> .merlin @echo "B $(COQLIB)ltac" >> .merlin @echo "B $(COQLIB)engine" >> .merlin clean:: rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex - rm -rf html mlihtml uninstall_me.sh +cd ./--version && $(MAKE) clean archclean:: rm -f *.cmx *.o +cd ./--version && $(MAKE) archclean printenv: @"$(COQBIN)coqtop" -config @echo 'OCAMLFIND = $(OCAMLFIND)' @echo 'PP = $(PP)' @echo 'COQFLAGS = $(COQFLAGS)' @echo 'COQLIBINSTALL = $(COQLIBINSTALL)' @echo 'COQDOCINSTALL = $(COQDOCINSTALL)' ################### # # # Implicit rules. # # # ################### # WARNING # # This Makefile has been automagically generated # Edit at your own risks ! # # END OF WARNING

Usage summary: coq_makefile .... [file.v] ... [file.ml[i4]?] ... [file.ml{lib,pack}] ... [any] ... [-extra[-phony] result dependencies command] ... [-I dir] ... [-R physicalpath logicalpath] ... [-Q physicalpath logicalpath] ... [VARIABLE = value] ... [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file] [-h] [--help] [file.v]: Coq file to be compiled [file.ml[i4]?]: Objective Caml file to be compiled [file.ml{lib,pack}]: ocamlbuild file that describes a Objective Caml library/module [any] : subdirectory that should be "made" and has a Makefile itself to do so. Very fragile and discouraged. [-extra result dependencies command]: add target "result" with command "command" and dependencies "dependencies". If "result" is not generic (do not contains a %), "result" is built by _make all_ and deleted by _make clean_. [-extra-phony result dependencies command]: add a PHONY target "result" with command "command" and dependencies "dependencies". Note that _-extra-phony foo bar ""_ is a regular way to add the target "bar" as as a dependencies of an already defined target "foo". [-I dir]: look for Objective Caml dependencies in "dir" [-R physicalpath logicalpath]: look for Coq dependencies resursively starting from "physicalpath". The logical path associated to the physical path is "logicalpath". [-Q physicalpath logicalpath]: look for Coq dependencies starting from "physicalpath". The logical path associated to the physical path is "logicalpath". [VARIABLE = value]: Add the variable definition "VARIABLE=value" [-byte]: compile with byte-code version of coq [-opt]: compile with native-code version of coq [-arg opt]: send option "opt" to coqc [-install opt]: where opt is "user" to force install into user directory, "none" to build a makefile with no install target or "global" to force install in $COQLIB directory [-f file]: take the contents of file as arguments [-o file]: output should go in file file Output file outside the current directory is forbidden. [-h]: print this usage summary [--help]: equivalent to [-h]