#  -*- Fundamental -*- 

# ACL2 Version 1.9 -- A Computational Logic for Applicative Common Lisp
# Copyright (C) 1997  Computational Logic, Inc.

# This program is free software; you can redistribute it and/or modify
# it under the terms of the GNU General Public License as published by
# the Free Software Foundation; either version 2 of the License, or
# (at your option) any later version.

# This program is distributed in the hope that it will be useful,
# but WITHOUT ANY WARRANTY; without even the implied warranty of
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
# GNU General Public License for more details.

# You should have received a copy of the GNU General Public License
# along with this program; if not, write to the Free Software
# Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.

# Written by:  Matt Kaufmann               and J Strother Moore
# email:       Matt_Kaufmann@email.mot.com and Moore@cs.utexas.edu
# Computational Logic, Inc.
# 1717 West Sixth Street, Suite 290
# Austin, TX 78703-4776 U.S.A.

# This file certifies all the books that come with the system.
# This is not a particularly elegant approach; actually, Bishop Brock
# has created a makefile in public/ that suggests a more elegant approach.
# For now, however, this will suffice.

# We execute :q followed by (LP) in each ACL2 session because some versions of
# ACL2 start up inside (LP) and some do not.  When we do not, the "command" :q
# seems harmless.

# This tells make to expect `suffix rules' for these file suffixes.

.SUFFIXES: .cert .lisp

# See the comment in public/makefile for EXT.  Here, we use the GCL setting.

ACL2 = acl2

all:	cowles.log arithmetic.log meta.log public.log data-structures.log nqthm.log bdd.log
	echo "Done; used ${ACL2}."

cowles.log:  cowles/acl2-agp.cert cowles/acl2-asg.cert cowles/acl2-crg.cert 
	rm -f workxxx
	echo ':q' > workxxx
	echo '(LP)' >> workxxx
	echo '(ld "certify.lisp")' >> workxxx
	cd cowles ; (${ACL2} < ../workxxx > ../cowles.log)
	rm -f workxxx

cowles/acl2-agp.cert: cowles/acl2-agp.lisp

cowles/acl2-asg.cert: cowles/acl2-asg.lisp

cowles/acl2-crg.cert : cowles/acl2-crg.lisp

arithmetic.log:  cowles arithmetic/equalities.cert arithmetic/inequalities.cert arithmetic/rational-listp.cert arithmetic/rationals-with-axioms.cert arithmetic/top.cert
	rm -f workxxx
	echo ':q' > workxxx
	echo '(LP)' >> workxxx
	echo '(ld "certify.lisp")' >> workxxx
	cd arithmetic ; (${ACL2} < ../workxxx > ../arithmetic.log)
	rm -f workxxx

arithmetic/equalities.cert: arithmetic/equalities.lisp

arithmetic/inequalities.cert: arithmetic/inequalities.lisp

arithmetic/rational-listp.cert: arithmetic/rational-listp.lisp

arithmetic/rationals-with-axioms.cert: arithmetic/rationals-with-axioms.lisp

arithmetic/top.cert: arithmetic/top.lisp

meta.log:  arithmetic meta/term-defuns.cert meta/term-lemmas.cert meta/meta-plus-equal.cert meta/meta-plus-lessp.cert meta/meta-times-equal.cert meta/meta.cert arithmetic/top-with-meta.cert
	rm -f workxxx
	echo ':q' > workxxx
	echo '(LP)' >> workxxx
	echo '(ld "certify.lisp")' >> workxxx
	cd meta ; (${ACL2} < ../workxxx > ../meta.log)
	echo ':q' > workxxx
	echo '(LP)' >> workxxx
	echo '(certify-book "top-with-meta")' >> workxxx
	cd arithmetic ; (${ACL2} < ../workxxx >> ../meta.log)

meta/term-defuns.cert: meta/term-defuns.lisp

meta/term-lemmas.cert: meta/term-lemmas.lisp

meta/meta-plus-equal.cert: meta/meta-plus-equal.lisp

meta/meta-plus-lessp.cert: meta/meta-plus-lessp.lisp

meta/meta-times-equal.cert: meta/meta-times-equal.lisp

meta/meta.cert: meta/meta.lisp

arithmetic/top-with-meta.cert: arithmetic/top-with-meta.lisp

public.log:  arithmetic
	echo '(value :q)' > workxxx
	echo '(with-open-file (str "workyyy" :direction :output) (format str "~a" acl2::*compiled-file-extension*))' >> workxxx
	${ACL2} < workxxx
	rm -f workxxx
	(cd public ; make ACL2=${ACL2} EXT=`cat ../workyyy`) > public.log
	rm -f workyyy

data-structures.log:  arithmetic
	echo '(value :q)' > workxxx
	echo '(with-open-file (str "workyyy" :direction :output) (format str "~a" acl2::*compiled-file-extension*))' >> workxxx
	${ACL2} < workxxx
	rm -f workxxx
	(cd data-structures ; make ACL2=${ACL2} EXT=`cat ../workyyy`) > data-structures.log
	rm -f workyyy

nqthm.log:
	rm -f workxxx
	echo ':q' > workxxx
	echo '(LP)' >> workxxx
	BOOKDIR=`pwd`/nqthm/ ; echo "(assign nqthm-dir \"$$BOOKDIR\")" >> workxxx
	echo '(ld "certify.lisp")' >> workxxx
	cd nqthm ; (${ACL2} < ../workxxx >> ../nqthm.log)
	rm -f workxxx

bdd.log:
	rm -f workxxx
	echo ':q' > workxxx
	echo '(LP)' >> workxxx
	echo '(ld "certify.lisp")' >> workxxx
	cd bdd ; (${ACL2} < ../workxxx >> ../bdd.log)
	rm -f workxxx