diff options
| -rw-r--r-- | Makefile.build | 6 | ||||
| -rw-r--r-- | Makefile.common | 2 | ||||
| -rw-r--r-- | Makefile.doc | 18 |
3 files changed, 16 insertions, 10 deletions
diff --git a/Makefile.build b/Makefile.build index a90eb0eb99..74845263c9 100644 --- a/Makefile.build +++ b/Makefile.build @@ -637,12 +637,12 @@ install-binaries:: install-$(BEST) install-tools install-byte:: $(MKDIR) $(FULLBINDIR) - $(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(FULLBINDIR) + $(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(CSDPCERT) $(FULLBINDIR) cd $(FULLBINDIR); ln -sf coqtop.byte$(EXE) coqtop$(EXE) install-opt:: $(MKDIR) $(FULLBINDIR) - $(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(COQTOPOPT) $(FULLBINDIR) + $(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(COQTOPOPT) $(CSDPCERT) $(FULLBINDIR) cd $(FULLBINDIR); ln -sf coqtop.opt$(EXE) coqtop$(EXE) install-tools:: @@ -866,7 +866,7 @@ endif %.ml: %.mll $(SHOW)'OCAMLLEX $<' - $(HIDE)$(OCAMLLEX) "$*.mll" -o $@ + $(HIDE)$(OCAMLLEX) -o $@ "$*.mll" %.ml %.mli: %.mly $(SHOW)'OCAMLYACC $<' diff --git a/Makefile.common b/Makefile.common index 915f383e0c..b58032077e 100644 --- a/Makefile.common +++ b/Makefile.common @@ -877,7 +877,7 @@ VO_TARGETS:=logic arith bool narith zarith qarith lists strings sets \ setoids sorting natural integer rational numbers noreal \ omega micromega ring setoid_ring dp xml extraction field fourier jprover \ funind cc programs subtac rtauto -DOC_TARGETS:=doc doc-html doc-ps doc-pdf stdlib refman tutorial faq rectutorial +DOC_TARGETS:=doc doc-html doc-ps doc-pdf stdlib refman tutorial faq rectutorial refman-quick refman-nodep stdlib-nodep STAGE3_TARGETS:=world install coqide coqide-files coq coqlib \ coqlight states pcoq-files check init theories theories-light contrib \ $(DOC_TARGETS) $(VO_TARGETS) diff --git a/Makefile.doc b/Makefile.doc index 55d5d77ce7..241ba8bc47 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -27,13 +27,19 @@ doc-ps:\ doc/tutorial/Tutorial.v.ps doc/refman/Reference-Manual.ps \ doc/faq/FAQ.v.ps doc/stdlib/Library.ps doc/RecTutorial/RecTutorial.v.ps -refman:\ +refman: coq + $(MAKE) -f Makefile.stage3 refman-nodep + +refman-nodep:\ doc/refman/html/index.html doc/refman/Reference-Manual.ps doc/refman/Reference-Manual.pdf tutorial:\ doc/tutorial/Tutorial.v.html doc/tutorial/Tutorial.v.ps doc/tutorial/Tutorial.v.pdf -stdlib:\ +stdlib: $(THEORIESVO) $(COQDOC) + $(MAKE) -f Makefile.stage3 stdlib-nodep + +stdlib-nodep:\ doc/stdlib/html/index.html doc/stdlib/Library.ps doc/stdlib/Library.pdf faq:\ @@ -47,7 +53,7 @@ rectutorial:\ ### Implicit rules ###################################################################### -%.v.tex: %.tex coq +%.v.tex: %.tex (cd `dirname $<`; $(COQSRC)/$(COQTEX) $(COQTEXOPTS) `basename $<`) %.ps: %.dvi @@ -103,7 +109,7 @@ doc/refman/html/index.html: doc/refman/Reference-Manual.html $(REFMANPNGFILES) \ $(INSTALLLIB) doc/refman/cover.html doc/refman/menu.html doc/refman/html $(INSTALLLIB) doc/refman/index.html doc/refman/html -doc/refman-quick: +refman-quick: (cd doc/refman; \ $(PDFLATEX) Reference-Manual.tex; \ $(HEVEA) $(HEVEAOPTS) ./Reference-Manual.tex) @@ -152,7 +158,7 @@ doc/faq/html/index.html: doc/faq/FAQ.v.html ### Standard library (browsable html format) -doc/stdlib/index-body.html: $(THEORIESVO:.vo=.glob) $(COQDOC) +doc/stdlib/index-body.html: - rm -rf doc/stdlib/html $(MKDIR) doc/stdlib/html $(COQDOC) -q -d doc/stdlib/html --multi-index --html \ @@ -169,7 +175,7 @@ doc/stdlib/html/index.html: doc/stdlib/index-list.html doc/stdlib/index-body.htm ### Standard library (light version, full version is definitely too big) -doc/stdlib/Library.coqdoc.tex: $(THEORIESLIGHTVO:.vo=.glob) $(COQDOC) +doc/stdlib/Library.coqdoc.tex: $(COQSRC)/$(COQDOC) -q --gallina --body-only --latex --stdout \ -R theories Coq $(THEORIESLIGHTVO:.vo=.v) >> $@ |