# $Id: Portfile,v 1.15 2006/06/05 03:45:24 gwright Exp $

PortSystem 1.0
name		acl2
version		3.0
revision	2
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.)						\

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

homepage	http://www.cs.utexas.edu/users/moore/acl2/v3-0
master_sites	${homepage}/distrib/:sources				\
		${homepage}/distrib/acl2-sources/books:workshops	\
		${homepage}/distrib/acl2-sources/books:nonstd

checksums	acl2.tar.gz      md5 026065c1221850d7748de7b9cc23c7fc \
		workshops.tar.gz md5 3df53e22578f45333eb606862b57121b \
		nonstd.tar.gz    md5 89e062516f1243209aacd6a0a354ac30

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

depends_build	port:openmcl

build.target	"large LISP=openmcl"
set heap_image	"saved_acl2.dppccl"

variant sbcl	{ depends_build-delete	port:openmcl
		  depends_build-append	port:sbcl
		  build.target	"large LISP=sbcl"

		  global heap_image
		  set heap_image "saved_acl2.core"
}

set target_path	${prefix}/share/${name}/${version}

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

		  if {[variant_isset sbcl]} {
			build.target	"large-acl2r LISP=sbcl"
			set heap_image	"saved_acl2r.core"
		  }
		}

variant certify	{ post-activate	{ cd ${target_path}
				  set clogfile ${prefix}/share/${name}/${version}/certify-books.log
				  ui_msg "certify-books log will be in ${clogfile}"
				  system "make clean-books"
				  system "make certify-books > ${clogfile} 2>&1"
				}
		}

variant regression	{ post-activate	{ cd ${target_path}
				  set rlogfile ${prefix}/share/${name}/${version}/regression.log
				  ui_msg "regression log will be in ${rlogfile}"
				  system "make clean-books"
				  system "make regression > ${rlogfile} 2>&1"
				}
		}

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]

		  if {[variant_isset sbcl]} {
		  	puts $script "#!/bin/sh"
			puts $script "export ACL2_SYSTEM_BOOKS=${prefix}/share/${name}/${version}/books"
		  	puts $script "sbcl --core ${target_path}/${heap_image} --userinit /dev/null --eval \'(acl2::sbcl-restart)\'"
		  	puts $script ""
		  } else {
		  	puts $script "#!/bin/sh"
			puts $script "export ACL2_SYSTEM_BOOKS=${prefix}/share/${name}/${version}/books"
		  	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"

		  file delete ${destroot}${prefix}/share/${name}/${version}/saved_acl2
		  file copy   ${destroot}${prefix}/bin/acl2 \
			      ${destroot}${prefix}/share/${name}/${version}/saved_acl2
		}