diff options
-rw-r--r-- | Makefile.build | 36 | ||||
-rw-r--r-- | Makefile.common | 5 | ||||
-rw-r--r-- | Makefile.doc | 32 | ||||
-rw-r--r-- | test-suite/Makefile | 3 |
4 files changed, 52 insertions, 24 deletions
diff --git a/Makefile.build b/Makefile.build index 925e537f5..857cb3914 100644 --- a/Makefile.build +++ b/Makefile.build @@ -187,6 +187,8 @@ kernel/copcodes.ml: kernel/byterun/coq_instruct.h # Main targets (coqmktop, coqtop.opt, coqtop.byte) ########################################################################### +.PHONY: coqbinaries coq coqlib coqlight states + coqbinaries:: ${COQBINARIES} ${CSDPCERT} ${FAKEIDE} coq: coqlib tools coqbinaries @@ -197,14 +199,14 @@ coqlight: theories-light tools coqbinaries states:: states/initial.coq -$(COQTOPOPT): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) +$(COQTOPOPT): $(BESTCOQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) -o $@ + $(HIDE)$(BESTCOQMKTOP) -boot -opt $(OPTFLAGS) -o $@ $(STRIP) $@ -$(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) +$(COQTOPBYTE): $(BESTCOQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(COQMKTOP) -boot -top $(BYTEFLAGS) -o $@ + $(HIDE)$(BESTCOQMKTOP) -boot -top $(BYTEFLAGS) -o $@ $(COQTOPEXE): $(ORDER_ONLY_SEP) $(BESTCOQTOP) cd bin; ln -sf coqtop.$(BEST)$(EXE) coqtop$(EXE) @@ -292,6 +294,8 @@ plugins/micromega/csdpcert$(EXE): $(CSDPCERTCMO:.cmo=$(BESTOBJ)) # CoqIde special targets ########################################################################### +.PHONY: coqide coqide-binaries coqide-no coqide-byte coqide-opt coqide-files + # target to build CoqIde coqide:: coqide-files coqide-binaries states @@ -323,6 +327,9 @@ $(COQIDE): # install targets +.PHONY: install-coqide install-ide-no install-ide-byte install-ide-opt +.PHONY: install-ide-files install-ide-info install-im + FULLIDELIB=$(FULLCOQLIB)/ide install-coqide:: install-ide-$(HASCOQIDE) install-ide-files install-ide-info @@ -364,13 +371,14 @@ install-im: # tests ########################################################################### +.PHONY: validate check test-suite $(ALLSTDLIB).v + VALIDOPTS=-silent -o -m validate:: $(BESTCHICKEN) $(ALLVO) $(SHOW)'COQCHK <theories & plugins>' $(HIDE)$(BESTCHICKEN) -boot $(VALIDOPTS) $(ALLMODS) -.PHONY: $(ALLSTDLIB).v $(ALLSTDLIB).v: $(SHOW)'MAKE $(notdir $@)' $(HIDE)echo "Require $(ALLMODS)." > $@ @@ -388,6 +396,9 @@ test-suite: world $(ALLSTDLIB).v # partial targets: 1) core ML parts ################################################################## +.PHONY: lib kernel byterun library proofs tactics interp parsing pretyping +.PHONY: highparsing toplevel hightactics + lib: lib/lib.cma kernel: kernel/kernel.cma byterun: $(BYTERUN) @@ -405,6 +416,10 @@ hightactics: tactics/hightactics.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 + init: $(INITVO) theories: $(THEORIESVO) @@ -434,6 +449,9 @@ noreal: logic arith bool zarith qarith lists sets fsets relations \ # 3) plugins ########################################################################### +.PHONY: plugins omega micromega ring setoid_ring nsatz dp xml extraction +.PHONY: field fourier funind cc subtac rtauto pluginsopt + plugins: $(PLUGINSVO) omega: $(OMEGAVO) $(OMEGACMA) $(ROMEGAVO) $(ROMEGACMA) micromega: $(MICROMEGAVO) $(MICROMEGACMA) $(CSDPCERT) @@ -472,6 +490,8 @@ theories/Numbers/Natural/BigN/NMake_gen.v: theories/Numbers/Natural/BigN/NMake_g # tools ########################################################################### +.PHONY: printers tools + printers: $(DEBUGPRINTERS) tools:: $(TOOLS) $(DEBUGPRINTERS) $(COQDEPBOOT) @@ -511,7 +531,7 @@ $(COQDOC): $(COQDOCCMO:.cmo=$(BESTOBJ)) # fake_ide : for debugging or test-suite purpose, a fake ide simulating # a connection to coqtop -ideslave -$(FAKEIDE): toplevel/ide_intf.mli toplevel/ide_intf.ml tools/fake_ide.ml +$(FAKEIDE): toplevel/ide_intf$(BESTOBJ) tools/fake_ide$(BESTOBJ) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml,,unix) @@ -556,6 +576,10 @@ FULLCOQDOCDIR=$(COQDOCDIR) FULLDOCDIR=$(DOCDIR) endif +.PHONY: install-coq install-coqlight install-binaries install-byte install-opt +.PHONY: install-tools install-library install-library-light +.PHONY: install-coq-info install-coq-manpages install-emacs install-latex + install-coq: install-binaries install-library install-coq-info install-coqlight: install-binaries install-library-light diff --git a/Makefile.common b/Makefile.common index cd8f2063b..b7ff5da4f 100644 --- a/Makefile.common +++ b/Makefile.common @@ -16,18 +16,22 @@ COQMKTOPBYTE:=bin/coqmktop.byte$(EXE) COQMKTOPOPT:=bin/coqmktop.opt$(EXE) BESTCOQMKTOP:=bin/coqmktop.$(BEST)$(EXE) COQMKTOP:=bin/coqmktop$(EXE) + COQCBYTE:=bin/coqc.byte$(EXE) COQCOPT:=bin/coqc.opt$(EXE) BESTCOQC:=bin/coqc.$(BEST)$(EXE) COQC:=bin/coqc$(EXE) + COQTOPBYTE:=bin/coqtop.byte$(EXE) COQTOPOPT:=bin/coqtop.opt$(EXE) BESTCOQTOP:=bin/coqtop.$(BEST)$(EXE) COQTOPEXE:=bin/coqtop$(EXE) + CHICKENBYTE:=bin/coqchk.byte$(EXE) CHICKENOPT:=bin/coqchk.opt$(EXE) BESTCHICKEN:=bin/coqchk.$(BEST)$(EXE) CHICKEN:=bin/coqchk$(EXE) + FAKEIDE:=bin/fake_ide$(EXE) ifeq ($(CAMLP4),camlp4) @@ -66,7 +70,6 @@ BESTOBJ:=$(if $(OPT),.cmx,.cmo) COQBINARIES:= $(COQMKTOP) $(COQC) \ $(COQTOPBYTE) $(if $(OPT),$(COQTOPOPT)) $(COQTOPEXE) \ $(CHICKENBYTE) $(if $(OPT),$(CHICKENOPT)) $(CHICKEN) -OTHERBINARIES:=$(COQMKTOPBYTE) $(COQCBYTE) CSDPCERT:=plugins/micromega/csdpcert$(EXE) diff --git a/Makefile.doc b/Makefile.doc index dc3ae8b5f..42f9bf7aa 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -11,9 +11,12 @@ ### General rules ###################################################################### -.PHONY: doc doc-html doc-pdf doc-ps refman tutorial stdlib faq rectutorial +.PHONY: doc doc-html doc-pdf doc-ps refman refman-quick tutorial +.PHONY: stdlib full-stdlib faq rectutorial -doc: refman faq tutorial rectutorial stdlib ide/index_urls.txt +INDEXURLS:=doc/refman/html/index_url.txt + +doc: refman faq tutorial rectutorial stdlib $(INDEXURLS) doc-html:\ doc/tutorial/Tutorial.v.html doc/refman/html/index.html \ @@ -120,8 +123,11 @@ doc/refman/cover.html: doc/common/styles/html/$(HTMLSTYLE)/cover.html doc/refman/styles.hva: doc/common/styles/html/$(HTMLSTYLE)/styles.hva $(INSTALLLIB) $< doc/refman -doc/refman/html/index.html: doc/refman/Reference-Manual.html $(REFMANPNGFILES) \ - doc/refman/cover.html doc/refman/styles.hva doc/refman/index.html +INDEXES:= doc/refman/html/command-index.html doc/refman/html/tactic-index.html +ALLINDEXES:= doc/refman/html/index.html $(INDEXES) + +$(ALLINDEXES): doc/refman/Reference-Manual.html $(REFMANPNGFILES) \ + doc/refman/cover.html doc/refman/styles.hva doc/refman/index.html - rm -rf doc/refman/html $(MKDIR) doc/refman/html $(INSTALLLIB) $(REFMANPNGFILES) doc/refman/html @@ -136,6 +142,14 @@ refman-quick: $(HEVEA) $(HEVEAOPTS) ./Reference-Manual.tex) ###################################################################### +# Index file for CoqIDE +###################################################################### + +doc/refman/html/index_url.txt: $(INDEXES) + cat $< | grep li-indexenv | grep HREF | sed -e 's@.*<TT>\(.*\)</TT>.*, <A HREF="\(.*\)">.*@\1,\2@' > $@ + + +###################################################################### # Tutorial ###################################################################### @@ -281,16 +295,6 @@ doc/RecTutorial/RecTutorial.html: doc/RecTutorial/RecTutorial.tex (cd doc/RecTutorial; $(HEVEA) $(HEVEAOPTS) RecTutorial) ###################################################################### -# Index file for CoqIDE -###################################################################### - -# Not robust, improve... -ide/index_urls.txt: doc/refman/html/index.html - @ rm -f doc/refman/html/index_urls.txt - cat doc/refman/html/command-index.html doc/refman/html/tactic-index.html | grep li-indexenv | grep HREF | sed -e 's@.*<TT>\(.*\)</TT>.*, <A HREF="\(.*\)">.*@\1,\2@' > doc/refman/html/index_urls.txt - - -###################################################################### # Install all documentation files ###################################################################### diff --git a/test-suite/Makefile b/test-suite/Makefile index e628614ab..828a710b1 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -97,9 +97,6 @@ clean: -name '*.stamp' -o -name '*.vo' -o -name '*.log' \ \) -print0 | xargs -0 rm -f -distclean: clean - $(HIDE)find . -name '*.log' -print0 | xargs -0 rm -f - ####################################################################### # Per-subsystem targets ####################################################################### |