From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- Makefile.common | 392 +++++++++++++------------------------------------------- 1 file changed, 90 insertions(+), 302 deletions(-) (limited to 'Makefile.common') diff --git a/Makefile.common b/Makefile.common index 1a903539..49fe1fd9 100644 --- a/Makefile.common +++ b/Makefile.common @@ -14,19 +14,32 @@ COQMKTOP:=bin/coqmktop$(EXE) -COQC:=bin/coqc$(EXE) - COQTOPBYTE:=bin/coqtop.byte$(EXE) COQTOPEXE:=bin/coqtop$(EXE) -CHICKENBYTE:=bin/coqchk.byte$(EXE) -CHICKEN:=bin/coqchk$(EXE) +COQDEP:=bin/coqdep$(EXE) +COQMAKEFILE:=bin/coq_makefile$(EXE) +GALLINA:=bin/gallina$(EXE) +COQTEX:=bin/coq-tex$(EXE) +COQWC:=bin/coqwc$(EXE) +COQDOC:=bin/coqdoc$(EXE) +COQC:=bin/coqc$(EXE) +COQWORKMGR:=bin/coqworkmgr$(EXE) -ifeq ($(CAMLP4),camlp4) -CAMLP4MOD:=camlp4lib -else -CAMLP4MOD:=gramlib -endif +TOOLS:=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQWC) $(COQDOC) $(COQC)\ + $(COQWORKMGR) + +COQDEPBOOT:=bin/coqdep_boot$(EXE) +OCAMLLIBDEP:=bin/ocamllibdep$(EXE) +FAKEIDE:=bin/fake_ide$(EXE) + +PRIVATEBINARIES:=$(FAKEIDE) $(OCAMLLIBDEP) $(COQDEPBOOT) + +CSDPCERT:=plugins/micromega/csdpcert$(EXE) + +########################################################################### +# Object and Source files +########################################################################### ifeq ($(HASNATDYNLINK)-$(BEST),true-opt) DEPNATDYN:= @@ -39,119 +52,22 @@ INSTALLLIB:=install -m 644 INSTALLSH:=./install.sh MKDIR:=install -d -COQIDEBYTE:=bin/coqide.byte$(EXE) -COQIDE:=bin/coqide$(EXE) -COQIDEAPP:=bin/CoqIDE_$(VERSION).app -COQIDEINAPP:=$(COQIDEAPP)/Contents/MacOS/coqide - -ifeq ($(BEST),opt) -OPT:=opt -else -OPT:= -endif - -BESTOBJ:=$(if $(OPT),.cmx,.cmo) -BESTLIB:=$(if $(OPT),.cmxa,.cma) -BESTDYN:=$(if $(OPT),.cmxs,.cma) - -COQBINARIES:= $(COQMKTOP) \ - $(COQTOPBYTE) $(COQTOPEXE) \ - $(CHICKENBYTE) $(CHICKEN) - -CSDPCERT:=plugins/micromega/csdpcert$(EXE) - CORESRCDIRS:=\ config lib kernel kernel/byterun library \ proofs tactics pretyping interp stm \ - toplevel parsing printing grammar intf + toplevel parsing printing intf engine ltac -PLUGINS:=\ +PLUGINDIRS:=\ omega romega micromega quote \ setoid_ring extraction fourier \ cc funind firstorder derive \ - rtauto nsatz syntax decl_mode btauto + rtauto nsatz syntax decl_mode btauto \ + ssrmatching SRCDIRS:=\ $(CORESRCDIRS) \ tools tools/coqdoc \ - $(addprefix plugins/, $(PLUGINS)) - -IDESRCDIRS:= $(CORESRCDIRS) ide ide/utils - -# Order is relevant here because kernel and checker contain files -# with the same name -CHKSRCDIRS:= checker lib config kernel parsing - -########################################################################### -# Tools -########################################################################### - -COQDEP:=bin/coqdep$(EXE) -COQDEPBOOT:=bin/coqdep_boot$(EXE) -COQMAKEFILE:=bin/coq_makefile$(EXE) -GALLINA:=bin/gallina$(EXE) -COQTEX:=bin/coq-tex$(EXE) -COQWC:=bin/coqwc$(EXE) -COQDOC:=bin/coqdoc$(EXE) -FAKEIDE:=bin/fake_ide$(EXE) -COQWORKMGR:=bin/coqworkmgr$(EXE) - -TOOLS:=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQWC) $(COQDOC) $(COQC)\ - $(COQWORKMGR) - -PRIVATEBINARIES:=$(FAKEIDE) $(COQDEPBOOT) - -########################################################################### -# Documentation -########################################################################### - -LATEX:=latex -BIBTEX:=BIBINPUTS=.: bibtex -min-crossrefs=10 -MAKEINDEX:=makeindex -PDFLATEX:=pdflatex -DVIPS:=dvips -FIG2DEV:=fig2dev -CONVERT:=convert -HEVEA:=hevea -HACHA:=hacha -HEVEAOPTS:=-fix -exec xxdate.exe -HEVEALIB:=/usr/local/lib/hevea:/usr/lib/hevea -HTMLSTYLE:=simple -export TEXINPUTS:=$(HEVEALIB): -COQTEXOPTS:=-boot -n 72 -sl -small - -DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex - -REFMANCOQTEXFILES:=$(addprefix doc/refman/, \ - RefMan-gal.v.tex RefMan-ext.v.tex \ - RefMan-mod.v.tex RefMan-tac.v.tex \ - RefMan-cic.v.tex RefMan-lib.v.tex \ - RefMan-tacex.v.tex RefMan-syn.v.tex \ - RefMan-oth.v.tex RefMan-ltac.v.tex \ - RefMan-decl.v.tex RefMan-pro.v.tex RefMan-sch.v.tex \ - Cases.v.tex Coercion.v.tex CanonicalStructures.v.tex Extraction.v.tex \ - Program.v.tex Omega.v.tex Micromega.v.tex Polynom.v.tex Nsatz.v.tex \ - Setoid.v.tex Classes.v.tex Universes.v.tex \ - Misc.v.tex) - -REFMANTEXFILES:=$(addprefix doc/refman/, \ - headers.sty Reference-Manual.tex \ - RefMan-pre.tex RefMan-int.tex RefMan-com.tex \ - RefMan-uti.tex RefMan-ide.tex RefMan-add.tex RefMan-modr.tex \ - AsyncProofs.tex ) \ - $(REFMANCOQTEXFILES) \ - -REFMANEPSFILES:=doc/refman/coqide.eps doc/refman/coqide-queries.eps - -REFMANFILES:=$(REFMANTEXFILES) $(DOCCOMMON) $(REFMANEPSFILES) doc/refman/biblio.bib - -REFMANPNGFILES:=$(REFMANEPSFILES:.eps=.png) - - - -########################################################################### -# Object and Source files -########################################################################### + $(addprefix plugins/, $(PLUGINDIRS)) COQRUN := coqrun LIBCOQRUN:=kernel/byterun/lib$(COQRUN).a @@ -161,111 +77,69 @@ BYTERUN:=$(addprefix kernel/byterun/, \ coq_fix_code.o coq_memory.o coq_values.o coq_interp.o ) # LINK ORDER: -# Beware that highparsing.cma should appear before hightactics.cma +# Beware that highparsing.cma should appear before ltac.cma # respecting this order is useful for developers that want to load or link # the libraries directly CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \ - pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \ + engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \ parsing/parsing.cma printing/printing.cma tactics/tactics.cma \ - stm/stm.cma toplevel/toplevel.cma parsing/highparsing.cma tactics/hightactics.cma + stm/stm.cma toplevel/toplevel.cma parsing/highparsing.cma ltac/ltac.cma TOPLOOPCMA:=stm/proofworkertop.cma stm/tacworkertop.cma stm/queryworkertop.cma -GRAMMARCMA:=tools/compat5.cmo grammar/grammar.cma - -OMEGACMA:=plugins/omega/omega_plugin.cma -ROMEGACMA:=plugins/romega/romega_plugin.cma -MICROMEGACMA:=plugins/micromega/micromega_plugin.cma -QUOTECMA:=plugins/quote/quote_plugin.cma -RINGCMA:=plugins/setoid_ring/newring_plugin.cma -NSATZCMA:=plugins/nsatz/nsatz_plugin.cma -FOURIERCMA:=plugins/fourier/fourier_plugin.cma -EXTRACTIONCMA:=plugins/extraction/extraction_plugin.cma -FUNINDCMA:=plugins/funind/recdef_plugin.cma -FOCMA:=plugins/firstorder/ground_plugin.cma -CCCMA:=plugins/cc/cc_plugin.cma -BTAUTOCMA:=plugins/btauto/btauto_plugin.cma -RTAUTOCMA:=plugins/rtauto/rtauto_plugin.cma -NATSYNTAXCMA:=plugins/syntax/nat_syntax_plugin.cma -OTHERSYNTAXCMA:=$(addprefix plugins/syntax/, \ - z_syntax_plugin.cma \ - numbers_syntax_plugin.cma \ - r_syntax_plugin.cma \ - ascii_syntax_plugin.cma \ - string_syntax_plugin.cma ) -DECLMODECMA:=plugins/decl_mode/decl_mode_plugin.cma -DERIVECMA:=plugins/derive/derive_plugin.cma - -PLUGINSCMA:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) $(DECLMODECMA) \ - $(QUOTECMA) $(RINGCMA) \ - $(FOURIERCMA) $(EXTRACTIONCMA) \ - $(CCCMA) $(FOCMA) $(RTAUTOCMA) $(BTAUTOCMA) \ - $(FUNINDCMA) $(NSATZCMA) $(NATSYNTAXCMA) $(OTHERSYNTAXCMA) \ - $(DERIVECMA) - -ifneq ($(HASNATDYNLINK),false) - STATICPLUGINS:= - INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) \ - $(FUNINDCMA) $(NATSYNTAXCMA) - INITPLUGINSOPT:=$(INITPLUGINS:.cma=.cmxs) - PLUGINS:=$(PLUGINSCMA) - PLUGINSOPT:=$(PLUGINSCMA:.cma=.cmxs) -else -ifeq ($(BEST),byte) - STATICPLUGINS:= - INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) \ - $(FUNINDCMA) $(NATSYNTAXCMA) - INITPLUGINSOPT:=$(INITPLUGINS:.cma=.cmxs) - PLUGINS:=$(PLUGINSCMA) - PLUGINSOPT:=$(PLUGINSCMA:.cma=.cmxs) -else - STATICPLUGINS:=$(PLUGINSCMA) - INITPLUGINS:= - INITPLUGINSOPT:= - PLUGINS:= - PLUGINSOPT:= -endif -endif - -LINKCMO:=$(CORECMA) $(STATICPLUGINS) -LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cma=.cmxa) - -IDEDEPS:=lib/clib.cma lib/xml_lexer.cmo lib/xml_parser.cmo lib/xml_printer.cmo lib/errors.cmo lib/spawn.cmo -IDECMA:=ide/ide.cma -IDETOPLOOPCMA=ide/coqidetop.cma - -LINKIDE:=$(IDEDEPS) $(IDECDEPS) $(IDECMA) ide/coqide_main.ml -LINKIDEOPT:=$(IDEOPTCDEPS) $(patsubst %.cma,%.cmxa,$(IDEDEPS:.cmo=.cmx)) $(IDECMA:.cma=.cmxa) ide/coqide_main.ml +GRAMMARCMA:=grammar/compat5.cmo grammar/grammar.cma # modules known by the toplevel of Coq OBJSMOD:=$(shell cat $(CORECMA:.cma=.mllib)) -IDEMOD:=$(shell cat ide/ide.mllib) - -# coqmktop, coqc - -COQENVCMO:=lib/clib.cma lib/errors.cmo - -COQMKTOPCMO:=$(COQENVCMO) tools/tolink.cmo tools/coqmktop.cmo - -COQCCMO:=$(COQENVCMO) toplevel/usage.cmo tools/coqc.cmo - -## Misc - -CSDPCERTCMO:=$(addprefix plugins/micromega/, \ - mutils.cmo micromega.cmo \ - sos_types.cmo sos_lib.cmo sos.cmo csdpcert.cmo ) - -DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/printers.cma - -COQDEPCMO:=$(COQENVCMO) tools/coqdep_lexer.cmo tools/coqdep_common.cmo tools/coqdep.cmo - -COQDOCCMO:=lib/clib.cma $(addprefix tools/coqdoc/, \ - cdglobals.cmo alpha.cmo index.cmo tokens.cmo output.cmo cpretty.cmo main.cmo ) +########################################################################### +# plugins object files +########################################################################### + +OMEGACMO:=plugins/omega/omega_plugin.cmo +ROMEGACMO:=plugins/romega/romega_plugin.cmo +MICROMEGACMO:=plugins/micromega/micromega_plugin.cmo +QUOTECMO:=plugins/quote/quote_plugin.cmo +RINGCMO:=plugins/setoid_ring/newring_plugin.cmo +NSATZCMO:=plugins/nsatz/nsatz_plugin.cmo +FOURIERCMO:=plugins/fourier/fourier_plugin.cmo +EXTRACTIONCMO:=plugins/extraction/extraction_plugin.cmo +FUNINDCMO:=plugins/funind/recdef_plugin.cmo +FOCMO:=plugins/firstorder/ground_plugin.cmo +CCCMO:=plugins/cc/cc_plugin.cmo +BTAUTOCMO:=plugins/btauto/btauto_plugin.cmo +RTAUTOCMO:=plugins/rtauto/rtauto_plugin.cmo +NATSYNTAXCMO:=plugins/syntax/nat_syntax_plugin.cmo +OTHERSYNTAXCMO:=$(addprefix plugins/syntax/, \ + z_syntax_plugin.cmo \ + numbers_syntax_plugin.cmo \ + r_syntax_plugin.cmo \ + ascii_syntax_plugin.cmo \ + string_syntax_plugin.cmo ) +DECLMODECMO:=plugins/decl_mode/decl_mode_plugin.cmo +DERIVECMO:=plugins/derive/derive_plugin.cmo +SSRMATCHINGCMO:=plugins/ssrmatching/ssrmatching_plugin.cmo + +PLUGINSCMO:=$(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) $(DECLMODECMO) \ + $(QUOTECMO) $(RINGCMO) \ + $(FOURIERCMO) $(EXTRACTIONCMO) \ + $(CCCMO) $(FOCMO) $(RTAUTOCMO) $(BTAUTOCMO) \ + $(FUNINDCMO) $(NSATZCMO) $(NATSYNTAXCMO) $(OTHERSYNTAXCMO) \ + $(DERIVECMO) $(SSRMATCHINGCMO) + +ifeq ($(HASNATDYNLINK)-$(BEST),false-opt) + STATICPLUGINS:=$(PLUGINSCMO) + PLUGINS:= +else + STATICPLUGINS:= + PLUGINS:=$(PLUGINSCMO) +endif +PLUGINSOPT:=$(PLUGINSCMO:.cmo=.cmxs) -COQMAKEFILECMO:=lib/clib.cma ide/project_file.cmo tools/coq_makefile.cmo +LINKCMO:=$(CORECMA) $(STATICPLUGINS) +LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cmo=.cmx) ########################################################################### # vo files @@ -273,127 +147,41 @@ COQMAKEFILECMO:=lib/clib.cma ide/project_file.cmo tools/coq_makefile.cmo ## we now retrieve the names of .vo file to compile in */vo.itarget files -cat_vo_itarget = $(addprefix $(1)/,$(shell cat $(1)/vo.itarget)) - -## Theories - -INITVO:=$(call cat_vo_itarget, theories/Init) -LOGICVO:=$(call cat_vo_itarget, theories/Logic) -STRUCTURESVO:=$(call cat_vo_itarget, theories/Structures) -ARITHVO:=$(call cat_vo_itarget, theories/Arith) -SORTINGVO:=$(call cat_vo_itarget, theories/Sorting) -BOOLVO:=$(call cat_vo_itarget, theories/Bool) -PARITHVO:=$(call cat_vo_itarget, theories/PArith) -NARITHVO:=$(call cat_vo_itarget, theories/NArith) -ZARITHVO:=$(call cat_vo_itarget, theories/ZArith) -QARITHVO:=$(call cat_vo_itarget, theories/QArith) -LISTSVO:=$(call cat_vo_itarget, theories/Lists) -VECTORSVO:=$(call cat_vo_itarget, theories/Vectors) -STRINGSVO:=$(call cat_vo_itarget, theories/Strings) -SETSVO:=$(call cat_vo_itarget, theories/Sets) -FSETSVO:=$(call cat_vo_itarget, theories/FSets) -MSETSVO:=$(call cat_vo_itarget, theories/MSets) -RELATIONSVO:=$(call cat_vo_itarget, theories/Relations) -WELLFOUNDEDVO:=$(call cat_vo_itarget, theories/Wellfounded) -REALSVO:=$(call cat_vo_itarget, theories/Reals) -NUMBERSVO:=$(call cat_vo_itarget, theories/Numbers) -SETOIDSVO:=$(call cat_vo_itarget, theories/Setoids) -UNICODEVO:=$(call cat_vo_itarget, theories/Unicode) -CLASSESVO:=$(call cat_vo_itarget, theories/Classes) -PROGRAMVO:=$(call cat_vo_itarget, theories/Program) -COMPATVO:=$(call cat_vo_itarget, theories/Compat) - -THEORIESVO:=\ - $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) \ - $(UNICODEVO) $(CLASSESVO) $(PROGRAMVO) \ - $(RELATIONSVO) $(WELLFOUNDEDVO) $(SETOIDSVO) \ - $(LISTSVO) $(STRINGSVO) \ - $(PARITHVO) $(NARITHVO) $(ZARITHVO) \ - $(SETSVO) $(FSETSVO) $(MSETSVO) \ - $(REALSVO) $(SORTINGVO) $(QARITHVO) \ - $(NUMBERSVO) $(STRUCTURESVO) $(VECTORSVO) \ - $(COMPATVO) - -THEORIESLIGHTVO:= $(INITVO) $(LOGICVO) $(UNICODEVO) $(ARITHVO) - -## Plugins - -OMEGAVO:=$(call cat_vo_itarget, plugins/omega) -ROMEGAVO:=$(call cat_vo_itarget, plugins/romega) -MICROMEGAVO:=$(call cat_vo_itarget, plugins/micromega) -QUOTEVO:=$(call cat_vo_itarget, plugins/quote) -RINGVO:=$(call cat_vo_itarget, plugins/setoid_ring) -NSATZVO:=$(call cat_vo_itarget, plugins/nsatz) -FOURIERVO:=$(call cat_vo_itarget, plugins/fourier) -FUNINDVO:=$(call cat_vo_itarget, plugins/funind) -BTAUTOVO:=$(call cat_vo_itarget, plugins/btauto) -RTAUTOVO:=$(call cat_vo_itarget, plugins/rtauto) -EXTRACTIONVO:=$(call cat_vo_itarget, plugins/extraction) -CCVO:= -DERIVEVO:=$(call cat_vo_itarget, plugins/derive) - -PLUGINSVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) \ - $(FOURIERVO) $(CCVO) $(FUNINDVO) \ - $(RTAUTOVO) $(BTAUTOVO) $(RINGVO) $(QUOTEVO) \ - $(NSATZVO) $(EXTRACTIONVO) $(DERIVEVO) +THEORIESVO:= $(foreach f, $(wildcard theories/*/vo.itarget), \ + $(addprefix $(dir $(f)),$(shell cat $(f)))) + +PLUGINSVO:= $(foreach f, $(wildcard plugins/*/vo.itarget), \ + $(addprefix $(dir $(f)),$(shell cat $(f)))) ALLVO:= $(THEORIESVO) $(PLUGINSVO) VFILES:= $(ALLVO:.vo=.v) + +## More specific targets + +THEORIESLIGHTVO:= \ + $(filter theories/Init/% theories/Logic/% theories/Unicode/% theories/Arith/%, $(THEORIESVO)) + ALLSTDLIB := test-suite/misc/universes/all_stdlib # convert a (stdlib) filename into a module name: # remove .vo, replace theories and plugins by Coq, and replace slashes by dots vo_to_mod = $(subst /,.,$(patsubst theories/%,Coq.%,$(patsubst plugins/%,Coq.%,$(1:.vo=)))) +ALLMODS:=$(call vo_to_mod,$(ALLVO)) + + # Converting a stdlib filename into native compiler filenames # Used for install targets vo_to_cm = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.cm*))))) vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.o))))) -ALLMODS:=$(call vo_to_mod,$(ALLVO)) - LIBFILES:=$(THEORIESVO) $(PLUGINSVO) $(call vo_to_cm,$(THEORIESVO)) \ $(call vo_to_cm,$(PLUGINSVO)) $(call vo_to_obj,$(THEORIESVO)) \ $(call vo_to_obj,$(PLUGINSVO)) \ $(PLUGINSVO:.vo=.v) $(THEORIESVO:.vo=.v) \ $(PLUGINSVO:.vo=.glob) $(THEORIESVO:.vo=.glob) -LIBFILESLIGHT:=$(THEORIESLIGHTVO) - -########################################################################### -# Miscellaneous -########################################################################### - -MANPAGES:=man/coq-tex.1 man/coqdep.1 man/gallina.1 \ - man/coqc.1 man/coqtop.1 man/coqtop.byte.1 man/coqtop.opt.1 \ - man/coqwc.1 man/coqdoc.1 man/coqide.1 \ - man/coq_makefile.1 man/coqmktop.1 man/coqchk.1 - -########################################################################### -# Source documentation -########################################################################### - -OCAMLDOCDIR=dev/ocamldoc - -DOCMLIS=$(wildcard ./lib/*.mli ./intf/*.mli ./kernel/*.mli ./library/*.mli \ - ./pretyping/*.mli ./interp/*.mli printing/*.mli \ - ./parsing/*.mli ./proofs/*.mli \ - ./tactics/*.mli ./stm/*.mli ./toplevel/*.mli) - -# Defining options to generate dependencies graphs -DOT=dot -ODOCDOTOPTS=-dot -dot-reduce - -########################################################################### -# GTK for Coqide MacOS bundle -########################################################################### - -GTKSHARE=$(shell pkg-config --variable=prefix gtk+-2.0)/share -GTKBIN=$(shell pkg-config --variable=prefix gtk+-2.0)/bin -GTKLIBS=$(shell pkg-config --variable=libdir gtk+-2.0) - - # For emacs: # Local Variables: # mode: makefile -- cgit v1.2.3