# $Id: Portfile,v 1.11 2004/10/19 16:37:28 gwright Exp $

PortSystem 1.0
name		acl2
version		2.9
revision	1
categories	math
maintainers	gwright@opendarwin.org
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.)						\
#									\
#		The :dir :system path specifier is broken in this	\
#		build because the system path is hardcoded into the	\
#		the lisp images as the original build directory. This	\
#		may be fixed in a future release.			\
#
#		To exit ACL2, enter :q or at the prompt.		\
#		This will bring	up an ordinary OpenMCL prompt. Enter	\
#		(good-bye) or (ccl:quit) to exit OpenMCL.


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

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

checksums	acl2.tar.gz      md5 160e1553a738b5709d16822580a2dcb6 \
		workshops.tar.gz md5 4dcdceca907a309ea207747cefa4c257 \
		nonstd.tar.gz    md5 61fbce09d26a889a9adcf7dd0a6eae58

depends_build	bin:openmcl:openmcl

post-extract	{ cd ${workpath}
		  file rename ${name}-sources ${name}-${version}
		  file rename workshops ${name}-${version}/books
		  file rename nonstd    ${name}-${version}/books
		}

use_configure	no

build.target	"large LISP=openmcl"

set heap_image	"saved_acl2.dppccl"
set target_path	${prefix}/share/${name}/${version}

variant nonstd	{ build.target 	 "large-acl2r LISP=openmcl"
		  set heap_image "saved_acl2r.dppccl"
		}

variant certify	{ post-activate	{ cd ${target_path}
				  system "make certify-books"
				}
		}

variant regression	{ post-activate	{ cd ${target_path}
				  system "make regression"
				}
		}

destroot	{ file mkdir ${destroot}/${target_path}
		  foreach f [glob -directory ${workpath}/${name}-${version} *] {
			file copy $f ${destroot}/${target_path}
		  }
		}

post-destroot	{ set script [open "${destroot}${prefix}/bin/acl2" w 755]
		  puts $script "#!/bin/sh"
		  puts $script "openmcl --eval \"(acl2::acl2-default-restart)\" --image-name ${target_path}/${heap_image}"
		  puts $script ""
		  close $script
		  system "chmod 755 ${destroot}${prefix}/bin/acl2"
		}