diff options
Diffstat (limited to 'Makefile.common')
-rw-r--r-- | Makefile.common | 182 |
1 files changed, 97 insertions, 85 deletions
diff --git a/Makefile.common b/Makefile.common index 444a7ee5..d752a5be 100644 --- a/Makefile.common +++ b/Makefile.common @@ -12,28 +12,16 @@ # Executables ########################################################################### -COQMKTOPBYTE:=bin/coqmktop.byte$(EXE) -COQMKTOPOPT:=bin/coqmktop.opt$(EXE) -BESTCOQMKTOP:=bin/coqmktop.$(BEST)$(EXE) COQMKTOP:=bin/coqmktop$(EXE) -COQCBYTE:=bin/coqc.byte$(EXE) -COQCOPT:=bin/coqc.opt$(EXE) -BESTCOQC:=bin/coqc.$(BEST)$(EXE) COQC:=bin/coqc$(EXE) COQTOPBYTE:=bin/coqtop.byte$(EXE) -COQTOPOPT:=bin/coqtop.opt$(EXE) -BESTCOQTOP:=bin/coqtop.$(BEST)$(EXE) COQTOPEXE:=bin/coqtop$(EXE) CHICKENBYTE:=bin/coqchk.byte$(EXE) -CHICKENOPT:=bin/coqchk.opt$(EXE) -BESTCHICKEN:=bin/coqchk.$(BEST)$(EXE) CHICKEN:=bin/coqchk$(EXE) -FAKEIDE:=bin/fake_ide$(EXE) - ifeq ($(CAMLP4),camlp4) CAMLP4MOD:=camlp4lib else @@ -41,12 +29,8 @@ CAMLP4MOD:=gramlib endif ifeq ($(HASNATDYNLINK)-$(BEST),true-opt) - DYNLINKCMXA:=dynlink.cmxa - NATDYNLINKDEF:=-DHasDynlink DEPNATDYN:= else - DYNLINKCMXA:= - NATDYNLINKDEF:= DEPNATDYN:=-natdynlink no endif @@ -56,8 +40,9 @@ INSTALLSH:=./install.sh MKDIR:=install -d COQIDEBYTE:=bin/coqide.byte$(EXE) -COQIDEOPT:=bin/coqide.opt$(EXE) COQIDE:=bin/coqide$(EXE) +COQIDEAPP:=bin/CoqIDE_$(VERSION).app +COQIDEINAPP:=$(COQIDEAPP)/Contents/MacOS/coqide ifeq ($(BEST),opt) OPT:=opt @@ -66,35 +51,39 @@ OPT:= endif BESTOBJ:=$(if $(OPT),.cmx,.cmo) +BESTLIB:=$(if $(OPT),.cmxa,.cma) +BESTDYN:=$(if $(OPT),.cmxs,.cma) -COQBINARIES:= $(COQMKTOP) $(COQC) \ - $(COQTOPBYTE) $(if $(OPT),$(COQTOPOPT)) $(COQTOPEXE) \ - $(CHICKENBYTE) $(if $(OPT),$(CHICKENOPT)) $(CHICKEN) +COQBINARIES:= $(COQMKTOP) \ + $(COQTOPBYTE) $(COQTOPEXE) \ + $(CHICKENBYTE) $(CHICKEN) CSDPCERT:=plugins/micromega/csdpcert$(EXE) CORESRCDIRS:=\ config lib kernel kernel/byterun library \ - proofs tactics pretyping interp toplevel \ - parsing + proofs tactics pretyping interp stm \ + toplevel parsing printing grammar intf PLUGINS:=\ - omega romega micromega quote ring \ - setoid_ring xml extraction fourier \ - cc funind firstorder field subtac \ - rtauto nsatz syntax decl_mode + omega romega micromega quote \ + setoid_ring extraction fourier \ + cc funind firstorder derive \ + rtauto nsatz syntax decl_mode btauto SRCDIRS:=\ $(CORESRCDIRS) \ - tools tools/coqdoc scripts ide/utils ide \ + tools tools/coqdoc \ $(addprefix plugins/, $(PLUGINS)) -# Order is relevent here because kernel and checker contain files +IDESRCDIRS:= $(CORESRCDIRS) ide ide/utils + +# Order is relevant here because kernel and checker contain files # with the same name -CHKSRCDIRS:= checker lib config kernel +CHKSRCDIRS:= checker lib config kernel parsing ########################################################################### -# tools +# Tools ########################################################################### COQDEP:=bin/coqdep$(EXE) @@ -104,8 +93,13 @@ 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) -TOOLS:=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQWC) $(COQDOC) +PRIVATEBINARIES:=$(FAKEIDE) $(COQDEPBOOT) ########################################################################### # Documentation @@ -130,11 +124,11 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \ 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-sch.v.tex \ - RefMan-pro.v.tex \ - Cases.v.tex Coercion.v.tex Extraction.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 Helm.tex Classes.v.tex ) + Setoid.v.tex Classes.v.tex AsyncProofs.v.tex Universes.v.tex \ + Misc.v.tex) REFMANTEXFILES:=$(addprefix doc/refman/, \ headers.sty Reference-Manual.tex \ @@ -158,8 +152,6 @@ COQRUN := coqrun LIBCOQRUN:=kernel/byterun/lib$(COQRUN).a DLLCOQRUN:=$(dir $(LIBCOQRUN))dll$(COQRUN)$(DLLEXT) -CONFIG:=config/coq_config.cmo - BYTERUN:=$(addprefix kernel/byterun/, \ coq_fix_code.o coq_memory.o coq_values.o coq_interp.o ) @@ -168,28 +160,27 @@ BYTERUN:=$(addprefix kernel/byterun/, \ # respecting this order is useful for developers that want to load or link # the libraries directly -CORECMA:=lib/lib.cma kernel/kernel.cma library/library.cma \ +CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \ pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \ - parsing/parsing.cma tactics/tactics.cma toplevel/toplevel.cma \ - parsing/highparsing.cma tactics/hightactics.cma + parsing/parsing.cma printing/printing.cma tactics/tactics.cma \ + stm/stm.cma toplevel/toplevel.cma parsing/highparsing.cma tactics/hightactics.cma + +TOPLOOPCMA:=stm/proofworkertop.cma stm/tacworkertop.cma stm/queryworkertop.cma -GRAMMARCMA:=parsing/grammar.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/ring/ring_plugin.cma -NEWRINGCMA:=plugins/setoid_ring/newring_plugin.cma +RINGCMA:=plugins/setoid_ring/newring_plugin.cma NSATZCMA:=plugins/nsatz/nsatz_plugin.cma -FIELDCMA:=plugins/field/field_plugin.cma -XMLCMA:=plugins/xml/xml_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 -SUBTACCMA:=plugins/subtac/subtac_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/, \ @@ -199,17 +190,19 @@ OTHERSYNTAXCMA:=$(addprefix plugins/syntax/, \ 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) $(NEWRINGCMA) $(FIELDCMA) \ - $(FOURIERCMA) $(EXTRACTIONCMA) $(XMLCMA) \ - $(CCCMA) $(FOCMA) $(SUBTACCMA) $(RTAUTOCMA) \ - $(FUNINDCMA) $(NSATZCMA) $(NATSYNTAXCMA) $(OTHERSYNTAXCMA) + $(QUOTECMA) $(RINGCMA) \ + $(FOURIERCMA) $(EXTRACTIONCMA) \ + $(CCCMA) $(FOCMA) $(RTAUTOCMA) $(BTAUTOCMA) \ + $(FUNINDCMA) $(NSATZCMA) $(NATSYNTAXCMA) $(OTHERSYNTAXCMA) \ + $(DERIVECMA) ifneq ($(HASNATDYNLINK),false) STATICPLUGINS:= INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) \ - $(XMLCMA) $(FUNINDCMA) $(SUBTACCMA) $(NATSYNTAXCMA) + $(FUNINDCMA) $(NATSYNTAXCMA) INITPLUGINSOPT:=$(INITPLUGINS:.cma=.cmxs) PLUGINS:=$(PLUGINSCMA) PLUGINSOPT:=$(PLUGINSCMA:.cma=.cmxs) @@ -221,34 +214,29 @@ else PLUGINSOPT:= endif -INITPLUGINSBEST:=$(if $(OPT),$(INITPLUGINSOPT),$(INITPLUGINS)) +LINKCMO:=$(CORECMA) $(STATICPLUGINS) +LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cma=.cmxa) -LINKCMO:=$(CONFIG) $(CORECMA) $(STATICPLUGINS) -LINKCMX:=$(CONFIG:.cmo=.cmx) $(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cma=.cmxa) - -IDEDEPS:=$(CONFIG) lib/flags.cmo lib/xml_lexer.cmo lib/xml_parser.cmo \ - lib/xml_utils.cmo toplevel/ide_intf.cmo +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) $(IDECMA) ide/coqide_main.ml -LINKIDEOPT:=$(IDEOPTDEPS) $(IDEDEPS:.cmo=.cmx) $(IDECMA:.cma=.cmxa) ide/coqide_main_opt.ml +LINKIDE:=$(IDEDEPS) $(IDECDEPS) $(IDECMA) ide/coqide_main.ml +LINKIDEOPT:=$(IDEOPTCDEPS) $(patsubst %.cma,%.cmxa,$(IDEDEPS:.cmo=.cmx)) $(IDECMA:.cma=.cmxa) ide/coqide_main.ml # modules known by the toplevel of Coq -OBJSMOD:=Coq_config $(shell cat $(CORECMA:.cma=.mllib)) +OBJSMOD:=$(shell cat $(CORECMA:.cma=.mllib)) IDEMOD:=$(shell cat ide/ide.mllib) # coqmktop, coqc -COQENVCMO:=$(CONFIG) \ - lib/pp_control.cmo lib/pp.cmo lib/compat.cmo lib/flags.cmo \ - lib/segmenttree.cmo lib/unicodetable.cmo lib/util.cmo lib/errors.cmo lib/system.cmo \ - lib/envars.cmo +COQENVCMO:=lib/clib.cma lib/errors.cmo -COQMKTOPCMO:=$(COQENVCMO) scripts/tolink.cmo scripts/coqmktop.cmo +COQMKTOPCMO:=$(COQENVCMO) tools/tolink.cmo tools/coqmktop.cmo -COQCCMO:=$(COQENVCMO) toplevel/usage.cmo scripts/coqc.cmo +COQCCMO:=$(COQENVCMO) toplevel/usage.cmo tools/coqc.cmo ## Misc @@ -260,9 +248,11 @@ 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:=$(CONFIG) $(addprefix tools/coqdoc/, \ +COQDOCCMO:=lib/clib.cma $(addprefix tools/coqdoc/, \ cdglobals.cmo alpha.cmo index.cmo tokens.cmo output.cmo cpretty.cmo main.cmo ) +COQMAKEFILECMO:=lib/clib.cma ide/project_file.cmo tools/coq_makefile.cmo + ########################################################################### # vo files ########################################################################### @@ -299,13 +289,16 @@ CLASSESVO:=$(call cat_vo_itarget, theories/Classes) PROGRAMVO:=$(call cat_vo_itarget, theories/Program) THEORIESVO:=\ - $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(PARITHVO) $(NARITHVO) $(ZARITHVO) \ - $(SETOIDSVO) $(LISTSVO) $(STRINGSVO) $(SETSVO) $(FSETSVO) $(MSETSVO) \ - $(RELATIONSVO) $(WELLFOUNDEDVO) $(REALSVO) $(SORTINGVO) $(QARITHVO) \ - $(NUMBERSVO) $(UNICODEVO) $(CLASSESVO) $(PROGRAMVO) $(STRUCTURESVO) \ - $(VECTORSVO) + $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) \ + $(UNICODEVO) $(CLASSESVO) $(PROGRAMVO) \ + $(RELATIONSVO) $(WELLFOUNDEDVO) $(SETOIDSVO) \ + $(LISTSVO) $(STRINGSVO) \ + $(PARITHVO) $(NARITHVO) $(ZARITHVO) \ + $(SETSVO) $(FSETSVO) $(MSETSVO) \ + $(REALSVO) $(SORTINGVO) $(QARITHVO) \ + $(NUMBERSVO) $(STRUCTURESVO) $(VECTORSVO) -THEORIESLIGHTVO:= $(INITVO) $(LOGICVO) $(ARITHVO) +THEORIESLIGHTVO:= $(INITVO) $(LOGICVO) $(UNICODEVO) $(ARITHVO) ## Plugins @@ -313,21 +306,20 @@ 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/ring) -FIELDVO:=$(call cat_vo_itarget, plugins/field) -NEWRINGVO:=$(call cat_vo_itarget, plugins/setoid_ring) +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) -XMLVO:= CCVO:= +DERIVEVO:=$(call cat_vo_itarget, plugins/derive) -PLUGINSVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) $(RINGVO) $(FIELDVO) \ - $(XMLVO) $(FOURIERVO) $(CCVO) $(FUNINDVO) \ - $(RTAUTOVO) $(NEWRINGVO) $(QUOTEVO) \ - $(NSATZVO) $(EXTRACTIONVO) +PLUGINSVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) \ + $(FOURIERVO) $(CCVO) $(FUNINDVO) \ + $(RTAUTOVO) $(BTAUTOVO) $(RINGVO) $(QUOTEVO) \ + $(NSATZVO) $(EXTRACTIONVO) $(DERIVEVO) ALLVO:= $(THEORIESVO) $(PLUGINSVO) VFILES:= $(ALLVO:.vo=.v) @@ -337,9 +329,20 @@ ALLSTDLIB := test-suite/misc/universes/all_stdlib # 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=)))) +# 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) +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) ########################################################################### @@ -357,15 +360,24 @@ MANPAGES:=man/coq-tex.1 man/coqdep.1 man/gallina.1 \ OCAMLDOCDIR=dev/ocamldoc -DOCMLIS=$(wildcard ./lib/*.mli ./kernel/*.mli ./library/*.mli \ - ./pretyping/*.mli ./interp/*.mli \ +DOCMLIS=$(wildcard ./lib/*.mli ./intf/*.mli ./kernel/*.mli ./library/*.mli \ + ./pretyping/*.mli ./interp/*.mli printing/*.mli \ ./parsing/*.mli ./proofs/*.mli \ - ./tactics/*.mli ./toplevel/*.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 |