diff options
| -rw-r--r-- | CHANGES | 4 | ||||
| -rw-r--r-- | Makefile | 6 | ||||
| -rw-r--r-- | Makefile.doc | 31 |
3 files changed, 37 insertions, 4 deletions
@@ -23,7 +23,7 @@ Tactics - New tactics constr_eq, is_evar and has_evar. - Remove the two-argument variant of "decide equality". - New experimental tactical "timeout <n> <tac>". Since <n> is a time - in second for the moment, this feature should rather be avoided + in second for the moment, this feature should rather be avoided in scripts meant to be machine-independent. Vernacular commands @@ -85,6 +85,8 @@ Internal infrastructure for both make and ocamlbuild, etc. - Support of cross-compilation via mingw toward Windows, contact P. Letouzey for more informations. +- new Makefile rules mli-doc to make html of mli in dev/doc/html and + full-stdlib to get a HUGE pdf with all the stdlib. Extraction @@ -182,9 +182,9 @@ docclean: doc/*/*.hatoc doc/*/*.haux doc/*/*.hcomind doc/*/*.herrind doc/*/*.hidx doc/*/*.hind \ doc/*/*.htacind doc/*/*.htoc doc/*/*.v.html rm -f doc/stdlib/index-list.html doc/stdlib/index-body.html \ - doc/stdlib/Library.coqdoc.tex doc/stdlib/library.files \ - doc/stdlib/library.files.ls - rm -f doc/*/*.ps doc/*/*.pdf + doc/stdlib/*Library.coqdoc.tex doc/stdlib/library.files \ + doc/stdlib/library.files.ls doc/stdlib/FullLibrary.tex + rm -f doc/*/*.ps doc/*/*.pdf rm -rf doc/refman/html doc/stdlib/html doc/faq/html doc/tutorial/tutorial.v.html rm -f doc/refman/euclid.ml doc/refman/euclid.mli rm -f doc/refman/heapsort.ml doc/refman/heapsort.mli 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 ###################################################################### |