acl2  most recent diff

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.2 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

Web Darwinports.com




# $Id: Portfile 24865 2007-05-06 22:44:57Z gwright macports.org $

PortSystem 1.0
Name: acl2
Version: 3.2
set shortversion v3-2
Category: math
Maintainers: gwright macports.org
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. # (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/${shortversion}
master_sites ${homepage}/distrib/:sources ${homepage}/distrib/acl2-sources/books:workshops ${homepage}/distrib/acl2-sources/books:nonstd

checksums acl2.tar.gz md5 406a6349fb20483fd2b75f21f984157e workshops.tar.gz md5 218a53abcbb53bac3c286c28df9ee0ad nonstd.tar.gz md5 58b6f12ec3b68cf6c0ba30b8bd040d4b

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_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"

Variant: openmcl conflicts i386 {
depends_run-delete port:sbcl
depends_run-append port:openmcl

global heap_image
global heap_image_nonstd
set heap_image "saved_acl2.dppccl"
set heap_image_nonstd "saved_acl2r.dppccl"
}

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

Variant: certify { }
Variant: regression { }
Variant: nonstd { }

build { if {[variant_isset openmcl]} {
cd ${worksrcpath}
system "make large LISP=openmcl"
if {[variant_isset nonstd]} {
system "make large-acl2r LISP=openmcl"
}
} else {
cd ${worksrcpath}
system "make large LISP=sbcl"
if {[variant_isset nonstd]} {
system "make large-acl2r LISP=sbcl"
}
}
}

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

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 openmcl]} {
puts $script "#!/bin/sh"
puts $script "export ACL2_SYSTEM_BOOKS=${destroot}${prefix}/share/${name}/${version}/books"
puts $script "openmcl --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 openmcl]} {
puts $script "#!/bin/sh"
puts $script "export ACL2_SYSTEM_BOOKS=${destroot}${prefix}/share/${name}/${version}/books"
puts $script "openmcl --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]} {
cd ${destroot}/${target_path}
set clogfile ${destroot}${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"
}

if {[variant_isset regression]} {
cd ${destroot}/${target_path}
set rlogfile ${destroot}${prefix}/share/${name}/${version}/regression.log
ui_msg "regression log will be in ${rlogfile}"
system "make clean-books"
system "make regression > ${rlogfile} 2>&1"

if {[variant_isset nonstd]} {
set rlogfile_nonstd ${destroot}${prefix}/share/${name}/${version}/regression-nonstd.log
ui_msg "regression-nonstd log will be in ${rlogfile_nonstd}"
system "make ACL2=${destroot}${prefix}/share/${name}/${version}/saved_acl2r regression-nonstd > ${rlogfile_nonstd} 2>&1"
}
}

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 openmcl]} {
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 ""
} 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 openmcl]} {
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_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"
}
}

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: