diff options
Diffstat (limited to 'Makefile.common')
-rw-r--r-- | Makefile.common | 158 |
1 files changed, 54 insertions, 104 deletions
diff --git a/Makefile.common b/Makefile.common index 46bf2175..b560bae5 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,29 @@ 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) SRCDIRS:=\ config tools tools/coqdoc scripts lib \ kernel kernel/byterun library proofs tactics \ - pretyping interp toplevel parsing ide/utils \ - ide \ + pretyping interp toplevel/utils 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) + rtauto nsatz syntax decl_mode) # Order is relevent here because kernel and checker contain files # with the same name @@ -139,10 +152,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 +167,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 @@ -182,8 +193,9 @@ 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) \ +PLUGINSCMA:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) $(DECLMODECMA) \ $(QUOTECMA) $(RINGCMA) $(NEWRINGCMA) $(DPCMA) $(FIELDCMA) \ $(FOURIERCMA) $(EXTRACTIONCMA) $(XMLCMA) \ $(CCCMA) $(FOCMA) $(SUBTACCMA) $(RTAUTOCMA) \ @@ -204,24 +216,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 +238,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 +274,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 +294,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) @@ -341,6 +327,7 @@ PLUGINSVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) $(RINGVO) $(FIELDVO) \ 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 +338,6 @@ ALLMODS:=$(call vo_to_mod,$(ALLVO)) LIBFILES:=$(THEORIESVO) $(PLUGINSVO) LIBFILESLIGHT:=$(THEORIESLIGHTVO) - ########################################################################### # Miscellaneous ########################################################################### @@ -363,56 +349,20 @@ MANPAGES:=man/coq-tex.1 man/coqdep.1 man/gallina.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: |