# $Id: Portfile,v 1.2 2003/05/13 15:47:54 gwright Exp $

PortSystem 1.0
name		acl2
version		2.7
categories	math
maintainers	gwright@comcast.net
platforms	darwin
description	Applicative Common Lisp / A Computational Logic
long_description	\
		ACL2 (Applicative Common Lisp / A Computational \
		Logic) is the successor to nqthm, the Boyer-Moore \
		theorem prover. \
		\
		ACL2 can be used to automatically or semi-automatically \
		prove theorems and has been used extensively in real \
		applications (e.g., proving the correctness of certain \
		calculations in the floating point unit of the AMD K5 \
		microprocessor. \
		\
		ACL2 is a very large, multipurpose system. \
		You can use it as a programming language, \
		a specification language, a modeling language, \
		a formal mathematical logic, or a semi-automatic \
		theorem prover. Because the meta-language is the same \
		as the language (a subset of Common Lisp), it is very \
		flexible.

#user_notes	Users who want to use ACL2 for serious work should \
#		install the certify variant (sudo port install +certify), \
#		which will certify (i.e., prove all of the theorems) \
#		in the included examples. This can take several hours. \
#		(Just over eight and a half hours on an 800 MHz G4 TiBook.) \
#		\
#		To exit ACL2, enter :q at the prompt. This will bring \
#		up an ordinary OpenMCL prompt. Enter (ccl::quit) to \
#		exit OpenMCL.

#bugs		The ACL2 command line prompt is wrong. The OpenMCL \
#		prompt should be suppressed, but isn't. Nevertheless, \
#		ACl2 input is correctly interpreted at the OpenMCL \
#		"?" prompt.

distfiles	${name}${extract.sufx}:source \
		workshops${extract.sufx}:extrabooks \
		nonstd${extract.sufx}:extrabooks

homepage	http://www.cs.utexas.edu/users/moore/acl2/
master_sites	ftp://ftp.cs.utexas.edu/pub/moore/acl2/v2-7/:source \
		ftp://ftp.cs.utexas.edu/pub/moore/acl2/v2-7/acl2-sources/books/:extrabooks

checksums	acl2.tar.gz	 md5 970f5dfdc146b60bae6dd05c70160370 \
		workshops.tar.gz md5 01da24181e1fefa7ce046e0c615b8e93 \
		nonstd.tar.gz	 md5 1b43ea3a74927820881300b2ff06704d


patchfiles	patch-Makefile patch-acl2-check.lisp patch-acl2-init.lisp \
		patch-acl2.lisp patch-axioms.lisp patch-interface-raw.lisp

depends_build	bin:openmcl:openmcl

pre-patch	{ cd ${workpath}
		  file rename ${name}-sources ${name}-${version}
		  file rename workshops ${name}-${version}/books
		  file rename nonstd    ${name}-${version}/books
		}

configure	{ }

build.target	"large LISP=openmcl"

variant certify	{ post-build	{ cd ${workpath}/${worksrcdir}
				  system "make ACL2=\"openmcl -I ${workpath}/${worksrcdir}/saved_acl2\" regression"
				}
		}

install		{ file mkdir ${destroot}/${prefix}/share/${name}/${version}
		  cd ${workpath}/${name}-${version}
		  system "tar cf - . | ( cd ${destroot}/${prefix}/share/${name}/${version} && tar xf - )"
		}

post-install	{ set script [open "${destroot}${prefix}/bin/acl2" w 755]
		  puts $script "#!/bin/sh"
		  puts $script "openmcl --eval \"(acl2::lp)\" --image-name ${prefix}/share/${name}/${version}/saved_acl2"
		  puts $script ""
		  close $script
		  system "chmod 755 ${destroot}${prefix}/bin/acl2"
		}