View the most recent changes for the acl2 port at: acl2.darwinports.com/diff
Scroll down toward the bottom of the page to get installation instructions for acl2.
The raw portfile for acl2 3.5 is located here:
http://acl2.darwinports.com/dports/math/acl2/Portfile
Find related portfiles with the unique DarwinPorts.com search feature.
Check for any related Fink projects here: pdb.finkproject.org/pdb/package.php/acl2

The acl2 Portfile 52543 2009-06-18 17:59:47Z jmr macports.org $

PortSystem 1.0

Name: acl2
Version: 3.5
set shortversion v3-5
Category: math
Maintainers: gwright
Platform: 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.

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

Homepage: http://www.cs.utexas.edu/users/moore/acl2/${shortversion}
Master Sites: ${homepage}/distrib/:sources ${homepage}/distrib/acl2-sources/books:workshops ${homepage}/distrib/acl2-sources/books:nonstd

Checksums: acl2-${version}.tar.gz md5 a2738f4582d14f74664c93dad93ac055 sha1 d4052a49a3c2112eeb04cf97570e2caea8df38dd rmd160 167b61cd8a812de804225096f4f3f04b87ba84cb workshops-${version}.tar.gz md5 5ae8123cadfe323c3088a3666112ce07 sha1 b3a10d4cd876cb6ccde96920f0103ec0d89f7e2f rmd160 63401f257b8b61564ed660681f82776c762d43da nonstd-${version}.tar.gz md5 7de68f04ee468e25b24a230507cdb663 sha1 71e1da0cf417ef85f1002279b67227d729822a6e rmd160 caa90d4a742fb1df8ddeb24686bc49a2d79754ab


# ACL2 is distributed without a version number attached to the files.
# So we can't tell if we have the latest version of a file by looking
# at the name. (This breaks also MacPorts checksum handling.)
# Here, the files are manually fetched and renamed with a version number.
#
# MacPorts should always checksum the distribution files, instead
# of assuming that if a file's name is unchanged, the previously computed
# checksum is valid.
fetch {
ui_msg "starting special fetch procedure for acl2"
file mkdir ${distpath}

if {![file exists ${distpath}/acl2-${version}.tar.gz]} {
eval curl fetch http://www.cs.utexas.edu/users/moore/acl2/v3-5/distrib/acl2.tar.gz ${distpath}/acl2.tar.gz.TMP
file rename -force "${distpath}/acl2.tar.gz.TMP" "${distpath}/acl2-${version}.tar.gz"
}

if {![file exists ${distpath}/workshops-${version}.tar.gz]} {
eval curl fetch http://www.cs.utexas.edu/users/moore/acl2/v3-5/distrib/acl2-sources/books/workshops.tar.gz ${distpath}/workshops.tar.gz.TMP
file rename -force "${distpath}/workshops.tar.gz.TMP" "${distpath}/workshops-${version}.tar.gz"
}

if {![file exists ${distpath}/nonstd-${version}.tar.gz]} {
eval curl fetch http://www.cs.utexas.edu/users/moore/acl2/v3-5/distrib/acl2-sources/books/nonstd.tar.gz ${distpath}/nonstd.tar.gz.TMP
file rename -force "${distpath}/nonstd.tar.gz.TMP" "${distpath}/nonstd-${version}.tar.gz"
}

ui_msg "completed special fetch procedure for acl2"
}

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

use_configure no

depends_run 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 i386 {
global ccl_ext
set ccl_ext dx86cl
}

platform x86_64 {
global ccl_ext
set ccl_ext dx86cl64

global ccl_script
set ccl_script ccl64
}

platform powerpc {
global ccl_ext
set ccl_ext dppccl
}

platform 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_run-delete port:sbcl
depends_run-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 large LISP=${prefix}/bin/ccl"
if {[variant_isset nonstd]} {
system "cd ${worksrcpath} && make large-acl2r LISP=${prefix}/bin/ccl"
}
} else {
system "cd ${worksrcpath} && make large 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}/${name}-${version} *] {
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 you haven't already installed Darwin Ports, you can find easy instructions for doing so at the main Darwin Ports page.
Once Darwin Ports has been installed, in a terminal window and while online, type the following and hit return:

%  cd /opt/local/bin/portslocation/dports/acl2
%  sudo port install acl2  
Password: 

You will then be prompted for your root password, which you should enter. You may have to wait for a few minutes while the software is retrieved from the network and installed for you. Y ou should see something that looks similar to:

--->  Fetching acl2
--->  Verifying checksum for acl2
--->  Extracting acl2
--->  Configuring acl2
--->  Building acl2 with target all

--->  Staging acl2 into destroot

--->  Installing acl2

- Make sure that you do not close the terminal window while Darwin Ports is working. Once the software has been installed, you can find further information about using acl2 with these commands:

%  man acl2
%  apropos acl2
%  which acl2
%  locate acl2

 Where to find more information: