[49312] trunk/dports/math/acl2/Portfile
gwright at macports.org
gwright at macports.org
Tue Apr 7 04:10:00 PDT 2009
Revision: 49312
http://trac.macports.org/changeset/49312
Author: gwright at macports.org
Date: 2009-04-07 04:10:00 -0700 (Tue, 07 Apr 2009)
Log Message:
-----------
Version bump to 3.4, also change openmcl variant to ccl variant
(openmcl port is renamed).
Modified Paths:
--------------
trunk/dports/math/acl2/Portfile
Modified: trunk/dports/math/acl2/Portfile
===================================================================
--- trunk/dports/math/acl2/Portfile 2009-04-07 11:06:49 UTC (rev 49311)
+++ trunk/dports/math/acl2/Portfile 2009-04-07 11:10:00 UTC (rev 49312)
@@ -1,11 +1,12 @@
# $Id$
PortSystem 1.0
+
name acl2
-version 3.2
-set shortversion v3-2
+version 3.4
+set shortversion v3-4
categories math
-maintainers gwright at macports.org
+maintainers gwright
platforms darwin
description Applicative Common Lisp / A Computational Logic
long_description \
@@ -31,9 +32,8 @@
# 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
@@ -43,9 +43,18 @@
${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
+checksums acl2.tar.gz \
+ md5 00c210b69b585941d856616c7a66c463 \
+ sha1 9326fb97f7a351bc41943bb433d34e98d1dbf84f \
+ rmd160 72217c49caa9f0857f517483c76b0745dc01eb70 \
+ workshops.tar.gz \
+ md5 f7b5d5be32399d48407ec3a768d914b0 \
+ sha1 c0dbfaba2f1b24aa7d5484934e90cb118a830f1c \
+ rmd160 60a2336f09a861d5250403ece8208b94e41d1132 \
+ nonstd.tar.gz \
+ md5 d5e664da07b1f12f98c90a161cc77701 \
+ sha1 6e3cdb1c1e905bcf41cde2e4873678c1ae3bcdfc \
+ rmd160 0539a6c6843476fa69c20c4e99d01ad7928f5a6b
post-extract {
file rename ${workpath}/${name}-sources ${workpath}/${name}-${version}
@@ -62,26 +71,71 @@
set run_script "saved_acl2"
set run_script_nonstd "saved_acl2r"
-variant openmcl conflicts i386 {
+# 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 ppc {
+ 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:openmcl
+ depends_run-append port:ccl
- global heap_image
- global heap_image_nonstd
- set heap_image "saved_acl2.dppccl"
- set heap_image_nonstd "saved_acl2r.dppccl"
+ 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 { }
-variant regression { }
-variant nonstd { }
+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 openmcl]} {
- system "cd ${worksrcpath} && make large LISP=openmcl"
+build { if {[variant_isset ccl]} {
+ system "cd ${worksrcpath} && make large LISP=ccl"
if {[variant_isset nonstd]} {
- system "cd ${worksrcpath} && make large-acl2r LISP=openmcl"
+ system "cd ${worksrcpath} && make large-acl2r LISP=ccl"
}
} else {
system "cd ${worksrcpath} && make large LISP=sbcl"
@@ -95,15 +149,23 @@
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 openmcl]} {
+ if {[variant_isset ccl]} {
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 "${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"
@@ -119,10 +181,10 @@
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]} {
+ if {[variant_isset ccl]} {
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 "${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"
@@ -141,24 +203,23 @@
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 ${destroot}${prefix}/share/${name}/${version}/certify-books.log
+ 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 > ${clogfile} 2>&1"
+ system "cd ${destroot}/${target_path} && make certify-books 2>&1 | tee ${destroot}/${clogfile}"
}
if {[variant_isset regression]} {
- set rlogfile ${destroot}${prefix}/share/${name}/${version}/regression.log
+ 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 > ${rlogfile} 2>&1"
+ system "cd ${destroot}/${target_path} && make regression 2>&1 | tee ${destroot}/${rlogfile}"
if {[variant_isset nonstd]} {
- set rlogfile_nonstd ${destroot}${prefix}/share/${name}/${version}/regression-nonstd.log
+ 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 > ${rlogfile_nonstd} 2>&1"
+ system "cd ${destroot}/${target_path} && make ACL2=${destroot}${prefix}/share/${name}/${version}/saved_acl2r regression-nonstd 2>&1 | tee ${destroot}/${rlogfile_nonstd}"
}
}
@@ -166,10 +227,10 @@
file delete ${destroot}${prefix}/share/${name}/${version}/${run_script}
set script [open "${destroot}${prefix}/bin/acl2" w 755]
- if {[variant_isset openmcl]} {
+ if {[variant_isset ccl]} {
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 "${ccl_script} --eval \"(acl2::acl2-default-restart)\" --image-name ${target_path}/${heap_image}"
puts $script ""
} else {
puts $script "#!/bin/sh"
@@ -185,10 +246,10 @@
file delete ${destroot}${prefix}/share/${name}/${version}/${run_script_nonstd}
set script [open "${destroot}${prefix}/bin/acl2r" w 755]
- if {[variant_isset openmcl]} {
+ if {[variant_isset ccl]} {
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 "${ccl_script} --eval \"(acl2::acl2-default-restart)\" --image-name ${target_path}/${heap_image_nonstd}"
puts $script ""
} else {
puts $script "#!/bin/sh"
@@ -200,6 +261,16 @@
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}
+ }
}
-
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.macosforge.org/pipermail/macports-changes/attachments/20090407/07c84dfc/attachment-0001.html>
More information about the macports-changes
mailing list