diff --git a/books/bookvol10.3.pamphlet b/books/bookvol10.3.pamphlet
index ad36c9b..e2f0b11 100644
--- a/books/bookvol10.3.pamphlet
+++ b/books/bookvol10.3.pamphlet
@@ -97011,16 +97011,17 @@ What is the purpose of the HACKPI domain?
HACKPI is a hack provided for the benefit of the axiom interpreter.
As a mathematical type, it is the simple transcendental extension
-Q(\pi) of the rational numbers. This type allows interactive users
-to use the name '%pi' without a type both where a numerical value is expected
-[ as in draw(sin x,x=-%pi..%pi) ] or when the exact symbolic value is meant.
-The interpreter defaults a typeless %pi to HACKPI and then uses the various
-conversions to cast it further as required by the context.
-
-One could argue that it is unfair to single %pi out from other constants,
-but it occurs frequently enough in school examples (specially for graphs)
-so it was worth a special hack. In a non-interactive environment (library),
-HACKPI would not exist.
+\verb|Q(\pi)| of the rational numbers. This type allows interactive
+users to use the name \verb|'%pi'| without a type both where a numerical
+value is expected [ as in \verb|draw(sin x,x=-%pi..%pi)| ] or when the
+exact symbolic value is meant. The interpreter defaults a typeless
+\verb|%pi| to HACKPI and then uses the various conversions to cast it
+further as required by the context.
+
+One could argue that it is unfair to single \verb|%pi| out from other
+constants, but it occurs frequently enough in school examples
+(specially for graphs) so it was worth a special hack. In a
+non-interactive environment (library), HACKPI would not exist.
(Manuel Bronstein)
diff --git a/books/bookvol13.pamphlet b/books/bookvol13.pamphlet
index 2c49dad..3c49d1e 100644
--- a/books/bookvol13.pamphlet
+++ b/books/bookvol13.pamphlet
@@ -92,7 +92,29 @@ formally proven ``bridge'' to primitive-recursive versions of those
functions operating on lists.
\end{quote}
-Coq expresses programs using OCAML \cite{OCAML} so we will have to
+{\center{\includegraphics{ps/LLVMtoACL2.eps}}}
+
+Hardin \cite{Hard13} describes the toolchain thus:
+\begin{quote}
+Our translation toolchain architecture is shown in Figure 1. The left
+side of tthe figure depicts a typical compiler frontend producing LLVM
+intermediate code. LLVM output can be produced either as a binary
+``bitcode'' (.bc) file, or as text (.ll file). We chose to parse the
+text form, producing an abstract syntax tree (AST) representation of
+the LLVM program. Our translator then converts the AST to ACL2
+source. The ACL2 source file can then be admitted into an ACL2
+session, along with conjectures that one wishes to prove about the
+code, which ACL2 processes mostly automatically. In addition to
+proving theorems about the translated LLVM code, ACL2 can also be used
+to execute test vectors at reasonable speed.
+\end{quote}
+
+Note that you can see the intermediate form from clang with
+\begin{verbatim}
+clang -O4 -S -emit-llvm foo.c
+\end{verbatim}
+
+Both Coq and the Hardin translator use OCAML \cite{OCAML} so we will have to
learn that language.
\chapter{It is an interesting problem}
@@ -102,9 +124,13 @@ learn that language.
\chapter{Here is how my idea compares to others}
\chapter{Details}
\section{Installed Software}
+Install CLANG, LLVM
+\begin{verbatim}
+http://llvm.org/releases/download.html
+\end{verbatim}
Install OCAML
\begin{verbatim}
-sudo apt-get install ocaml-camlp4-devel ocaml-ocamldoc ocaml-findlib-devel ocaml-extlib-devel ocaml-calendar-devel ocaml
+sudo apt-get install ocaml
\end{verbatim}
\begin{thebibliography}{99}
\section{Coq Spad proofs}
diff --git a/books/bookvol4.pamphlet b/books/bookvol4.pamphlet
index 8f8a5bc..b2e53ed 100644
--- a/books/bookvol4.pamphlet
+++ b/books/bookvol4.pamphlet
@@ -335,16 +335,17 @@ November 10, 2003 ((iHy))
HACKPI is a hack provided for the benefit of the axiom interpreter.
As a mathematical type, it is the simple transcendental extension
-Q(\pi) of the rational numbers. This type allows interactive users
-to use the name '%pi' without a type both where a numerical value is expected
-[ as in draw(sin x,x=-%pi..%pi) ] or when the exact symbolic value is meant.
-The interpreter defaults a typeless %pi to HACKPI and then uses the various
-conversions to cast it further as required by the context.
-
-One could argue that it is unfair to single %pi out from other constants,
-but it occurs frequently enough in school examples (specially for graphs)
-so it was worth a special hack. In a non-interactive environment (library),
-HACKPI would not exist.
+\verb|Q(\pi)| of the rational numbers. This type allows interactive
+users to use the name \verb|'%pi'| without a type both where a numerical
+value is expected [ as in \verb|draw(sin x,x=-%pi..%pi)| ] or when the
+exact symbolic value is meant. The interpreter defaults a typeless
+\verb|%pi| to HACKPI and then uses the various conversions to cast it
+further as required by the context.
+
+One could argue that it is unfair to single \verb|%pi| out from other
+constants, but it occurs frequently enough in school examples
+(specially for graphs) so it was worth a special hack. In a
+non-interactive environment (library), HACKPI would not exist.
(Manuel Bronstein)
@@ -427,8 +428,8 @@ ZIPS=/research/test/zips
\section{The runtime structure of Axiom}
\begin{center}
-\includegraphics{architecture.eps}\\
-{\bf Runtime Structure}
+\includegraphics{ps/architecture.eps}\\
+{\bf Runtime Structure \cite{Ba14}}
\end{center}
\subsection{The build step}
@@ -6677,10 +6678,10 @@ The explanation for the steps follow. The steps are:
\end{enumerate}
\section{Makefile}
-This book is actually a literate program\cite{2} and can contain
+This book is actually a literate program\cite{Kn92} and can contain
executable source code. In particular, the Makefile for this book
is part of the source of the book and is included below. Axiom
-uses the ``noweb'' literate programming system by Norman Ramsey\cite{6}.
+uses the ``noweb'' literate programming system by Norman Ramsey\cite{Ra03}.
\begin{chunk}{*}
PROJECT=bookvol4
TANGLE=/usr/local/bin/NOTANGLE
@@ -6697,25 +6698,20 @@ all:
\end{chunk}
\eject
\begin{thebibliography}{99}
-\bibitem{1} Jenks, R.J. and Sutor, R.S.
-``Axiom -- The Scientific Computation System''
-Springer-Verlag New York (1992)
-ISBN 0-387-97855-0
-\bibitem{2} Knuth, Donald E., ``Literate Programming''
+
+\bibitem[Baker 14]{Ba14} Baker, Martin\\
+``Axiom Architecture''\\
+\verb|www.euclideanspace.com/prog/scratchpad/internals/ccode|
+
+\bibitem[Knuth 92]{Kn92} Knuth, Donald E.\\
+``Literate Programming''\\
Center for the Study of Language and Information
-ISBN 0-937073-81-4
-Stanford CA (1992)
-\bibitem{3} Daly, Timothy, ``The Axiom Wiki Website''\\
-{\bf http://axiom.axiom-developer.org}
-\bibitem{4} Watt, Stephen, ``Aldor'',\\
-{\bf http://www.aldor.org}
-\bibitem{5} Lamport, Leslie, ``Latex -- A Document Preparation System'',
-Addison-Wesley, New York ISBN 0-201-52983-1
-\bibitem{6} Ramsey, Norman ``Noweb -- A Simple, Extensible Tool for
-Literate Programming''\\
-{\bf http://www.eecs.harvard.edu/ $\tilde{}$nr/noweb}
-\bibitem{7} Daly, Timothy, ``The Axiom Literate Documentation''\\
-{\bf http://axiom.axiom-developer.org/axiom-website/documentation.html}
+ISBN 0-937073-81-4 Stanford CA (1992)
+
+\bibitem[Ramsey 03]{Ra03} Ramsey, Norman\\
+``Noweb--A Simple, Extensible Tool for Literate Programming''\\
+\verb|www.eecs.harvard.edu/~nr/noweb|
+
\end{thebibliography}
\printindex
\end{document}
diff --git a/books/dvipdfm.def b/books/dvipdfm.def
index 5acbbb9..e554f00 100644
--- a/books/dvipdfm.def
+++ b/books/dvipdfm.def
@@ -1,21 +1,25 @@
%%
%% This is file `dvipdfm.def',
-%% Copyright (C) 1994 David Carlisle Sebastian Rahtz
-%% Copyright (C) 1995 1996 1997 1998 1999 David Carlisle
-%% Copyright (C) 1989 1999 Mark Wicks
+%% and was *not* generated with the docstrip utility.
%%
+%% It was hand edited from several docstripped def
+%% files that are distributed with the Graphics Bundle
%%
-%% This file is part of the Standard LaTeX `Graphics Bundle'.
-%% It may be distributed under the terms of the LaTeX Project Public
-%% License, as described in lppl.txt in the base LaTeX distribution.
-%% Either version 1.0 or, at your option, any later version.
+%% A modified version of this file may be distributed, but it should
+%% be distributed with a *different* name. Changed files must be
+%% distributed *together with a complete and unchanged* distribution
+%% of these files.
+%%
+%% In compliance with the above statement, the unmodified graphics
+%% bundle is available from the same site you obtained this
+%% modified file. However, it is contained in a separate
+%% tar file to conserve bandwidth. You can get the
+%% unmodified Graphics Bundle at
%%
-%% In addition to the copy in the standard latex graphics distribution,
-%% the master copy of this file is available at the following URL
%% http://odo.kettering.edu/dvipdfm/
%%
\ProvidesFile{dvipdfm.def}
- [1998/11/24 vx.x Driver-dependant file]
+ [1999/9/6 vx.x Driver-dependant file]
\def\c@lor@arg#1{%
\dimen@#1\p@
\ifdim\dimen@<\z@\dimen@\maxdimen\fi
@@ -24,7 +28,7 @@
\fi}
\def\color@gray#1#2{%
\c@lor@arg{#2}%
- \edef#1{bg #2}%
+ \edef#1{gray #2}%
}
\def\color@cmyk#1#2{\c@lor@@cmyk#2\@@#1}
\def\c@lor@@cmyk#1,#2,#3,#4\@@#5{%
@@ -32,14 +36,14 @@
\c@lor@arg{#1}%
\c@lor@arg{#2}%
\c@lor@arg{#3}%
- \edef#5{ [ #1 #2 #3 #4 ] }%
+ \edef#5{cmyk #1 #2 #3 #4}%
}
\def\color@rgb#1#2{\c@lor@@rgb#2\@@#1}
\def\c@lor@@rgb#1,#2,#3\@@#4{%
\c@lor@arg{#1}%
\c@lor@arg{#2}%
\c@lor@arg{#3}%
- \edef#4{[ #1 #2 #3 ]}%
+ \edef#4{rgb #1 #2 #3}%
}
\def\color@RGB#1#2{\c@lor@@RGB#2\@@#1}
\def\c@lor@@RGB#1,#2,#3\@@#4{%
@@ -66,39 +70,62 @@
{\edef#4{ #1}}%
}
% \def\c@lor@to@ps#1 #2\@@{\csname c@lor@ps@#1\endcsname#2 \@@}
-% \def\c@lor@ps@#1 #2\@@{TeXDict begin #1 end}
+% \def\c@lor@ps@#1 #2\@@{TeXDict beginclude@ #1 end}
% \def\c@lor@ps@rgb#1\@@{#1 setrgbcolor}
% \def\c@lor@ps@hsb#1\@@{#1 sethsbcolor}
% \def\c@lor@ps@cmyk#1\@@{#1 setcmykcolor}
% \def\c@lor@ps@gray#1\@@{#1 setgray}
-\def\current@color{0}
+\def\current@color{gray 0}
\def\set@color{%
- \special{pdf: bc \current@color}\aftergroup\reset@color}
-\def\reset@color{\special{pdf:ec}}
-\def\set@page@color{\special{%
- pdf: bgc \current@color}}
+ \special{color push \current@color}\aftergroup\reset@color}
+\def\reset@color{\special{color pop}}
+\def\set@page@color{\special{background \current@color}}
\def\define@color@named#1#2{%
\expandafter\let\csname col@#1\endcsname\@nnil}
\def\Ginclude@bmp#1{%
+\message{<#1>}%
\special{pdf: image width \the\Gin@req@width\space height
\the\Gin@req@height\space depth \the\z@ (#1)}}
-\def\Ginclude@pdf#1{%
- \special{pdf: epdf width \the\Gin@req@width\space height
-\the\Gin@req@height\space depth \the\z@ (#1)}}
+\def\Ginclude@eps#1{%
+ \message{<#1>}%
+ \bgroup
+ \def\@tempa{!}%
+ \dimen@\Gin@req@width
+ \dimen@ii.1bp%
+ \divide\dimen@\dimen@ii
+ \@tempdima\Gin@req@height
+ \divide\@tempdima\dimen@ii
+ \special{PSfile="#1"\space
+ llx=\Gin@llx\space
+ lly=\Gin@lly\space
+ urx=\Gin@urx\space
+ ury=\Gin@ury\space
+ \ifx\Gin@scalex\@tempa\else rwi=\number\dimen@\space\fi
+ \ifx\Gin@scaley\@tempa\else rhi=\number\@tempdima\space\fi
+ \ifGin@clip clip\fi}%
+ \egroup}
\def\Grot@start{%
-\special{pdf: bt rotate \Grot@angle\space }}
-\def\Grot@end{\special{pdf: et}}
-\def\Gscale@start{\special{pdf: bt xscale \Gscale@x\space yscale \Gscale@y}}
-\def\Gscale@end{\special{pdf: et}}
+\special{ps: gsave currentpoint currentpoint translate
+\Grot@angle\space neg rotate neg exch neg exch translate}}
+\def\Grot@end{\special{ps: currentpoint grestore moveto}}
+\def\Gscale@start{\special{ps: gsave currentpoint currentpoint translate
+\Gscale@x\space\Gscale@y\space scale neg exch neg exch translate}}
+% \def\Gscale@start{\special{ps: currentpoint currentpoint translate
+% \Gscale@x\space\Gscale@y\space scale neg exch neg exch translate}}
+\def\Gscale@end{\special{ps: currentpoint grestore moveto}}
+% \def\Gscale@end{\special{ps: currentpoint currentpoint translate
+% 1 \Gscale@x\space div 1 \Gscale@x\space div scale neg exch neg exch translate}}
% \def\Gin@PS@raw#1{\special{ps: #1}}
% \def\Gin@PS@restored#1{\special{" #1}}
% \def\Gin@PS@literal@header#1{\AtBeginDvi{\special{! #1}}}
% \def\Gin@PS@file@header#1{\AtBeginDvi{\special{header=#1}}}
-\def\Gin@extensions{.jpg,.jpeg,.pdf}
+\def\Gin@extensions{.jpg,.jpeg,.pdf,.png}
\@namedef{Gin@rule@.jpg}#1{{bmp}{.bb}{#1}}
\@namedef{Gin@rule@.jpeg}#1{{bmp}{.bb}{#1}}
-\@namedef{Gin@rule@.pdf}#1{{pdf}{.bb}{#1}}
+\@namedef{Gin@rule@.png}#1{{bmp}{.bb}{#1}}
+\@namedef{Gin@rule@.pdf}#1{{eps}{.bb}{#1}}
\@namedef{Gin@rule@*}#1{{eps}{\Gin@ext}{#1}}
\endinput
%%
%% End of file `dvipdfm.def'.
+
diff --git a/changelog b/changelog
index d652374..032ec36 100644
--- a/changelog
+++ b/changelog
@@ -1,3 +1,5 @@
+20140614 tpd src/axiom-website/patches.html 20140614.05.tpd.patch
+20140614 tpd Fixup broken build issues
20140614 tpd src/axiom-website/patches.html 20140614.04.tpd.patch
20140614 tpd src/axiom-website/books.html add bookvol13
20140614 tpd books/Makefile add bookvol13
diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html
index 5e10e71..51cd602 100644
--- a/src/axiom-website/patches.html
+++ b/src/axiom-website/patches.html
@@ -4454,6 +4454,8 @@ buglist bug 7253: There are no library operations named 'when'
buglist bug 7254: f==n+->sum(sum(1/i,i=1..j),j=1..n) complains
20140614.04.tpd.patch
books/bookvol13 Proving Axiom Correct
+20140614.05.tpd.patch
+Fixup broken build issues