Portfile

# $Id: Portfile 22478 2007-03-02 05:16:40Z pipping@macports.org $

PortSystem 1.0
name acl2
version 3.0
revision 2
categories math
maintainers nomaintainer@macports.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
}