diff options
| -rw-r--r-- | Makefile | 8 | ||||
| -rw-r--r-- | Makefile.build | 912 | ||||
| -rw-r--r-- | Makefile.checker | 86 | ||||
| -rw-r--r-- | Makefile.common | 286 | ||||
| -rw-r--r-- | Makefile.dev | 223 | ||||
| -rw-r--r-- | Makefile.doc | 137 | ||||
| -rw-r--r-- | Makefile.ide | 254 | ||||
| -rw-r--r-- | Makefile.install | 136 |
8 files changed, 1066 insertions, 976 deletions
@@ -153,7 +153,7 @@ noconfig: # To speed-up things a bit, let's dissuade make to attempt rebuilding makefiles -Makefile Makefile.build Makefile.common config/Makefile : ; +Makefile $(wildcard Makefile.*) config/Makefile : ; ########################################################################### # Cleaning @@ -173,7 +173,7 @@ cruftclean: ml4clean indepclean: rm -f $(GENFILES) - rm -f $(COQTOPBYTE) $(CHICKENBYTE) $(FAKEIDE) + rm -f $(COQTOPBYTE) $(CHICKENBYTE) find . \( -name '*~' -o -name '*.cm[ioat]' -o -name '*.cmti' \) -delete rm -f */*.pp[iox] plugins/*/*.pp[iox] rm -rf $(SOURCEDOCDIR) @@ -206,8 +206,8 @@ archclean: clean-ide optclean voclean rm -f $(ALLSTDLIB).* optclean: - rm -f $(COQTOPEXE) $(COQMKTOP) $(COQC) $(CHICKEN) $(COQDEPBOOT) - rm -f $(TOOLS) $(CSDPCERT) + rm -f $(COQTOPEXE) $(COQMKTOP) $(CHICKEN) + rm -f $(TOOLS) $(PRIVATEBINARIES) $(CSDPCERT) find . -name '*.cmx' -o -name '*.cmxs' -o -name '*.cmxa' -o -name '*.[soa]' -o -name '*.so' | xargs rm -f clean-ide: diff --git a/Makefile.build b/Makefile.build index 7edc62028..69228e379 100644 --- a/Makefile.build +++ b/Makefile.build @@ -10,30 +10,40 @@ # some variables. ########################################################################### -# Starting rule +# Default starting rule ########################################################################### -# build the different subsystems: coq, coqide -world: revision coq coqide documentation +# build the different subsystems: -.PHONY: world +world: coq coqide documentation revision + +coq: coqlib coqbinaries tools printers + +.PHONY: world coq ########################################################################### # Includes ########################################################################### -include Makefile.common -include Makefile.doc - +# This list of ml files used to be in the main Makefile, we moved it here +# to avoid exhausting the variable env in Win32 MLFILES := $(MLSTATICFILES) $(GENMLFILES) $(ML4FILES:.ml4=.ml) -DEPENDENCIES := \ - $(addsuffix .d, $(MLFILES) $(MLIFILES) $(MLLIBFILES) $(CFILES) $(VFILES)) -# This include below will lauch the build of all concerned .d. +include Makefile.common +include Makefile.doc ## provides the 'documentation' rule +include Makefile.checker +include Makefile.ide ## provides the 'coqide' rule +include Makefile.install +include Makefile.dev ## provides the 'printers' and 'revision' rules + +# This include below will lauch the build of all .d. # The - at front is for disabling warnings about currently missing ones. # For creating the missing .d, make will recursively build things like # coqdep_boot (for the .v.d files) or grammar.cma (for .ml4 -> .ml -> .ml.d). +DEPENDENCIES := \ + $(addsuffix .d, $(MLFILES) $(MLIFILES) $(MLLIBFILES) $(CFILES) $(VFILES)) + -include $(DEPENDENCIES) # All dependency includes must be declared secondary, otherwise make will @@ -43,7 +53,6 @@ DEPENDENCIES := \ .SECONDARY: $(DEPENDENCIES) $(GENFILES) $(ML4FILES:.ml4=.ml) - ########################################################################### # Compilation options ########################################################################### @@ -56,7 +65,6 @@ NO_RECALC_DEPS= READABLE_ML4= # non-empty means .ml of .ml4 will be ascii instead of binary VALIDATE= COQ_XML= # is "-xml" when building XML library -VM= # is "-no-vm" to not use the vm" TIMED= # non-empty will activate a default time command # when compiling .v (see $(STDTIME) below) @@ -75,7 +83,7 @@ TIMECMD= # if you prefer a specific time command instead of $(STDTIME) STDTIME=/usr/bin/time -f "$* (user: %U mem: %M ko)" TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) -COQOPTS=$(COQ_XML) $(VM) $(NATIVECOMPUTE) +COQOPTS=$(COQ_XML) $(NATIVECOMPUTE) BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile # The SHOW and HIDE variables control whether make will echo complete commands @@ -104,12 +112,32 @@ LINKMETADATA= CODESIGN=true endif +# Best OCaml compiler, used in a generic way + +ifeq ($(BEST),opt) +OPT:=opt +BESTOBJ:=.cmx +BESTLIB:=.cmxa +BESTDYN:=.cmxs +else +OPT:= +BESTOBJ:=.cmo +BESTLIB:=.cma +BESTDYN:=.cma +endif + +define bestobj +$(patsubst %.cma,%$(BESTLIB),$(patsubst %.cmo,%$(BESTOBJ),$(1))) +endef + define bestocaml $(if $(OPT),\ $(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) $(LINKMETADATA) -o $@ $(1) $(addsuffix .cmxa,$(2)) $^ && $(STRIP) $@ && $(CODESIGN) $@,\ $(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(CUSTOM) -o $@ $(1) $(addsuffix .cma,$(2)) $^) endef +# Camlp4 / Camlp5 settings + CAMLP4DEPS:=tools/compat5.cmo grammar/grammar.cma ifeq ($(CAMLP4),camlp5) CAMLP4USE=pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION) @@ -172,13 +200,11 @@ endif TOTARGET = > "$@" || (RV=$$?; rm -f "$@"; exit $${RV}) ########################################################################### -# Compilation option for .c files +# Compilation of .c files ########################################################################### CINCLUDES= -I $(CAMLHLIB) -# libcoqrun.a, dllcoqrun.so - # NB: We used to do a ranlib after ocamlmklib, but it seems that # ocamlmklib is already doing it @@ -186,7 +212,6 @@ $(LIBCOQRUN): kernel/byterun/coq_jumptbl.h $(BYTERUN) cd $(dir $(LIBCOQRUN)) && \ $(OCAMLFIND) ocamlmklib -oc $(COQRUN) $(foreach u,$(BYTERUN),$(notdir $(u))) -#coq_jumptbl.h is required only if you have GCC 2.0 or later kernel/byterun/coq_jumptbl.h : kernel/byterun/coq_instruct.h sed -n -e '/^ /s/ \([A-Z]\)/ \&\&coq_lbl_\1/gp' \ -e '/^}/q' $< $(TOTARGET) @@ -195,6 +220,17 @@ kernel/copcodes.ml: kernel/byterun/coq_instruct.h sed -n -e '/^enum/p' -e 's/,//g' -e '/^ /p' $< | \ awk -f kernel/make-opcodes $(TOTARGET) +%.o: %.c + $(SHOW)'OCAMLC $<' + $(HIDE)cd $(dir $<) && $(OCAMLC) -ccopt "$(CFLAGS)" -c $(notdir $<) + +%_stubs.c.d: $(D_DEPEND_BEFORE_SRC) %_stubs.c $(D_DEPEND_AFTER_SRC) + $(SHOW)'CCDEP $<' + $(HIDE)echo "$@ $(@:.c.d=.o): $(@:.c.d=.c)" > $@ + +%.c.d: $(D_DEPEND_BEFORE_SRC) %.c $(D_DEPEND_AFTER_SRC) $(GENHFILES) + $(SHOW)'CCDEP $<' + $(HIDE)$(OCAMLC) -ccopt "-MM -MQ $@ -MQ $(<:.c=.o) -isystem $(CAMLHLIB)" $< $(TOTARGET) ########################################################################### # grammar/grammar.cma @@ -264,25 +300,16 @@ grammar/%.cmi: grammar/%.mli # Main targets (coqmktop, coqtop.opt, coqtop.byte) ########################################################################### -.PHONY: coqbinaries coq coqlib coqlight states +.PHONY: coqbinaries -coqbinaries: ${COQBINARIES} ${CSDPCERT} ${FAKEIDE} +coqbinaries: $(COQMKTOP) $(COQTOPEXE) $(COQTOPBYTE) \ + $(CHICKEN) $(CHICKENBYTE) $(CSDPCERT) $(FAKEIDE) -coq: coqlib tools coqbinaries - -coqlib: theories plugins - -coqlight: theories-light tools coqbinaries - -states: theories/Init/Prelude.vo - -miniopt: $(COQTOPEXE) pluginsopt -minibyte: $(COQTOPBYTE) pluginsbyte ifeq ($(BEST),opt) $(COQTOPEXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) $(LINKMETADATA) -thread -o $@ + $(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) $(LINKMETADATA) -o $@ $(STRIP) $@ $(CODESIGN) $@ else @@ -292,28 +319,13 @@ endif $(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(COQMKTOP) -boot -top $(BYTEFLAGS) -thread -o $@ + $(HIDE)$(COQMKTOP) -boot -top $(BYTEFLAGS) -o $@ -LOCALCHKLIBS:=$(addprefix -I , $(CHKSRCDIRS) ) -CHKLIBS:=$(LOCALCHKLIBS) -I $(MYCAMLP4LIB) - -ifeq ($(BEST),opt) -$(CHICKEN): checker/check.cmxa checker/main.ml - $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) $(LINKMETADATA) -thread -o $@ $(SYSCMXA) $^ - $(STRIP) $@ - $(CODESIGN) $@ -else -$(CHICKEN): $(CHICKENBYTE) - cp $< $@ -endif +# coqmktop -$(CHICKENBYTE): checker/check.cma checker/main.ml - $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) $(CUSTOM) -thread -o $@ $(SYSCMA) $^ +COQMKTOPCMO:=lib/clib.cma lib/errors.cmo tools/tolink.cmo tools/coqmktop.cmo -# coqmktop -$(COQMKTOP): $(patsubst %.cma,%$(BESTLIB),$(COQMKTOPCMO:.cmo=$(BESTOBJ))) +$(COQMKTOP): $(call bestobj, $(COQMKTOPCMO)) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD)) @@ -324,351 +336,19 @@ tools/tolink.ml: Makefile.build Makefile.common $(HIDE)echo "let core_objs = \""$(OBJSMOD)"\"" >> $@ # coqc -$(COQC): $(patsubst %.cma,%$(BESTLIB),$(COQCCMO:.cmo=$(BESTOBJ))) - $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD)) - -# Target for libraries .cma and .cmxa - -# The dependency over the .mllib is somewhat artificial, since -# ocamlc -a won't use this file, hence the $(filter-out ...) below. -# But this ensures that the .cm(x)a is rebuilt when needed, -# (especially when removing a module in the .mllib). -# We used to have a "order-only" dependency over .mllib.d here, -# but the -include mechanism should already ensure that we have -# up-to-date dependencies. - -%.cma: %.mllib - $(SHOW)'OCAMLC -a -o $@' - $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -a -o $@ $(filter-out %.mllib, $^) - -%.cmxa: %.mllib - $(SHOW)'OCAMLOPT -a -o $@' - $(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -a -o $@ $(filter-out %.mllib, $^) - -# For the checker, different flags may be used - -checker/check.cma: checker/check.mllib | md5chk - $(SHOW)'OCAMLC -a -o $@' - $(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) -a -o $@ $(filter-out %.mllib, $^) -checker/check.cmxa: checker/check.mllib | md5chk - $(SHOW)'OCAMLOPT -a -o $@' - $(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) -a -o $@ $(filter-out %.mllib, $^) - -########################################################################### -# Csdp to micromega special targets -########################################################################### +COQCCMO:=lib/clib.cma lib/errors.cmo toplevel/usage.cmo tools/coqc.cmo -plugins/micromega/csdpcert$(EXE): $(CSDPCERTCMO:.cmo=$(BESTOBJ)) \ - $(addsuffix $(BESTLIB), lib/clib) +$(COQC): $(call bestobj, $(COQCCMO)) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml,,nums unix clib) - -########################################################################### -# CoqIde special targets -########################################################################### - -.PHONY: coqide coqide-binaries coqide-no coqide-byte coqide-opt coqide-files - -# target to build CoqIde -coqide: coqide-files coqide-binaries theories/Init/Prelude.vo - -COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS)) $(COQIDEINCLUDES) - -.SUFFIXES:.vo - -IDEFILES=$(wildcard ide/*.lang) ide/coq_style.xml ide/coq.png ide/MacOS/default_accel_map - -coqide-binaries: coqide-$(HASCOQIDE) ide-toploop -coqide-no: -coqide-byte: $(COQIDEBYTE) $(COQIDE) -coqide-opt: $(COQIDEBYTE) $(COQIDE) -coqide-files: $(IDEFILES) -ifeq ($(BEST),opt) -ide-toploop: $(IDETOPLOOPCMA) $(IDETOPLOOPCMA:.cma=.cmxs) -else -ide-toploop: $(IDETOPLOOPCMA) -endif - -ifeq ($(HASCOQIDE),opt) -$(COQIDE): $(LINKIDEOPT) - $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ unix.cmxa threads.cmxa lablgtk.cmxa \ - lablgtksourceview2.cmxa str.cmxa $(IDEFLAGS:.cma=.cmxa) $^ - $(STRIP) $@ -else -$(COQIDE): $(COQIDEBYTE) - cp $< $@ -endif - -$(COQIDEBYTE): $(LINKIDE) - $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ unix.cma threads.cma lablgtk.cma \ - lablgtksourceview2.cma str.cma $(IDEFLAGS) $(IDECDEPSFLAGS) $^ - -# install targets - -.PHONY: install-coqide install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles - -ifeq ($(HASCOQIDE),no) -install-coqide: install-ide-toploop -else -install-coqide: install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles -endif - -install-ide-bin: - $(MKDIR) $(FULLBINDIR) - $(INSTALLBIN) $(COQIDE) $(FULLBINDIR) - -install-ide-toploop: - $(MKDIR) $(FULLCOQLIB)/toploop - $(INSTALLBIN) $(IDETOPLOOPCMA) $(FULLCOQLIB)/toploop/ -ifeq ($(BEST),opt) - $(INSTALLBIN) $(IDETOPLOOPCMA:.cma=.cmxs) $(FULLCOQLIB)/toploop/ -endif - -install-ide-devfiles: - $(MKDIR) $(FULLCOQLIB) - $(INSTALLSH) $(FULLCOQLIB) $(IDECMA) \ - $(foreach lib,$(IDECMA:.cma=_MLLIB_DEPENDENCIES),$(addsuffix .cmi,$($(lib)))) -ifeq ($(BEST),opt) - $(INSTALLSH) $(FULLCOQLIB) $(IDECMA:.cma=.cmxa) $(IDECMA:.cma=.a) -endif - -install-ide-files: #Please update $(COQIDEAPP)/Contents/Resources/ at the same time - $(MKDIR) $(FULLDATADIR) - $(INSTALLLIB) ide/coq.png ide/*.lang ide/coq_style.xml $(FULLDATADIR) - $(MKDIR) $(FULLCONFIGDIR) - if [ $(IDEINT) = QUARTZ ] ; then $(INSTALLLIB) ide/mac_default_accel_map $(FULLCONFIGDIR)/coqide.keys ; fi - -install-ide-info: - $(MKDIR) $(FULLDOCDIR) - $(INSTALLLIB) ide/FAQ $(FULLDOCDIR)/FAQ-CoqIde - -########################################################################### -# CoqIde MacOS special targets -########################################################################### - -.PHONY: $(COQIDEAPP)/Contents - -$(COQIDEAPP)/Contents: - rm -rdf $@ - $(MKDIR) $@ - sed -e "s/VERSION/$(VERSION4MACOS)/g" ide/MacOS/Info.plist.template > $@/Info.plist - $(MKDIR) "$@/MacOS" - -$(COQIDEINAPP): ide/macos_prehook.cmx $(LINKIDEOPT) | $(COQIDEAPP)/Contents - $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ \ - unix.cmxa lablgtk.cmxa lablgtksourceview2.cmxa str.cmxa \ - threads.cmxa $(IDEFLAGS:.cma=.cmxa) $^ - $(STRIP) $@ - -$(COQIDEAPP)/Contents/Resources/share: $(COQIDEAPP)/Contents - $(MKDIR) $@/coq/ - $(INSTALLLIB) ide/coq.png ide/*.lang ide/coq_style.xml $@/coq/ - $(MKDIR) $@/gtksourceview-2.0/{language-specs,styles} - $(INSTALLLIB) "$(GTKSHARE)/"gtksourceview-2.0/language-specs/{def.lang,language2.rng} $@/gtksourceview-2.0/language-specs/ - $(INSTALLLIB) "$(GTKSHARE)/"gtksourceview-2.0/styles/{styles.rng,classic.xml} $@/gtksourceview-2.0/styles/ - cp -R "$(GTKSHARE)/"locale $@ - cp -R "$(GTKSHARE)/"icons $@ - cp -R "$(GTKSHARE)/"themes $@ - -$(COQIDEAPP)/Contents/Resources/loaders: $(COQIDEAPP)/Contents - $(MKDIR) $@ - $(INSTALLLIB) $$("$(GTKBIN)/gdk-pixbuf-query-loaders" | sed -n -e '5 s!.*= \(.*\)$$!\1!p')/libpixbufloader-png.so $@ - -$(COQIDEAPP)/Contents/Resources/immodules: $(COQIDEAPP)/Contents - $(MKDIR) $@ - $(INSTALLLIB) "$(GTKLIBS)/gtk-2.0/2.10.0/immodules/"*.so $@ - - -$(COQIDEAPP)/Contents/Resources/etc: $(COQIDEAPP)/Contents/Resources/lib - $(MKDIR) $@/xdg/coq - $(INSTALLLIB) ide/MacOS/default_accel_map $@/xdg/coq/coqide.keys - $(MKDIR) $@/gtk-2.0 - { "$(GTKBIN)/gdk-pixbuf-query-loaders" $@/../loaders/*.so |\ - sed -e "s!/.*\(/loaders/.*.so\)!@executable_path/../Resources/\1!"; } \ - > $@/gtk-2.0/gdk-pixbuf.loaders - { "$(GTKBIN)/gtk-query-immodules-2.0" $@/../immodules/*.so |\ - sed -e "s!/.*\(/immodules/.*.so\)!@executable_path/../Resources/\1!" |\ - sed -e "s!/.*\(/share/locale\)!@executable_path/../Resources/\1!"; } \ - > $@/gtk-2.0/gtk-immodules.loaders - $(MKDIR) $@/pango - echo "[Pango]" > $@/pango/pangorc - -$(COQIDEAPP)/Contents/Resources/lib: $(COQIDEAPP)/Contents/Resources/immodules $(COQIDEAPP)/Contents/Resources/loaders $(COQIDEAPP)/Contents $(COQIDEINAPP) - $(MKDIR) $@ - $(INSTALLLIB) $(GTKLIBS)/charset.alias $@/ - $(MKDIR) $@/pango/1.8.0/modules - $(INSTALLLIB) "$(GTKLIBS)/pango/1.8.0/modules/"*.so $@/pango/1.8.0/modules/ - { "$(GTKBIN)/pango-querymodules" $@/pango/1.8.0/modules/*.so |\ - sed -e "s!/.*\(/pango/1.8.0/modules/.*.so\)!@executable_path/../Resources/lib\1!"; } \ - > $@/pango/1.8.0/modules.cache - - for i in $$(otool -L $(COQIDEINAPP) |sed -n -e "\@$(GTKLIBS)@ s/[^/]*\(\/[^ ]*\) .*$$/\1/p"); \ - do cp $$i $@/; \ - ide/MacOS/relatify_with-respect-to_.sh $@/$$(basename $$i) $(GTKLIBS) $@; \ - done - for i in $@/../loaders/*.so $@/../immodules/*.so $@/pango/1.8.0/modules/*.so; \ - do \ - for j in $$(otool -L $$i | sed -n -e "\@$(GTKLIBS)@ s/[^/]*\(\/[^ ]*\) .*$$/\1/p"); \ - do cp $$j $@/; ide/MacOS/relatify_with-respect-to_.sh $@/$$(basename $$j) $(GTKLIBS) $@; done; \ - ide/MacOS/relatify_with-respect-to_.sh $$i $(GTKLIBS) $@; \ - done - EXTRAWORK=1; \ - while [ $${EXTRAWORK} -eq 1 ]; \ - do EXTRAWORK=0; \ - for i in $@/*.dylib; \ - do for j in $$(otool -L $$i | sed -n -e "\@$(GTKLIBS)@ s/[^/]*\(\/[^ ]*\) .*$$/\1/p"); \ - do EXTRAWORK=1; cp $$j $@/; ide/MacOS/relatify_with-respect-to_.sh $@/$$(basename $$j) $(GTKLIBS) $@; done; \ - done; \ - done - ide/MacOS/relatify_with-respect-to_.sh $(COQIDEINAPP) $(GTKLIBS) $@ - -$(COQIDEAPP)/Contents/Resources:$(COQIDEAPP)/Contents/Resources/etc $(COQIDEAPP)/Contents/Resources/share - $(INSTALLLIB) ide/MacOS/*.icns $@ - -$(COQIDEAPP):$(COQIDEAPP)/Contents/Resources - $(CODESIGN) $@ - -########################################################################### -# tests -########################################################################### - -.PHONY: validate check test-suite $(ALLSTDLIB).v md5chk - -md5chk: - $(SHOW)'MD5SUM cic.mli' - $(HIDE)if grep -q `$(MD5SUM) checker/cic.mli` checker/values.ml; \ - then true; else echo "Error: outdated checker/values.ml"; false; fi - -VALIDOPTS=$(if $(VERBOSE),,-silent) -o -m - -validate: $(CHICKEN) | $(ALLVO) - $(SHOW)'COQCHK <theories & plugins>' - $(HIDE)$(CHICKEN) -boot $(VALIDOPTS) $(ALLMODS) - -$(ALLSTDLIB).v: - $(SHOW)'MAKE $(notdir $@)' - $(HIDE)echo "Require $(ALLMODS)." > $@ - -MAKE_TSOPTS=-C test-suite -s VERBOSE=$(VERBOSE) - -check: validate test-suite - -test-suite: world $(ALLSTDLIB).v - $(MAKE) $(MAKE_TSOPTS) clean - $(MAKE) $(MAKE_TSOPTS) all - $(MAKE) $(MAKE_TSOPTS) report - -################################################################## -# partial targets: 1) core ML parts -################################################################## - -.PHONY: lib kernel byterun library proofs tactics interp parsing pretyping -.PHONY: engine highparsing stm toplevel ltac - -lib: lib/clib.cma lib/lib.cma -kernel: kernel/kernel.cma -byterun: $(BYTERUN) -library: library/library.cma -engine: engine/engine.cma -proofs: proofs/proofs.cma -tactics: tactics/tactics.cma -interp: interp/interp.cma -parsing: parsing/parsing.cma -pretyping: pretyping/pretyping.cma -highparsing: parsing/highparsing.cma -stm: stm/stm.cma -toplevel: toplevel/toplevel.cma -ltac: ltac/ltac.cma - -########################################################################### -# 2) theories and plugins files -########################################################################### - -.PHONY: init theories theories-light -.PHONY: logic arith bool narith zarith qarith lists strings sets -.PHONY: fsets relations wellfounded reals setoids sorting numbers noreal -.PHONY: msets mmaps compat - -init: $(INITVO) - -theories: $(THEORIESVO) -theories-light: $(THEORIESLIGHTVO) - -logic: $(LOGICVO) -arith: $(ARITHVO) -bool: $(BOOLVO) -narith: $(NARITHVO) -zarith: $(ZARITHVO) -qarith: $(QARITHVO) -lists: $(LISTSVO) -strings: $(STRINGSVO) -sets: $(SETSVO) -fsets: $(FSETSVO) -relations: $(RELATIONSVO) -wellfounded: $(WELLFOUNDEDVO) -reals: $(REALSVO) -setoids: $(SETOIDSVO) -sorting: $(SORTINGVO) -numbers: $(NUMBERSVO) -unicode: $(UNICODEVO) -classes: $(CLASSESVO) -program: $(PROGRAMVO) -structures: $(STRUCTURESVO) -vectors: $(VECTORSVO) -msets: $(MSETSVO) -compat: $(COMPATVO) - -noreal: unicode logic arith bool zarith qarith lists sets fsets \ - relations wellfounded setoids sorting - -########################################################################### -# 3) plugins -########################################################################### - -.PHONY: plugins omega micromega setoid_ring nsatz extraction -.PHONY: fourier funind cc rtauto btauto pluginsopt pluginsbyte - -plugins: $(PLUGINSVO) -omega: $(OMEGAVO) $(OMEGACMA) $(ROMEGAVO) $(ROMEGACMA) -micromega: $(MICROMEGAVO) $(MICROMEGACMA) $(CSDPCERT) -setoid_ring: $(RINGVO) $(RINGCMA) -nsatz: $(NSATZVO) $(NSATZCMA) -extraction: $(EXTRACTIONCMA) -fourier: $(FOURIERVO) $(FOURIERCMA) -funind: $(FUNINDCMA) $(FUNINDVO) -cc: $(CCVO) $(CCCMA) -rtauto: $(RTAUTOVO) $(RTAUTOCMA) -btauto: $(BTAUTOVO) $(BTAUTOCMA) - -pluginsopt: $(PLUGINSOPT) -pluginsbyte: $(PLUGINS) - -########################################################################### -# rules to make theories and plugins -########################################################################### - -theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_DEP) - $(SHOW)'COQC $(COQ_XML) -noinit $<' - $(HIDE)rm -f theories/Init/$*.glob - $(HIDE)$(BOOTCOQC) $< $(COQ_XML) -noinit -R theories Coq - -theories/Numbers/Natural/BigN/NMake_gen.v: theories/Numbers/Natural/BigN/NMake_gen.ml - $(OCAML) $< $(TOTARGET) + $(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD)) ########################################################################### -# tools +# other tools ########################################################################### -.PHONY: printers tools - -printers: $(DEBUGPRINTERS) - -tools: $(TOOLS) $(DEBUGPRINTERS) $(OCAMLLIBDEP) +.PHONY: +tools: $(TOOLS) $(OCAMLLIBDEP) $(COQDEPBOOT) # coqdep_boot : a basic version of coqdep, with almost no dependencies. @@ -694,355 +374,139 @@ $(OCAMLLIBDEP): tools/ocamllibdep.ml # The full coqdep (unused by this build, but distributed by make install) -$(COQDEP): $(patsubst %.cma,%$(BESTLIB),$(COQDEPCMO:.cmo=$(BESTOBJ))) +COQDEPCMO:=lib/clib.cma lib/errors.cmo lib/minisys.cmo lib/system.cmo \ + tools/coqdep_lexer.cmo tools/coqdep_common.cmo tools/coqdep.cmo + +$(COQDEP): $(call bestobj, $(COQDEPCMO)) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD)) -$(GALLINA): $(addsuffix $(BESTOBJ), tools/gallina_lexer tools/gallina) +$(GALLINA): $(call bestobj, tools/gallina_lexer.cmo tools/gallina.cmo) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml,,) -$(COQMAKEFILE): $(patsubst %.cma,%$(BESTLIB),$(COQMAKEFILECMO:.cmo=$(BESTOBJ))) +COQMAKEFILECMO:=lib/clib.cma ide/project_file.cmo tools/coq_makefile.cmo + +$(COQMAKEFILE): $(call bestobj,$(COQMAKEFILECMO)) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml,,str unix threads) -$(COQTEX): tools/coq_tex$(BESTOBJ) +$(COQTEX): $(call bestobj, tools/coq_tex.cmo) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml,,str) -$(COQWC): tools/coqwc$(BESTOBJ) +$(COQWC): $(call bestobj, tools/coqwc.cmo) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml,,) -$(COQDOC): $(patsubst %.cma,%$(BESTLIB),$(COQDOCCMO:.cmo=$(BESTOBJ))) +COQDOCCMO:=lib/clib.cma $(addprefix tools/coqdoc/, \ + cdglobals.cmo alpha.cmo index.cmo tokens.cmo output.cmo cpretty.cmo main.cmo ) + +$(COQDOC): $(call bestobj, $(COQDOCCMO)) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml,,str unix) -$(COQWORKMGR): $(addsuffix $(BESTOBJ), stm/coqworkmgrApi tools/coqworkmgr) \ - $(addsuffix $(BESTLIB), lib/clib) +$(COQWORKMGR): $(call bestobj, lib/clib.cma stm/coqworkmgrApi.cmo tools/coqworkmgr.cmo) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml,, $(SYSMOD) clib) + $(HIDE)$(call bestocaml,, $(SYSMOD)) # fake_ide : for debugging or test-suite purpose, a fake ide simulating # a connection to coqtop -ideslave -$(FAKEIDE): lib/clib$(BESTLIB) lib/errors$(BESTOBJ) \ - lib/spawn$(BESTOBJ) ide/document$(BESTOBJ) \ - ide/serialize$(BESTOBJ) ide/xml_lexer$(BESTOBJ) \ - ide/xml_parser$(BESTOBJ) ide/xml_printer$(BESTOBJ) \ - ide/xmlprotocol$(BESTOBJ) tools/fake_ide$(BESTOBJ) | \ - $(IDETOPLOOPCMA:.cma=$(BESTDYN)) +FAKEIDECMO:= lib/clib.cma lib/errors.cmo lib/spawn.cmo ide/document.cmo \ + ide/serialize.cmo ide/xml_lexer.cmo ide/xml_parser.cmo ide/xml_printer.cmo \ + ide/xmlprotocol.cmo tools/fake_ide.cmo + +$(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOPLOOPCMA:.cma=$(BESTDYN)) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml,-I ide,str unix threads) # votour: a small vo explorer (based on the checker) -bin/votour: lib/cObj$(BESTOBJ) checker/analyze$(BESTOBJ) checker/values$(BESTOBJ) checker/votour.ml +bin/votour: $(call bestobj, lib/cObj.cmo checker/analyze.cmo checker/values.cmo) checker/votour.ml $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml, -I checker,) -# Special rule for the compatibility-with-camlp5 extension for camlp4 - -ifeq ($(CAMLP4),camlp4) -tools/compat5.cmo: tools/compat5.mlp - $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) $(CAMLP4FLAGS) -impl' -impl $< -tools/compat5b.cmo: tools/compat5b.mlp - $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) $(CAMLP4FLAGS) -impl' -impl $< -else -tools/compat5.cmo: tools/compat5.ml - $(OCAMLC) -c $< -endif - ########################################################################### -# Documentation : cf Makefile.doc +# Csdp to micromega special targets ########################################################################### -documentation: doc-$(WITHDOC) -doc-all: doc -doc-no: +CSDPCERTCMO:=lib/clib.cma $(addprefix plugins/micromega/, \ + mutils.cmo micromega.cmo \ + sos_types.cmo sos_lib.cmo sos.cmo csdpcert.cmo ) -.PHONY: documentation doc-all doc-no +$(CSDPCERT): $(call bestobj, $(CSDPCERTCMO)) + $(SHOW)'OCAMLBEST -o $@' + $(HIDE)$(call bestocaml,,nums unix) ########################################################################### -# Installation +# tests ########################################################################### -ifeq ($(LOCAL),true) -install: - @echo "Nothing to install in a local build!" -else -install: install-coq install-coqide install-doc-$(WITHDOC) -endif - -install-doc-all: install-doc -install-doc-no: - -.PHONY: install install-doc-all install-doc-no +.PHONY: validate check test-suite $(ALLSTDLIB).v -#These variables are intended to be set by the caller to make -#COQINSTALLPREFIX= -#OLDROOT= - - # Can be changed for a local installation (to make packages). - # You must NOT put a "/" at the end (Cygnus for win32 does not like "//"). - -ifdef COQINSTALLPREFIX -FULLBINDIR=$(BINDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) -FULLCOQLIB=$(COQLIBINSTALL:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) -FULLCONFIGDIR=$(CONFIGDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) -FULLDATADIR=$(DATADIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) -FULLMANDIR=$(MANDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) -FULLEMACSLIB=$(EMACSLIB:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) -FULLCOQDOCDIR=$(COQDOCDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) -FULLDOCDIR=$(DOCDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) -else -FULLBINDIR=$(BINDIR) -FULLCOQLIB=$(COQLIBINSTALL) -FULLCONFIGDIR=$(CONFIGDIR) -FULLDATADIR=$(DATADIR) -FULLMANDIR=$(MANDIR) -FULLEMACSLIB=$(EMACSLIB) -FULLCOQDOCDIR=$(COQDOCDIR) -FULLDOCDIR=$(DOCDIR) -endif - -.PHONY: install-coq install-coqlight install-binaries install-byte install-opt -.PHONY: install-tools install-library install-library-light install-devfiles -.PHONY: install-coq-info install-coq-manpages install-emacs install-latex - -install-coq: install-binaries install-library install-coq-info install-devfiles -install-coqlight: install-binaries install-library-light - -install-binaries: install-tools - $(MKDIR) $(FULLBINDIR) - $(INSTALLBIN) $(COQC) $(COQTOPBYTE) $(COQTOPEXE) $(CHICKEN) $(FULLBINDIR) - $(MKDIR) $(FULLCOQLIB)/toploop - $(INSTALLBIN) $(TOPLOOPCMA) $(FULLCOQLIB)/toploop/ -ifeq ($(BEST),opt) - $(INSTALLBIN) $(TOPLOOPCMA:.cma=.cmxs) $(FULLCOQLIB)/toploop/ -endif - - -install-tools: - $(MKDIR) $(FULLBINDIR) - # recopie des fichiers de style pour coqide - $(MKDIR) $(FULLCOQLIB)/tools/coqdoc - touch $(FULLCOQLIB)/tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc/coqdoc.css # to have the mode according to umask (bug #1715) - $(INSTALLLIB) tools/coqdoc/coqdoc.css tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc - $(INSTALLBIN) $(TOOLS) $(FULLBINDIR) - -# The list of .cmi to install, including the ones obtained -# from .mli without .ml, and the ones obtained from .ml without .mli - -INSTALLCMI = $(sort \ - $(filter-out checker/% ide/% tools/%, $(MLIFILES:.mli=.cmi)) \ - $(foreach lib,$(CORECMA) $(PLUGINSCMA), $(addsuffix .cmi,$($(lib:.cma=_MLLIB_DEPENDENCIES))))) - -install-devfiles: - $(MKDIR) $(FULLBINDIR) - $(INSTALLBIN) $(COQMKTOP) $(FULLBINDIR) - $(MKDIR) $(FULLCOQLIB) - $(INSTALLSH) $(FULLCOQLIB) $(LINKCMO) $(GRAMMARCMA) - $(INSTALLSH) $(FULLCOQLIB) $(INSTALLCMI) -ifeq ($(BEST),opt) - $(INSTALLSH) $(FULLCOQLIB) $(LINKCMX) $(CORECMA:.cma=.a) $(STATICPLUGINS:.cma=.a) -endif - -install-library: - $(MKDIR) $(FULLCOQLIB) - $(INSTALLSH) $(FULLCOQLIB) $(LIBFILES) $(PLUGINS) - $(MKDIR) $(FULLCOQLIB)/user-contrib -ifndef CUSTOM - $(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB) -endif -ifeq ($(BEST),opt) - $(INSTALLLIB) $(LIBCOQRUN) $(FULLCOQLIB) - $(INSTALLSH) $(FULLCOQLIB) $(PLUGINSOPT) -endif -# csdpcert is not meant to be directly called by the user; we install -# it with libraries - -$(MKDIR) $(FULLCOQLIB)/plugins/micromega - $(INSTALLBIN) $(CSDPCERT) $(FULLCOQLIB)/plugins/micromega - rm -f $(FULLCOQLIB)/revision - -$(INSTALLLIB) revision $(FULLCOQLIB) - -install-library-light: - $(MKDIR) $(FULLCOQLIB) - $(INSTALLSH) $(FULLCOQLIB) $(LIBFILESLIGHT) $(INITPLUGINS) - rm -f $(FULLCOQLIB)/revision - -$(INSTALLLIB) revision $(FULLCOQLIB) -ifndef CUSTOM - $(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB) -endif -ifeq ($(BEST),opt) - $(INSTALLLIB) $(LIBCOQRUN) $(FULLCOQLIB) - $(INSTALLSH) $(FULLCOQLIB) $(INITPLUGINSOPT) -endif +VALIDOPTS=$(if $(VERBOSE),,-silent) -o -m -install-coq-info: install-coq-manpages install-emacs install-latex +validate: $(CHICKEN) | $(ALLVO) + $(SHOW)'COQCHK <theories & plugins>' + $(HIDE)$(CHICKEN) -boot $(VALIDOPTS) $(ALLMODS) -install-coq-manpages: - $(MKDIR) $(FULLMANDIR)/man1 - $(INSTALLLIB) $(MANPAGES) $(FULLMANDIR)/man1 +$(ALLSTDLIB).v: + $(SHOW)'MAKE $(notdir $@)' + $(HIDE)echo "Require $(ALLMODS)." > $@ -install-emacs: - $(MKDIR) $(FULLEMACSLIB) - $(INSTALLLIB) tools/gallina-db.el tools/coq-font-lock.el tools/gallina-syntax.el tools/gallina.el tools/coq-inferior.el $(FULLEMACSLIB) +MAKE_TSOPTS=-C test-suite -s VERBOSE=$(VERBOSE) -# command to update TeX' kpathsea database -#UPDATETEX = $(MKTEXLSR) /usr/share/texmf /var/spool/texmf $(BASETEXDIR) > /dev/null +check: validate test-suite -install-latex: - $(MKDIR) $(FULLCOQDOCDIR) - $(INSTALLLIB) tools/coqdoc/coqdoc.sty $(FULLCOQDOCDIR) -# -$(UPDATETEX) +test-suite: world $(ALLSTDLIB).v + $(MAKE) $(MAKE_TSOPTS) clean + $(MAKE) $(MAKE_TSOPTS) all + $(MAKE) $(MAKE_TSOPTS) report ########################################################################### -# Documentation of the source code (using ocamldoc) +### Special rules (Camlp5 / Camlp4) ########################################################################### -.PHONY: source-doc mli-doc ml-doc - -source-doc: mli-doc $(OCAMLDOCDIR)/coq.pdf - -$(OCAMLDOCDIR)/coq.tex: $(DOCMLIS:.mli=.cmi) - $(SHOW)'OCAMLDOC -latex -o $@' - $(HIDE)$(OCAMLFIND) ocamldoc -latex -rectypes -I $(MYCAMLP4LIB) $(MLINCLUDES)\ - $(DOCMLIS) -noheader -t "Coq mlis documentation" \ - -intro $(OCAMLDOCDIR)/docintro -o $@.tmp - $(SHOW)'OCAMLDOC utf8 fix' - $(HIDE)$(OCAMLDOCDIR)/fix-ocamldoc-utf8 $@.tmp - $(HIDE)cat $(OCAMLDOCDIR)/header.tex $@.tmp > $@ - rm $@.tmp - -mli-doc: $(DOCMLIS:.mli=.cmi) - $(SHOW)'OCAMLDOC -html' - $(HIDE)$(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads -I $(MYCAMLP4LIB) $(MLINCLUDES) \ - $(DOCMLIS) -d $(OCAMLDOCDIR)/html -colorize-code \ - -t "Coq mlis documentation" -intro $(OCAMLDOCDIR)/docintro \ - -css-style style.css - -ml-dot: $(MLFILES) - $(OCAMLFIND) ocamldoc -dot -dot-reduce -rectypes -I +threads -I $(CAMLLIB) -I $(MYCAMLP4LIB) $(MLINCLUDES) \ - $(filter $(addsuffix /%.ml,$(CORESRCDIRS)),$(MLFILES)) -o $(OCAMLDOCDIR)/coq.dot - -%_dep.png: %.dot - $(DOT) -Tpng $< -o $@ - -%_types.dot: %.mli - $(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -dot-types -o $@ $< - -OCAMLDOC_MLLIBD = $(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ \ - $(foreach lib,$(|:.mllib.d=_MLLIB_DEPENDENCIES),$(addsuffix .ml,$($(lib)))) - -%.dot: | %.mllib.d - $(OCAMLDOC_MLLIBD) - -ml-doc: - $(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads $(MLINCLUDES) $(COQIDEFLAGS) -d $(OCAMLDOCDIR) $(MLSTATICFILES) - -parsing/parsing.dot : | parsing/parsing.mllib.d parsing/highparsing.mllib.d - $(OCAMLDOC_MLLIBD) - -grammar/grammar.dot : | grammar/grammar.mllib.d - $(OCAMLDOC_MLLIBD) - -tactics/tactics.dot: | tactics/tactics.mllib.d ltac/ltac.mllib.d - $(OCAMLDOC_MLLIBD) - -%.dot: %.mli - $(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $< +# Special rule for the compatibility-with-camlp5 extension for camlp4 -$(OCAMLDOCDIR)/%.pdf: $(OCAMLDOCDIR)/%.tex - $(SHOW)'PDFLATEX $*.tex' - $(HIDE)(cd $(OCAMLDOCDIR) ; pdflatex -interaction=batchmode $*.tex && pdflatex -interaction=batchmode $*.tex) - $(HIDE)(cd doc/tools/; show_latex_messages -no-overfull ../../$(OCAMLDOCDIR)/$*.log) +ifeq ($(CAMLP4),camlp4) +tools/compat5.cmo: tools/compat5.mlp + $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) $(CAMLP4FLAGS) -impl' -impl $< +tools/compat5b.cmo: tools/compat5b.mlp + $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) $(CAMLP4FLAGS) -impl' -impl $< +else +tools/compat5.cmo: tools/compat5.ml + $(OCAMLC) -c $< +endif ########################################################################### -### Special rules +# Default rules for compiling ML code ########################################################################### -dev/printers.cma: dev/printers.mllib - $(SHOW)'Testing $@' - $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -thread $(SYSCMA) $(P4CMA) $(filter-out %.mllib, $^) -o test-printer - @rm -f test-printer - $(SHOW)'OCAMLC -a $@' - $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -thread $(SYSCMA) $(P4CMA) $(filter-out %.mllib, $^) -linkall -a -o $@ +# Target for libraries .cma and .cmxa -ide/coqide_main.ml: ide/coqide_main.ml4 config/Makefile # no camlp4deps here - $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) $(CAMLP4FLAGS) $(PR_O) $(CAMLP4USE) -D$(IDEINT) -impl $< -o $@ - -# pretty printing of the revision number when compiling a checked out -# source tree -.PHONY: revision - -revision: - $(SHOW)'CHECK revision' - $(HIDE)rm -f revision.new -ifeq ($(CHECKEDOUT),svn) - $(HIDE)set -e; \ - if test -x "`which svn`"; then \ - export LC_ALL=C;\ - svn info . | sed -ne '/URL/s/.*\/\([^\/]\{1,\}\)/\1/p' > revision.new; \ - svn info . | sed -ne '/Revision/s/Revision: \([0-9]\{1,\}\)/\1/p'>> revision.new; \ - fi -endif -ifeq ($(CHECKEDOUT),gnuarch) - $(HIDE)set -e; \ - if test -x "`which tla`"; then \ - LANG=C; export LANG; \ - tla tree-version > revision.new ; \ - tla tree-revision | sed -ne 's|.*--||p' >> revision.new ; \ - fi -endif -ifeq ($(CHECKEDOUT),git) - $(HIDE)set -e; \ - if test -x "`which git`"; then \ - LANG=C; export LANG; \ - GIT_BRANCH=$$(git branch -a | sed -ne '/^\* /s/^\* \(.*\)/\1/p'); \ - GIT_HOST=$$(hostname); \ - GIT_PATH=$$(pwd); \ - (echo "$${GIT_HOST}:$${GIT_PATH},$${GIT_BRANCH}") > revision.new; \ - (echo "$$(git log -1 --pretty='format:%H')") >> revision.new; \ - fi -endif - $(HIDE)set -e; \ - if test -e revision.new; then \ - if test -e revision; then \ - if test "`cat revision`" = "`cat revision.new`" ; then \ - rm -f revision.new; \ - else \ - mv -f revision.new revision; \ - fi; \ - else \ - mv -f revision.new revision; \ - fi \ - fi +# The dependency over the .mllib is somewhat artificial, since +# ocamlc -a won't use this file, hence the $(filter-out ...) below. +# But this ensures that the .cm(x)a is rebuilt when needed, +# (especially when removing a module in the .mllib). +# We used to have a "order-only" dependency over .mllib.d here, +# but the -include mechanism should already ensure that we have +# up-to-date dependencies. -########################################################################### -# Default rules -########################################################################### +%.cma: %.mllib + $(SHOW)'OCAMLC -a -o $@' + $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -a -o $@ $(filter-out %.mllib, $^) -## Three flavor of flags: checker/* ide/* and normal files +%.cmxa: %.mllib + $(SHOW)'OCAMLOPT -a -o $@' + $(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -a -o $@ $(filter-out %.mllib, $^) COND_BYTEFLAGS= \ - $(if $(filter checker/%,$<), $(CHKLIBS) -thread, \ - $(if $(filter ide/%,$<), $(COQIDEFLAGS), \ - $(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide,) $(MLINCLUDES) -thread)) $(BYTEFLAGS) + $(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide,) $(MLINCLUDES) $(BYTEFLAGS) COND_OPTFLAGS= \ - $(if $(filter checker/%,$<), $(CHKLIBS) -thread, \ - $(if $(filter ide/%,$<), $(COQIDEFLAGS), \ - $(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide,) $(MLINCLUDES) -thread)) $(OPTFLAGS) - -%.o: %.c - $(SHOW)'OCAMLC $<' - $(HIDE)cd $(dir $<) && $(OCAMLC) -ccopt "$(CFLAGS)" -c $(notdir $<) - -%.o: %.rc - $(SHOW)'WINDRES $<' - $(HIDE)i686-w64-mingw32-windres -i $< -o $@ + $(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide,) $(MLINCLUDES) $(OPTFLAGS) %.cmi: %.mli $(SHOW)'OCAMLC $<' @@ -1103,87 +567,75 @@ plugins/%_mod.ml: plugins/%.mllib $(HIDE)$(CAMLP4O) $(CAMLP4FLAGS) $(PR_O) \ $(CAMLP4DEPS) $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< -o $@ -%.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP) - $(SHOW)'COQC $<' - $(HIDE)rm -f $*.glob - $(HIDE)$(BOOTCOQC) $< -ifdef VALIDATE - $(SHOW)'COQCHK $(call vo_to_mod,$@)' - $(HIDE)$(CHICKEN) -boot -silent -norec $(call vo_to_mod,$@) \ - || ( RV=$$?; rm -f "$@"; exit $${RV} ) -endif ########################################################################### -# Dependencies +# Dependencies of ML code ########################################################################### -# Since OCaml 3.12.1, we could use again ocamldep directly, thanks to -# the option -ml-synonym - -OCAMLDEP_NG = $(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 - -checker/%.ml.d: $(D_DEPEND_BEFORE_SRC) checker/%.ml $(D_DEPEND_AFTER_SRC) $(GENFILES) - $(SHOW)'OCAMLDEP $<' - $(HIDE)$(OCAMLDEP_NG) $(LOCALCHKLIBS) "$<" $(TOTARGET) - -checker/%.mli.d: $(D_DEPEND_BEFORE_SRC) checker/%.mli $(D_DEPEND_AFTER_SRC) $(GENFILES) - $(SHOW)'OCAMLDEP $<' - $(HIDE)$(OCAMLDEP_NG) $(LOCALCHKLIBS) "$<" $(TOTARGET) +# Ocamldep is now used directly again (thanks to -ml-synonym in OCaml >= 3.12) +OCAMLDEP = $(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 %.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml $(D_DEPEND_AFTER_SRC) $(GENFILES) $(SHOW)'OCAMLDEP $<' - $(HIDE)$(OCAMLDEP_NG) $(DEPFLAGS) "$<" $(TOTARGET) + $(HIDE)$(OCAMLDEP) $(DEPFLAGS) "$<" $(TOTARGET) %.mli.d: $(D_DEPEND_BEFORE_SRC) %.mli $(D_DEPEND_AFTER_SRC) $(GENFILES) $(SHOW)'OCAMLDEP $<' - $(HIDE)$(OCAMLDEP_NG) $(DEPFLAGS) "$<" $(TOTARGET) - -checker/%.mllib.d: $(D_DEPEND_BEFORE_SRC) checker/%.mllib $(D_DEPEND_AFTER_SRC) $(OCAMLLIBDEP) $(GENFILES) - $(SHOW)'OCAMLLIBDEP $<' - $(HIDE)$(OCAMLLIBDEP) $(LOCALCHKLIBS) "$<" $(TOTARGET) - -dev/%.mllib.d: $(D_DEPEND_BEFORE_SRC) dev/%.mllib $(D_DEPEND_AFTER_SRC) $(OCAMLLIBDEP) $(GENFILES) - $(SHOW)'OCAMLLIBDEP $<' - $(HIDE)$(OCAMLLIBDEP) $(DEPFLAGS) -I dev "$<" $(TOTARGET) + $(HIDE)$(OCAMLDEP) $(DEPFLAGS) "$<" $(TOTARGET) %.mllib.d: $(D_DEPEND_BEFORE_SRC) %.mllib $(D_DEPEND_AFTER_SRC) $(OCAMLLIBDEP) $(GENFILES) $(SHOW)'OCAMLLIBDEP $<' $(HIDE)$(OCAMLLIBDEP) $(DEPFLAGS) "$<" $(TOTARGET) -%.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENVFILES) - $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEPBOOT) -boot $(DEPNATDYN) "$<" $(TOTARGET) +########################################################################### +# Compilation of .v files +########################################################################### -%_stubs.c.d: $(D_DEPEND_BEFORE_SRC) %_stubs.c $(D_DEPEND_AFTER_SRC) - $(SHOW)'CCDEP $<' - $(HIDE)echo "$@ $(@:.c.d=.o): $(@:.c.d=.c)" > $@ +# NB: for make world, no need to mention explicitly the .cmxs of the plugins, +# since they are all mentioned in at least one Declare ML Module in some .v -%.c.d: $(D_DEPEND_BEFORE_SRC) %.c $(D_DEPEND_AFTER_SRC) $(GENHFILES) - $(SHOW)'CCDEP $<' - $(HIDE)$(OCAMLC) -ccopt "-MM -MQ $@ -MQ $(<:.c=.o) -isystem $(CAMLHLIB)" $< $(TOTARGET) +coqlib: theories plugins -########################################################################### -# this sets up developper supporting stuff -########################################################################### +theories: $(THEORIESVO) +plugins: $(PLUGINSVO) -.PHONY: devel otags -devel: $(DEBUGPRINTERS) +.PHONY: coqlib theories plugins -# NOTA : otags only accepts camlp4 as preprocessor, so the following rule -# won't build tags of .ml4 when compiling with camlp5 -otags: - otags $(MLIFILES) $(filter-out configure.ml, $(MLSTATICFILES)) \ - $(if $(filter camlp5,$(CAMLP4)), , \ - -pa op -pa g -pa m -pa rq $(addprefix -pa , $(CAMLP4DEPS)) \ - $(addprefix -impl , $(ML4FILES))) +# One of the .v files is macro-generated +theories/Numbers/Natural/BigN/NMake_gen.v: theories/Numbers/Natural/BigN/NMake_gen.ml + $(OCAML) $< $(TOTARGET) + +# The .vo files in Init are built with the -noinit option + +theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_DEP) + $(SHOW)'COQC $(COQ_XML) -noinit $<' + $(HIDE)rm -f theories/Init/$*.glob + $(HIDE)$(BOOTCOQC) $< $(COQ_XML) -noinit -R theories Coq + +# The general rule for building .vo files : + +%.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP) + $(SHOW)'COQC $<' + $(HIDE)rm -f $*.glob + $(HIDE)$(BOOTCOQC) $< +ifdef VALIDATE + $(SHOW)'COQCHK $(call vo_to_mod,$@)' + $(HIDE)$(CHICKEN) -boot -silent -norec $(call vo_to_mod,$@) \ + || ( RV=$$?; rm -f "$@"; exit $${RV} ) +endif + +# Dependencies of .v files + +%.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENVFILES) + $(SHOW)'COQDEP $<' + $(HIDE)$(COQDEPBOOT) -boot $(DEPNATDYN) "$<" $(TOTARGET) ########################################################################### # To speed-up things a bit, let's dissuade make to attempt rebuilding makefiles -Makefile Makefile.build Makefile.common config/Makefile : ; - +Makefile $(wildcard Makefile.*) config/Makefile : ; # For emacs: # Local Variables: diff --git a/Makefile.checker b/Makefile.checker new file mode 100644 index 000000000..3ea0baced --- /dev/null +++ b/Makefile.checker @@ -0,0 +1,86 @@ +####################################################################### +# v # The Coq Proof Assistant / The Coq Development Team # +# <O___,, # INRIA-Rocquencourt & LRI-CNRS-Orsay # +# \VV/ ############################################################# +# // # This file is distributed under the terms of the # +# # GNU Lesser General Public License Version 2.1 # +####################################################################### + +## Makefile rules for building Coqchk + +## NB: For the moment, the build system of Coqchk is part of +## the one of Coq. In particular, this Makefile.checker is included in +## Makefile.build. Please ensure that the rules define here are +## indeed specific to files of the form checker/* + +# The binaries + +CHICKENBYTE:=bin/coqchk.byte$(EXE) +CHICKEN:=bin/coqchk$(EXE) + +# The sources + +CHKLIBS:= -I config -I lib -I checker + +## NB: currently, both $(OPTFLAGS) and $(BYTEFLAGS) contain -thread + +# The rules + +ifeq ($(BEST),opt) +$(CHICKEN): checker/check.cmxa checker/main.ml + $(SHOW)'OCAMLOPT -o $@' + $(HIDE)$(OCAMLOPT) $(SYSCMXA) $(CHKLIBS) $(OPTFLAGS) $(LINKMETADATA) -o $@ $^ + $(STRIP) $@ + $(CODESIGN) $@ +else +$(CHICKEN): $(CHICKENBYTE) + cp $< $@ +endif + +$(CHICKENBYTE): checker/check.cma checker/main.ml + $(SHOW)'OCAMLC -o $@' + $(HIDE)$(OCAMLC) $(SYSCMA) $(CHKLIBS) $(BYTEFLAGS) $(CUSTOM) -o $@ $^ + +checker/check.cma: checker/check.mllib | md5chk + $(SHOW)'OCAMLC -a -o $@' + $(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) -a -o $@ $(filter-out %.mllib, $^) + +checker/check.cmxa: checker/check.mllib | md5chk + $(SHOW)'OCAMLOPT -a -o $@' + $(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) -a -o $@ $(filter-out %.mllib, $^) + +checker/%.ml.d: checker/%.ml + $(SHOW)'OCAMLDEP $<' + $(HIDE)$(OCAMLFIND) ocamldep -slash $(CHKLIBS) "$<" $(TOTARGET) + +checker/%.mli.d: checker/%.mli + $(SHOW)'OCAMLDEP $<' + $(HIDE)$(OCAMLFIND) ocamldep -slash $(CHKLIBS) "$<" $(TOTARGET) + +checker/%.mllib.d: checker/%.mllib | $(OCAMLLIBDEP) + $(SHOW)'OCAMLLIBDEP $<' + $(HIDE)$(OCAMLLIBDEP) $(CHKLIBS) "$<" $(TOTARGET) + +checker/%.cmi: checker/%.mli + $(SHOW)'OCAMLC $<' + $(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) -c $< + +checker/%.cmo: checker/%.ml + $(SHOW)'OCAMLC $<' + $(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) -c $< + +checker/%.cmx: checker/%.ml + $(SHOW)'OCAMLOPT $<' + $(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) $(HACKMLI) -c $< + +md5chk: + $(SHOW)'MD5SUM cic.mli' + $(HIDE)if grep -q `$(MD5SUM) checker/cic.mli` checker/values.ml; \ + then true; else echo "Error: outdated checker/values.ml"; false; fi + +.PHONY: md5chk + +# For emacs: +# Local Variables: +# mode: makefile +# End: diff --git a/Makefile.common b/Makefile.common index 86a7ea847..463006c49 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,27 +52,6 @@ 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 \ @@ -76,82 +68,6 @@ SRCDIRS:=\ tools tools/coqdoc \ $(addprefix plugins/, $(PLUGINS)) -IDESRCDIRS:= $(CORESRCDIRS) ide ide/utils - -CHKSRCDIRS:= config lib checker - -########################################################################### -# Tools -########################################################################### - -COQDEP:=bin/coqdep$(EXE) -COQDEPBOOT:=bin/coqdep_boot$(EXE) -OCAMLLIBDEP:=bin/ocamllibdep$(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) $(OCAMLLIBDEP) $(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 -########################################################################### - COQRUN := coqrun LIBCOQRUN:=kernel/byterun/lib$(COQRUN).a DLLCOQRUN:=$(dir $(LIBCOQRUN))dll$(COQRUN)$(DLLEXT) @@ -173,6 +89,14 @@ TOPLOOPCMA:=stm/proofworkertop.cma stm/tacworkertop.cma stm/queryworkertop.cma GRAMMARCMA:=tools/compat5.cmo grammar/grammar.cma +# modules known by the toplevel of Coq + +OBJSMOD:=$(shell cat $(CORECMA:.cma=.mllib)) + +########################################################################### +# plugins object files +########################################################################### + OMEGACMA:=plugins/omega/omega_plugin.cma ROMEGACMA:=plugins/romega/romega_plugin.cma MICROMEGACMA:=plugins/micromega/micromega_plugin.cma @@ -230,169 +154,47 @@ endif LINKCMO:=$(CORECMA) $(STATICPLUGINS) LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cma=.cmxa) -IDEDEPS:=lib/clib.cma 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 - -# 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) lib/minisys.cmo lib/system.cmo 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 ) - -COQMAKEFILECMO:=lib/clib.cma ide/project_file.cmo tools/coq_makefile.cmo - ########################################################################### # vo files ########################################################################### ## 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 \ - ./engine/*.mli ./pretyping/*.mli ./interp/*.mli printing/*.mli \ - ./parsing/*.mli ./proofs/*.mli \ - ./tactics/*.mli ./stm/*.mli ./toplevel/*.mli ./ltac/*.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 diff --git a/Makefile.dev b/Makefile.dev new file mode 100644 index 000000000..f35b861c1 --- /dev/null +++ b/Makefile.dev @@ -0,0 +1,223 @@ +####################################################################### +# v # The Coq Proof Assistant / The Coq Development Team # +# <O___,, # INRIA-Rocquencourt & LRI-CNRS-Orsay # +# \VV/ ############################################################# +# // # This file is distributed under the terms of the # +# # GNU Lesser General Public License Version 2.1 # +####################################################################### + +# Extra targets for developpers : +# debug printers, revision, partial targets ... + +######################### +# Debug printers in dev/ +######################### + +.PHONY: devel printers + +DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/printers.cma + +devel: printers +printers: $(DEBUGPRINTERS) + +dev/printers.cma: dev/printers.mllib + $(SHOW)'Testing $@' + $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(SYSCMA) $(P4CMA) $(filter-out %.mllib, $^) -o test-printer + @rm -f test-printer + $(SHOW)'OCAMLC -a $@' + $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(SYSCMA) $(P4CMA) $(filter-out %.mllib, $^) -linkall -a -o $@ + +dev/%.mllib.d: dev/%.mllib | $(OCAMLLIBDEP) $(GENFILES) + $(SHOW)'OCAMLLIBDEP $<' + $(HIDE)$(OCAMLLIBDEP) $(DEPFLAGS) -I dev "$<" $(TOTARGET) + +############ +# revision +############ + +# display the revision number when compiling a checked out source tree + +revision: + $(SHOW)'CHECK revision' + $(HIDE)rm -f revision.new +ifeq ($(CHECKEDOUT),svn) + $(HIDE)set -e; \ + if test -x "`which svn`"; then \ + export LC_ALL=C;\ + svn info . | sed -ne '/URL/s/.*\/\([^\/]\{1,\}\)/\1/p' > revision.new; \ + svn info . | sed -ne '/Revision/s/Revision: \([0-9]\{1,\}\)/\1/p'>> revision.new; \ + fi +endif +ifeq ($(CHECKEDOUT),gnuarch) + $(HIDE)set -e; \ + if test -x "`which tla`"; then \ + LANG=C; export LANG; \ + tla tree-version > revision.new ; \ + tla tree-revision | sed -ne 's|.*--||p' >> revision.new ; \ + fi +endif +ifeq ($(CHECKEDOUT),git) + $(HIDE)set -e; \ + if test -x "`which git`"; then \ + LANG=C; export LANG; \ + GIT_BRANCH=$$(git branch -a | sed -ne '/^\* /s/^\* \(.*\)/\1/p'); \ + GIT_HOST=$$(hostname); \ + GIT_PATH=$$(pwd); \ + (echo "$${GIT_HOST}:$${GIT_PATH},$${GIT_BRANCH}") > revision.new; \ + (echo "$$(git log -1 --pretty='format:%H')") >> revision.new; \ + fi +endif + $(HIDE)set -e; \ + if test -e revision.new; then \ + if test -e revision; then \ + if test "`cat revision`" = "`cat revision.new`" ; then \ + rm -f revision.new; \ + else \ + mv -f revision.new revision; \ + fi; \ + else \ + mv -f revision.new revision; \ + fi \ + fi + +.PHONY: revision + +################### +# Partial builds +################### + +# The following partial targets are normally not necessary +# for a complete build of coq, see instead 'make world' for that. +# But these partial targets could be quite handy for quick builds +# of specific components of Coq. + +############################### +### 1) general-purpose targets +############################### + +coqlight: theories-light tools coqbinaries + +states: theories/Init/Prelude.vo + +miniopt: $(COQTOPEXE) pluginsopt +minibyte: $(COQTOPBYTE) pluginsbyte + +pluginsopt: $(PLUGINSOPT) +pluginsbyte: $(PLUGINS) + +.PHONY: coqlight states miniopt minibyte pluginsopt pluginsbyte + +########################## +### 2) core ML components +########################## + +lib: lib/clib.cma lib/lib.cma +kernel: kernel/kernel.cma +byterun: $(BYTERUN) +library: library/library.cma +engine: engine/engine.cma +proofs: proofs/proofs.cma +tactics: tactics/tactics.cma +interp: interp/interp.cma +parsing: parsing/parsing.cma +pretyping: pretyping/pretyping.cma +highparsing: parsing/highparsing.cma +stm: stm/stm.cma +toplevel: toplevel/toplevel.cma +ltac: ltac/ltac.cma + +.PHONY: lib kernel byterun library proofs tactics interp parsing pretyping +.PHONY: engine highparsing stm toplevel ltac + +###################### +### 3) theories files +###################### + +init: $(filter theories/Init/%, $(THEORIESVO)) +logic: $(filter theories/Logic/%, %(THEORIESVO)) +arith: $(filter theories/Arith/%, $(THEORIESVO)) +bool: $(filter theories/Bool/%, $(THEORIESVO)) +parith: $(filter theories/PArith/%, $(THEORIESVO)) +narith: $(filter theories/NArith/%, $(THEORIESVO)) +zarith: $(filter theories/ZArith/%, $(THEORIESVO)) +qarith: $(filter theories/QArith/%, $(THEORIESVO)) +lists: $(filter theories/Lists/%, $(THEORIESVO)) +strings: $(filter theories/Strings/%, $(THEORIESVO)) +sets: $(filter theories/Sets/%, $(THEORIESVO)) +fsets: $(filter theories/FSets/%, $(THEORIESVO)) +relations: $(filter theories/Relations/%, $(THEORIESVO)) +wellfounded: $(filter theories/Wellfounded/%, $(THEORIESVO)) +reals: $(filter theories/Reals/%, $(THEORIESVO)) +setoids: $(filter theories/Setoids/%, $(THEORIESVO)) +sorting: $(filter theories/Sorting/%, $(THEORIESVO)) +numbers: $(filter theories/Numbers/%, $(THEORIESVO)) +unicode: $(filter theories/Unicode/%, $(THEORIESVO)) +classes: $(filter theories/Classes/%, $(THEORIESVO)) +program: $(filter theories/Program/%, $(THEORIESVO)) +structures: $(filter theories/Structures/%, $(THEORIESVO)) +vectors: $(filter theories/Vectors/%, $(THEORIESVO)) +msets: $(filter theories/MSets/%, $(THEORIESVO)) +compat: $(filter theories/Compat/%, $(THEORIESVO)) + +theories-light: $(THEORIESLIGHTVO) + +noreal: unicode logic arith bool zarith qarith lists sets fsets \ + relations wellfounded setoids sorting + +.PHONY: init theories-light noreal +.PHONY: logic arith bool narith zarith qarith lists strings sets +.PHONY: fsets relations wellfounded reals setoids sorting numbers +.PHONY: msets mmaps compat + +################ +### 4) plugins +################ + +OMEGAVO:=$(filter plugins/omega/%, $(PLUGINSVO)) +ROMEGAVO:=$(filter plugins/romega/%, $(PLUGINSVO)) +MICROMEGAVO:=$(filter plugins/micromega/%, $(PLUGINSVO)) +QUOTEVO:=$(filter plugins/quote/%, $(PLUGINSVO)) +RINGVO:=$(filter plugins/setoid_ring/%, $(PLUGINSVO)) +NSATZVO:=$(filter plugins/nsatz/%, $(PLUGINSVO)) +FOURIERVO:=$(filter plugins/fourier/%, $(PLUGINSVO)) +FUNINDVO:=$(filter plugins/funind/%, $(PLUGINSVO)) +BTAUTOVO:=$(filter plugins/btauto/%, $(PLUGINSVO)) +RTAUTOVO:=$(filter plugins/rtauto/%, $(PLUGINSVO)) +EXTRACTIONVO:=$(filter plugins/extraction/%, $(PLUGINSVO)) +CCVO:= +DERIVEVO:=$(filter plugins/derive/%, $(PLUGINSVO)) + +omega: $(OMEGAVO) $(OMEGACMA) $(ROMEGAVO) $(ROMEGACMA) +micromega: $(MICROMEGAVO) $(MICROMEGACMA) $(CSDPCERT) +setoid_ring: $(RINGVO) $(RINGCMA) +nsatz: $(NSATZVO) $(NSATZCMA) +extraction: $(EXTRACTIONCMA) +fourier: $(FOURIERVO) $(FOURIERCMA) +funind: $(FUNINDCMA) $(FUNINDVO) +cc: $(CCVO) $(CCCMA) +rtauto: $(RTAUTOVO) $(RTAUTOCMA) +btauto: $(BTAUTOVO) $(BTAUTOCMA) + +.PHONY: omega micromega setoid_ring nsatz extraction +.PHONY: fourier funind cc rtauto btauto + +################################# +### Misc other development rules +################################# + +# NOTA : otags only accepts camlp4 as preprocessor, so the following rule +# won't build tags of .ml4 when compiling with camlp5 + +otags: + otags $(MLIFILES) $(filter-out configure.ml, $(MLSTATICFILES)) \ + $(if $(filter camlp5,$(CAMLP4)), , \ + -pa op -pa g -pa m -pa rq $(addprefix -pa , $(CAMLP4DEPS)) \ + $(addprefix -impl , $(ML4FILES))) + +.PHONY: otags + + +# For emacs: +# Local Variables: +# mode: makefile +# End: diff --git a/Makefile.doc b/Makefile.doc index b7251ce57..6c345025a 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -1,3 +1,11 @@ +####################################################################### +# v # The Coq Proof Assistant / The Coq Development Team # +# <O___,, # INRIA-Rocquencourt & LRI-CNRS-Orsay # +# \VV/ ############################################################# +# // # This file is distributed under the terms of the # +# # GNU Lesser General Public License Version 2.1 # +####################################################################### + # Makefile for the Coq documentation # To compile documentation, you need the following tools: @@ -5,6 +13,61 @@ # Pdf: pdflatex # Html: hevea (http://hevea.inria.fr) >= 1.05 +# The main entry point : + +documentation: doc-$(WITHDOC) ## see $(WITHDOC) in config/Makefile +doc-all: doc +doc-no: + +.PHONY: documentation doc-all doc-no + +###################################################################### +### Variables +###################################################################### + +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) + + ###################################################################### ### General rules ###################################################################### @@ -339,6 +402,80 @@ install-doc-index-urls: $(MKDIR) $(FULLDATADIR) $(INSTALLLIB) $(INDEXURLS) $(FULLDATADIR) + +########################################################################### +# Documentation of the source code (using ocamldoc) +########################################################################### + +OCAMLDOCDIR=dev/ocamldoc + +DOCMLIS=$(wildcard ./lib/*.mli ./intf/*.mli ./kernel/*.mli ./library/*.mli \ + ./engine/*.mli ./pretyping/*.mli ./interp/*.mli printing/*.mli \ + ./parsing/*.mli ./proofs/*.mli \ + ./tactics/*.mli ./stm/*.mli ./toplevel/*.mli ./ltac/*.mli) + +# Defining options to generate dependencies graphs +DOT=dot +ODOCDOTOPTS=-dot -dot-reduce + +.PHONY: source-doc mli-doc ml-doc + +source-doc: mli-doc $(OCAMLDOCDIR)/coq.pdf + +$(OCAMLDOCDIR)/coq.tex: $(DOCMLIS:.mli=.cmi) + $(SHOW)'OCAMLDOC -latex -o $@' + $(HIDE)$(OCAMLFIND) ocamldoc -latex -rectypes -I $(MYCAMLP4LIB) $(MLINCLUDES)\ + $(DOCMLIS) -noheader -t "Coq mlis documentation" \ + -intro $(OCAMLDOCDIR)/docintro -o $@.tmp + $(SHOW)'OCAMLDOC utf8 fix' + $(HIDE)$(OCAMLDOCDIR)/fix-ocamldoc-utf8 $@.tmp + $(HIDE)cat $(OCAMLDOCDIR)/header.tex $@.tmp > $@ + rm $@.tmp + +mli-doc: $(DOCMLIS:.mli=.cmi) + $(SHOW)'OCAMLDOC -html' + $(HIDE)$(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads -I $(MYCAMLP4LIB) $(MLINCLUDES) \ + $(DOCMLIS) -d $(OCAMLDOCDIR)/html -colorize-code \ + -t "Coq mlis documentation" -intro $(OCAMLDOCDIR)/docintro \ + -css-style style.css + +ml-dot: $(MLFILES) + $(OCAMLFIND) ocamldoc -dot -dot-reduce -rectypes -I +threads -I $(CAMLLIB) -I $(MYCAMLP4LIB) $(MLINCLUDES) \ + $(filter $(addsuffix /%.ml,$(CORESRCDIRS)),$(MLFILES)) -o $(OCAMLDOCDIR)/coq.dot + +%_dep.png: %.dot + $(DOT) -Tpng $< -o $@ + +%_types.dot: %.mli + $(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -dot-types -o $@ $< + +OCAMLDOC_MLLIBD = $(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ \ + $(foreach lib,$(|:.mllib.d=_MLLIB_DEPENDENCIES),$(addsuffix .ml,$($(lib)))) + +%.dot: | %.mllib.d + $(OCAMLDOC_MLLIBD) + +ml-doc: + $(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads $(MLINCLUDES) $(COQIDEFLAGS) -d $(OCAMLDOCDIR) $(MLSTATICFILES) + +parsing/parsing.dot : | parsing/parsing.mllib.d parsing/highparsing.mllib.d + $(OCAMLDOC_MLLIBD) + +grammar/grammar.dot : | grammar/grammar.mllib.d + $(OCAMLDOC_MLLIBD) + +tactics/tactics.dot: | tactics/tactics.mllib.d ltac/ltac.mllib.d + $(OCAMLDOC_MLLIBD) + +%.dot: %.mli + $(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $< + +$(OCAMLDOCDIR)/%.pdf: $(OCAMLDOCDIR)/%.tex + $(SHOW)'PDFLATEX $*.tex' + $(HIDE)(cd $(OCAMLDOCDIR) ; pdflatex -interaction=batchmode $*.tex && pdflatex -interaction=batchmode $*.tex) + $(HIDE)(cd doc/tools/; show_latex_messages -no-overfull ../../$(OCAMLDOCDIR)/$*.log) + + # For emacs: # Local Variables: # mode: makefile diff --git a/Makefile.ide b/Makefile.ide new file mode 100644 index 000000000..8d6b5de36 --- /dev/null +++ b/Makefile.ide @@ -0,0 +1,254 @@ +####################################################################### +# v # The Coq Proof Assistant / The Coq Development Team # +# <O___,, # INRIA-Rocquencourt & LRI-CNRS-Orsay # +# \VV/ ############################################################# +# // # This file is distributed under the terms of the # +# # GNU Lesser General Public License Version 2.1 # +####################################################################### + +## Makefile rules for building the CoqIDE interface + +## NB: For the moment, the build system of CoqIDE is part of +## the one of Coq. In particular, this Makefile.ide is included in +## Makefile.build. Please ensure that the rules define here are +## indeed specific to files of the form ide/* + +## Coqide-related variables set by ./configure in config/Makefile + +#COQIDEINCLUDES : something like -I +lablgtk2 +#HASCOQIDE : opt / byte / no +#IDEFLAGS : some extra cma, for instance +#IDEOPTCDEPS : on windows, ide/ide_win32_stubs.o ide/coq_icon.o +#IDECDEPS +#IDECDEPSFLAGS +#IDEINT : X11 / QUARTZ / WIN32 + +## CoqIDE Executable + +COQIDEBYTE:=bin/coqide.byte$(EXE) +COQIDE:=bin/coqide$(EXE) +COQIDEAPP:=bin/CoqIDE_$(VERSION).app +COQIDEINAPP:=$(COQIDEAPP)/Contents/MacOS/coqide + +## CoqIDE source directory and files + +# Note : for just building bin/coqide, we could only consider +# config, lib, ide and ide/utils. But the coqidetop plugin (the +# one that will be loaded by coqtop -ideslave) refers to some +# core modules of coq, for instance printing/*. + +IDESRCDIRS:= $(CORESRCDIRS) ide ide/utils + +COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS)) $(COQIDEINCLUDES) + +IDEDEPS:=lib/clib.cma 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 + +IDEFILES=$(wildcard ide/*.lang) ide/coq_style.xml ide/coq.png ide/MacOS/default_accel_map + +## 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) + + +########################################################################### +# CoqIde special targets +########################################################################### + +.PHONY: coqide coqide-binaries coqide-no coqide-byte coqide-opt coqide-files + +# target to build CoqIde +coqide: coqide-files coqide-binaries theories/Init/Prelude.vo + +coqide-binaries: coqide-$(HASCOQIDE) ide-toploop +coqide-no: +coqide-byte: $(COQIDEBYTE) $(COQIDE) +coqide-opt: $(COQIDEBYTE) $(COQIDE) +coqide-files: $(IDEFILES) +ifeq ($(BEST),opt) +ide-toploop: $(IDETOPLOOPCMA) $(IDETOPLOOPCMA:.cma=.cmxs) +else +ide-toploop: $(IDETOPLOOPCMA) +endif + +ifeq ($(HASCOQIDE),opt) +$(COQIDE): $(LINKIDEOPT) + $(SHOW)'OCAMLOPT -o $@' + $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ unix.cmxa threads.cmxa lablgtk.cmxa \ + lablgtksourceview2.cmxa str.cmxa $(IDEFLAGS:.cma=.cmxa) $^ + $(STRIP) $@ +else +$(COQIDE): $(COQIDEBYTE) + cp $< $@ +endif + +$(COQIDEBYTE): $(LINKIDE) + $(SHOW)'OCAMLC -o $@' + $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ unix.cma threads.cma lablgtk.cma \ + lablgtksourceview2.cma str.cma $(IDEFLAGS) $(IDECDEPSFLAGS) $^ + +ide/coqide_main.ml: ide/coqide_main.ml4 config/Makefile # no camlp4deps here + $(SHOW)'CAMLP4O $<' + $(HIDE)$(CAMLP4O) $(CAMLP4FLAGS) $(PR_O) $(CAMLP4USE) -D$(IDEINT) -impl $< -o $@ + + +ide/%.cmi: ide/%.mli + $(SHOW)'OCAMLC $<' + $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -c $< + +ide/%.cmo: ide/%.ml + $(SHOW)'OCAMLC $<' + $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -c $< + +ide/%.cmx: ide/%.ml + $(SHOW)'OCAMLOPT $<' + $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) $(HACKMLI) -c $< + + +#################### +## Install targets +#################### + +.PHONY: install-coqide install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles + +ifeq ($(HASCOQIDE),no) +install-coqide: install-ide-toploop +else +install-coqide: install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles +endif + +install-ide-bin: + $(MKDIR) $(FULLBINDIR) + $(INSTALLBIN) $(COQIDE) $(FULLBINDIR) + +install-ide-toploop: + $(MKDIR) $(FULLCOQLIB)/toploop + $(INSTALLBIN) $(IDETOPLOOPCMA) $(FULLCOQLIB)/toploop/ +ifeq ($(BEST),opt) + $(INSTALLBIN) $(IDETOPLOOPCMA:.cma=.cmxs) $(FULLCOQLIB)/toploop/ +endif + +install-ide-devfiles: + $(MKDIR) $(FULLCOQLIB) + $(INSTALLSH) $(FULLCOQLIB) $(IDECMA) \ + $(foreach lib,$(IDECMA:.cma=_MLLIB_DEPENDENCIES),$(addsuffix .cmi,$($(lib)))) +ifeq ($(BEST),opt) + $(INSTALLSH) $(FULLCOQLIB) $(IDECMA:.cma=.cmxa) $(IDECMA:.cma=.a) +endif + +install-ide-files: #Please update $(COQIDEAPP)/Contents/Resources/ at the same time + $(MKDIR) $(FULLDATADIR) + $(INSTALLLIB) ide/coq.png ide/*.lang ide/coq_style.xml $(FULLDATADIR) + $(MKDIR) $(FULLCONFIGDIR) + if [ $(IDEINT) = QUARTZ ] ; then $(INSTALLLIB) ide/mac_default_accel_map $(FULLCONFIGDIR)/coqide.keys ; fi + +install-ide-info: + $(MKDIR) $(FULLDOCDIR) + $(INSTALLLIB) ide/FAQ $(FULLDOCDIR)/FAQ-CoqIde + +########################################################################### +# CoqIde MacOS special targets +########################################################################### + +.PHONY: $(COQIDEAPP)/Contents + +$(COQIDEAPP)/Contents: + rm -rdf $@ + $(MKDIR) $@ + sed -e "s/VERSION/$(VERSION4MACOS)/g" ide/MacOS/Info.plist.template > $@/Info.plist + $(MKDIR) "$@/MacOS" + +$(COQIDEINAPP): ide/macos_prehook.cmx $(LINKIDEOPT) | $(COQIDEAPP)/Contents + $(SHOW)'OCAMLOPT -o $@' + $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ \ + unix.cmxa lablgtk.cmxa lablgtksourceview2.cmxa str.cmxa \ + threads.cmxa $(IDEFLAGS:.cma=.cmxa) $^ + $(STRIP) $@ + +$(COQIDEAPP)/Contents/Resources/share: $(COQIDEAPP)/Contents + $(MKDIR) $@/coq/ + $(INSTALLLIB) ide/coq.png ide/*.lang ide/coq_style.xml $@/coq/ + $(MKDIR) $@/gtksourceview-2.0/{language-specs,styles} + $(INSTALLLIB) "$(GTKSHARE)/"gtksourceview-2.0/language-specs/{def.lang,language2.rng} $@/gtksourceview-2.0/language-specs/ + $(INSTALLLIB) "$(GTKSHARE)/"gtksourceview-2.0/styles/{styles.rng,classic.xml} $@/gtksourceview-2.0/styles/ + cp -R "$(GTKSHARE)/"locale $@ + cp -R "$(GTKSHARE)/"icons $@ + cp -R "$(GTKSHARE)/"themes $@ + +$(COQIDEAPP)/Contents/Resources/loaders: $(COQIDEAPP)/Contents + $(MKDIR) $@ + $(INSTALLLIB) $$("$(GTKBIN)/gdk-pixbuf-query-loaders" | sed -n -e '5 s!.*= \(.*\)$$!\1!p')/libpixbufloader-png.so $@ + +$(COQIDEAPP)/Contents/Resources/immodules: $(COQIDEAPP)/Contents + $(MKDIR) $@ + $(INSTALLLIB) "$(GTKLIBS)/gtk-2.0/2.10.0/immodules/"*.so $@ + + +$(COQIDEAPP)/Contents/Resources/etc: $(COQIDEAPP)/Contents/Resources/lib + $(MKDIR) $@/xdg/coq + $(INSTALLLIB) ide/MacOS/default_accel_map $@/xdg/coq/coqide.keys + $(MKDIR) $@/gtk-2.0 + { "$(GTKBIN)/gdk-pixbuf-query-loaders" $@/../loaders/*.so |\ + sed -e "s!/.*\(/loaders/.*.so\)!@executable_path/../Resources/\1!"; } \ + > $@/gtk-2.0/gdk-pixbuf.loaders + { "$(GTKBIN)/gtk-query-immodules-2.0" $@/../immodules/*.so |\ + sed -e "s!/.*\(/immodules/.*.so\)!@executable_path/../Resources/\1!" |\ + sed -e "s!/.*\(/share/locale\)!@executable_path/../Resources/\1!"; } \ + > $@/gtk-2.0/gtk-immodules.loaders + $(MKDIR) $@/pango + echo "[Pango]" > $@/pango/pangorc + +$(COQIDEAPP)/Contents/Resources/lib: $(COQIDEAPP)/Contents/Resources/immodules $(COQIDEAPP)/Contents/Resources/loaders $(COQIDEAPP)/Contents $(COQIDEINAPP) + $(MKDIR) $@ + $(INSTALLLIB) $(GTKLIBS)/charset.alias $@/ + $(MKDIR) $@/pango/1.8.0/modules + $(INSTALLLIB) "$(GTKLIBS)/pango/1.8.0/modules/"*.so $@/pango/1.8.0/modules/ + { "$(GTKBIN)/pango-querymodules" $@/pango/1.8.0/modules/*.so |\ + sed -e "s!/.*\(/pango/1.8.0/modules/.*.so\)!@executable_path/../Resources/lib\1!"; } \ + > $@/pango/1.8.0/modules.cache + + for i in $$(otool -L $(COQIDEINAPP) |sed -n -e "\@$(GTKLIBS)@ s/[^/]*\(\/[^ ]*\) .*$$/\1/p"); \ + do cp $$i $@/; \ + ide/MacOS/relatify_with-respect-to_.sh $@/$$(basename $$i) $(GTKLIBS) $@; \ + done + for i in $@/../loaders/*.so $@/../immodules/*.so $@/pango/1.8.0/modules/*.so; \ + do \ + for j in $$(otool -L $$i | sed -n -e "\@$(GTKLIBS)@ s/[^/]*\(\/[^ ]*\) .*$$/\1/p"); \ + do cp $$j $@/; ide/MacOS/relatify_with-respect-to_.sh $@/$$(basename $$j) $(GTKLIBS) $@; done; \ + ide/MacOS/relatify_with-respect-to_.sh $$i $(GTKLIBS) $@; \ + done + EXTRAWORK=1; \ + while [ $${EXTRAWORK} -eq 1 ]; \ + do EXTRAWORK=0; \ + for i in $@/*.dylib; \ + do for j in $$(otool -L $$i | sed -n -e "\@$(GTKLIBS)@ s/[^/]*\(\/[^ ]*\) .*$$/\1/p"); \ + do EXTRAWORK=1; cp $$j $@/; ide/MacOS/relatify_with-respect-to_.sh $@/$$(basename $$j) $(GTKLIBS) $@; done; \ + done; \ + done + ide/MacOS/relatify_with-respect-to_.sh $(COQIDEINAPP) $(GTKLIBS) $@ + +$(COQIDEAPP)/Contents/Resources:$(COQIDEAPP)/Contents/Resources/etc $(COQIDEAPP)/Contents/Resources/share + $(INSTALLLIB) ide/MacOS/*.icns $@ + +$(COQIDEAPP):$(COQIDEAPP)/Contents/Resources + $(CODESIGN) $@ + +########################################################################### +# CoqIde for Windows special targets +########################################################################### + +%.o: %.rc + $(SHOW)'WINDRES $<' + $(HIDE)i686-w64-mingw32-windres -i $< -o $@ + + +# For emacs: +# Local Variables: +# mode: makefile +# End: diff --git a/Makefile.install b/Makefile.install new file mode 100644 index 000000000..ed29bc1e7 --- /dev/null +++ b/Makefile.install @@ -0,0 +1,136 @@ +####################################################################### +# v # The Coq Proof Assistant / The Coq Development Team # +# <O___,, # INRIA-Rocquencourt & LRI-CNRS-Orsay # +# \VV/ ############################################################# +# // # This file is distributed under the terms of the # +# # GNU Lesser General Public License Version 2.1 # +####################################################################### + +# This makefile regroups installation rules +# It is included by Makefile.build + +ifeq ($(LOCAL),true) +install: + @echo "Nothing to install in a local build!" +else +install: install-coq install-coqide install-doc-$(WITHDOC) +endif + +install-doc-all: install-doc +install-doc-no: + +.PHONY: install install-doc-all install-doc-no + +#These variables are intended to be set by the caller to make +#COQINSTALLPREFIX= +#OLDROOT= + + # Can be changed for a local installation (to make packages). + # You must NOT put a "/" at the end (Cygnus for win32 does not like "//"). + +ifdef COQINSTALLPREFIX +FULLBINDIR=$(BINDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) +FULLCOQLIB=$(COQLIBINSTALL:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) +FULLCONFIGDIR=$(CONFIGDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) +FULLDATADIR=$(DATADIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) +FULLMANDIR=$(MANDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) +FULLEMACSLIB=$(EMACSLIB:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) +FULLCOQDOCDIR=$(COQDOCDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) +FULLDOCDIR=$(DOCDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) +else +FULLBINDIR=$(BINDIR) +FULLCOQLIB=$(COQLIBINSTALL) +FULLCONFIGDIR=$(CONFIGDIR) +FULLDATADIR=$(DATADIR) +FULLMANDIR=$(MANDIR) +FULLEMACSLIB=$(EMACSLIB) +FULLCOQDOCDIR=$(COQDOCDIR) +FULLDOCDIR=$(DOCDIR) +endif + +.PHONY: install-coq install-binaries install-byte install-opt +.PHONY: install-tools install-library install-devfiles +.PHONY: install-coq-info install-coq-manpages install-emacs install-latex + +install-coq: install-binaries install-library install-coq-info install-devfiles + +install-binaries: install-tools + $(MKDIR) $(FULLBINDIR) + $(INSTALLBIN) $(COQC) $(COQTOPBYTE) $(COQTOPEXE) $(CHICKEN) $(FULLBINDIR) + $(MKDIR) $(FULLCOQLIB)/toploop + $(INSTALLBIN) $(TOPLOOPCMA) $(FULLCOQLIB)/toploop/ +ifeq ($(BEST),opt) + $(INSTALLBIN) $(TOPLOOPCMA:.cma=.cmxs) $(FULLCOQLIB)/toploop/ +endif + + +install-tools: + $(MKDIR) $(FULLBINDIR) + # recopie des fichiers de style pour coqide + $(MKDIR) $(FULLCOQLIB)/tools/coqdoc + touch $(FULLCOQLIB)/tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc/coqdoc.css # to have the mode according to umask (bug #1715) + $(INSTALLLIB) tools/coqdoc/coqdoc.css tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc + $(INSTALLBIN) $(TOOLS) $(FULLBINDIR) + +# The list of .cmi to install, including the ones obtained +# from .mli without .ml, and the ones obtained from .ml without .mli + +INSTALLCMI = $(sort \ + $(filter-out checker/% ide/% tools/%, $(MLIFILES:.mli=.cmi)) \ + $(foreach lib,$(CORECMA) $(PLUGINSCMA), $(addsuffix .cmi,$($(lib:.cma=_MLLIB_DEPENDENCIES))))) + +install-devfiles: + $(MKDIR) $(FULLBINDIR) + $(INSTALLBIN) $(COQMKTOP) $(FULLBINDIR) + $(MKDIR) $(FULLCOQLIB) + $(INSTALLSH) $(FULLCOQLIB) $(LINKCMO) $(GRAMMARCMA) + $(INSTALLSH) $(FULLCOQLIB) $(INSTALLCMI) +ifeq ($(BEST),opt) + $(INSTALLSH) $(FULLCOQLIB) $(LINKCMX) $(CORECMA:.cma=.a) $(STATICPLUGINS:.cma=.a) +endif + +install-library: + $(MKDIR) $(FULLCOQLIB) + $(INSTALLSH) $(FULLCOQLIB) $(LIBFILES) $(PLUGINS) + $(MKDIR) $(FULLCOQLIB)/user-contrib +ifndef CUSTOM + $(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB) +endif +ifeq ($(BEST),opt) + $(INSTALLLIB) $(LIBCOQRUN) $(FULLCOQLIB) + $(INSTALLSH) $(FULLCOQLIB) $(PLUGINSOPT) +endif +# csdpcert is not meant to be directly called by the user; we install +# it with libraries + -$(MKDIR) $(FULLCOQLIB)/plugins/micromega + $(INSTALLBIN) $(CSDPCERT) $(FULLCOQLIB)/plugins/micromega + rm -f $(FULLCOQLIB)/revision + -$(INSTALLLIB) revision $(FULLCOQLIB) + +install-coq-info: install-coq-manpages install-emacs install-latex + +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 + +install-coq-manpages: + $(MKDIR) $(FULLMANDIR)/man1 + $(INSTALLLIB) $(MANPAGES) $(FULLMANDIR)/man1 + +install-emacs: + $(MKDIR) $(FULLEMACSLIB) + $(INSTALLLIB) tools/gallina-db.el tools/coq-font-lock.el tools/gallina-syntax.el tools/gallina.el tools/coq-inferior.el $(FULLEMACSLIB) + +# command to update TeX' kpathsea database +#UPDATETEX = $(MKTEXLSR) /usr/share/texmf /var/spool/texmf $(BASETEXDIR) > /dev/null + +install-latex: + $(MKDIR) $(FULLCOQDOCDIR) + $(INSTALLLIB) tools/coqdoc/coqdoc.sty $(FULLCOQDOCDIR) +# -$(UPDATETEX) + +# For emacs: +# Local Variables: +# mode: makefile +# End: |