diff --git a/Makefile b/Makefile
index a26e500..f9ccaf9 100644
--- a/Makefile
+++ b/Makefile
@@ -50,11 +50,10 @@ BYE:=bye
#GCLVERSION=gcl-2.6.8pre2
#GCLVERSION=gcl-2.6.8pre3
#GCLVERSION=gcl-2.6.8pre4
-GCLVERSION=gcl-2.6.8pre7
+#GCLVERSION=gcl-2.6.8pre7
+GCLVERSION=gcl-cygwin
GCLDIR:=${LSP}/${GCLVERSION}
-GCLOPTS="--enable-vssize=65536*2 --enable-locbfd --disable-dynsysbfd \
- --disable-statsysbfd --enable-maxpage=512*1024 --disable-xgcl \
- --disable-tkconfig"
+GCLOPTS="--enable-vssize=65536*2 --disable-xgcl --disable-tkconfig"
LISP:=lsp
##### C related variables
@@ -293,5 +292,12 @@ clean:
@ for i in `find src -name "Makefile"` ; do rm -f $$i ; done
@ for i in `find src -name "Makefile.dvi"` ; do rm -f $$i ; done
@ rm -f lastBuildDate
- @ rm -f books/tangle
+ @ rm -f books/tangle.o
+ @ rm -f Makefile.pdf books/Makefile.pdf
+ @ rm -f lsp/Makefile.pdf lsp/Makefile.pdf src/Makefile.pdf
+ @ rm -f src/algebra/Makefile.pdf src/clef/Makefile.pdf
+ @ rm -f src/doc/Makefile.pdf src/lib/Makefile.pdf
+ @ rm -f src/etc/Makefile.pdf src/input/Makefile.pdf
+ @ rm -f src/interp/Makefile.pdf
+ @ rm -f src/scripts/Makefile.pdf src/share/Makefile.pdf
diff --git a/Makefile.pamphlet b/Makefile.pamphlet
index 24b427a..0b352b4 100644
--- a/Makefile.pamphlet
+++ b/Makefile.pamphlet
@@ -219,11 +219,11 @@ clean:
@ for i in `find src -name "Makefile"` ; do rm -f $$i ; done
@ for i in `find src -name "Makefile.dvi"` ; do rm -f $$i ; done
@ rm -f lastBuildDate
- @ rm -f books/tangle
+ @ rm -f books/tangle.o
@ rm -f Makefile.pdf books/Makefile.pdf
@ rm -f lsp/Makefile.pdf lsp/Makefile.pdf src/Makefile.pdf
@ rm -f src/algebra/Makefile.pdf src/clef/Makefile.pdf
- @ rm -f src/doc/Makefile.pdf
+ @ rm -f src/doc/Makefile.pdf src/lib/Makefile.pdf
@ rm -f src/etc/Makefile.pdf src/input/Makefile.pdf
@ rm -f src/interp/Makefile.pdf
@ rm -f src/scripts/Makefile.pdf src/share/Makefile.pdf
@@ -690,7 +690,7 @@ lspdir: ${MNT}/${SYS}/bin/document ${LSP}/Makefile
@echo =====================================
@echo lsp BUILDING GCL COMMON LISP
@echo =====================================
- @(cd lsp ; ${ENV} ${MAKE} gcldir ) 1>/dev/null 2>/dev/null
+ (cd lsp ; ${ENV} DESTDIR= ${MAKE} gcldir )
# @(cd lsp ; ${ENV} ${MAKE} ccldir )
\getchunk{LSPMakefile}
@@ -876,7 +876,8 @@ forget to erase the lsp/Makefile the wrong patches will be applied.
#GCLVERSION=gcl-2.6.8pre2
#GCLVERSION=gcl-2.6.8pre3
#GCLVERSION=gcl-2.6.8pre4
-GCLVERSION=gcl-2.6.8pre7
+#GCLVERSION=gcl-2.6.8pre7
+GCLVERSION=gcl-cygwin
\end{chunk}
\subsubsection{The GCLOPTS configure variable}
@@ -886,8 +887,7 @@ to system. We create an environment variable here so we can add options
to the configure command in the lsp/Makefile.pamphlet.
\begin{chunk}{GCLOPTS}
-GCLOPTS="--enable-vssize=65536*2 --enable-statsysbfd \
- --enable-maxpage=256*1024 --disable-xgcl --disable-tkconfig"
+GCLOPTS="--enable-vssize=65536*2 --disable-xgcl --disable-tkconfig"
\end{chunk}
It turns out that we can successfully build GCL on many more systems
if we set the GCLOPTS to build a local BFD.
@@ -898,15 +898,11 @@ with the message
Error: Cannot get relocated section contents
\end{verbatim}
\begin{chunk}{GCLOPTS-LOCBFD}
-GCLOPTS="--enable-vssize=65536*2 --enable-locbfd --disable-dynsysbfd \
- --disable-statsysbfd --enable-maxpage=512*1024 --disable-xgcl \
- --disable-tkconfig"
+GCLOPTS="--enable-vssize=65536*2 --disable-xgcl --disable-tkconfig"
\end{chunk}
For the gcl-2.6.8pre7 version we move to using the custreloc option.
\begin{chunk}{GCLOPTS-CUSTRELOC}
-GCLOPTS="--enable-vssize=65536*2 --disable-locbfd --disable-dynsysbfd \
- --disable-statsysbfd --enable-maxpage=512*1024 --disable-xgcl \
- --disable-tkconfig --enable-custreloc --disable-tkconfig"
+GCLOPTS="--enable-vssize=65536*2 --disable-xgcl --disable-tkconfig"
\end{chunk}
For the MACOSX port we need the following options. The ``--disable-nls'' means
that we will not be supporting natural language internationalization.
@@ -916,9 +912,7 @@ setting of the ``canonical'' variable, which is in turn set by a shell script.
We need to add ``--enable-locbfd'' and ``--disable-dlopen'' due to the error
``unexec: not enough room for load commands for new \_\_DATA segments''.
\begin{chunk}{GCLOPTS-MACPORT}
-GCLOPTS="--enable-vssize=65536*2 --disable-nls --disable-locbfd \
- --disable-statsysbfd --enable-custreloc --disable-tkconfig \
- --enable-machine=powerpc-macosx --disable-xgcl --disable-dlopen"
+GCLOPTS="--enable-vssize=65536*2 --disable-xgcl --disable-tkconfig"
\end{chunk}
\subsection{Makefile.freebsd}
\begin{chunk}{Makefile.freebsd}
diff --git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index e9bd176..5c53c87 100644
--- a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ -4076,8 +4076,7 @@ This may ease the achievement of proofs.
\bibitem[Daly 10]{Daly10} Daly, Timothy\\
``Intel Instruction Semantics Generator''\\
-\verb|daly.axiom-developer.org/TimothyDaly_files/publications/sei/|
-\verb|intel/intel.pdf
+\verb|daly.axiom-developer.org/TimothyDaly_files/publications/sei/intel/intel.pdf|
%\verb|axiom-developer.org/axiom-website/papers/Daly10.pdf|
\begin{adjustwidth}{2.5em}{0pt}
@@ -4292,6 +4291,19 @@ Addison-Wesley ISBN 0-321-14306-X
``The Semantics of Destructive Lisp''\\
Center for the Study of Language and Information ISBN 0-937073-06-7
+\begin{adjustwidth}{2.5em}{0pt}
+Our basic premise is that the ability to construct and modify programs
+will not improve without a new and comprehensive look at the entire
+programming process. Past theoretical research, say, in the logic of
+programs, has tended to focus on methods for reasoning about
+individual programs; little has been done, it seems to us, to develop
+a sound understanding of the process of programming -- the process by
+which programs evolve in concept and in practice. At present, we lack
+the means to describe the techniques of program construction and
+improvement in ways that properly link verification, documentation and
+adaptability.
+\end{adjustwidth}
+
\bibitem[Newcombe 13]{Newc13} Newcombe, Chris; Rath, Tim; Zhang, Fan;
Munteanu, Bogdan; Brooker, Marc; Deardeuff, Michael\\
``Use of Formal Methods at Amazon Web Services''\\
diff --git a/changelog b/changelog
index ea7ea0a..d9dd419 100644
--- a/changelog
+++ b/changelog
@@ -1,3 +1,8 @@
+20140726 tpd src/axiom-website/patches.html 20140726.01.tpd.patch
+20140726 tpd Makefile move to GCL cygwin
+20140726 tpd lsp/Makefile move to GCL cygwin
+20140726 tpd zips/gcl-cgywin.tgz move to GCL cygwin
+20140726 tpd books/bookvolbib fix typo
20140724 tpd src/axiom-website/patches.html 20140724.02.tpd.patch
20140724 tpd books/bookvol13 add Daly10 for proving Axiom
20140724 tpd books/bookvolbib add Daly10 for proving Axiom
diff --git a/lsp/Makefile.pamphlet b/lsp/Makefile.pamphlet
index 2b2764e..9b45cd1 100644
--- a/lsp/Makefile.pamphlet
+++ b/lsp/Makefile.pamphlet
@@ -1681,6 +1681,91 @@ clean:
@echo 25 cleaning ${LSP}/ccl
@( cd ccl ; ${ENV} ${MAKE} clean )
\end{chunk}
+
+\subsection{The GCL-cygwin stanza}
+This stanza will be written when the GCLVERSION variable is
+``gcl-cygwin''. It will overwrite the default version. See the
+top level Makefile.pamphlet.
+
+The compiler::link function call was suggested by Camm as a
+way around patching the lisp system. The function creates a
+new lisp image ld and C objects prior to save-system.
+\begin{verbatim}
+ echo '(compiler::link \
+\end{verbatim}
+The first argument can be used to compile and load lisp code.
+\begin{verbatim}
+ (list (compile-file "${BOOKS}/tangle.lisp")) \
+\end{verbatim}
+The second argument gives the file location for the save-system
+\begin{verbatim}
+ "${OUT}/lisp" \
+\end{verbatim}
+The third argument sets up various internal variables, including
+the
+\begin{verbatim}
+ (format nil \
+ "(progn \
+ (let ((*load-path* (cons ~S *load-path*)) \
+ (si::*load-types* ~S)) \
+ (compiler::emit-fn t)) \
+ (setq *tmp-dir* "${TMP}") \
+ (makunbound (quote *system-banner*)) \
+ (when (fboundp (quote si::sgc-on)) (si::sgc-on t)) \
+ #-native-reloc (setq compiler::*default-system-p* t))" \
+ si::*system-directory* \
+ (quote (list #+native-reloc".o" ".lsp"))) \
+\end{verbatim}
+The fourth argument is a list of binaries to link
+\begin{verbatim}
+ "${OBJ}/${SYS}/lib/cfuns-c.o \
+ ${OBJ}/${SYS}/lib/sockio-c.o \
+ ${OBJ}/${SYS}/lib/libspad.a")' \
+\end{verbatim}
+and the compiler::link command is piped into the lisp image.
+\begin{verbatim}
+ | unixport/saved_gcl )
+\end{verbatim}
+
+\begin{chunk}{gcl-cygwin}
+# gcl version cygwin
+OUT=${OBJ}/${SYS}/bin
+
+all:
+ @echo 1 building ${LSP} ${GCLVERSION}
+
+gcldir:
+ @echo 2 building ${GCLVERSION}
+ @tar -zxf ${ZIPS}/${GCLVERSION}.tgz
+ (cd ${GCLVERSION} ; \
+ ./configure ${GCLOPTS} ; \
+ ${ENV} ${MAKE} ; \
+ echo '(compiler::link (list (compile-file "${BOOKS}/tangle.lisp")) "${OUT}/lisp" (format nil "(progn (let ((*load-path* (cons ~S *load-path*)) (si::*load-types* ~S)) (compiler::emit-fn t)) (makunbound (quote *system-banner*)) (when (fboundp (quote si::sgc-on)) (si::sgc-on t)) #-native-reloc (setq compiler::*default-system-p* t))" si::*system-directory* (quote (list #+native-reloc".o" ".lsp"))) "${OBJ}/${SYS}/lib/cfuns-c.o ${OBJ}/${SYS}/lib/sockio-c.o ${OBJ}/${SYS}/lib/libspad.a")' | bin/gcl )
+ @echo 13 finished system build on `date` | tee >gcldir
+
+ccldir: ${LSP}/ccl/Makefile
+ @echo 14 building CCL
+ @mkdir -p ${INT}/ccl
+ @mkdir -p ${OBJ}/${SYS}/ccl
+ @( cd ccl ; ${ENV} ${MAKE} )
+
+${LSP}/ccl/Makefile: ${LSP}/ccl/Makefile.pamphlet
+ @echo 15 making ${LSP}/ccl/Makefile from ${LSP}/ccl/Makefile.pamphlet
+ @( cd ccl ; ${DOCUMENT} ${NOISE} Makefile )
+
+document:
+ @echo 16 making docs in ${LSP}
+ @mkdir -p ${INT}/doc/lsp/ccl
+ @( cd ccl ; ${ENV} ${MAKE} document )
+
+clean:
+ @echo 17 cleaning ${LSP}/ccl
+ @( cd ccl ; ${ENV} ${MAKE} clean )
+
+\end{chunk}
+
+
+
\eject
\begin{thebibliography}{99}
\bibitem{1} nothing
diff --git a/patch b/patch
index 5eb7093..ada37f6 100644
--- a/patch
+++ b/patch
@@ -1,13 +1,4 @@
-books/bookvol13, bookvolbib add Daly for proving Axiom
+Makefile, lsp/Makefile, zips/gcl-cygwin.tgz use the latest gcl
-\bibitem[Daly 10]{Daly10} Daly, Timothy\\
-``Intel Instruction Semantics Generator''\\
-\verb|daly.axiom-developer.org/TimothyDaly_files/publications/sei/|
-\verb|intel/intel.pamphlet|
-
-\begin{adjustwidth}{2.5em}{0pt}
-Given an Intel x86 binary, extract the semantics of the instruction
-stream as Conditional Concurrent Assignments (CCAs). These CCAs
-represent the semantics of each individual instruction. They can be
-composed to represent higher level semantics.
-\end{adjustwidth}
+Camm has fixed Axiom to use compiler::link.
+Axiom has moved to the latest GCL release.
diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html
index c41f16f..246d856 100644
--- a/src/axiom-website/patches.html
+++ b/src/axiom-website/patches.html
@@ -4564,6 +4564,8 @@ books/bookvol10.1 expand section on interpolation formulas
books/bookvol13, bookvolbib add Mason86 for proving Axiom
20140724.02.tpd.patch
books/bookvol13, bookvolbib add Daly10 for proving Axiom
+20140726.01.tpd.patch
+Makefile, lsp/Makefile, zips/gcl-cygwin.tgz use the latest gcl