diff options
Diffstat (limited to 'Makefile.common')
| -rw-r--r-- | Makefile.common | 194 |
1 files changed, 73 insertions, 121 deletions
diff --git a/Makefile.common b/Makefile.common index 46bf2175..444a7ee5 100644 --- a/Makefile.common +++ b/Makefile.common @@ -1,4 +1,3 @@ - ####################################################################### # v # The Coq Proof Assistant / The Coq Development Team # # <O___,, # INRIA-Rocquencourt & LRI-CNRS-Orsay # @@ -17,20 +16,31 @@ 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) -ifneq ($(HASNATDYNLINK),false) +FAKEIDE:=bin/fake_ide$(EXE) + +ifeq ($(CAMLP4),camlp4) +CAMLP4MOD:=camlp4lib +else +CAMLP4MOD:=gramlib +endif + +ifeq ($(HASNATDYNLINK)-$(BEST),true-opt) DYNLINKCMXA:=dynlink.cmxa NATDYNLINKDEF:=-DHasDynlink DEPNATDYN:= @@ -50,26 +60,34 @@ COQIDEOPT:=bin/coqide.opt$(EXE) COQIDE:=bin/coqide$(EXE) ifeq ($(BEST),opt) -COQBINARIES:= $(COQMKTOP) $(COQC) \ - $(COQTOPBYTE) $(COQTOPOPT) $(COQTOPEXE) $(CHICKENBYTE) $(CHICKENOPT) $(CHICKEN) +OPT:=opt else -COQBINARIES:= $(COQMKTOP) $(COQC) \ - $(COQTOPBYTE) $(COQTOPEXE) $(CHICKENBYTE) $(CHICKEN) +OPT:= endif -OTHERBINARIES:=$(COQMKTOPBYTE) $(COQCBYTE) + +BESTOBJ:=$(if $(OPT),.cmx,.cmo) + +COQBINARIES:= $(COQMKTOP) $(COQC) \ + $(COQTOPBYTE) $(if $(OPT),$(COQTOPOPT)) $(COQTOPEXE) \ + $(CHICKENBYTE) $(if $(OPT),$(CHICKENOPT)) $(CHICKEN) CSDPCERT:=plugins/micromega/csdpcert$(EXE) +CORESRCDIRS:=\ + config lib kernel kernel/byterun library \ + proofs tactics pretyping interp toplevel \ + parsing + +PLUGINS:=\ + omega romega micromega quote ring \ + setoid_ring xml extraction fourier \ + cc funind firstorder field subtac \ + rtauto nsatz syntax decl_mode + SRCDIRS:=\ - config tools tools/coqdoc scripts lib \ - kernel kernel/byterun library proofs tactics \ - pretyping interp toplevel parsing ide/utils \ - ide \ - $(addprefix plugins/, \ - omega romega micromega quote ring dp \ - setoid_ring xml extraction fourier \ - cc funind firstorder field subtac \ - rtauto nsatz syntax) + $(CORESRCDIRS) \ + tools tools/coqdoc scripts ide/utils ide \ + $(addprefix plugins/, $(PLUGINS)) # Order is relevent here because kernel and checker contain files # with the same name @@ -101,8 +119,8 @@ HEVEA:=hevea HEVEAOPTS:=-fix -exec xxdate.exe HEVEALIB:=/usr/local/lib/hevea:/usr/lib/hevea HTMLSTYLE:=simple -export TEXINPUTS:=$(COQSRC)/doc:$(HEVEALIB): -COQTEXOPTS:=-n 72 -image "$(COQSRC)/$(COQTOPEXE) -boot" -sl -small +export TEXINPUTS:=$(HEVEALIB): +COQTEXOPTS:=-boot -n 72 -sl -small DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex @@ -112,14 +130,15 @@ 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-decl.v.tex RefMan-sch.v.tex \ + RefMan-pro.v.tex \ Cases.v.tex Coercion.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 ) REFMANTEXFILES:=$(addprefix doc/refman/, \ headers.sty Reference-Manual.tex \ - RefMan-pre.tex RefMan-int.tex RefMan-pro.tex RefMan-com.tex \ + RefMan-pre.tex RefMan-int.tex RefMan-com.tex \ RefMan-uti.tex RefMan-ide.tex RefMan-add.tex RefMan-modr.tex ) \ $(REFMANCOQTEXFILES) \ @@ -139,10 +158,6 @@ COQRUN := coqrun LIBCOQRUN:=kernel/byterun/lib$(COQRUN).a DLLCOQRUN:=$(dir $(LIBCOQRUN))dll$(COQRUN)$(DLLEXT) -CLIBS:=unix.cma - -CAMLP4OBJS:=gramlib.cma - CONFIG:=config/coq_config.cmo BYTERUN:=$(addprefix kernel/byterun/, \ @@ -158,6 +173,8 @@ CORECMA:=lib/lib.cma kernel/kernel.cma library/library.cma \ parsing/parsing.cma tactics/tactics.cma toplevel/toplevel.cma \ parsing/highparsing.cma tactics/hightactics.cma +GRAMMARCMA:=parsing/grammar.cma + OMEGACMA:=plugins/omega/omega_plugin.cma ROMEGACMA:=plugins/romega/romega_plugin.cma MICROMEGACMA:=plugins/micromega/micromega_plugin.cma @@ -165,7 +182,6 @@ QUOTECMA:=plugins/quote/quote_plugin.cma RINGCMA:=plugins/ring/ring_plugin.cma NEWRINGCMA:=plugins/setoid_ring/newring_plugin.cma NSATZCMA:=plugins/nsatz/nsatz_plugin.cma -DPCMA:=plugins/dp/dp_plugin.cma FIELDCMA:=plugins/field/field_plugin.cma XMLCMA:=plugins/xml/xml_plugin.cma FOURIERCMA:=plugins/fourier/fourier_plugin.cma @@ -182,16 +198,17 @@ OTHERSYNTAXCMA:=$(addprefix plugins/syntax/, \ r_syntax_plugin.cma \ ascii_syntax_plugin.cma \ string_syntax_plugin.cma ) +DECLMODECMA:=plugins/decl_mode/decl_mode_plugin.cma -PLUGINSCMA:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) \ - $(QUOTECMA) $(RINGCMA) $(NEWRINGCMA) $(DPCMA) $(FIELDCMA) \ +PLUGINSCMA:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) $(DECLMODECMA) \ + $(QUOTECMA) $(RINGCMA) $(NEWRINGCMA) $(FIELDCMA) \ $(FOURIERCMA) $(EXTRACTIONCMA) $(XMLCMA) \ $(CCCMA) $(FOCMA) $(SUBTACCMA) $(RTAUTOCMA) \ $(FUNINDCMA) $(NSATZCMA) $(NATSYNTAXCMA) $(OTHERSYNTAXCMA) ifneq ($(HASNATDYNLINK),false) STATICPLUGINS:= - INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) $(DPCMA) \ + INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) \ $(XMLCMA) $(FUNINDCMA) $(SUBTACCMA) $(NATSYNTAXCMA) INITPLUGINSOPT:=$(INITPLUGINS:.cma=.cmxs) PLUGINS:=$(PLUGINSCMA) @@ -204,24 +221,21 @@ else PLUGINSOPT:= endif -ifeq ($(BEST),opt) - INITPLUGINSBEST:=$(INITPLUGINSOPT) -else - INITPLUGINSBEST:=$(INITPLUGINS) -endif - -CMA:=$(CLIBS) $(CAMLP4OBJS) -CMXA:=$(CMA:.cma=.cmxa) +INITPLUGINSBEST:=$(if $(OPT),$(INITPLUGINSOPT),$(INITPLUGINS)) 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 IDECMA:=ide/ide.cma +LINKIDE:=$(IDEDEPS) $(IDECMA) ide/coqide_main.ml +LINKIDEOPT:=$(IDEOPTDEPS) $(IDEDEPS:.cmo=.cmx) $(IDECMA:.cma=.cmxa) ide/coqide_main_opt.ml + # modules known by the toplevel of Coq -OBJSMOD:=Coq_config \ - $(foreach lib,$(CORECMA),$(shell cat $(lib:.cma=.mllib))) +OBJSMOD:=Coq_config $(shell cat $(CORECMA:.cma=.mllib)) IDEMOD:=$(shell cat ide/ide.mllib) @@ -229,51 +243,25 @@ IDEMOD:=$(shell cat ide/ide.mllib) 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/system.cmo \ + lib/segmenttree.cmo lib/unicodetable.cmo lib/util.cmo lib/errors.cmo lib/system.cmo \ lib/envars.cmo COQMKTOPCMO:=$(COQENVCMO) scripts/tolink.cmo scripts/coqmktop.cmo -COQMKTOPCMX:=$(COQMKTOPCMO:.cmo=.cmx) COQCCMO:=$(COQENVCMO) toplevel/usage.cmo scripts/coqc.cmo -COQCCMX:=$(COQCCMO:.cmo=.cmx) ## Misc CSDPCERTCMO:=$(addprefix plugins/micromega/, \ - mutils.cmo micromega.cmo mfourier.cmo certificate.cmo \ + mutils.cmo micromega.cmo \ sos_types.cmo sos_lib.cmo sos.cmo csdpcert.cmo ) -CSDPCERTCMX:= $(CSDPCERTCMO:.cmo=.cmx) - DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/printers.cma -COQDEPBOOTML:=tools/coqdep_lexer.ml tools/coqdep_common.ml tools/coqdep_boot.ml -COQDEPML:=tools/coqdep_lexer.ml tools/coqdep_common.ml tools/coqdep.ml - -COQDEPCMO:=$(COQENVCMO) $(COQDEPML:.ml=.cmo) -COQDEPCMX:=$(COQDEPCMO:.cmo=.cmx) - -GALLINACMO:=tools/gallina_lexer.cmo tools/gallina.cmo -GALLINACMX:=$(GALLINACMO:.cmo=.cmx) +COQDEPCMO:=$(COQENVCMO) tools/coqdep_lexer.cmo tools/coqdep_common.cmo tools/coqdep.cmo COQDOCCMO:=$(CONFIG) $(addprefix tools/coqdoc/, \ cdglobals.cmo alpha.cmo index.cmo tokens.cmo output.cmo cpretty.cmo main.cmo ) -COQDOCCMX:=$(COQDOCCMO:.cmo=.cmx) - -# grammar modules with camlp4 - -GRAMMARCMA:=parsing/grammar.cma - -GRAMMARML4:=lib/compat.ml4 lib/pp.ml4 parsing/q_util.ml4 parsing/pcoq.ml4 \ - parsing/argextend.ml4 parsing/tacextend.ml4 parsing/vernacextend.ml4 \ - parsing/g_prim.ml4 parsing/g_tactic.ml4 \ - parsing/g_ltac.ml4 parsing/g_constr.ml4 \ - parsing/lexer.ml4 parsing/q_coqast.ml4 - -STAGE1_ML4:=$(GRAMMARML4) parsing/q_constr.ml4 -STAGE1:=parsing/grammar.cma parsing/q_constr.cmo - ########################################################################### # vo files @@ -291,10 +279,12 @@ 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) @@ -309,10 +299,11 @@ CLASSESVO:=$(call cat_vo_itarget, theories/Classes) PROGRAMVO:=$(call cat_vo_itarget, theories/Program) THEORIESVO:=\ - $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(NARITHVO) $(ZARITHVO) \ + $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(PARITHVO) $(NARITHVO) $(ZARITHVO) \ $(SETOIDSVO) $(LISTSVO) $(STRINGSVO) $(SETSVO) $(FSETSVO) $(MSETSVO) \ $(RELATIONSVO) $(WELLFOUNDEDVO) $(REALSVO) $(SORTINGVO) $(QARITHVO) \ - $(NUMBERSVO) $(UNICODEVO) $(CLASSESVO) $(PROGRAMVO) $(STRUCTURESVO) + $(NUMBERSVO) $(UNICODEVO) $(CLASSESVO) $(PROGRAMVO) $(STRUCTURESVO) \ + $(VECTORSVO) THEORIESLIGHTVO:= $(INITVO) $(LOGICVO) $(ARITHVO) @@ -328,7 +319,6 @@ NEWRINGVO:=$(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) -DPVO:=$(call cat_vo_itarget, plugins/dp) RTAUTOVO:=$(call cat_vo_itarget, plugins/rtauto) EXTRACTIONVO:=$(call cat_vo_itarget, plugins/extraction) XMLVO:= @@ -336,11 +326,12 @@ CCVO:= PLUGINSVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) $(RINGVO) $(FIELDVO) \ $(XMLVO) $(FOURIERVO) $(CCVO) $(FUNINDVO) \ - $(RTAUTOVO) $(NEWRINGVO) $(DPVO) $(QUOTEVO) \ + $(RTAUTOVO) $(NEWRINGVO) $(QUOTEVO) \ $(NSATZVO) $(EXTRACTIONVO) ALLVO:= $(THEORIESVO) $(PLUGINSVO) VFILES:= $(ALLVO:.vo=.v) +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 @@ -351,7 +342,6 @@ ALLMODS:=$(call vo_to_mod,$(ALLVO)) LIBFILES:=$(THEORIESVO) $(PLUGINSVO) LIBFILESLIGHT:=$(THEORIESLIGHTVO) - ########################################################################### # Miscellaneous ########################################################################### @@ -361,58 +351,20 @@ MANPAGES:=man/coq-tex.1 man/coqdep.1 man/gallina.1 \ man/coqwc.1 man/coqdoc.1 man/coqide.1 \ man/coq_makefile.1 man/coqmktop.1 man/coqchk.1 -DATE=$(shell LANG=C date +"%B %Y") - -SOURCEDOCDIR=dev/source-doc - -CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.o %.cmi %.cma %.cmxa %.a %.cmxs %.dep.ps %.dot - -### Targets forwarded by Makefile to a specific stage: - -## Enumeration of targets that require being done at stage1 - -STAGE1_TARGETS:= $(STAGE1) $(COQDEPBOOT) \ - $(GENFILES) \ - source-doc revision toplevel/mltop.byteml toplevel/mltop.optml \ - $(STAGE1_ML4:.ml4=.ml4-preprocessed) - -STAGE1_IMPLICITS:= - -ifdef CM_STAGE1 - STAGE1_IMPLICITS+=$(CAML_OBJECT_PATTERNS) -endif - -## Enumeration of targets that require being done at stage2 - -VO_TARGETS:=logic arith bool narith zarith qarith lists strings sets \ - fsets relations wellfounded ints reals \ - setoids sorting natural integer rational numbers noreal \ - omega micromega ring setoid_ring dp xml extraction field fourier \ - funind cc subtac rtauto - -DOC_TARGETS:=doc doc-html doc-ps doc-pdf stdlib refman tutorial faq \ - rectutorial refman-quick refman-nodep stdlib-nodep \ - install-doc install-doc-meta install-doc-html install-doc-printable install-doc-index-url \ - ide/index_urls.txt - -DOC_TARGET_PATTERNS:=%.dvi %.ps %.eps %.pdf %.html %.v.tex %.hva - -STAGE2_TARGETS:=$(COQBINARIES) lib kernel byterun library proofs tactics \ - interp parsing pretyping highparsing toplevel hightactics \ - coqide-binaries coqide-byte coqide-opt $(COQIDEOPT) $(COQIDEBYTE) $(COQIDE) \ - $(CSDPCERT) coqbinaries $(TOOLS) tools \ - printers debug initplugins plugins \ - world install coqide coqide-files coq coqlib \ - coqlight states check init theories theories-light \ - $(DOC_TARGETS) $(VO_TARGETS) validate +########################################################################### +# Source documentation +########################################################################### -STAGE2_IMPLICITS:= %.vo %.glob states/% install-% %.ml4-preprocessed \ - $(DOC_TARGET_PATTERNS) +OCAMLDOCDIR=dev/ocamldoc -ifndef CM_STAGE1 - STAGE2_IMPLICITS+=$(CAML_OBJECT_PATTERNS) -endif +DOCMLIS=$(wildcard ./lib/*.mli ./kernel/*.mli ./library/*.mli \ + ./pretyping/*.mli ./interp/*.mli \ + ./parsing/*.mli ./proofs/*.mli \ + ./tactics/*.mli ./toplevel/*.mli) +# Defining options to generate dependencies graphs +DOT=dot +ODOCDOTOPTS=-dot -dot-reduce # For emacs: # Local Variables: |