From c610787b676b38a34ca0d2c947f5040e74f2f3e2 Mon Sep 17 00:00:00 2001 From: Tim Daly Date: Wed, 15 Jul 2015 22:39:59 -0400 Subject: [PATCH] Makefile: extract and run proof code automatically Goal: Prove Axiom correct If the command line include "ACL2=acl2" then the system extracts the 'acl2' chunk from the books and run acl2 proof code automatically. --- Makefile | 7 +++++-- Makefile.pamphlet | 11 ++++++++--- books/Makefile.pamphlet | 14 +++++++++++++- books/bookvol5.pamphlet | 15 +++++++++++---- changelog | 4 ++++ patch | 11 +++-------- src/axiom-website/patches.html | 2 ++ 7 files changed, 46 insertions(+), 18 deletions(-) diff --git a/Makefile b/Makefile index 6c61f63..250cb8f 100644 --- a/Makefile +++ b/Makefile @@ -10,6 +10,7 @@ MNT:=${SPD}/mnt TMP:=${OBJ}/tmp ZIPS:=${SPD}/zips BOOKS:=${SPD}/books +PROOFS:=${OBJ}/${SYS}/proofs SPAD:=${SPD}/mnt/${SYS} SRCDIRS:="interpdir sharedir algebradir etcdir docdir \ graphdir smandir hyperdir browserdir inputdir" @@ -104,6 +105,7 @@ OBJ=${OBJ} \ PART=${PART} \ PATCH=${PATCH} \ PLF=${PLF} \ +PROOFS=${PROOFS} \ RANLIB=${RANLIB} \ RUNTYPE=${RUNTYPE} \ SPAD=${SPAD} \ @@ -128,8 +130,8 @@ all: rootdirs tanglec libspad @ echo 1 making a ${SYS} system, PART=${PART} SUBPART=${SUBPART} @ echo 2 Environment ${ENV} @ ${BOOKS}/tanglec Makefile.pamphlet "Makefile.${SYS}" >Makefile.${SYS} - @ cp books/dvipdfm.def ${MNT}/${SYS}/doc - @ cp books/changepage.sty ${MNT}/${SYS}/doc + @ cp ${BOOKS}/dvipdfm.def ${MNT}/${SYS}/doc + @ cp ${BOOKS}/changepage.sty ${MNT}/${SYS}/doc @ ${EXTRACT} Makefile.pamphlet @ cp Makefile.pdf ${MNT}/${SYS}/doc/src/root.Makefile.pdf @ if [ "${RUNTYPE}" = "parallel" ] ; then \ @@ -200,6 +202,7 @@ rootdirs: mkdir -p ${OBJ}/${SYS}/interp mkdir -p ${OBJ}/${SYS}/lib mkdir -p ${OBJ}/${SYS}/sman + mkdir -p ${OBJ}/${SYS}/proofs mkdir -p ${MNT}/doc mkdir -p ${MNT}/${SYS}/algebra mkdir -p ${MNT}/${SYS}/autoload diff --git a/Makefile.pamphlet b/Makefile.pamphlet index bb0737b..3bfebce 100644 --- a/Makefile.pamphlet +++ b/Makefile.pamphlet @@ -91,8 +91,8 @@ all: rootdirs tanglec libspad @ echo 1 making a ${SYS} system, PART=${PART} SUBPART=${SUBPART} @ echo 2 Environment ${ENV} @ ${BOOKS}/tanglec Makefile.pamphlet "Makefile.${SYS}" >Makefile.${SYS} - @ cp books/dvipdfm.def ${MNT}/${SYS}/doc - @ cp books/changepage.sty ${MNT}/${SYS}/doc + @ cp ${BOOKS}/dvipdfm.def ${MNT}/${SYS}/doc + @ cp ${BOOKS}/changepage.sty ${MNT}/${SYS}/doc @ ${EXTRACT} Makefile.pamphlet @ cp Makefile.pdf ${MNT}/${SYS}/doc/src/root.Makefile.pdf @ if [ "${RUNTYPE}" = "parallel" ] ; then \ @@ -163,6 +163,7 @@ rootdirs: mkdir -p ${OBJ}/${SYS}/interp mkdir -p ${OBJ}/${SYS}/lib mkdir -p ${OBJ}/${SYS}/sman + mkdir -p ${OBJ}/${SYS}/proofs mkdir -p ${MNT}/doc mkdir -p ${MNT}/${SYS}/algebra mkdir -p ${MNT}/${SYS}/autoload @@ -471,12 +472,13 @@ MNT:=${SPD}/mnt TMP:=${OBJ}/tmp ZIPS:=${SPD}/zips BOOKS:=${SPD}/books -SPAD:=${SPD}/mnt/${SYS} SRCDIRS:="interpdir sharedir algebradir etcdir docdir \ graphdir smandir hyperdir browserdir inputdir" SYS:=$(notdir $(AXIOM)) DAASE:=${SRC}/share +PROOFS:=${OBJ}/${SYS}/proofs +SPAD:=${SPD}/mnt/${SYS} SPADBIN:=${MNT}/${SYS}/bin DOCUMENT:=${SPADBIN}/document @@ -520,6 +522,7 @@ RUNTYPE:=serial # alltests, notests TESTSET:=notests BUILD:=full +ACL2:= \end{chunk} @@ -527,6 +530,7 @@ BUILD:=full \begin{chunk}{ENVAR} ENV:= \ +ACL2=${ACL2} \ AWK=${AWK} \ BOOKS=${BOOKS} \ BUILD=${BUILD} \ @@ -553,6 +557,7 @@ OBJ=${OBJ} \ PART=${PART} \ PATCH=${PATCH} \ PLF=${PLF} \ +PROOFS=${PROOFS} \ RANLIB=${RANLIB} \ RUNTYPE=${RUNTYPE} \ SPAD=${SPAD} \ diff --git a/books/Makefile.pamphlet b/books/Makefile.pamphlet index 1f7c11a..892c0e3 100644 --- a/books/Makefile.pamphlet +++ b/books/Makefile.pamphlet @@ -39,10 +39,12 @@ BOOKPDF=${PDF}/bookvol0.pdf ${PDF}/bookvol1.pdf ${PDF}/bookvol2.pdf \ ${PDF}/bookvol11.pdf ${PDF}/bookvol12.pdf ${PDF}/bookvol13.pdf \ ${PDF}/bookvolbib.pdf +PROVE=${PROOFS}/acl2.lisp OTHER= ${PDF}/refcard.pdf ${PDF}/endpaper.pdf ${PDF}/rosetta.pdf -all: announce ${PDF}/axiom.bib ${OTHER} ${BOOKPDF} ${PDF}/toc.pdf spadedit +all: announce ${PDF}/axiom.bib ${PROVE} ${OTHER} ${BOOKPDF} \ + ${PDF}/toc.pdf spadedit @(cd ${PDF} ; ${RM} *.out *.toc *.sty *.def *.png) announce: @@ -55,6 +57,16 @@ finish: @ echo FINISHED BUILDING PDF FILES books/Makefile @ echo ========================================== +${PROOFS}/acl2.lisp: + @ echo =========================================== + @ echo making ${PROOFS}/acl2.lisp + @ echo =========================================== + @ ${BOOKS}/tanglec ${BOOKS}/bookvol5.pamphlet acl2 >${PROOFS}/acl2.lisp + @ if [ .${ACL2} = .acl2 ] ; \ + then \ + ( cd ${PROOFS} ; echo '(ld "acl2.lisp")' | acl2 >acl2.output ) ; \ + fi ; + ${PDF}/axiom.bib: @ echo =========================================== @ echo making ${PDF}/axiom.bib from ${IN}/bookvolbib.pamphlet diff --git a/books/bookvol5.pamphlet b/books/bookvol5.pamphlet index 8d8276f..0321320 100644 --- a/books/bookvol5.pamphlet +++ b/books/bookvol5.pamphlet @@ -61484,15 +61484,17 @@ There are 8 parts of an htPage: \defun{isWrapped}{isWrapped} This was proven by ACL2 to accept any input and return either T or NIL. Note that ACL2 does not support FLOATP. -\begin{verbatim} +\begin{chunk}{defun isWrapped 0 ACL2} (defun isWrapped (x) (or (and (consp x) (eq (car x) 'wrapped)) (acl2-numberp x) (stringp x))) -==> -(OR (EQUAL (ISWRAPPED X) T) (EQUAL (ISWRAPPED X) NIL)) -\end{verbatim} +;==> +;(OR (EQUAL (ISWRAPPED X) T) (EQUAL (ISWRAPPED X) NIL)) + +\end{chunk} + \sig{isWrapped}{t}{(or t nil)} \begin{chunk}{defun isWrapped :proven} (defun |isWrapped| (x) @@ -61503,6 +61505,11 @@ Note that ACL2 does not support FLOATP. \end{chunk} +\chapter{The Proofs} +\begin{chunk}{acl2} +\getchunk{defun isWrapped 0 ACL2} +\end{chunk} + \chapter{The Interpreter} \begin{chunk}{Interpreter} (setq *print-array* nil) diff --git a/changelog b/changelog index d151468..3b7940b 100644 --- a/changelog +++ b/changelog @@ -1,3 +1,7 @@ +20150715 tpd src/axiom-website/patches.html 20150715.02.tpd.patch +20150715 tpd books/bookvol5 add the 'acl2' chapter and chunks +20150715 tpd books/Makefile extract and run proof code automatically +20150715 tpd Makefile extract and run proof code automatically 20150715 tpd src/axiom-website/patches.html 20150715.01.tpd.patch 20150715 tpd src/interp/i-util merge isWrapped function into bookvol5 20150715 tpd books/bookvol5: Use ACL2 to prove isWrapped function diff --git a/patch b/patch index 5d558f9..b3f2a6f 100644 --- a/patch +++ b/patch @@ -1,11 +1,6 @@ -books/bookvol5: Use ACL2 to prove isWrapped function +Makefile: extract and run proof code automatically Goal: Prove Axiom correct -This is the first example of using ACL2 against the Axiom -common lisp code to prove the function correct. The signature -for isWrapped is - - isWrapped: t -> (or t nil) - -It is a predicate that takes any argument and returns either t or nil. +If the command line include "ACL2=acl2" then the system extracts the +'acl2' chunk from the books and run acl2 proof code automatically. diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html index 0a0ba1c..d12a010 100644 --- a/src/axiom-website/patches.html +++ b/src/axiom-website/patches.html @@ -5102,6 +5102,8 @@ readme Add Laurent Thery to credits
src/interp/i-coerce.lisp fix use of eqType assignment
20150715.01.tpd.patch books/bookvol5: Use ACL2 to prove isWrapped function
+20150715.02.tpd.patch +Makefile: extract and run proof code automatically
-- 1.7.5.4