diff options
| author |  pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-08 16:26:04 +0000 |
|---|---|---|
| committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-08 16:26:04 +0000 |
| commit | e618ce61c4ecbdcd046256e2eaad25919fa35de1 (patch) | |
| tree | b6e9d04f04479a47ecf5ff86acb3a2f49d5098e3 /Makefile.doc | |
| parent | e0aea9a731c81e9bdae6e7c41b0d9fab9fae4d6c (diff) | |
Add "make full-stdlib" to make all the doc in pdf as ask by bug 2395
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13976 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.doc')
| -rw-r--r-- | Makefile.doc | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/Makefile.doc b/Makefile.doc index 584e25394..dc3ae8b5f 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -36,6 +36,9 @@ tutorial: \ stdlib: \ doc/stdlib/html/index.html doc/stdlib/Library.ps doc/stdlib/Library.pdf +full-stdlib: \ + doc/stdlib/html/index.html doc/stdlib/FullLibrary.ps doc/stdlib/FullLibrary.pdf + faq: doc/faq/html/index.html doc/faq/FAQ.v.ps doc/faq/FAQ.v.pdf rectutorial: doc/RecTutorial/RecTutorial.html \ @@ -229,6 +232,34 @@ doc/stdlib/Library.pdf: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Li $(PDFLATEX) -interaction=batchmode Library;\ ../tools/show_latex_messages -no-overfull Library.log) +### Standard library (full version if you're crazy enouth to try) + +doc/stdlib/FullLibrary.tex: doc/stdlib/Library.tex + sed -e 's/Library.coqdoc/FullLibrary.coqdoc/g;s/\\begin{document}/\\newcommand{\\textlambda}{\\ensuremath{\\lambda}}\\newcommand{\\textPi}{\\ensuremath{\\Pi}}\\begin{document}/' $< > $@ + +ifdef QUICK +doc/stdlib/FullLibrary.coqdoc.tex: + $(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \ + -R theories Coq $(THEORIESVO:.vo=.v) > $@ + sed -i "" -e 's///g' $@ +else +doc/stdlib/FullLibrary.coqdoc.tex: $(COQDOC) $(THEORIESVO) + $(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \ + -R theories Coq $(THEORIESVO:.vo=.v) > $@ + sed -i "" -e 's///g' $@ +endif + +doc/stdlib/FullLibrary.dvi: $(DOCCOMMON) doc/stdlib/FullLibrary.coqdoc.tex doc/stdlib/FullLibrary.tex + (cd doc/stdlib;\ + $(LATEX) -interaction=batchmode FullLibrary;\ + $(LATEX) -interaction=batchmode FullLibrary > /dev/null;\ + ../tools/show_latex_messages -no-overfull FullLibrary.log) + +doc/stdlib/FullLibrary.pdf: $(DOCCOMMON) doc/stdlib/FullLibrary.coqdoc.tex doc/stdlib/FullLibrary.dvi + (cd doc/stdlib;\ + $(PDFLATEX) -interaction=batchmode FullLibrary;\ + ../tools/show_latex_messages -no-overfull FullLibrary.log) + ###################################################################### # Tutorial on inductive types ###################################################################### |