diff options
Diffstat (limited to 'doc/stdlib')
-rwxr-xr-x | doc/stdlib/Library.tex | 11 | ||||
-rw-r--r-- | doc/stdlib/index-list.html.template | 275 | ||||
-rw-r--r-- | doc/stdlib/index-trailer.html | 2 | ||||
-rwxr-xr-x | doc/stdlib/make-library-files | 36 | ||||
-rwxr-xr-x | doc/stdlib/make-library-index | 32 |
5 files changed, 352 insertions, 4 deletions
diff --git a/doc/stdlib/Library.tex b/doc/stdlib/Library.tex index 58b2dc6df..9fae7495b 100755 --- a/doc/stdlib/Library.tex +++ b/doc/stdlib/Library.tex @@ -3,15 +3,18 @@ \usepackage[latin1]{inputenc} \usepackage[T1]{fontenc} \usepackage{fullpage} -\usepackage[noweb]{coqweb} +\usepackage{coqdoc} -\input{./title} -\input{./macros} +\input{../common/version} +\input{../common/title} +\input{../common/macros} \begin{document} \coverpage{The standard library}% {\ } +{This material is distributed under the terms of the GNU Lesser +General Public License Version 2.1.} \tableofcontents @@ -53,7 +56,7 @@ is also a version of this document in HTML format on the WWW, which you can access from the \Coq\ home page at \texttt{http://coq.inria.fr/library}. -\input{library.coqweb.tex} +\input{library.coqdoc} \end{document} diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template new file mode 100644 index 000000000..fbed33ccf --- /dev/null +++ b/doc/stdlib/index-list.html.template @@ -0,0 +1,275 @@ +<html> + +<head> +<link rel="stylesheet" href="style.css" type="text/css"> +<title>The Coq Standard Library +</head> + +<body> + +<H1>The Coq Standard Library</H1> + +Here is a short description of the Coq standard library, which is +distributed with the system. +It provides a set of modules directly available +through the <tt>Require Import</tt> command. +<p> +The standard library is composed of the following subdirectories: + +<p> + +<dl> + <dt> <b>Init</b>: + The core library (automatically loaded when starting Coq) + <dd> +theories/Init/Notations.v +theories/Init/Datatypes.v +theories/Init/Logic.v +theories/Init/Logic_Type.v +theories/Init/Peano.v +theories/Init/Specif.v +theories/Init/Wf.v +(theories/Init/Prelude.v) + + <dt> <b>Logic</b>: + Classical logic and dependent equality + <dd> +theories/Logic/Classical_Pred_Set.v +theories/Logic/Classical_Pred_Type.v +theories/Logic/Classical_Prop.v +theories/Logic/Classical_Type.v +(theories/Logic/Classical.v) +theories/Logic/Decidable.v +theories/Logic/Eqdep_dec.v +theories/Logic/Eqdep.v +theories/Logic/JMeq.v +theories/Logic/RelationalChoice.v +theories/Logic/ClassicalChoice.v +theories/Logic/ChoiceFacts.v +theories/Logic/ClassicalDescription.v +theories/Logic/ClassicalFacts.v +theories/Logic/Berardi.v +theories/Logic/Diaconescu.v +theories/Logic/Hurkens.v +theories/Logic/ProofIrrelevance.v + + <dt> <b>Arith</b>: + Basic Peano arithmetic + <dd> +theories/Arith/Le.v +theories/Arith/Lt.v +theories/Arith/Plus.v +theories/Arith/Minus.v +theories/Arith/Mult.v +theories/Arith/Gt.v +theories/Arith/Between.v +theories/Arith/Peano_dec.v +theories/Arith/Compare_dec.v +(theories/Arith/Arith.v) +theories/Arith/Min.v +theories/Arith/Max.v +theories/Arith/Compare.v +theories/Arith/Div2.v +theories/Arith/Div.v +theories/Arith/EqNat.v +theories/Arith/Euclid.v +theories/Arith/Even.v +theories/Arith/Bool_nat.v +theories/Arith/Factorial.v +theories/Arith/Wf_nat.v + + <dt> <b>NArith</b>: + Binary positive integers + <dd> + +theories/NArith/BinPos.v +theories/NArith/BinNat.v +(theories/NArith/NArith.v) +theories/NArith/Pnat.v + + <dt> <b>ZArith</b>: + Binary integers + <dd> +theories/ZArith/BinInt.v +theories/ZArith/Zorder.v +theories/ZArith/Zcompare.v +theories/ZArith/Znat.v +theories/ZArith/Zmin.v +theories/ZArith/Zabs.v +theories/ZArith/Zeven.v +theories/ZArith/auxiliary.v +theories/ZArith/ZArith_dec.v +theories/ZArith/Zbool.v +theories/ZArith/Zmisc.v +theories/ZArith/Wf_Z.v +theories/ZArith/Zhints.v +(theories/ZArith/ZArith_base.v) +theories/ZArith/Zcomplements.v +theories/ZArith/Zsqrt.v +theories/ZArith/Zpower.v +theories/ZArith/Zdiv.v +theories/ZArith/Zlogarithm.v +(theories/ZArith/ZArith.v) +theories/ZArith/Zwf.v +theories/ZArith/Zbinary.v +theories/ZArith/Znumtheory.v + + <dt> <b>Reals</b>: + Formalization of real numbers + <dd> +theories/Reals/Rdefinitions.v +theories/Reals/Raxioms.v +theories/Reals/RIneq.v +theories/Reals/DiscrR.v +(theories/Reals/Rbase.v) +theories/Reals/RList.v +theories/Reals/Ranalysis.v +theories/Reals/Rbasic_fun.v +theories/Reals/Rderiv.v +theories/Reals/Rfunctions.v +theories/Reals/Rgeom.v +theories/Reals/R_Ifp.v +theories/Reals/Rlimit.v +theories/Reals/Rseries.v +theories/Reals/Rsigma.v +theories/Reals/R_sqr.v +theories/Reals/Rtrigo_fun.v +theories/Reals/Rtrigo.v +theories/Reals/SplitAbsolu.v +theories/Reals/SplitRmult.v +theories/Reals/Alembert.v +theories/Reals/AltSeries.v +theories/Reals/ArithProp.v +theories/Reals/Binomial.v +theories/Reals/Cauchy_prod.v +theories/Reals/Cos_plus.v +theories/Reals/Cos_rel.v +theories/Reals/Exp_prop.v +theories/Reals/Integration.v +theories/Reals/MVT.v +theories/Reals/NewtonInt.v +theories/Reals/PSeries_reg.v +theories/Reals/PartSum.v +theories/Reals/R_sqrt.v +theories/Reals/Ranalysis1.v +theories/Reals/Ranalysis2.v +theories/Reals/Ranalysis3.v +theories/Reals/Ranalysis4.v +theories/Reals/Rcomplete.v +theories/Reals/RiemannInt.v +theories/Reals/RiemannInt_SF.v +theories/Reals/Rpower.v +theories/Reals/Rprod.v +theories/Reals/Rsqrt_def.v +theories/Reals/Rtopology.v +theories/Reals/Rtrigo_alt.v +theories/Reals/Rtrigo_calc.v +theories/Reals/Rtrigo_def.v +theories/Reals/Rtrigo_reg.v +theories/Reals/SeqProp.v +theories/Reals/SeqSeries.v +theories/Reals/Sqrt_reg.v +(theories/Reals/Reals.v) + + <dt> <b>Bool</b>: + Booleans (basic functions and results) + <dd> +theories/Bool/Bool.v +theories/Bool/BoolEq.v +theories/Bool/DecBool.v +theories/Bool/IfProp.v +theories/Bool/Sumbool.v +theories/Bool/Zerob.v +theories/Bool/Bvector.v + + <dt> <b>Lists</b>: + Polymorphic lists, Streams (infinite sequences) + <dd> +theories/Lists/List.v +theories/Lists/ListSet.v +theories/Lists/TheoryList.v +theories/Lists/Streams.v +theories/Lists/MonoList.v + + <dt> <b>Sets</b>: + Sets (classical, constructive, finite, infinite, powerset, + etc.) + <dd> +theories/Sets/Classical_sets.v +theories/Sets/Constructive_sets.v +theories/Sets/Cpo.v +theories/Sets/Ensembles.v +theories/Sets/Finite_sets_facts.v +theories/Sets/Finite_sets.v +theories/Sets/Image.v +theories/Sets/Infinite_sets.v +theories/Sets/Integers.v +theories/Sets/Multiset.v +theories/Sets/Partial_Order.v +theories/Sets/Permut.v +theories/Sets/Powerset_Classical_facts.v +theories/Sets/Powerset_facts.v +theories/Sets/Powerset.v +theories/Sets/Relations_1_facts.v +theories/Sets/Relations_1.v +theories/Sets/Relations_2_facts.v +theories/Sets/Relations_2.v +theories/Sets/Relations_3_facts.v +theories/Sets/Relations_3.v +theories/Sets/Uniset.v + + <dt> <b>Relations</b>: + Relations (definitions and basic results) + <dd> +theories/Relations/Relation_Definitions.v +theories/Relations/Relation_Operators.v +theories/Relations/Relations.v +theories/Relations/Operators_Properties.v +theories/Relations/Rstar.v +theories/Relations/Newman.v + + <dt> <b>Wellfounded</b>: + Well-founded Relations + <dd> +theories/Wellfounded/Disjoint_Union.v +theories/Wellfounded/Inclusion.v +theories/Wellfounded/Inverse_Image.v +theories/Wellfounded/Lexicographic_Exponentiation.v +theories/Wellfounded/Lexicographic_Product.v +theories/Wellfounded/Transitive_Closure.v +theories/Wellfounded/Union.v +theories/Wellfounded/Wellfounded.v +theories/Wellfounded/Well_Ordering.v + + <dt> <b>Sorting</b>: + Axiomatizations of sorts + <dd> +theories/Sorting/Heap.v +theories/Sorting/Permutation.v +theories/Sorting/Sorting.v + + <dt> <b>Setoids</b>: + <dd> +theories/Setoids/Setoid.v + + <dt> <b>IntMap</b>: + Finite sets/maps as trees indexed by addresses + <dd> +theories/IntMap/Addr.v +theories/IntMap/Adist.v +theories/IntMap/Addec.v +theories/IntMap/Adalloc.v +theories/IntMap/Map.v +theories/IntMap/Fset.v +theories/IntMap/Mapaxioms.v +theories/IntMap/Mapiter.v +theories/IntMap/Mapcanon.v +theories/IntMap/Mapsubset.v +theories/IntMap/Lsort.v +theories/IntMap/Mapfold.v +theories/IntMap/Mapcard.v +theories/IntMap/Mapc.v +theories/IntMap/Maplists.v +(theories/IntMap/Allmaps.v) + +</dl> diff --git a/doc/stdlib/index-trailer.html b/doc/stdlib/index-trailer.html new file mode 100644 index 000000000..308b1d01b --- /dev/null +++ b/doc/stdlib/index-trailer.html @@ -0,0 +1,2 @@ +</body> +</html> diff --git a/doc/stdlib/make-library-files b/doc/stdlib/make-library-files new file mode 100755 index 000000000..91e3cc3f4 --- /dev/null +++ b/doc/stdlib/make-library-files @@ -0,0 +1,36 @@ +#!/bin/sh + +# Needs COQTOP and GALLINA set + +# On garde la liste de tous les *.v avec dates dans library.files.ls +# Si elle a change depuis la derniere fois ou library.files n'existe pas +# on fabrique des .g (si besoin) et la liste library.files dans +# l'ordre de ls -tr des *.vo +# Ce dernier trie les fichiers dans l'ordre inverse de leur date de création +# En supposant que make fait son boulot, ca fait un tri topologique du +# graphe des dépendances + +LIBDIRS="Arith NArith ZArith Reals Logic Bool Lists IntMap Relations Sets Sorting Wellfounded Setoids" + +rm -f library.files.ls.tmp +(cd $COQTOP/theories; find $LIBDIR -name "*.v" -ls) > library.files.ls.tmp +if ! test -e library.files || ! cmp library.files.ls library.files.ls.tmp; then + mv -f library.files.ls.tmp library.files.ls + rm -f library.files; touch library.files + ABSOLUTE=`pwd`/library.files + cd $COQTOP/theories + echo $LIBDIRS + for rep in $LIBDIRS ; do + (cd $rep + echo $rep/intro.tex >> $ABSOLUTE + VOFILES=`ls -tr *.vo` + for file in $VOFILES ; do + VF=`basename $file \.vo` + if [ \( ! -e $VF.g \) -o \( $VF.v -nt $VF.g \) ] ; then + $GALLINA $VF.v + fi + echo $rep/$VF.g >> $ABSOLUTE + done + ) + done +fi diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index new file mode 100755 index 000000000..1da642df3 --- /dev/null +++ b/doc/stdlib/make-library-index @@ -0,0 +1,32 @@ +#!/bin/sh + +# Instantiate links to library files in index template + +FILE=$1 + +cp -f $FILE.template tmp +echo -n Building file index-list.prehtml ... +for i in $COQTOP/theories/*; do + d=`basename $i` + if [ "$d" != "Num" -a "$d" != "CVS" ]; then + for j in $i/*.v; do + b=`basename $j .v` + rm -f tmp2 + grep -q theories/$d/$b.v tmp + a=$? + if [ $a = 0 ]; then + sed -e "s/theories\/$d\/$b.v/<a href=\"Coq.$d.$b.html\">$b<\/a>/g" tmp > tmp2 + mv -f tmp2 tmp + else + echo Warning: theories/$d/$b.v is missing in the template file + fi + done + fi + rm -f tmp2 + sed -e "s/#$d#//" tmp > tmp2 + mv -f tmp2 tmp +done +a=`grep theories tmp` +if [ $? = 0 ]; then echo Warning: extra files:; echo $a; fi +mv tmp $FILE +echo Done |