From 8d060bec57bbe4dd6be130d787b51f1fef8bf8f4 Mon Sep 17 00:00:00 2001
From: Tim Daly <daly@axiom-developer.org>
Date: Thu, 16 Jul 2015 01:42:59 -0400
Subject: [PATCH] Makefile: extract and run proof code automatically

Goal: Prove Axiom correct

If the command line include "COQ=coq" then the system extracts the
'coq' chunk from the books and run coq proof code automatically.
---
 Makefile                       |    8 ++++++--
 Makefile.pamphlet              |    2 ++
 books/Makefile.pamphlet        |   13 ++++++++++++-
 changelog                      |    3 +++
 patch                          |    4 ++--
 src/axiom-website/patches.html |    2 ++
 6 files changed, 27 insertions(+), 5 deletions(-)

diff --git a/Makefile b/Makefile
index 250cb8f..63e2b50 100644
--- a/Makefile
+++ b/Makefile
@@ -10,13 +10,13 @@ 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"
 
 SYS:=$(notdir $(AXIOM))
 DAASE:=${SRC}/share
+PROOFS:=${OBJ}/${SYS}/proofs
+SPAD:=${SPD}/mnt/${SYS}
 
 SPADBIN:=${MNT}/${SYS}/bin
 DOCUMENT:=${SPADBIN}/document
@@ -76,9 +76,12 @@ RUNTYPE:=serial
 # alltests, notests
 TESTSET:=notests
 BUILD:=full
+ACL2:=
+COQ:=
 
 
 ENV:= \
+ACL2=${ACL2} \
 AWK=${AWK} \
 BOOKS=${BOOKS} \
 BUILD=${BUILD} \
@@ -86,6 +89,7 @@ BYE=${BYE} \
 CC=${CC} \
 CCF=${CCF} \
 COMMAND=${COMMAND} \
+COQ=${COQ} \
 DAASE=${DAASE} \
 DESTDIR=${DESTDIR} \
 DOCUMENT=${DOCUMENT} \
diff --git a/Makefile.pamphlet b/Makefile.pamphlet
index 3bfebce..a5db86b 100644
--- a/Makefile.pamphlet
+++ b/Makefile.pamphlet
@@ -523,6 +523,7 @@ RUNTYPE:=serial
 TESTSET:=notests
 BUILD:=full
 ACL2:=
+COQ:=
 
 \end{chunk}
 
@@ -538,6 +539,7 @@ BYE=${BYE} \
 CC=${CC} \
 CCF=${CCF} \
 COMMAND=${COMMAND} \
+COQ=${COQ} \
 DAASE=${DAASE} \
 DESTDIR=${DESTDIR} \
 DOCUMENT=${DOCUMENT} \
diff --git a/books/Makefile.pamphlet b/books/Makefile.pamphlet
index 892c0e3..76a54f4 100644
--- a/books/Makefile.pamphlet
+++ b/books/Makefile.pamphlet
@@ -39,7 +39,7 @@ 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
+PROVE=${PROOFS}/acl2.lisp ${PROOFS}/coq.lisp
 
 OTHER=  ${PDF}/refcard.pdf     ${PDF}/endpaper.pdf    ${PDF}/rosetta.pdf
 
@@ -67,6 +67,17 @@ ${PROOFS}/acl2.lisp:
 	    ( cd ${PROOFS} ; echo '(ld "acl2.lisp")' | acl2 >acl2.output ) ; \
 	   fi ; 
 
+${PROOFS}/coq.lisp:
+	@ echo ===========================================
+	@ echo making ${PROOFS}/coq.lisp
+	@ echo ===========================================
+	@ ${BOOKS}/tanglec ${BOOKS}/bookvol10.2.pamphlet coq \
+             >${PROOFS}/coq.lisp
+	@ if [ .${COQ} = .coq ] ; \
+	   then \
+	    ( cd ${PROOFS} ; echo "Insert COQ commands here" >coq.lisp ) ; \
+	   fi ; 
+
 ${PDF}/axiom.bib:
 	@ echo ===========================================
 	@ echo making ${PDF}/axiom.bib from ${IN}/bookvolbib.pamphlet
diff --git a/changelog b/changelog
index 3b7940b..e806e6f 100644
--- a/changelog
+++ b/changelog
@@ -1,3 +1,6 @@
+20150716 tpd src/axiom-website/patches.html 20150716.01.tpd.patch 
+20150716 tpd books/Makefile extract and run proof code automatically
+20150716 tpd Makefile extract and run proof code automatically
 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
diff --git a/patch b/patch
index b3f2a6f..2650206 100644
--- a/patch
+++ b/patch
@@ -2,5 +2,5 @@ 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.
+If the command line include "COQ=coq" then the system extracts the
+'coq' chunk from the books and run coq proof code automatically.
diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html
index d12a010..4afe204 100644
--- a/src/axiom-website/patches.html
+++ b/src/axiom-website/patches.html
@@ -5104,6 +5104,8 @@ src/interp/i-coerce.lisp fix use of eqType assignment<br/>
 books/bookvol5: Use ACL2 to prove isWrapped function<br/>
 <a href="patches/20150715.02.tpd.patch">20150715.02.tpd.patch</a>
 Makefile: extract and run proof code automatically<br/>
+<a href="patches/20150716.01.tpd.patch">20150716.01.tpd.patch</a>
+Makefile: extract and run proof code automatically<br/>
  </body>
 </html>
 
-- 
1.7.5.4