Permalink
Fetching contributors…
Cannot retrieve contributors at this time
284 lines (234 sloc) 11.1 KB
# -*- coding: utf-8; mode: tcl; tab-width: 4; indent-tabs-mode: nil; c-basic-offset: 4 -*- vim:fenc=utf-8:ft=tcl:et:sw=4:ts=4:sts=4
PortSystem 1.0
PortGroup github 1.0
name acl2
version 8.1
set shortversion v8-1
checksums md5 94892c1a269587237cc540a1053cd13d \
sha1 95b9501e89e23be9491616e52c36de48e7c46915 \
rmd160 f9a4cf4b0b8e17592e391851f9b6b9a6fbc4829d \
sha256 7d73f81c979ca3ec67d7c151cc344ab0a768b280f03f608770c3fad081ac80ea \
size 78539182
github.setup acl2-devel ${name}-devel ${version}
github.tarball_from releases
license BSD
categories math
maintainers {ijackson @JacksonIsaac} openmaintainer
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.
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.
"
homepage http://www.cs.utexas.edu/users/moore/acl2/${shortversion}
distname ${name}-${version}
use_configure no
depends_lib port:sbcl
set heap_image "saved_acl2.core"
set heap_image_nonstd "saved_acl2r.core"
set run_script "saved_acl2"
set run_script_nonstd "saved_acl2r"
# There is no universal binary for acl2, because there is no universal
# build of sbcl or ccl.
#
universal_variant no
# By converntion, the 64 bit version of Clozure CL is invoked by the
# script "ccl64"
#
# The ccl compiler produces a heap image whose filename extension depends
# on the platorm.
#
set ccl_script ccl
platform darwin i386 {
if {${build_arch} eq "i386"} {
global ccl_ext
set ccl_ext dx86cl
}
if {${build_arch} eq "x86_64"} {
global ccl_ext
set ccl_ext dx86cl64
global ccl_script
set ccl_script ccl64
}
}
platform darwin powerpc {
if {${build_arch} eq "powerpc"} {
global ccl_ext
set ccl_ext dppccl
}
if {${build_arch} eq "ppc64"} {
global ccl_ext
set ccl_ext dppccl64
global ccl_script
set ccl_script ccl64
}
}
# The emacs variant does not require that we use emacs from MacPorts,
# since many users prefer Aquamacs. It just copies the emacs support
# files to ${prefix}/share/emacs/site-lisp.
#
variant emacs description {Include support for using acl2 under emacs} { }
variant ccl description {Use ccl as the underlying lisp} {
depends_lib-delete port:sbcl
depends_lib-append port:ccl
global heap_image
global heap_image_nonstd
set heap_image saved_acl2.${ccl_ext}
set heap_image_nonstd saved_acl2r.${ccl_ext}
}
set target_path ${prefix}/share/${name}/${version}
variant certify description {Certify the included books} { }
variant regression description {Run the regression test suite (nb: takes hours)} { }
variant nonstd description {Build the nonstandard analysis books for handling real numbers} { }
build {
if {[variant_isset ccl]} {
system "cd ${worksrcpath} && make LISP=${prefix}/bin/${ccl_script}"
if {[variant_isset nonstd]} {
system "cd ${worksrcpath} && make large-acl2r LISP=${prefix}/bin/${ccl_script}"
}
} else {
system "cd ${worksrcpath} && make LISP=${prefix}/bin/sbcl"
if {[variant_isset nonstd]} {
system "cd ${worksrcpath} && make large-acl2r LISP=${prefix}/bin/sbcl"
}
}
}
destroot {
file mkdir ${destroot}/${target_path}
foreach f [glob -directory ${workpath}/${worksrcdir} *] {
file copy $f ${destroot}/${target_path}
}
if {[variant_isset emacs]} {
set emacs_target ${prefix}/share/emacs/site-lisp
file mkdir ${destroot}/${emacs_target}
file copy ${destroot}/${target_path}/emacs/emacs-acl2.el ${destroot}/${emacs_target}
file copy ${destroot}/${target_path}/emacs/monitor.el ${destroot}/${emacs_target}
ui_msg "Emacs support files for acl2 are in ${emacs_target}"
}
}
post-destroot {
file delete ${destroot}${prefix}/share/${name}/${version}/${run_script}
set script [open "${destroot}${prefix}/share/${name}/${version}/${run_script}" w 755]
if {[variant_isset ccl]} {
puts $script "#!/bin/sh"
puts $script "export ACL2_SYSTEM_BOOKS=${destroot}${prefix}/share/${name}/${version}/books"
puts $script "${ccl_script} --eval \"(acl2::acl2-default-restart)\" --load ${destroot}${prefix}/share/${name}/${version}/cert_location --image-name ${destroot}/${target_path}/${heap_image}"
puts $script ""
} else {
puts $script "#!/bin/sh"
puts $script "export ACL2_SYSTEM_BOOKS=${destroot}${prefix}/share/${name}/${version}/books"
puts $script "sbcl --core ${destroot}/${target_path}/${heap_image} --userinit /dev/null --eval \'(acl2::sbcl-restart)\' --load ${destroot}${prefix}/share/${name}/${version}/cert_location"
puts $script ""
}
close $script
system "chmod 755 ${destroot}${prefix}/share/${name}/${version}/${run_script}"
if {[variant_isset nonstd]} {
file delete ${destroot}${prefix}/share/${name}/${version}/${run_script_nonstd}
set script [open "${destroot}${prefix}/share/${name}/${version}/${run_script_nonstd}" w 755]
if {[variant_isset ccl]} {
puts $script "#!/bin/sh"
puts $script "export ACL2_SYSTEM_BOOKS=${destroot}${prefix}/share/${name}/${version}/books"
puts $script "${ccl_script} --eval \"(acl2::acl2-default-restart)\" --load ${destroot}${prefix}/share/${name}/${version}/cert_location --image-name ${destroot}/${target_path}/${heap_image_nonstd}"
puts $script ""
} else {
puts $script "#!/bin/sh"
puts $script "export ACL2_SYSTEM_BOOKS=${destroot}${prefix}/share/${name}/${version}/books"
puts $script "sbcl --core ${destroot}/${target_path}/${heap_image_nonstd} --userinit /dev/null --eval \'(acl2::sbcl-restart)\' --load ${destroot}${prefix}/share/${name}/${version}/cert_location"
puts $script ""
}
close $script
system "chmod 755 ${destroot}${prefix}/share/${name}/${version}/${run_script_nonstd}"
}
set script [open "${destroot}${prefix}/share/${name}/${version}/cert_location" w 755]
puts $script "(acl2::f-put-global \'acl2::old-certification-dir \"${destroot}${prefix}/share/${name}/${version}/books\" acl2::*the-live-state*)"
puts $script "(acl2::f-put-global \'acl2::new-certification-dir \"${prefix}/share/${name}/${version}/books\" acl2::*the-live-state*)"
close $script
if {[variant_isset certify]} {
set clogfile ${prefix}/share/${name}/${version}/certify-books.log
ui_msg "certify-books log will be in ${clogfile}"
system "cd ${destroot}/${target_path} && make clean-books"
system "cd ${destroot}/${target_path} && make certify-books 2>&1 | tee ${destroot}/${clogfile}"
}
if {[variant_isset regression]} {
set rlogfile ${prefix}/share/${name}/${version}/regression.log
ui_msg "regression log will be in ${rlogfile}"
system "cd ${destroot}/${target_path} && make clean-books"
system "cd ${destroot}/${target_path} && make regression 2>&1 | tee ${destroot}/${rlogfile}"
if {[variant_isset nonstd]} {
set rlogfile_nonstd ${prefix}/share/${name}/${version}/regression-nonstd.log
ui_msg "regression-nonstd log will be in ${rlogfile_nonstd}"
system "cd ${destroot}/${target_path} && make ACL2=${destroot}${prefix}/share/${name}/${version}/saved_acl2r regression-nonstd 2>&1 | tee ${destroot}/${rlogfile_nonstd}"
}
}
file delete ${destroot}${prefix}/share/${name}/${version}/cert_location
file delete ${destroot}${prefix}/share/${name}/${version}/${run_script}
set script [open "${destroot}${prefix}/bin/acl2" w 755]
if {[variant_isset ccl]} {
puts $script "#!/bin/sh"
puts $script "export ACL2_SYSTEM_BOOKS=${prefix}/share/${name}/${version}/books"
puts $script "${ccl_script} --eval \"(acl2::acl2-default-restart)\" --image-name ${target_path}/${heap_image}"
puts $script ""
} else {
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 ""
}
close $script
system "chmod 755 ${destroot}${prefix}/bin/acl2"
if {[variant_isset nonstd]} {
file delete ${destroot}${prefix}/share/${name}/${version}/${run_script_nonstd}
set script [open "${destroot}${prefix}/bin/acl2r" w 755]
if {[variant_isset ccl]} {
puts $script "#!/bin/sh"
puts $script "export ACL2_SYSTEM_BOOKS=${prefix}/share/${name}/${version}/books"
puts $script "${ccl_script} --eval \"(acl2::acl2-default-restart)\" --image-name ${target_path}/${heap_image_nonstd}"
puts $script ""
} else {
puts $script "#!/bin/sh"
puts $script "export ACL2_SYSTEM_BOOKS=${prefix}/share/${name}/${version}/books"
puts $script "sbcl --core ${target_path}/${heap_image_nonstd} --userinit /dev/null --eval \'(acl2::sbcl-restart)\'"
puts $script ""
}
close $script
system "chmod 755 ${destroot}${prefix}/bin/acl2r"
}
# Now remove all of the .out and build directory certificate files,
# and rename the final (installation directory) certificates:
foreach out_file [exec find ${destroot}/${target_path} -name "\*.out"] {
file delete ${out_file}
}
foreach cert_file [exec find ${destroot}/${target_path} -name "\*.cert"] {
file delete ${cert_file}
file rename ${cert_file}.final ${cert_file}
}
}
if {[variant_isset nonstd] && ![variant_isset ccl]} {
# acl2r raises error when build against sbcl.
# Even upstream uses ccl by default
# The following note will intimate the user to pass +ccl
# variant along with +nonstd if they face errors.
notes-append " \n"
notes-append "acl2r might raise heap memory errors for some users when using sbcl backend.
Please install +nonstd with +ccl variant to use acl2r, if you face any errors.
"
}