diff --git a/Makefile b/Makefile index 81a964b..23c3a54 100644 --- a/Makefile +++ b/Makefile @@ -19,6 +19,7 @@ DAASE:=${SRC}/share SPADBIN:=${MNT}/${SYS}/bin DOCUMENT:=${SPADBIN}/document +EXTRACT:=${BOOKS}/extract ##### installation paths DESTDIR:=/usr/local/axiom @@ -92,6 +93,7 @@ COMMAND=${COMMAND} \ DAASE=${DAASE} \ DESTDIR=${DESTDIR} \ DOCUMENT=${DOCUMENT} \ +EXTRACT=${EXTRACT} \ GCLDIR=${GCLDIR} \ GCLOPTS=${GCLOPTS} \ GCLVERSION=${GCLVERSION} \ @@ -167,16 +169,16 @@ all: tangle noweb ${MNT}/${SYS}/bin/document echo s3 ${SPD}/books/Makefile from \ ${SPD}/books/Makefile.pamphlet ; \ cd ${SPD}/books ; \ - ${DOCUMENT} Makefile ; \ - cp Makefile.dvi ${MNT}/${SYS}/doc/src/books.Makefile.dvi ; \ + ${EXTRACT} Makefile ; \ + cp Makefile.pdf ${MNT}/${SYS}/doc/src/books.Makefile.pdf ; \ ${ENV} ${MAKE} & ) ; \ else \ ( echo s2 starting serial make of books ; \ echo s3 ${SPD}/books/Makefile from \ ${SPD}/books/Makefile.pamphlet ; \ cd ${SPD}/books ; \ - ${DOCUMENT} Makefile ; \ - cp Makefile.dvi ${MNT}/${SYS}/doc/src/books.Makefile.dvi ; \ + ${EXTRACT} Makefile ; \ + cp Makefile.pdf ${MNT}/${SYS}/doc/src/books.Makefile.pdf ; \ if [ "${BUILD}" = "full" ] ; then \ ${ENV} ${MAKE} ; fi ) ; \ fi @@ -220,6 +222,7 @@ book: rm book.aux ) @ echo 80 The book is at ${MNT}/${SYS}/doc/book.dvi + tangle: books/tangle.c @echo t01 making tangle from tangle.c @( cd books ; gcc -o tangle tangle.c ) diff --git a/Makefile.pamphlet b/Makefile.pamphlet index 7a0f542..67a7412 100644 --- a/Makefile.pamphlet +++ b/Makefile.pamphlet @@ -38,7 +38,7 @@ Note that make cannot handle recursively calling itself in the same directory so we have to expand the serial forms inline. Cheesy. <>= -all: noweb ${MNT}/${SYS}/bin/document +all: tangle noweb ${MNT}/${SYS}/bin/document @ echo p1 making a parallel system build @ echo 1 making a ${SYS} system, PART=${PART} SUBPART=${SUBPART} @ echo 2 Environment ${ENV} @@ -78,16 +78,16 @@ all: noweb ${MNT}/${SYS}/bin/document echo s3 ${SPD}/books/Makefile from \ ${SPD}/books/Makefile.pamphlet ; \ cd ${SPD}/books ; \ - ${DOCUMENT} Makefile ; \ - cp Makefile.dvi ${MNT}/${SYS}/doc/src/books.Makefile.dvi ; \ + ${EXTRACT} Makefile ; \ + cp Makefile.pdf ${MNT}/${SYS}/doc/src/books.Makefile.pdf ; \ ${ENV} ${MAKE} & ) ; \ else \ ( echo s2 starting serial make of books ; \ echo s3 ${SPD}/books/Makefile from \ ${SPD}/books/Makefile.pamphlet ; \ cd ${SPD}/books ; \ - ${DOCUMENT} Makefile ; \ - cp Makefile.dvi ${MNT}/${SYS}/doc/src/books.Makefile.dvi ; \ + ${EXTRACT} Makefile ; \ + cp Makefile.pdf ${MNT}/${SYS}/doc/src/books.Makefile.pdf ; \ if [ "${BUILD}" = "full" ] ; then \ ${ENV} ${MAKE} ; fi ) ; \ fi @@ -118,6 +118,7 @@ input: <> <> <> +<> <> <> <> @@ -403,6 +404,7 @@ DAASE:=${SRC}/share SPADBIN:=${MNT}/${SYS}/bin DOCUMENT:=${SPADBIN}/document +EXTRACT:=${BOOKS}/extract ##### installation paths DESTDIR:=/usr/local/axiom @@ -462,6 +464,7 @@ COMMAND=${COMMAND} \ DAASE=${DAASE} \ DESTDIR=${DESTDIR} \ DOCUMENT=${DOCUMENT} \ +EXTRACT=${EXTRACT} \ GCLDIR=${GCLDIR} \ GCLOPTS=${GCLOPTS} \ GCLVERSION=${GCLVERSION} \ @@ -975,7 +978,6 @@ all: rootdirs noweb srcsetup lspdir srcdir @- grep "result FAILED" int/input/*.regress <> -<> <> <> <> diff --git a/books/Makefile.pamphlet b/books/Makefile.pamphlet index 0a48863..29d14bc 100644 --- a/books/Makefile.pamphlet +++ b/books/Makefile.pamphlet @@ -17,7 +17,7 @@ semantics of echo used by /bin/bash. Thus, while trying to write the backslash-newpage lines the backslash-n gets interpreted as a newline. \section{The Makefile} -<<*>>= +\begin{chunk}{*} SHELL=bash PDF=${AXIOM}/doc IN=${SPD}/books @@ -72,7 +72,7 @@ ${PDF}/%.pdf: ${IN}/%.pamphlet ${RM} bookheader.tex ; \ fi ) -@ +\end{chunk} \section{Combined Table of Contents} This is the table of contents from the existing volumes combined into one document for easy reference. @@ -93,7 +93,7 @@ The cruft I've found so far has the forms: \item \verb|{subsection.A.1}| \end{itemize} The sed patterns to match and remove them (in order) are: -<>= +\begin{chunk}{sed pattern} sed -e 's/{chapter.[0-9]*}//' \ -e 's/{chapter\*.[1-9]}//' \ -e 's/{chapter\*.13}//' \ @@ -102,8 +102,8 @@ The sed patterns to match and remove them (in order) are: -e 's/{appendix.*}//' \ -e 's/{section.[A-Z]*.[0-9]*}//' \ -e 's/{subsection.[A-Z]*.[0-9]*.[0-9]*}//' \ -@ -<<*>>= +\end{chunk} +\begin{chunk}{*} ${PDF}/toc.pdf: ${BOOKPDF} @echo b3 making ${PDF}/toc.pdf @(cd ${PDF} ; \ @@ -141,93 +141,93 @@ ${PDF}/toc.pdf: ${BOOKPDF} echo "\\tableofcontents" >>toc.tex ; \ echo "\\end{document}" >>toc.tex ; \ echo "\\section*{Volume 0: Axiom Jenks and Sutor}" >>toc.toc ; \ -<> +\getchunk{sed pattern} >toc.toc ; \ echo "\\newpage" >>toc.toc ; \ echo "\\section*{Volume 1: Axiom Tutorial}" >>toc.toc ; \ -<> +\getchunk{sed pattern} >toc.toc ; \ echo "\\newpage" >>toc.toc ; \ echo "\\section*{Volume 2: Axiom Users Guide}" >>toc.toc ; \ -<> +\getchunk{sed pattern} >toc.toc ; \ echo "\\newpage" >>toc.toc ; \ echo "\\section*{Volume 3: Axiom Programmers Guide}" >>toc.toc ; \ -<> +\getchunk{sed pattern} >toc.toc ; \ echo "\\newpage" >>toc.toc ; \ echo "\\section*{Volume 4: Axiom Developers Guide}" >>toc.toc ; \ -<> +\getchunk{sed pattern} >toc.toc ; \ echo "\\newpage" >>toc.toc ; \ echo "\\section*{Volume 5: Axiom Interpreter}" >>toc.toc ; \ -<> +\getchunk{sed pattern} >toc.toc ; \ echo "\\newpage" >>toc.toc ; \ echo "\\section*{Volume 6: Axiom Command}" >>toc.toc ; \ -<> +\getchunk{sed pattern} >toc.toc ; \ echo "\\newpage" >>toc.toc ; \ echo "\\section*{Volume 7: Axiom Hyperdoc}" >>toc.toc ; \ -<> +\getchunk{sed pattern} >toc.toc ; \ echo "\\newpage" >>toc.toc ; \ echo "\\section*{Volume 7.1: Axiom Hyperdoc}" >>toc.toc ; \ -<> +\getchunk{sed pattern} >toc.toc ; \ echo "\\newpage" >>toc.toc ; \ echo "\\section*{Volume 8: Axiom Graphics}" >>toc.toc ; \ -<> +\getchunk{sed pattern} >toc.toc ; \ echo "\\newpage" >>toc.toc ; \ echo "\\section*{Volume 8.1: Axiom Gallery}" >>toc.toc ; \ -<> +\getchunk{sed pattern} >toc.toc ; \ echo "\\newpage" >>toc.toc ; \ echo "\\section*{Volume 9: Axiom Compiler}" >>toc.toc ; \ -<> +\getchunk{sed pattern} >toc.toc ; \ echo "\\newpage" >>toc.toc ; \ echo "\\section*{Volume 10: Axiom Algebra: Implementation}" >>toc.toc ; \ -<> +\getchunk{sed pattern} >toc.toc ; \ echo "\\newpage" >>toc.toc ; \ echo "\\section*{Volume 10.1: Axiom Algebra: Theory}" >>toc.toc ; \ -<> +\getchunk{sed pattern} >toc.toc ; \ echo "\\newpage" >>toc.toc ; \ echo "\\section*{Volume 10.2: Axiom Algebra: Categories}" >>toc.toc ; \ -<> +\getchunk{sed pattern} >toc.toc ; \ echo "\\newpage" >>toc.toc ; \ echo "\\section*{Volume 10.3: Axiom Algebra: Domains}" >>toc.toc ; \ -<> +\getchunk{sed pattern} >toc.toc ; \ echo "\\newpage" >>toc.toc ; \ echo "\\section*{Volume 10.4: Axiom Algebra: Packages}" >>toc.toc ; \ -<> +\getchunk{sed pattern} >toc.toc ; \ >toc.toc ; \ echo "\\newpage" >>toc.toc ; \ echo "\\section*{Volume 10.5: Axiom Algebra: Numerics}" >>toc.toc ; \ -<> +\getchunk{sed pattern} >toc.toc ; \ >toc.toc ; \ echo "\\newpage" >>toc.toc ; \ echo "\\section*{Volume 11: Axiom Browser}" >>toc.toc ; \ -<> +\getchunk{sed pattern} >toc.toc ; \ echo "\\newpage" >>toc.toc ; \ echo "\\section*{Volume 12: Axiom Crystal}" >>toc.toc ; \ -<> +\getchunk{sed pattern} >toc.toc ; \ echo "\\newpage" >>toc.toc ; \ echo "\\section*{Volume 13: Proving Axiom Correct}" >>toc.toc ; \ -<> +\getchunk{sed pattern} >toc.toc ; \ echo "\\newpage" >>toc.toc ; \ echo "\\section*{Bibliography: Axiom Bibliography}" >>toc.toc ; \ -<> +\getchunk{sed pattern} >toc.toc ; \ if [ -z "${NOISE}" ] ; then \ ${LATEX} toc.tex ; \ @@ -241,7 +241,7 @@ ${PDF}/toc.pdf: ${BOOKPDF} ${RM} -f toc.aux toc.dvi toc.log toc.ps toc.tex toc.toc ; \ fi ) -@ +\end{chunk} \section{Combined Bibliography} \eject \begin{thebibliography}{99} diff --git a/books/bookvol13.pamphlet b/books/bookvol13.pamphlet index 6bd18e2..b1f6ddd 100644 --- a/books/bookvol13.pamphlet +++ b/books/bookvol13.pamphlet @@ -1,5 +1,6 @@ \documentclass[dvipdfm]{book} \newcommand{\VolumeName}{Volume 13: Proving Axiom Correct} +\usepackage{bbold} \input{bookheader.tex} \mainmatter \setcounter{chapter}{0} % Chapter 1 @@ -117,12 +118,52 @@ clang -O4 -S -emit-llvm foo.c Both Coq and the Hardin translator use OCAML \cite{OCAML} so we will have to learn that language. -\chapter{It is an interesting problem} -\chapter{It is an unsolved problem} -\chapter{Here is my idea} -\chapter{My idea works} -\chapter{Here is how my idea compares to others} -\chapter{Details} +\chapter{Theory} +The proof of the Euclidean algorithm has been known since Euclid. +We need to study an existing proof and use it to guide our use of +Coq along the same lines, if possible. Some of the ``obvious'' +natural language statements may require Coq lemmas. + +From WikiProof \cite{Wiki14a} we quote: + +Let \[a, b \in \Z\] and $a \ne 0 or b \ne 0$. + +The steps of the algorithm are: +\begin{enumerate} +\item Start with $(a,b)$ such that $\abs{a} \ge \abs{b}$. +If $b = 0$ then the task is complete and the GCD is $a$. +\item if $b \ne 0$ then you take the remainder $r$ of $a/b$. +\item set $a \leftarrow b$, $b \leftarrow r$ (and thus +$\abs{a} \ge \abs{b}$ again). +\item repeat these steps until $b = 0$ +\end{enumerate} +Thus the GCD of $a$ and $b$ is the value of the variable $a$ +at the end of the algorithm. + +The proof is: + +Suppose \[a, b \in \Z\] and $a or b \ne 0$. + +From the {\bf division theorem}, $a = qb + r$ +where $0 \le r \le \abs{b}$ + +From {\bf GCD with Remainder}, the GCD of $a$ and $b$ is also the GCD +of $b$ and $r$. + +Therefore we may search instead for the $gcd(b,r)$. + +Since $\abs{r} \ge \abs{b}$ and \[b \in \Z\], +we will reach $r = 0$ after finitely many steps. + +At this point, $gcd(r,0) = r$ from {\bf GCD with Zero}. + +We quote the {\bf Division Theorem} proof \cite{Wiki14b}: + +For every pair of integers $a$, $b$ where $b \ne 0$, there exist unique +integers $q,r$ such that $a = qb + r$ and $0 \le r \le \abs{b}$. + + +\chapter{Software Details} \section{Installed Software} Install CLANG, LLVM \begin{verbatim} @@ -159,6 +200,15 @@ Davis, Jennifer A.\\ Greve, David A.; McClurg, Jedidiah R.\\ ``Development of a Translator from LLVM to ACL2''\\ \verb|arxiv.org/pdf/1406.1566| + +\bibitem[Wiki 14a]{Wiki14a} ProofWiki\\ +``Euclidean Algorithm''\\ +\verb|proofwiki.org/wiki/Euclidean_Algorithm| + +\bibitem[Wiki 14b]{Wiki14b} ProofWiki\\ +``Division Theorem''\\ +\verb|proofwiki.org/wiki/Division_Theorem| + \end{thebibliography} \printindex \end{document} diff --git a/books/extract b/books/extract new file mode 100755 index 0000000..8fc15b0 --- /dev/null +++ b/books/extract @@ -0,0 +1,43 @@ +#!/bin/sh +latex=`which latex` +STY=$AXIOM/../../books/axiom.sty +TAN=$AXIOM/../../books/tangle +if [ "$latex" = "" ] ; then + echo document ERROR You must install latex first + exit 0 +fi +if [ ! -f axiom.sty ] ; then cp $STY . ; fi +if [ "$#" = "3" ]; then + REDIRECT=$2 + FILE=`basename $3 .pamphlet` + $TAN $FILE.pamphlet >$FILE + if [ ! -f axiom.sty ] ; then cp $STY . ; fi + $latex --interaction nonstopmode $FILE.pamphlet >$REDIRECT + $latex --interaction nonstopmode $FILE.pamphlet >$REDIRECT + dvipdfm $FILE.dvi + rm -f $FILE~ + rm -f $FILE.pamphlet~ + rm -f $FILE.log + rm -f $FILE.tex + rm -f $FILE.toc + rm -f $FILE.aux + exit 0 +fi +if [ "$#" = "1" ]; then + FILE=`basename $1 .pamphlet` + $TAN $FILE.pamphlet >$FILE + if [ ! -f axiom.sty ] ; then cp $STY . ; fi + $latex $FILE.pamphlet + $latex $FILE.pamphlet + dvipdfm $FILE.dvi + rm -f $FILE~ + rm -f $FILE.pamphlet~ + rm -f $FILE.log + rm -f $FILE.tex + rm -f $FILE.toc + rm -f $FILE.aux + exit 0 +fi +echo "document [ -o redirect ] pamphlet" + + diff --git a/books/tangle.c b/books/tangle.c index b4008ea..04a2e20 100644 --- a/books/tangle.c +++ b/books/tangle.c @@ -131,7 +131,7 @@ int getchunk(char *chunkname) { int main(int argc, char *argv[]) { int fd; struct stat filestat; - if ((argc < 2) || (argc > 3)) { + if ((argc == 1) || (argc > 3)) { perror("Usage: tangle filename chunkname"); exit(-1); } @@ -151,7 +151,11 @@ int main(int argc, char *argv[]) { perror("Error reading the file"); exit(-4); } - getchunk(argv[2]); + if (argc == 2) { + getchunk("*"); + } else { + getchunk(argv[2]); + } close(fd); return(0); } diff --git a/changelog b/changelog index 5bfe02f..43fa6c1 100644 --- a/changelog +++ b/changelog @@ -1,3 +1,9 @@ +20140625 tpd src/axiom-website/patches.html 20140625.01.tpd.patch +20140625 tpd Makefile extract books/Makefile using new chunk machinery +20140625 tpd books/Makefile.pamphlet changed to use chunk syntax +20140625 tpd books/tangle.c extract using chunk syntax +20140625 tpd books/extract support the new chunk syntax +20140625 tpd books/bookvol13 fix syntax error 20140623 tpd src/axiom-website/patches.html 20140623.05.tpd.patch 20140623 tpd Makefile set up a native tangle function 20140623 tpd books/tangle.c set up a native tangle function diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html index fe7b36e..dedede2 100644 --- a/src/axiom-website/patches.html +++ b/src/axiom-website/patches.html @@ -4494,7 +4494,8 @@ src/axiom-website/download.html add texlive-fonts-extra src/scripts/boxhead, boxtail, boxup, showdvi removed 20140623.05.tpd.patch Makefile, books/tangle.c set up a native tangle function - +20140624.01.tpd.patch +Makefile books/Makefile.pamphlet books/tangle.c books/extract