diff options
Diffstat (limited to 'src/versions/standard/Makefile')
| -rw-r--r-- | src/versions/standard/Makefile | 1252 |
1 files changed, 661 insertions, 591 deletions
diff --git a/src/versions/standard/Makefile b/src/versions/standard/Makefile index f71b0c8..2337ad7 100644 --- a/src/versions/standard/Makefile +++ b/src/versions/standard/Makefile @@ -1,712 +1,782 @@ -############################################################################# -## v # The Coq Proof Assistant ## -## <O___,, # INRIA - CNRS - LIX - LRI - PPS ## -## \VV/ # ## -## // # Makefile automagically generated by coq_makefile V8.6.1 ## -############################################################################# - -# WARNING +############################################################################### +## v # The Coq Proof Assistant ## +## <O___,, # INRIA - CNRS - LIX - LRI - PPS ## +## \VV/ # ## +## // # ## +############################################################################### +## GNUMakefile for Coq 8.7.2 + +# For debugging purposes (must stay here, don't move below) +INITIAL_VARS := $(.VARIABLES) +# To implement recursion we save the name of the main Makefile +SELF := $(lastword $(MAKEFILE_LIST)) +PARENT := $(firstword $(MAKEFILE_LIST)) + +# This file is generated by coq_makefile and contains many variable +# definitions, like the list of .v files or the path to Coq +include Makefile.conf + +# Put in place old names +VFILES := $(COQMF_VFILES) +MLIFILES := $(COQMF_MLIFILES) +MLFILES := $(COQMF_MLFILES) +ML4FILES := $(COQMF_ML4FILES) +MLPACKFILES := $(COQMF_MLPACKFILES) +MLLIBFILES := $(COQMF_MLLIBFILES) +INSTALLCOQDOCROOT := $(COQMF_INSTALLCOQDOCROOT) +OTHERFLAGS := $(COQMF_OTHERFLAGS) +COQ_SRC_SUBDIRS := $(COQMF_COQ_SRC_SUBDIRS) +OCAMLLIBS := $(COQMF_OCAMLLIBS) +SRC_SUBDIRS := $(COQMF_SRC_SUBDIRS) +COQLIBS := $(COQMF_COQLIBS) +COQLIBS_NOML := $(COQMF_COQLIBS_NOML) +LOCAL := $(COQMF_LOCAL) +COQLIB := $(COQMF_COQLIB) +DOCDIR := $(COQMF_DOCDIR) +OCAMLFIND := $(COQMF_OCAMLFIND) +CAMLP4 := $(COQMF_CAMLP4) +CAMLP4O := $(COQMF_CAMLP4O) +CAMLP4BIN := $(COQMF_CAMLP4BIN) +CAMLP4LIB := $(COQMF_CAMLP4LIB) +CAMLP4OPTIONS := $(COQMF_CAMLP4OPTIONS) +CAMLFLAGS := $(COQMF_CAMLFLAGS) +HASNATDYNLINK := $(COQMF_HASNATDYNLINK) + +Makefile.conf: Make + coq_makefile -f Make -o Makefile + +# This file can be created by the user to hook into double colon rules or +# add any other Makefile code he may need +-include Makefile.local + +# Parameters ################################################################## # -# This Makefile has been automagically generated -# Edit at your own risks ! -# -# END OF WARNING +# Parameters are make variable assignments. +# They can be passed to (each call to) make on the command line. +# They can also be put in Makefile.local once an for all. +# For retro-compatibility reasons they can be put in the _CoqProject, but this +# practice is discouraged since _CoqProject better not contain make specific +# code (be nice to user interfaces). + +# Print shell commands (set to non empty) +VERBOSE ?= + +# Time the Coq process (set to non empty), and how (see default value) +TIMED?= +TIMECMD?= +# Use /usr/bin/env time on linux, gtime on Mac OS +TIMEFMT?="$* (real: %e, user: %U, sys: %S, mem: %M ko)" +ifneq (,$(TIMED)) +ifeq (0,$(shell /usr/bin/env time -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?)) +STDTIME?=/usr/bin/env time -f $(TIMEFMT) +else +ifeq (0,$(shell gtime -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?)) +STDTIME?=gtime -f $(TIMEFMT) +else +STDTIME?=time +endif +endif +else +STDTIME?=/usr/bin/env time -f $(TIMEFMT) +endif +# Coq binaries +COQC ?= "$(COQBIN)coqc" +COQTOP ?= "$(COQBIN)coqtop" +COQCHK ?= "$(COQBIN)coqchk" +COQDEP ?= "$(COQBIN)coqdep" +GALLINA ?= "$(COQBIN)gallina" +COQDOC ?= "$(COQBIN)coqdoc" +COQMKTOP ?= "$(COQBIN)coqmktop" +COQMKFILE ?= "$(COQBIN)coq_makefile" + +# Timing scripts +COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file.py" +COQMAKE_BOTH_TIME_FILES ?= "$(COQLIB)/tools/make-both-time-files.py" +COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQLIB)/tools/make-both-single-timing-files.py" +BEFORE ?= +AFTER ?= + +# FIXME this should be generated by Coq (modules already linked by Coq) +CAMLDONTLINK=camlp5.gramlib,unix,str + +# OCaml binaries +CAMLC ?= "$(OCAMLFIND)" ocamlc -c +CAMLOPTC ?= "$(OCAMLFIND)" opt -c +CAMLLINK ?= "$(OCAMLFIND)" ocamlc -linkpkg -dontlink $(CAMLDONTLINK) +CAMLOPTLINK ?= "$(OCAMLFIND)" opt -linkpkg -dontlink $(CAMLDONTLINK) +CAMLDOC ?= "$(OCAMLFIND)" ocamldoc +CAMLDEP ?= "$(OCAMLFIND)" ocamldep -native -slash -ml-synonym .ml4 -ml-synonym .mlpack + +# DESTDIR is prepended to all installation paths +DESTDIR ?= + +# Debug builds, typically -g to OCaml, -debug to Coq. +CAMLDEBUG ?= +COQDEBUG ?= + +# Extra packages to be linked in (as in findlib -package) +CAMLPKGS ?= + +# Option for making timing files +TIMING?= +# Output file names for timed builds +TIME_OF_BUILD_FILE ?= time-of-build.log +TIME_OF_BUILD_BEFORE_FILE ?= time-of-build-before.log +TIME_OF_BUILD_AFTER_FILE ?= time-of-build-after.log +TIME_OF_PRETTY_BUILD_FILE ?= time-of-build-pretty.log +TIME_OF_PRETTY_BOTH_BUILD_FILE ?= time-of-build-both.log +TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line + +########## End of parameters ################################################## +# What follows may be relevant to you only if you need to +# extend this Makefile. If so, look for 'Extension point' here and +# put in Makefile.local double colon rules accordingly. +# E.g. to perform some work after the all target completes you can write +# +# post-all:: +# echo "All done!" # -# This Makefile was generated by the command line : -# coq_makefile -f Make -o Makefile +# in Makefile.local # +############################################################################### + -.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?= +# Flags ####################################################################### +# +# We define a bunch of variables combining the parameters + SHOW := $(if $(VERBOSE),@true "",@echo "") HIDE := $(if $(VERBOSE),,@) -# Here is a hack to make $(eval $(shell works: -define donewline +TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) +OPT?= -endef -includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr -d '\r' | tr '\n' '@'; }))) -$(call includecmdwithout@,$(COQBIN)coqtop -config) +# The DYNOBJ and DYNLIB variables are used by "coqdep -dyndep var" in .v.d +ifeq '$(OPT)' '-byte' +USEBYTE:=true +DYNOBJ:=.cma +DYNLIB:=.cma +else +USEBYTE:= +DYNOBJ:=.cmxs +DYNLIB:=.cmxs +endif -TIMED?= -TIMECMD?= -STDTIME?=/usr/bin/time -f "$* (user: %U mem: %M ko)" -TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) +COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) +COQCHKFLAGS?=-silent -o $(COQLIBS) +COQDOCFLAGS?=-interpolate -utf8 +COQDOCLIBS?=$(COQLIBS_NOML) -vo_to_obj = $(addsuffix .o,\ - $(filter-out Warning: Error:,\ - $(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(1)))) - -########################## -# # -# Libraries definitions. # -# # -########################## - -OCAMLLIBS?=-I "."\ - -I "bva"\ - -I "classes"\ - -I "array"\ - -I "cnf"\ - -I "euf"\ - -I "lfsc"\ - -I "lia"\ - -I "smtlib2"\ - -I "trace"\ - -I "verit"\ - -I "zchaff"\ - -I "versions/standard"\ - -I "versions/standard/Int63"\ - -I "versions/standard/Array"\ - -I "$(shell $(COQBIN)coqc -where)/plugins/micromega" -COQLIBS?=\ - -R "." SMTCoq\ - -I "."\ - -I "bva"\ - -I "classes"\ - -I "array"\ - -I "cnf"\ - -I "euf"\ - -I "lfsc"\ - -I "lia"\ - -I "smtlib2"\ - -I "trace"\ - -I "verit"\ - -I "zchaff"\ - -I "versions/standard"\ - -I "versions/standard/Int63"\ - -I "versions/standard/Array"\ - -I "$(shell $(COQBIN)coqc -where)/plugins/micromega" -COQCHKLIBS?=\ - -R "." SMTCoq -COQDOCLIBS?=\ - -R "." SMTCoq - -########################## -# # -# Variables definitions. # -# # -########################## - -CAMLLEX=$(CAMLBIN)ocamllex -CAMLYACC=$(CAMLBIN)ocamlyacc +# The version of Coq being run and the version of coq_makefile that +# generated this makefile +COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1) +COQMAKEFILE_VERSION:=8.7.2 -OPT?= -COQDEP?="$(COQBIN)coqdep" -c -COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML) -COQCHKFLAGS?=-silent -o -COQDOCFLAGS?=-interpolate -utf8 -COQC?=$(TIMER) "$(COQBIN)coqc" -GALLINA?="$(COQBIN)gallina" -COQDOC?="$(COQBIN)coqdoc" -COQCHK?="$(COQBIN)coqchk" -COQMKTOP?="$(COQBIN)coqmktop" - -COQSRCLIBS?=-I "$(COQLIB)kernel" \ --I "$(COQLIB)lib" \ --I "$(COQLIB)library" \ --I "$(COQLIB)parsing" \ --I "$(COQLIB)pretyping" \ --I "$(COQLIB)interp" \ --I "$(COQLIB)printing" \ --I "$(COQLIB)intf" \ --I "$(COQLIB)proofs" \ --I "$(COQLIB)tactics" \ --I "$(COQLIB)tools" \ --I "$(COQLIB)ltacprof" \ --I "$(COQLIB)toplevel" \ --I "$(COQLIB)stm" \ --I "$(COQLIB)grammar" \ --I "$(COQLIB)config" \ --I "$(COQLIB)ltac" \ --I "$(COQLIB)engine" \ - \ - -I "$(COQLIB)/plugins/btauto" \ - -I "$(COQLIB)/plugins/cc" \ - -I "$(COQLIB)/plugins/decl_mode" \ - -I "$(COQLIB)/plugins/derive" \ - -I "$(COQLIB)/plugins/extraction" \ - -I "$(COQLIB)/plugins/firstorder" \ - -I "$(COQLIB)/plugins/fourier" \ - -I "$(COQLIB)/plugins/funind" \ - -I "$(COQLIB)/plugins/ltac" \ - -I "$(COQLIB)/plugins/micromega" \ - -I "$(COQLIB)/plugins/nsatz" \ - -I "$(COQLIB)/plugins/omega" \ - -I "$(COQLIB)/plugins/quote" \ - -I "$(COQLIB)/plugins/romega" \ - -I "$(COQLIB)/plugins/rtauto" \ - -I "$(COQLIB)/plugins/setoid_ring" \ - -I "$(COQLIB)/plugins/ssrmatching" \ - -I "$(COQLIB)/plugins/syntax" \ - -I "$(COQLIB)/plugins/xml" -ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB) - -CAMLC?=$(OCAMLFIND) ocamlc -c -rectypes -thread -CAMLOPTC?=$(OCAMLFIND) opt -c -rectypes -thread -CAMLLINK?=$(OCAMLFIND) ocamlc -rectypes -thread -CAMLOPTLINK?=$(OCAMLFIND) opt -rectypes -thread -CAMLDEP?=$(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack -CAMLLIB?=$(shell $(OCAMLFIND) printconf stdlib) -GRAMMARS?=grammar.cma +COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)") + +CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB) + +# ocamldoc fails with unknown argument otherwise +CAMLDOCFLAGS=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS))) + +# FIXME This should be generated by Coq +GRAMMARS:=grammar.cma ifeq ($(CAMLP4),camlp5) CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo else CAMLP4EXTEND= endif -PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(COQLIB)/grammar compat5.cmo \ - $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl' - -################## -# # -# 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. # -# # -###################### - -VFILES:=versions/standard/Int63/Int63.v\ - versions/standard/Int63/Int63Native.v\ - versions/standard/Int63/Int63Op.v\ - versions/standard/Int63/Int63Axioms.v\ - versions/standard/Int63/Int63Properties.v\ - versions/standard/Array/PArray.v\ - versions/standard/Structures.v\ - bva/BVList.v\ - bva/Bva_checker.v\ - classes/SMT_classes.v\ - classes/SMT_classes_instances.v\ - array/FArray.v\ - array/Array_checker.v\ - cnf/Cnf.v\ - euf/Euf.v\ - lia/Lia.v\ - spl/Assumptions.v\ - spl/Syntactic.v\ - spl/Arithmetic.v\ - spl/Operators.v\ - Conversion_tactics.v\ - Misc.v\ - SMTCoq.v\ - ReflectFacts.v\ - PropToBool.v\ - BoolToProp.v\ - Tactics.v\ - SMT_terms.v\ - State.v\ - Trace.v - -ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),) --include $(addsuffix .d,$(VFILES)) +CAMLLIB:=$(shell "$(OCAMLFIND)" printconf stdlib 2> /dev/null) +ifeq (,$(CAMLLIB)) +PP=$(error "Cannot find the 'ocamlfind' binary used to build Coq ($(OCAMLFIND)). Pre-compiled binary packages of Coq do not support compiling plugins this way. Please download the sources of Coq and run the Windows build script.") else -ifeq ($(MAKECMDGOALS),) --include $(addsuffix .d,$(VFILES)) -endif +PP:=-pp '$(CAMLP4O) -I $(CAMLLIB) -I "$(COQLIB)/grammar" $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl' endif -.SECONDARY: $(addsuffix .d,$(VFILES)) - -VO=vo -VOFILES:=$(VFILES:.v=.$(VO)) -GLOBFILES:=$(VFILES:.v=.glob) -GFILES:=$(VFILES:.v=.g) -HTMLFILES:=$(VFILES:.v=.html) -GHTMLFILES:=$(VFILES:.v=.g.html) -OBJFILES=$(call vo_to_obj,$(VOFILES)) -ALLNATIVEFILES=$(OBJFILES:.o=.cmi) $(OBJFILES:.o=.cmo) $(OBJFILES:.o=.cmx) $(OBJFILES:.o=.cmxs) -NATIVEFILES=$(foreach f, $(ALLNATIVEFILES), $(wildcard $f)) -ML4FILES:=g_smtcoq.ml4 - -ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),) --include $(addsuffix .d,$(ML4FILES)) +ifneq (,$(TIMING)) +TIMING_ARG=-time +ifeq (after,$(TIMING)) +TIMING_EXT=after-timing +else +ifeq (before,$(TIMING)) +TIMING_EXT=before-timing else -ifeq ($(MAKECMDGOALS),) --include $(addsuffix .d,$(ML4FILES)) +TIMING_EXT=timing endif endif - -.SECONDARY: $(addsuffix .d,$(ML4FILES)) - -MLFILES:=versions/standard/structures.ml\ - trace/coqTerms.ml\ - trace/smtBtype.ml\ - trace/satAtom.ml\ - trace/smtAtom.ml\ - trace/smtCertif.ml\ - trace/smtCnf.ml\ - trace/smtCommands.ml\ - trace/smtForm.ml\ - trace/smtMisc.ml\ - trace/smtTrace.ml\ - smtlib2/smtlib2_parse.ml\ - smtlib2/smtlib2_lex.ml\ - smtlib2/smtlib2_ast.ml\ - smtlib2/smtlib2_genConstr.ml\ - smtlib2/smtlib2_util.ml\ - smtlib2/sExpr.ml\ - smtlib2/smtlib2_solver.ml\ - smtlib2/sExprParser.ml\ - smtlib2/sExprLexer.ml\ - verit/veritParser.ml\ - verit/veritLexer.ml\ - verit/verit.ml\ - verit/veritSyntax.ml\ - lfsc/shashcons.ml\ - lfsc/hstring.ml\ - lfsc/lfscParser.ml\ - lfsc/type.ml\ - lfsc/ast.ml\ - lfsc/builtin.ml\ - lfsc/tosmtcoq.ml\ - lfsc/converter.ml\ - lfsc/lfsc.ml\ - lfsc/lfscLexer.ml\ - zchaff/cnfParser.ml\ - zchaff/satParser.ml\ - zchaff/zchaff.ml\ - zchaff/zchaffParser.ml\ - lia/lia.ml - -ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),) --include $(addsuffix .d,$(MLFILES)) else -ifeq ($(MAKECMDGOALS),) --include $(addsuffix .d,$(MLFILES)) +TIMING_ARG= endif + +# Retro compatibility (DESTDIR is standard on Unix, DSTROOT is not) +ifdef DSTROOT +DESTDIR := $(DSTROOT) endif -.SECONDARY: $(addsuffix .d,$(MLFILES)) +concat_path = $(if $(1),$(1)/$(subst $(COQMF_WINDRIVE),/,$(2)),$(2)) -MLPACKFILES:=smtcoq_plugin.mlpack +COQLIBINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)user-contrib) +COQDOCINSTALL = $(call concat_path,$(DESTDIR),$(DOCDIR)user-contrib) +COQTOPINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)toploop) -ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),) --include $(addsuffix .d,$(MLPACKFILES)) +# Files ####################################################################### +# +# We here define a bunch of variables about the files being part of the +# Coq project in order to ease the writing of build target and build rules + +ALLSRCFILES := \ + $(VFILES) \ + $(ML4FILES) \ + $(MLFILES) \ + $(MLPACKFILES) \ + $(MLLIBFILES) \ + $(MLIFILES) + +# helpers +vo_to_obj = $(addsuffix .o,\ + $(filter-out Warning: Error:,\ + $(shell $(COQTOP) -q -noinit -batch -quiet -print-mod-uid $(1)))) +strip_dotslash = $(patsubst ./%,%,$(1)) +VO = vo + +VOFILES = $(VFILES:.v=.$(VO)) +GLOBFILES = $(VFILES:.v=.glob) +GFILES = $(VFILES:.v=.g) +HTMLFILES = $(VFILES:.v=.html) +GHTMLFILES = $(VFILES:.v=.g.html) +BEAUTYFILES = $(addsuffix .beautified,$(VFILES)) +TEXFILES = $(VFILES:.v=.tex) +GTEXFILES = $(VFILES:.v=.g.tex) +CMOFILES = \ + $(ML4FILES:.ml4=.cmo) \ + $(MLFILES:.ml=.cmo) \ + $(MLPACKFILES:.mlpack=.cmo) +CMXFILES = $(CMOFILES:.cmo=.cmx) +OFILES = $(CMXFILES:.cmx=.o) +CMAFILES = $(MLLIBFILES:.mllib=.cma) $(MLPACKFILES:.mlpack=.cma) +CMXAFILES = $(CMAFILES:.cma=.cmxa) +CMIFILES = \ + $(CMOFILES:.cmo=.cmi) \ + $(MLIFILES:.mli=.cmi) +# the /if/ is because old _CoqProject did not list a .ml(pack|lib) but just +# a .ml4 file +CMXSFILES = \ + $(MLPACKFILES:.mlpack=.cmxs) \ + $(CMXAFILES:.cmxa=.cmxs) \ + $(if $(MLPACKFILES)$(CMXAFILES),,\ + $(ML4FILES:.ml4=.cmxs) $(MLFILES:.ml=.cmxs)) + +# files that are packed into a plugin (no extension) +PACKEDFILES = \ + $(call strip_dotslash, \ + $(foreach lib, \ + $(call strip_dotslash, \ + $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES)),$($(lib)))) +# files that are archived into a .cma (mllib) +LIBEDFILES = \ + $(call strip_dotslash, \ + $(foreach lib, \ + $(call strip_dotslash, \ + $(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES)),$($(lib)))) +CMIFILESTOINSTALL = $(filter-out $(addsuffix .cmi,$(PACKEDFILES)),$(CMIFILES)) +CMOFILESTOINSTALL = $(filter-out $(addsuffix .cmo,$(PACKEDFILES)),$(CMOFILES)) +OBJFILES = $(call vo_to_obj,$(VOFILES)) +ALLNATIVEFILES = \ + $(OBJFILES:.o=.cmi) \ + $(OBJFILES:.o=.cmx) \ + $(OBJFILES:.o=.cmxs) +# trick: wildcard filters out non-existing files, so that `install` doesn't show +# warnings and `clean` doesn't pass to rm a list of files that is too long for +# the shell. +NATIVEFILES = $(wildcard $(ALLNATIVEFILES)) +FILESTOINSTALL = \ + $(VOFILES) \ + $(VFILES) \ + $(GLOBFILES) \ + $(NATIVEFILES) \ + $(CMIFILESTOINSTALL) +BYTEFILESTOINSTALL = \ + $(CMOFILESTOINSTALL) \ + $(CMAFILES) +ifeq '$(HASNATDYNLINK)' 'true' +DO_NATDYNLINK = yes +FILESTOINSTALL += $(CMXSFILES) $(CMXAFILES) $(CMOFILESTOINSTALL:.cmo=.cmx) else -ifeq ($(MAKECMDGOALS),) --include $(addsuffix .d,$(MLPACKFILES)) -endif +DO_NATDYNLINK = endif -.SECONDARY: $(addsuffix .d,$(MLPACKFILES)) - -MLIFILES:=versions/standard/structures.mli\ - trace/coqTerms.mli\ - trace/smtBtype.mli\ - trace/satAtom.mli\ - trace/smtAtom.mli\ - trace/smtCertif.mli\ - trace/smtCnf.mli\ - trace/smtCommands.mli\ - trace/smtForm.mli\ - trace/smtMisc.mli\ - trace/smtTrace.mli\ - smtlib2/smtlib2_parse.mli\ - smtlib2/smtlib2_lex.mli\ - smtlib2/smtlib2_ast.mli\ - smtlib2/smtlib2_genConstr.mli\ - smtlib2/smtlib2_util.mli\ - smtlib2/sExpr.mli\ - smtlib2/smtlib2_solver.mli\ - smtlib2/sExprParser.mli\ - verit/veritParser.mli\ - verit/veritLexer.mli\ - verit/verit.mli\ - verit/veritSyntax.mli\ - lfsc/shashcons.mli\ - lfsc/hstring.mli\ - lfsc/lfscParser.mli\ - lfsc/ast.mli\ - lfsc/translator_sig.mli\ - lfsc/tosmtcoq.mli\ - zchaff/cnfParser.mli\ - zchaff/satParser.mli\ - zchaff/zchaff.mli\ - zchaff/zchaffParser.mli\ - lia/lia.mli - -ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),) --include $(addsuffix .d,$(MLIFILES)) +ALLDFILES = $(addsuffix .d,$(ALLSRCFILES)) + +# Compilation targets ######################################################### + +all: + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all +.PHONY: all + +all.timing.diff: + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all.timing.diff TIME_OF_PRETTY_BUILD_EXTRA_FILES="" +.PHONY: all.timing.diff + +make-pretty-timed-before:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_BEFORE_FILE) +make-pretty-timed-after:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_AFTER_FILE) +make-pretty-timed make-pretty-timed-before make-pretty-timed-after:: + $(HIDE)rm -f pretty-timed-success.ok + $(HIDE)($(MAKE) --no-print-directory -f "$(PARENT)" $(TGTS) TIMED=1 2>&1 && touch pretty-timed-success.ok) | tee -a $(TIME_OF_BUILD_FILE) + $(HIDE)rm pretty-timed-success.ok # must not be -f; must fail if the touch failed +print-pretty-timed:: + $(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) +print-pretty-timed-diff:: + $(HIDE)$(COQMAKE_BOTH_TIME_FILES) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) +ifeq (,$(BEFORE)) +print-pretty-single-time-diff:: + @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing' + $(HIDE)false else -ifeq ($(MAKECMDGOALS),) --include $(addsuffix .d,$(MLIFILES)) +ifeq (,$(AFTER)) +print-pretty-single-time-diff:: + @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing' + $(HIDE)false +else +print-pretty-single-time-diff:: + $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) $(BEFORE) $(AFTER) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) endif endif +pretty-timed: + $(HIDE)$(MAKE) --no-print-directory -f "$(PARENT)" make-pretty-timed + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-timed +.PHONY: pretty-timed make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff -.SECONDARY: $(addsuffix .d,$(MLIFILES)) +# Extension points for actions to be performed before/after the all target +pre-all:: + @# Extension point + $(HIDE)if [ "$(COQMAKEFILE_VERSION)" != "$(COQ_VERSION)" ]; then\ + echo "W: This Makefile was generated by Coq $(COQMAKEFILE_VERSION)";\ + echo "W: while the current Coq version is $(COQ_VERSION)";\ + fi +.PHONY: pre-all -ALLCMOFILES:=$(ML4FILES:.ml4=.cmo) $(MLFILES:.ml=.cmo) $(MLPACKFILES:.mlpack=.cmo) -CMOFILES=$(filter-out $(addsuffix .cmo,$(foreach lib,$(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES) $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(ALLCMOFILES)) -CMXFILES=$(CMOFILES:.cmo=.cmx) -OFILES=$(CMXFILES:.cmx=.o) -CMIFILES=$(sort $(ALLCMOFILES:.cmo=.cmi) $(MLIFILES:.mli=.cmi)) -CMXSFILES=$(CMXFILES:.cmx=.cmxs) -ifeq '$(HASNATDYNLINK)' 'true' -HASNATDYNLINK_OR_EMPTY := yes -else -HASNATDYNLINK_OR_EMPTY := -endif +post-all:: + @# Extension point +.PHONY: post-all -####################################### -# # -# Definition of the toplevel targets. # -# # -####################################### +real-all: $(VOFILES) $(if $(USEBYTE),bytefiles,optfiles) +.PHONY: real-all -all: $(VOFILES) $(CMOFILES) $(if $(HASNATDYNLINK_OR_EMPTY),$(CMXSFILES)) +real-all.timing.diff: $(VOFILES:.vo=.v.timing.diff) +.PHONE: real-all.timing.diff -mlihtml: $(MLIFILES:.mli=.cmi) - mkdir $@ || rm -rf $@/* - $(OCAMLFIND) ocamldoc -html -rectypes -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli) +bytefiles: $(CMOFILES) $(CMAFILES) +.PHONY: bytefiles -all-mli.tex: $(MLIFILES:.mli=.cmi) - $(OCAMLFIND) ocamldoc -latex -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli) +optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES)) +.PHONY: optfiles +# FIXME, see Ralph's bugreport quick: $(VOFILES:.vo=.vio) +.PHONY: quick vio2vo: - $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio) -checkproofs: - $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio) -gallina: $(GFILES) - -html: $(GLOBFILES) $(VFILES) - - mkdir -p html - $(COQDOC) -toc $(COQDOCFLAGS) -html $(COQDOCLIBS) -d html $(VFILES) - -gallinahtml: $(GLOBFILES) $(VFILES) - - mkdir -p html - $(COQDOC) -toc $(COQDOCFLAGS) -html -g $(COQDOCLIBS) -d html $(VFILES) + $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) \ + -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio) +.PHONY: vio2vo -all.ps: $(VFILES) - $(COQDOC) -toc $(COQDOCFLAGS) -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^` - -all-gal.ps: $(VFILES) - $(COQDOC) -toc $(COQDOCFLAGS) -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^` - -all.pdf: $(VFILES) - $(COQDOC) -toc $(COQDOCFLAGS) -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^` - -all-gal.pdf: $(VFILES) - $(COQDOC) -toc $(COQDOCFLAGS) -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^` +checkproofs: + $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) \ + -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio) +.PHONY: checkproofs validate: $(VOFILES) - $(COQCHK) $(COQCHKFLAGS) $(COQCHKLIBS) $(notdir $(^:.vo=)) + $(TIMER) $(COQCHK) $(COQCHKFLAGS) $(notdir $(^:.vo=)) +.PHONY: validate -beautify: $(VFILES:=.beautified) - for file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done - @echo 'Do not do "make clean" until you are sure that everything went well!' - @echo 'If there were a problem, execute "for file in $$(find . -name \*.v.old -print); do mv $${file} $${file%.old}; done" in your shell/' +only: $(TGTS) +.PHONY: only -.PHONY: all archclean beautify byte clean cleanall gallina gallinahtml html install install-doc install-natdynlink install-toploop opt printenv quick uninstall userinstall validate vio2vo ./ smtcoq_plugin.mlpack.d +# Documentation targets ####################################################### -################### -# # -# Custom targets. # -# # -################### - -test: - cd ../unit-tests; make - -ztest: - cd ../unit-tests; make zchaff - -vtest: - cd ../unit-tests; make verit - -lfsctest: - cd ../unit-tests; make lfsc - -%.ml: %.mll - $(CAMLLEX) $< - -%.ml %.mli: %.mly - $(CAMLYACC) $< - -smtcoq_plugin.mlpack.d: verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml smtlib2/sExprParser.ml smtlib2/sExprLexer.ml lfsc/lfscParser.ml lfsc/lfscLexer.ml +html: $(GLOBFILES) $(VFILES) + $(SHOW)'COQDOC -d html $(GAL)' + $(HIDE)mkdir -p html + $(HIDE)$(COQDOC) \ + -toc $(COQDOCFLAGS) -html $(GAL) $(COQDOCLIBS) -d html $(VFILES) -################### -# # -# Subdirectories. # -# # -################### +mlihtml: $(MLIFILES:.mli=.cmi) + $(SHOW)'CAMLDOC -d $@' + $(HIDE)mkdir $@ || rm -rf $@/* + $(HIDE)$(CAMLDOC) -html \ + -d $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES) -./: - +cd "./" && $(MAKE) all +all-mli.tex: $(MLIFILES:.mli=.cmi) + $(SHOW)'CAMLDOC -latex $@' + $(HIDE)$(CAMLDOC) -latex \ + -o $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES) -##################################### -# # -# Ad-hoc implicit rules for mlpack. # -# # -##################################### +gallina: $(GFILES) -$(addsuffix .cmx,$(filter $(basename $(MLFILES)),$(smtcoq_plugin_MLPACK_DEPENDENCIES))): %.cmx: %.ml - $(SHOW)'CAMLOPT -c -for-pack Smtcoq_plugin $<' - $(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -for-pack Smtcoq_plugin $< +all.ps: $(VFILES) + $(SHOW)'COQDOC -ps $(GAL)' + $(HIDE)$(COQDOC) \ + -toc $(COQDOCFLAGS) -ps $(GAL) $(COQDOCLIBS) \ + -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)` -$(addsuffix .cmx,$(filter $(basename $(ML4FILES)),$(smtcoq_plugin_MLPACK_DEPENDENCIES))): %.cmx: %.ml4 - $(SHOW)'CAMLOPT -c -pp -for-pack Smtcoq_plugin $<' - $(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -for-pack Smtcoq_plugin $(PP) -impl $< +all.pdf: $(VFILES) + $(SHOW)'COQDOC -pdf $(GAL)' + $(HIDE)$(COQDOC) \ + -toc $(COQDOCFLAGS) -pdf $(GAL) $(COQDOCLIBS) \ + -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)` -#################### -# # -# Special targets. # -# # -#################### +# FIXME: not quite right, since the output name is different +gallinahtml: GAL=-g +gallinahtml: html -byte: - $(MAKE) all "OPT:=-byte" +all-gal.ps: GAL=-g +all-gal.ps: all.ps -opt: - $(MAKE) all "OPT:=-opt" +all-gal.pdf: GAL=-g +all-gal.pdf: all.pdf -userinstall: - +$(MAKE) USERINSTALL=true install +# ? +beautify: $(BEAUTYFILES) + for file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done + @echo 'Do not do "make clean" until you are sure that everything went well!' + @echo 'If there were a problem, execute "for file in $$(find . -name \*.v.old -print); do mv $${file} $${file%.old}; done" in your shell/' +.PHONY: beautify -install-natdynlink: - cd "." && for i in $(CMXSFILES); do \ - install -d "`dirname "$(DSTROOT)"$(COQLIBINSTALL)/SMTCoq/$$i`"; \ - install -m 0755 $$i "$(DSTROOT)"$(COQLIBINSTALL)/SMTCoq/$$i; \ +# Installation targets ######################################################## +# +# There rules can be extended in Makefile.local +# Extensions can't assume when they run. + +install: + $(HIDE)for f in $(FILESTOINSTALL); do\ + df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\ + if [ "$$?" != "0" -o -z "$$df" ]; then\ + echo SKIP "$$f" since it has no logical path;\ + else\ + install -d "$(COQLIBINSTALL)/$$df" &&\ + install -m 0644 "$$f" "$(COQLIBINSTALL)/$$df" &&\ + echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\ + fi;\ done - -install-toploop: $(MLLIBFILES:.mllib=.cmxs) - install -d "$(DSTROOT)"$(COQTOPINSTALL)/ - install -m 0755 $? "$(DSTROOT)"$(COQTOPINSTALL)/ - -install:$(if $(HASNATDYNLINK_OR_EMPTY),install-natdynlink) - cd "." && for i in $(VOFILES) $(VFILES) $(GLOBFILES) $(NATIVEFILES) $(CMOFILES) $(CMIFILES) $(CMAFILES); do \ - install -d "`dirname "$(DSTROOT)"$(COQLIBINSTALL)/SMTCoq/$$i`"; \ - install -m 0644 $$i "$(DSTROOT)"$(COQLIBINSTALL)/SMTCoq/$$i; \ + $(HIDE)$(MAKE) install-extra -f "$(SELF)" +install-extra:: + @# Extension point +.PHONY: install install-extra + +install-byte: + $(HIDE)for f in $(BYTEFILESTOINSTALL); do\ + df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\ + if [ "$$?" != "0" -o -z "$$df" ]; then\ + echo SKIP "$$f" since it has no logical path;\ + else\ + install -d "$(COQLIBINSTALL)/$$df" &&\ + install -m 0644 "$$f" "$(COQLIBINSTALL)/$$df" &&\ + echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\ + fi;\ done -install-doc: - install -d "$(DSTROOT)"$(COQDOCINSTALL)/SMTCoq/html - for i in html/*; do \ - install -m 0644 $$i "$(DSTROOT)"$(COQDOCINSTALL)/SMTCoq/$$i;\ +install-doc:: html mlihtml + @# Extension point + $(HIDE)install -d "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html" + $(HIDE)for i in html/*; do \ + dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\ + install -m 0644 "$$i" "$$dest";\ + echo INSTALL "$$i" "$$dest";\ done - install -d "$(DSTROOT)"$(COQDOCINSTALL)/SMTCoq/mlihtml - for i in mlihtml/*; do \ - install -m 0644 $$i "$(DSTROOT)"$(COQDOCINSTALL)/SMTCoq/$$i;\ + $(HIDE)install -d \ + "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml" + $(HIDE)for i in mlihtml/*; do \ + dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\ + install -m 0644 "$$i" "$$dest";\ + echo INSTALL "$$i" "$$dest";\ done - -uninstall_me.sh: Makefile - echo '#!/bin/sh' > $@ - printf 'cd "$${DSTROOT}"$(COQLIBINSTALL)/SMTCoq && rm -f $(CMXSFILES) && find . -type d -and -empty -delete\ncd "$${DSTROOT}"$(COQLIBINSTALL) && find "SMTCoq" -maxdepth 0 -and -empty -exec rmdir -p \{\} \;\n' >> "$@" - printf 'cd "$${DSTROOT}"$(COQLIBINSTALL)/SMTCoq && rm -f $(VOFILES) $(VFILES) $(GLOBFILES) $(NATIVEFILES) $(CMOFILES) $(CMIFILES) $(CMAFILES) && find . -type d -and -empty -delete\ncd "$${DSTROOT}"$(COQLIBINSTALL) && find "SMTCoq" -maxdepth 0 -and -empty -exec rmdir -p \{\} \;\n' >> "$@" - printf 'cd "$${DSTROOT}"$(COQDOCINSTALL)/SMTCoq \\\n' >> "$@" - printf '&& rm -f $(shell find "html" -maxdepth 1 -and -type f -print)\n' >> "$@" - printf 'cd "$${DSTROOT}"$(COQDOCINSTALL) && find SMTCoq/html -maxdepth 0 -and -empty -exec rmdir -p \{\} \;\n' >> "$@" - printf 'cd "$${DSTROOT}"$(COQDOCINSTALL)/SMTCoq \\\n' >> "$@" - printf '&& rm -f $(shell find "mlihtml" -maxdepth 1 -and -type f -print)\n' >> "$@" - printf 'cd "$${DSTROOT}"$(COQDOCINSTALL) && find SMTCoq/mlihtml -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 - @echo "B /home/artemis/Recherche/github.com/ckeller/smtcoq-lfsc/src/versions/standard" >> .merlin - @echo "S /home/artemis/Recherche/github.com/ckeller/smtcoq-lfsc/src/versions/standard" >> .merlin - @echo "B bva" >> .merlin - @echo "S bva" >> .merlin - @echo "B classes" >> .merlin - @echo "S classes" >> .merlin - @echo "B array" >> .merlin - @echo "S array" >> .merlin - @echo "B cnf" >> .merlin - @echo "S cnf" >> .merlin - @echo "B euf" >> .merlin - @echo "S euf" >> .merlin - @echo "B lfsc" >> .merlin - @echo "S lfsc" >> .merlin - @echo "B lia" >> .merlin - @echo "S lia" >> .merlin - @echo "B smtlib2" >> .merlin - @echo "S smtlib2" >> .merlin - @echo "B trace" >> .merlin - @echo "S trace" >> .merlin - @echo "B verit" >> .merlin - @echo "S verit" >> .merlin - @echo "B zchaff" >> .merlin - @echo "S zchaff" >> .merlin - @echo "B versions/standard" >> .merlin - @echo "S versions/standard" >> .merlin - @echo "B versions/standard/Int63" >> .merlin - @echo "S versions/standard/Int63" >> .merlin - @echo "B versions/standard/Array" >> .merlin - @echo "S versions/standard/Array" >> .merlin - @echo "B $(shell $(COQBIN)coqc -where)/plugins/micromega" >> .merlin - @echo "S $(shell $(COQBIN)coqc -where)/plugins/micromega" >> .merlin +.PHONY: install-doc + +uninstall:: + @# Extension point + $(HIDE)for f in $(FILESTOINSTALL); do \ + df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\ + instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\ + rm -f "$$instf" &&\ + echo RM "$$instf" &&\ + (rmdir "$(call concat_path,,$(COQLIBINSTALL)/$$df/)" 2>/dev/null || true); \ + done +.PHONY: uninstall + +uninstall-doc:: + @# Extension point + $(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html' + $(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html" + $(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml' + $(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml" + $(HIDE) rmdir "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/" || true +.PHONY: uninstall-doc + +# Cleaning #################################################################### +# +# There rules can be extended in Makefile.local +# Extensions can't assume when they run. clean:: - rm -f $(ALLCMOFILES) $(CMIFILES) $(CMAFILES) - rm -f $(ALLCMOFILES:.cmo=.cmx) $(CMXAFILES) $(CMXSFILES) $(ALLCMOFILES:.cmo=.o) $(CMXAFILES:.cmxa=.a) - rm -f $(addsuffix .d,$(MLFILES) $(MLIFILES) $(ML4FILES) $(MLLIBFILES) $(MLPACKFILES)) - rm -f $(OBJFILES) $(OBJFILES:.o=.native) $(NATIVEFILES) - find . -name .coq-native -type d -empty -delete - rm -f $(VOFILES) $(VOFILES:.vo=.vio) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old) - 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 - - rm -rf test - - rm -rf ztest - - rm -rf vtest - - rm -rf lfsctest - - rm -f ../unit-tests/*.vo ../unit-tests/*.zlog ../unit-tests/*.vtlog verit/veritParser.mli verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.mli smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml smtlib2/sExprParser.mli smtlib2/sExprParser.ml smtlib2/sExprLexer.ml + @# Extension point + $(SHOW)'CLEAN' + $(HIDE)rm -f $(CMOFILES) + $(HIDE)rm -f $(CMIFILES) + $(HIDE)rm -f $(CMAFILES) + $(HIDE)rm -f $(CMOFILES:.cmo=.cmx) + $(HIDE)rm -f $(CMXAFILES) + $(HIDE)rm -f $(CMXSFILES) + $(HIDE)rm -f $(CMOFILES:.cmo=.o) + $(HIDE)rm -f $(CMXAFILES:.cmxa=.a) + $(HIDE)rm -f $(ALLDFILES) + $(HIDE)rm -f $(NATIVEFILES) + $(HIDE)find . -name .coq-native -type d -empty -delete + $(HIDE)rm -f $(VOFILES) + $(HIDE)rm -f $(VOFILES:.vo=.vio) + $(HIDE)rm -f $(GFILES) + $(HIDE)rm -f $(BEAUTYFILES) $(VFILES:=.old) + $(HIDE)rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob all-mli.tex + $(HIDE)rm -f $(VFILES:.v=.glob) + $(HIDE)rm -f $(VFILES:.v=.tex) + $(HIDE)rm -f $(VFILES:.v=.g.tex) + $(HIDE)rm -f pretty-timed-success.ok + $(HIDE)rm -rf html mlihtml +.PHONY: clean cleanall:: clean - rm -f $(foreach f,$(VFILES:.v=),$(dir $(f)).$(notdir $(f)).aux) + @# Extension point + $(SHOW)'CLEAN *.aux *.timing' + $(HIDE)rm -f $(foreach f,$(VFILES:.v=),$(dir $(f)).$(notdir $(f)).aux) + $(HIDE)rm -f $(TIME_OF_BUILD_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) + $(HIDE)rm -f $(VOFILES:.vo=.v.timing) + $(HIDE)rm -f $(VOFILES:.vo=.v.before-timing) + $(HIDE)rm -f $(VOFILES:.vo=.v.after-timing) + $(HIDE)rm -f $(VOFILES:.vo=.v.timing.diff) +.PHONY: cleanall archclean:: - rm -f *.cmx *.o - +cd ./ && $(MAKE) archclean + @# Extension point + $(SHOW)'CLEAN *.cmx *.o' + $(HIDE)rm -f $(NATIVEFILES) + $(HIDE)rm -f $(CMOFILES:%.cmo=%.cmx) +.PHONY: archclean -printenv: - @"$(COQBIN)coqtop" -config - @echo 'OCAMLFIND = $(OCAMLFIND)' - @echo 'PP = $(PP)' - @echo 'COQFLAGS = $(COQFLAGS)' - @echo 'COQLIBINSTALL = $(COQLIBINSTALL)' - @echo 'COQDOCINSTALL = $(COQDOCINSTALL)' - -################### -# # -# Implicit rules. # -# # -################### +# Compilation rules ########################################################### $(MLIFILES:.mli=.cmi): %.cmi: %.mli $(SHOW)'CAMLC -c $<' - $(HIDE)$(CAMLC) $(ZDEBUG) $(ZFLAGS) $< - -$(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli - $(SHOW)'CAMLDEP $<' - $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) + $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $< $(ML4FILES:.ml4=.cmo): %.cmo: %.ml4 $(SHOW)'CAMLC -pp -c $<' - $(HIDE)$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $< + $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(PP) -impl $< -$(filter-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(ML4FILES:.ml4=.cmx)): %.cmx: %.ml4 - $(SHOW)'CAMLOPT -pp -c $<' - $(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $< - -$(addsuffix .d,$(ML4FILES)): %.ml4.d: %.ml4 - $(SHOW)'CAMLDEP -pp $<' - $(HIDE)$(CAMLDEP) $(OCAMLLIBS) $(PP) -impl "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) +$(ML4FILES:.ml4=.cmx): %.cmx: %.ml4 + $(SHOW)'CAMLOPT -pp -c $(FOR_PACK) $<' + $(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(PP) $(FOR_PACK) -impl $< $(MLFILES:.ml=.cmo): %.cmo: %.ml $(SHOW)'CAMLC -c $<' - $(HIDE)$(CAMLC) $(ZDEBUG) $(ZFLAGS) $< + $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $< -$(filter-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(MLFILES:.ml=.cmx)): %.cmx: %.ml - $(SHOW)'CAMLOPT -c $<' - $(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $< +$(MLFILES:.ml=.cmx): %.cmx: %.ml + $(SHOW)'CAMLOPT -c $(FOR_PACK) $<' + $(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(FOR_PACK) $< -$(addsuffix .d,$(MLFILES)): %.ml.d: %.ml - $(SHOW)'CAMLDEP $<' - $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) -$(filter-out $(MLLIBFILES:.mllib=.cmxs),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs) $(MLPACKFILES:.mlpack=.cmxs)): %.cmxs: %.cmx +$(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa $(SHOW)'CAMLOPT -shared -o $@' - $(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $< + $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ + -linkall -shared -o $@ $< -$(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa +$(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib + $(SHOW)'CAMLC -a -o $@' + $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^ + +$(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib + $(SHOW)'CAMLOPT -a -o $@' + $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^ + + +$(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmxa $(SHOW)'CAMLOPT -shared -o $@' - $(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -linkall -shared -o $@ $< + $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ + -shared -linkall -o $@ $< + +$(MLPACKFILES:.mlpack=.cmxa): %.cmxa: %.cmx + $(SHOW)'CAMLOPT -a -o $@' + $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $< + +$(MLPACKFILES:.mlpack=.cma): %.cma: %.cmo | %.mlpack + $(SHOW)'CAMLC -a -o $@' + $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^ $(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack $(SHOW)'CAMLC -pack -o $@' - $(HIDE)$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^ + $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^ $(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack $(SHOW)'CAMLOPT -pack -o $@' - $(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^ + $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^ -$(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack - $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) +# This rule is for _CoqProject with no .mllib nor .mlpack +$(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs)): %.cmxs: %.cmx + $(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@' + $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ + -shared -o $@ $< + +ifneq (,$(TIMING)) +TIMING_EXTRA = > $<.$(TIMING_EXT) +else +TIMING_EXTRA = +endif $(VOFILES): %.vo: %.v $(SHOW)COQC $< - $(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) $< + $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $< $(TIMING_EXTRA) +# FIXME ?merge with .vo / .vio ? $(GLOBFILES): %.glob: %.v - $(COQC) $(COQDEBUG) $(COQFLAGS) $< + $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $< $(VFILES:.v=.vio): %.vio: %.v - $(COQC) -quick $(COQDEBUG) $(COQFLAGS) $< + $(SHOW)COQC -quick $< + $(HIDE)$(TIMER) $(COQC) -quick $(COQDEBUG) $(COQFLAGS) $< + +$(addsuffix .timing.diff,$(VFILES)): %.timing.diff : %.before-timing %.after-timing + $(SHOW)PYTHON TIMING-DIFF $< + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-single-time-diff BEFORE=$*.before-timing AFTER=$*.after-timing TIME_OF_PRETTY_BUILD_FILE="$@" + +$(BEAUTYFILES): %.v.beautified: %.v + $(SHOW)'BEAUTIFY $<' + $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $< $(GFILES): %.g: %.v - $(GALLINA) $< + $(SHOW)'GALLINA $<' + $(HIDE)$(GALLINA) $< -$(VFILES:.v=.tex): %.tex: %.v - $(COQDOC) $(COQDOCFLAGS) -latex $< -o $@ +$(TEXFILES): %.tex: %.v + $(SHOW)'COQDOC -latex $<' + $(HIDE)$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@ -$(HTMLFILES): %.html: %.v %.glob - $(COQDOC) $(COQDOCFLAGS) -html $< -o $@ +$(GTEXFILES): %.g.tex: %.v + $(SHOW)'COQDOC -latex -g $<' + $(HIDE)$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@ -$(VFILES:.v=.g.tex): %.g.tex: %.v - $(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@ +$(HTMLFILES): %.html: %.v %.glob + $(SHOW)'COQDOC -html $<' + $(HIDE)$(COQDOC) $(COQDOCFLAGS) -html $< -o $@ $(GHTMLFILES): %.g.html: %.v %.glob - $(COQDOC) $(COQDOCFLAGS) -html -g $< -o $@ + $(SHOW)'COQDOC -html -g $<' + $(HIDE)$(COQDOC) $(COQDOCFLAGS) -html -g $< -o $@ + +# Dependency files ############################################################ + +ifneq ($(filter-out archclean clean cleanall printenv make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff,$(MAKECMDGOALS)),) + -include $(ALLDFILES) +else + ifeq ($(MAKECMDGOALS),) + -include $(ALLDFILES) + endif +endif + +.SECONDARY: $(ALLDFILES) + +redir_if_ok = > "$@" || ( RV=$$?; rm -f "$@"; exit $$RV ) + +$(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli + $(SHOW)'CAMLDEP $<' + $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) + +$(addsuffix .d,$(ML4FILES)): %.ml4.d: %.ml4 + $(SHOW)'CAMLDEP -pp $<' + $(HIDE)$(CAMLDEP) $(OCAMLLIBS) $(PP) -impl "$<" $(redir_if_ok) + +$(addsuffix .d,$(MLFILES)): %.ml.d: %.ml + $(SHOW)'CAMLDEP $<' + $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) + +$(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib + $(SHOW)'COQDEP $<' + $(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok) + +$(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack + $(SHOW)'COQDEP $<' + $(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok) $(addsuffix .d,$(VFILES)): %.v.d: %.v $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEP) $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) + $(HIDE)$(COQDEP) $(COQLIBS) -dyndep var -c "$<" $(redir_if_ok) -$(addsuffix .beautified,$(VFILES)): %.v.beautified: - $(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*.v +# Misc ######################################################################## -# WARNING -# -# This Makefile has been automagically generated -# Edit at your own risks ! -# -# END OF WARNING +byte: + $(HIDE)$(MAKE) all "OPT:=-byte" -f "$(SELF)" +.PHONY: byte +opt: + $(HIDE)$(MAKE) all "OPT:=-opt" -f "$(SELF)" +.PHONY: opt + +# This is deprecated. To extend this makefile use +# extension points and Makefile.local +printenv:: + $(warning printenv is deprecated) + $(warning write extensions in Makefile.local or include Makefile.conf) + @echo 'LOCAL = $(LOCAL)' + @echo 'COQLIB = $(COQLIB)' + @echo 'DOCDIR = $(DOCDIR)' + @echo 'OCAMLFIND = $(OCAMLFIND)' + @echo 'CAMLP4 = $(CAMLP4)' + @echo 'CAMLP4O = $(CAMLP4O)' + @echo 'CAMLP4BIN = $(CAMLP4BIN)' + @echo 'CAMLP4LIB = $(CAMLP4LIB)' + @echo 'CAMLP4OPTIONS = $(CAMLP4OPTIONS)' + @echo 'HASNATDYNLINK = $(HASNATDYNLINK)' + @echo 'SRC_SUBDIRS = $(SRC_SUBDIRS)' + @echo 'COQ_SRC_SUBDIRS = $(COQ_SRC_SUBDIRS)' + @echo 'OCAMLFIND = $(OCAMLFIND)' + @echo 'PP = $(PP)' + @echo 'COQFLAGS = $(COQFLAGS)' + @echo 'COQLIBINSTALL = $(COQLIBINSTALL)' + @echo 'COQDOCINSTALL = $(COQDOCINSTALL)' +.PHONY: printenv + +# Generate a .merlin file. If you need to append directives to this +# file you can extend the merlin-hook target in Makefile.local +.merlin: + $(SHOW)'FILL .merlin' + $(HIDE)echo 'FLG $(COQMF_CAMLFLAGS)' > .merlin + $(HIDE)echo 'B $(COQLIB)' >> .merlin + $(HIDE)echo 'S $(COQLIB)' >> .merlin + $(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \ + echo 'B $(COQLIB)$(d)' >> .merlin;) + $(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \ + echo 'S $(COQLIB)$(d)' >> .merlin;) + $(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'B $(d)' >> .merlin;) + $(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'S $(d)' >> .merlin;) + $(HIDE)$(MAKE) merlin-hook -f "$(SELF)" +.PHONY: merlin + +merlin-hook:: + @# Extension point +.PHONY: merlin-hook + +# prints all variables +debug: + $(foreach v,\ + $(sort $(filter-out $(INITIAL_VARS) INITIAL_VARS,\ + $(.VARIABLES))),\ + $(info $(v) = $($(v)))) +.PHONY: debug + +.DEFAULT_GOAL := all |