mirror of
https://github.com/macports/macports-ports.git
synced 2026-07-12 18:20:25 -07:00
281 lines
11 KiB
Tcl
281 lines
11 KiB
Tcl
# -*- 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.7
|
|
set shortversion v8-7
|
|
|
|
checksums rmd160 74d8498e51681d8e70c75fa2ebdaa7fa1a3d1b36 \
|
|
sha256 370433766f56737e597b09c0fd8f837d2df889ec8ed51efa9fc869a93185ce89 \
|
|
size 248186554
|
|
|
|
github.setup acl2-devel ${name}-devel ${version}
|
|
github.tarball_from releases
|
|
|
|
license BSD
|
|
categories math
|
|
|
|
maintainers {ijackson @JacksonIsaac} openmaintainer
|
|
|
|
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 path:bin/sbcl: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 path:bin/sbcl: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.
|
|
"
|
|
}
|