<pre style='margin:0'>
Jackson Isaac (JacksonIsaac) pushed a commit to branch master
in repository macports-ports.
</pre>
<p><a href="https://github.com/macports/macports-ports/commit/5f96c4aae21e36d370bc0684b2c5d2e0d0d80ced">https://github.com/macports/macports-ports/commit/5f96c4aae21e36d370bc0684b2c5d2e0d0d80ced</a></p>
<pre style="white-space: pre; background: #F8F8F8"><span style='display:block; white-space:pre;color:#808000;'>commit 5f96c4aae21e36d370bc0684b2c5d2e0d0d80ced
</span>Author: ijackson <ijackson@macports.org>
AuthorDate: Fri Apr 13 00:58:15 2018 +0530
<span style='display:block; white-space:pre;color:#404040;'> acl2: Add modeline and update formatting
</span>---
math/acl2/Portfile | 481 +++++++++++++++++++++++++++--------------------------
1 file changed, 243 insertions(+), 238 deletions(-)
<span style='display:block; white-space:pre;color:#808080;'>diff --git a/math/acl2/Portfile b/math/acl2/Portfile
</span><span style='display:block; white-space:pre;color:#808080;'>index f7d961b..7cd55db 100644
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>--- a/math/acl2/Portfile
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ b/math/acl2/Portfile
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -1,57 +1,60 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-PortSystem 1.0
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-name acl2
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-version 3.5
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-set shortversion v3-5
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-categories math
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-maintainers nomaintainer
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-platforms darwin
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-description Applicative Common Lisp / A Computational Logic
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-long_description \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- ACL2 (Applicative Common Lisp / A Computational \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- Logic) is the successor to nqthm, the Boyer-Moore \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- theorem prover. \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- ACL2 can be used to automatically or semi-automatically \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- prove theorems and has been used extensively in real \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- applications (e.g., proving the correctness of certain \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- calculations in the floating point unit of the AMD K5 \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- microprocessor. \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- ACL2 is a very large, multipurpose system. \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- You can use it as a programming language, \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- a specification language, a modeling language, \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- a formal mathematical logic, or a semi-automatic \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- theorem prover. Because the meta-language is the same \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- as the language (a subset of Common Lisp), it is very \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- flexible.
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-#user_notes Users who want to use ACL2 for serious work should \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-# install the certify variant (sudo port install +certify), \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-# which will certify (i.e., prove all of the theorems) \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-# in the included examples. This can take several hours.
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-distfiles ${name}-${version}${extract.suffix}:sources \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- workshops-${version}${extract.suffix}:workshops \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- nonstd-${version}${extract.suffix}:nonstd
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-homepage http://www.cs.utexas.edu/users/moore/acl2/${shortversion}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-master_sites ${homepage}/distrib/:sources \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- ${homepage}/distrib/acl2-sources/books:workshops \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- ${homepage}/distrib/acl2-sources/books:nonstd
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-checksums acl2-${version}.tar.gz \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- md5 a2738f4582d14f74664c93dad93ac055 \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- sha1 d4052a49a3c2112eeb04cf97570e2caea8df38dd \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- rmd160 167b61cd8a812de804225096f4f3f04b87ba84cb \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- workshops-${version}.tar.gz \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- md5 5ae8123cadfe323c3088a3666112ce07 \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- sha1 b3a10d4cd876cb6ccde96920f0103ec0d89f7e2f \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- rmd160 63401f257b8b61564ed660681f82776c762d43da \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- nonstd-${version}.tar.gz \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- md5 7de68f04ee468e25b24a230507cdb663 \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- sha1 71e1da0cf417ef85f1002279b67227d729822a6e \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+# -*- 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
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+PortSystem 1.0
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+name acl2
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+version 3.5
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+set shortversion v3-5
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+categories math
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+maintainers nomaintainer
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+platforms darwin
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+description Applicative Common Lisp / A Computational Logic
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+long_description \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ ACL2 (Applicative Common Lisp / A Computational \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ Logic) is the successor to nqthm, the Boyer-Moore \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ theorem prover. \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ ACL2 can be used to automatically or semi-automatically \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ prove theorems and has been used extensively in real \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ applications (e.g., proving the correctness of certain \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ calculations in the floating point unit of the AMD K5 \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ microprocessor.\
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ ACL2 is a very large, multipurpose system. \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ You can use it as a programming language, \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ a specification language, a modeling language, \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ a formal mathematical logic, or a semi-automatic \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ theorem prover. Because the meta-language is the same \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ as the language (a subset of Common Lisp), it is very \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ flexible.
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+# user_notes Users who want to use ACL2 for serious work should
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+# install the certify variant (sudo port install +certify),
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+# which will certify (i.e., prove all of the theorems)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+# in the included examples. This can take several hours.
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+distfiles ${name}-${version}${extract.suffix}:sources \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ workshops-${version}${extract.suffix}:workshops \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ nonstd-${version}${extract.suffix}:nonstd
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+homepage http://www.cs.utexas.edu/users/moore/acl2/${shortversion}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+master_sites ${homepage}/distrib/:sources \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ ${homepage}/distrib/acl2-sources/books:workshops \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ ${homepage}/distrib/acl2-sources/books:nonstd
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+checksums acl2-${version}.tar.gz \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ md5 a2738f4582d14f74664c93dad93ac055 \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ sha1 d4052a49a3c2112eeb04cf97570e2caea8df38dd \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ rmd160 167b61cd8a812de804225096f4f3f04b87ba84cb \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ workshops-${version}.tar.gz \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ md5 5ae8123cadfe323c3088a3666112ce07 \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ sha1 b3a10d4cd876cb6ccde96920f0103ec0d89f7e2f \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ rmd160 63401f257b8b61564ed660681f82776c762d43da \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ nonstd-${version}.tar.gz \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ md5 7de68f04ee468e25b24a230507cdb663 \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ sha1 71e1da0cf417ef85f1002279b67227d729822a6e \
</span> rmd160 caa90d4a742fb1df8ddeb24686bc49a2d79754ab
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -63,47 +66,47 @@ checksums acl2-${version}.tar.gz \
</span> # MacPorts should always checksum the distribution files, instead
# of assuming that if a file's name is unchanged, the previously computed
# checksum is valid.
<span style='display:block; white-space:pre;background:#ffe0e0;'>-fetch {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- ui_msg "starting special fetch procedure for acl2"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- file mkdir ${distpath}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- if {![file exists ${distpath}/acl2-${version}.tar.gz]} {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- curl fetch http://www.cs.utexas.edu/users/moore/acl2/v3-5/distrib/acl2.tar.gz ${distpath}/acl2.tar.gz.TMP
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- file rename -force "${distpath}/acl2.tar.gz.TMP" "${distpath}/acl2-${version}.tar.gz"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- }
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- if {![file exists ${distpath}/workshops-${version}.tar.gz]} {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- curl fetch http://www.cs.utexas.edu/users/moore/acl2/v3-5/distrib/acl2-sources/books/workshops.tar.gz ${distpath}/workshops.tar.gz.TMP
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- file rename -force "${distpath}/workshops.tar.gz.TMP" "${distpath}/workshops-${version}.tar.gz"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- }
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- if {![file exists ${distpath}/nonstd-${version}.tar.gz]} {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- curl fetch http://www.cs.utexas.edu/users/moore/acl2/v3-5/distrib/acl2-sources/books/nonstd.tar.gz ${distpath}/nonstd.tar.gz.TMP
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- file rename -force "${distpath}/nonstd.tar.gz.TMP" "${distpath}/nonstd-${version}.tar.gz"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- }
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- ui_msg "completed special fetch procedure for acl2"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+fetch {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ ui_msg "starting special fetch procedure for acl2"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ file mkdir ${distpath}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ if {![file exists ${distpath}/acl2-${version}.tar.gz]} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ curl fetch http://www.cs.utexas.edu/users/moore/acl2/v3-5/distrib/acl2.tar.gz ${distpath}/acl2.tar.gz.TMP
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ file rename -force "${distpath}/acl2.tar.gz.TMP" "${distpath}/acl2-${version}.tar.gz"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ if {![file exists ${distpath}/workshops-${version}.tar.gz]} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ curl fetch http://www.cs.utexas.edu/users/moore/acl2/v3-5/distrib/acl2-sources/books/workshops.tar.gz ${distpath}/workshops.tar.gz.TMP
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ file rename -force "${distpath}/workshops.tar.gz.TMP" "${distpath}/workshops-${version}.tar.gz"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ if {![file exists ${distpath}/nonstd-${version}.tar.gz]} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ curl fetch http://www.cs.utexas.edu/users/moore/acl2/v3-5/distrib/acl2-sources/books/nonstd.tar.gz ${distpath}/nonstd.tar.gz.TMP
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ file rename -force "${distpath}/nonstd.tar.gz.TMP" "${distpath}/nonstd-${version}.tar.gz"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ ui_msg "completed special fetch procedure for acl2"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+}
</span>
<span style='display:block; white-space:pre;background:#ffe0e0;'>-post-extract {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- file rename ${workpath}/${name}-sources ${workpath}/${name}-${version}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- file rename ${workpath}/workshops ${workpath}/${name}-${version}/books
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- file rename ${workpath}/nonstd ${workpath}/${name}-${version}/books
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+post-extract {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ file rename ${workpath}/${name}-sources ${workpath}/${name}-${version}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ file rename ${workpath}/workshops ${workpath}/${name}-${version}/books
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ file rename ${workpath}/nonstd ${workpath}/${name}-${version}/books
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+}
</span>
<span style='display:block; white-space:pre;background:#ffe0e0;'>-use_configure no
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+use_configure no
</span>
<span style='display:block; white-space:pre;background:#ffe0e0;'>-depends_run port:sbcl
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+depends_run port:sbcl
</span>
<span style='display:block; white-space:pre;background:#ffe0e0;'>-set heap_image "saved_acl2.core"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-set heap_image_nonstd "saved_acl2r.core"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-set run_script "saved_acl2"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-set run_script_nonstd "saved_acl2r"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+set heap_image "saved_acl2.core"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+set heap_image_nonstd "saved_acl2r.core"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+set run_script "saved_acl2"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+set run_script_nonstd "saved_acl2r"
</span>
# There is no universal binary for acl2, because there is no universal
# build of sbcl or ccl.
#
<span style='display:block; white-space:pre;background:#ffe0e0;'>-universal_variant no
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+universal_variant no
</span>
# By converntion, the 64 bit version of Clozure CL is invoked by the
# script "ccl64"
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -111,7 +114,7 @@ universal_variant no
</span> # The ccl compiler produces a heap image whose filename extension depends
# on the platorm.
#
<span style='display:block; white-space:pre;background:#ffe0e0;'>-set ccl_script ccl
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+set ccl_script ccl
</span>
platform i386 {
global ccl_ext
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -146,161 +149,163 @@ platform ppc64 {
</span> variant emacs description {Include support for using acl2 under emacs} { }
variant ccl description {Use ccl as the underlying lisp} {
<span style='display:block; white-space:pre;background:#ffe0e0;'>- depends_run-delete port:sbcl
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- depends_run-append port:ccl
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ depends_run-delete port:sbcl
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ depends_run-append port:ccl
</span>
<span style='display:block; white-space:pre;background:#ffe0e0;'>- global heap_image
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- global heap_image_nonstd
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- set heap_image saved_acl2.${ccl_ext}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- set heap_image_nonstd saved_acl2r.${ccl_ext}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ global heap_image
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ global heap_image_nonstd
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ set heap_image saved_acl2.${ccl_ext}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ set heap_image_nonstd saved_acl2r.${ccl_ext}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+}
</span>
<span style='display:block; white-space:pre;background:#ffe0e0;'>-set target_path ${prefix}/share/${name}/${version}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+set target_path ${prefix}/share/${name}/${version}
</span>
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} { }
<span style='display:block; white-space:pre;background:#ffe0e0;'>-build { if {[variant_isset ccl]} {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- system "cd ${worksrcpath} && make large LISP=${prefix}/bin/ccl"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- if {[variant_isset nonstd]} {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- system "cd ${worksrcpath} && make large-acl2r LISP=${prefix}/bin/ccl"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- }
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- } else {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- system "cd ${worksrcpath} && make large LISP=${prefix}/bin/sbcl"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- if {[variant_isset nonstd]} {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- system "cd ${worksrcpath} && make large-acl2r LISP=${prefix}/bin/sbcl"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- }
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- }
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- }
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-destroot { file mkdir ${destroot}/${target_path}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- foreach f [glob -directory ${workpath}/${name}-${version} *] {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- file copy $f ${destroot}/${target_path}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- }
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- if {[variant_isset emacs]} {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- set emacs_target ${prefix}/share/emacs/site-lisp
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- file mkdir ${destroot}/${emacs_target}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- file copy ${destroot}/${target_path}/emacs/emacs-acl2.el ${destroot}/${emacs_target}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- file copy ${destroot}/${target_path}/emacs/monitor.el ${destroot}/${emacs_target}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- ui_msg "Emacs support files for acl2 are in ${emacs_target}"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- }
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- }
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-post-destroot { file delete ${destroot}${prefix}/share/${name}/${version}/${run_script}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- set script [open "${destroot}${prefix}/share/${name}/${version}/${run_script}" w 755]
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- if {[variant_isset ccl]} {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- puts $script "#!/bin/sh"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- puts $script "export ACL2_SYSTEM_BOOKS=${destroot}${prefix}/share/${name}/${version}/books"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- puts $script "${ccl_script} --eval \"(acl2::acl2-default-restart)\" --load ${destroot}${prefix}/share/${name}/${version}/cert_location --image-name ${destroot}/${target_path}/${heap_image}"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- puts $script ""
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- } else {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- puts $script "#!/bin/sh"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- puts $script "export ACL2_SYSTEM_BOOKS=${destroot}${prefix}/share/${name}/${version}/books"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- puts $script "sbcl --core ${destroot}/${target_path}/${heap_image} --userinit /dev/null --eval \'(acl2::sbcl-restart)\' --load ${destroot}${prefix}/share/${name}/${version}/cert_location"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- puts $script ""
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- }
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- close $script
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- system "chmod 755 ${destroot}${prefix}/share/${name}/${version}/${run_script}"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- if {[variant_isset nonstd]} {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- file delete ${destroot}${prefix}/share/${name}/${version}/${run_script_nonstd}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- set script [open "${destroot}${prefix}/share/${name}/${version}/${run_script_nonstd}" w 755]
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- if {[variant_isset ccl]} {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- puts $script "#!/bin/sh"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- puts $script "export ACL2_SYSTEM_BOOKS=${destroot}${prefix}/share/${name}/${version}/books"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 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}"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- puts $script ""
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- } else {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- puts $script "#!/bin/sh"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- puts $script "export ACL2_SYSTEM_BOOKS=${destroot}${prefix}/share/${name}/${version}/books"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 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"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- puts $script ""
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- }
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- close $script
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- system "chmod 755 ${destroot}${prefix}/share/${name}/${version}/${run_script_nonstd}"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- }
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- set script [open "${destroot}${prefix}/share/${name}/${version}/cert_location" w 755]
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- puts $script "(acl2::f-put-global \'acl2::old-certification-dir \"${destroot}${prefix}/share/${name}/${version}/books\" acl2::*the-live-state*)"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- puts $script "(acl2::f-put-global \'acl2::new-certification-dir \"${prefix}/share/${name}/${version}/books\" acl2::*the-live-state*)"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- close $script
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- if {[variant_isset certify]} {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- set clogfile ${prefix}/share/${name}/${version}/certify-books.log
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- ui_msg "certify-books log will be in ${clogfile}"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- system "cd ${destroot}/${target_path} && make clean-books"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- system "cd ${destroot}/${target_path} && make certify-books 2>&1 | tee ${destroot}/${clogfile}"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- }
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- if {[variant_isset regression]} {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- set rlogfile ${prefix}/share/${name}/${version}/regression.log
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- ui_msg "regression log will be in ${rlogfile}"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- system "cd ${destroot}/${target_path} && make clean-books"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- system "cd ${destroot}/${target_path} && make regression 2>&1 | tee ${destroot}/${rlogfile}"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- if {[variant_isset nonstd]} {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- set rlogfile_nonstd ${prefix}/share/${name}/${version}/regression-nonstd.log
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- ui_msg "regression-nonstd log will be in ${rlogfile_nonstd}"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- system "cd ${destroot}/${target_path} && make ACL2=${destroot}${prefix}/share/${name}/${version}/saved_acl2r regression-nonstd 2>&1 | tee ${destroot}/${rlogfile_nonstd}"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- }
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- }
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- file delete ${destroot}${prefix}/share/${name}/${version}/cert_location
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- file delete ${destroot}${prefix}/share/${name}/${version}/${run_script}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- set script [open "${destroot}${prefix}/bin/acl2" w 755]
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- if {[variant_isset ccl]} {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- puts $script "#!/bin/sh"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- puts $script "export ACL2_SYSTEM_BOOKS=${prefix}/share/${name}/${version}/books"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- puts $script "${ccl_script} --eval \"(acl2::acl2-default-restart)\" --image-name ${target_path}/${heap_image}"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- puts $script ""
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- } else {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- puts $script "#!/bin/sh"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- puts $script "export ACL2_SYSTEM_BOOKS=${prefix}/share/${name}/${version}/books"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- puts $script "sbcl --core ${target_path}/${heap_image} --userinit /dev/null --eval \'(acl2::sbcl-restart)\'"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- puts $script ""
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- }
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- close $script
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- system "chmod 755 ${destroot}${prefix}/bin/acl2"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- if {[variant_isset nonstd]} {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- file delete ${destroot}${prefix}/share/${name}/${version}/${run_script_nonstd}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- set script [open "${destroot}${prefix}/bin/acl2r" w 755]
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- if {[variant_isset ccl]} {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- puts $script "#!/bin/sh"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- puts $script "export ACL2_SYSTEM_BOOKS=${prefix}/share/${name}/${version}/books"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- puts $script "${ccl_script} --eval \"(acl2::acl2-default-restart)\" --image-name ${target_path}/${heap_image_nonstd}"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- puts $script ""
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- } else {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- puts $script "#!/bin/sh"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- puts $script "export ACL2_SYSTEM_BOOKS=${prefix}/share/${name}/${version}/books"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- puts $script "sbcl --core ${target_path}/${heap_image_nonstd} --userinit /dev/null --eval \'(acl2::sbcl-restart)\'"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- puts $script ""
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- }
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- close $script
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- system "chmod 755 ${destroot}${prefix}/bin/acl2r"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- }
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-# Now remove all of the .out and build directory certificate files,
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-# and rename the final (installation directory) certificates:
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- foreach out_file [exec find ${destroot}/${target_path} -name "\*.out"] {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- file delete ${out_file}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- }
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- foreach cert_file [exec find ${destroot}/${target_path} -name "\*.cert"] {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- file delete ${cert_file}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- file rename ${cert_file}.final ${cert_file}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- }
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+build {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ if {[variant_isset ccl]} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ system "cd ${worksrcpath} && make large LISP=${prefix}/bin/ccl"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ if {[variant_isset nonstd]} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ system "cd ${worksrcpath} && make large-acl2r LISP=${prefix}/bin/ccl"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ } else {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ system "cd ${worksrcpath} && make large LISP=${prefix}/bin/sbcl"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ if {[variant_isset nonstd]} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ system "cd ${worksrcpath} && make large-acl2r LISP=${prefix}/bin/sbcl"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+destroot {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ file mkdir ${destroot}/${target_path}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ foreach f [glob -directory ${workpath}/${name}-${version} *] {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ file copy $f ${destroot}/${target_path}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ if {[variant_isset emacs]} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ set emacs_target ${prefix}/share/emacs/site-lisp
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ file mkdir ${destroot}/${emacs_target}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ file copy ${destroot}/${target_path}/emacs/emacs-acl2.el ${destroot}/${emacs_target}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ file copy ${destroot}/${target_path}/emacs/monitor.el ${destroot}/${emacs_target}
</span>
<span style='display:block; white-space:pre;background:#e0ffe0;'>+ ui_msg "Emacs support files for acl2 are in ${emacs_target}"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+post-destroot {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ file delete ${destroot}${prefix}/share/${name}/${version}/${run_script}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ set script [open "${destroot}${prefix}/share/${name}/${version}/${run_script}" w 755]
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ if {[variant_isset ccl]} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ puts $script "#!/bin/sh"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ puts $script "export ACL2_SYSTEM_BOOKS=${destroot}${prefix}/share/${name}/${version}/books"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ puts $script "${ccl_script} --eval \"(acl2::acl2-default-restart)\" --load ${destroot}${prefix}/share/${name}/${version}/cert_location --image-name ${destroot}/${target_path}/${heap_image}"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ puts $script ""
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ } else {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ puts $script "#!/bin/sh"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ puts $script "export ACL2_SYSTEM_BOOKS=${destroot}${prefix}/share/${name}/${version}/books"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ puts $script "sbcl --core ${destroot}/${target_path}/${heap_image} --userinit /dev/null --eval \'(acl2::sbcl-restart)\' --load ${destroot}${prefix}/share/${name}/${version}/cert_location"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ puts $script ""
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ close $script
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ system "chmod 755 ${destroot}${prefix}/share/${name}/${version}/${run_script}"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ if {[variant_isset nonstd]} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ file delete ${destroot}${prefix}/share/${name}/${version}/${run_script_nonstd}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ set script [open "${destroot}${prefix}/share/${name}/${version}/${run_script_nonstd}" w 755]
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ if {[variant_isset ccl]} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ puts $script "#!/bin/sh"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ puts $script "export ACL2_SYSTEM_BOOKS=${destroot}${prefix}/share/${name}/${version}/books"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 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}"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ puts $script ""
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ } else {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ puts $script "#!/bin/sh"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ puts $script "export ACL2_SYSTEM_BOOKS=${destroot}${prefix}/share/${name}/${version}/books"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 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"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ puts $script ""
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ close $script
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ system "chmod 755 ${destroot}${prefix}/share/${name}/${version}/${run_script_nonstd}"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ set script [open "${destroot}${prefix}/share/${name}/${version}/cert_location" w 755]
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ puts $script "(acl2::f-put-global \'acl2::old-certification-dir \"${destroot}${prefix}/share/${name}/${version}/books\" acl2::*the-live-state*)"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ puts $script "(acl2::f-put-global \'acl2::new-certification-dir \"${prefix}/share/${name}/${version}/books\" acl2::*the-live-state*)"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ close $script
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ if {[variant_isset certify]} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ set clogfile ${prefix}/share/${name}/${version}/certify-books.log
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ ui_msg "certify-books log will be in ${clogfile}"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ system "cd ${destroot}/${target_path} && make clean-books"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ system "cd ${destroot}/${target_path} && make certify-books 2>&1 | tee ${destroot}/${clogfile}"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ if {[variant_isset regression]} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ set rlogfile ${prefix}/share/${name}/${version}/regression.log
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ ui_msg "regression log will be in ${rlogfile}"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ system "cd ${destroot}/${target_path} && make clean-books"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ system "cd ${destroot}/${target_path} && make regression 2>&1 | tee ${destroot}/${rlogfile}"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ if {[variant_isset nonstd]} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ set rlogfile_nonstd ${prefix}/share/${name}/${version}/regression-nonstd.log
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ ui_msg "regression-nonstd log will be in ${rlogfile_nonstd}"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ system "cd ${destroot}/${target_path} && make ACL2=${destroot}${prefix}/share/${name}/${version}/saved_acl2r regression-nonstd 2>&1 | tee ${destroot}/${rlogfile_nonstd}"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ file delete ${destroot}${prefix}/share/${name}/${version}/cert_location
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ file delete ${destroot}${prefix}/share/${name}/${version}/${run_script}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ set script [open "${destroot}${prefix}/bin/acl2" w 755]
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ if {[variant_isset ccl]} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ puts $script "#!/bin/sh"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ puts $script "export ACL2_SYSTEM_BOOKS=${prefix}/share/${name}/${version}/books"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ puts $script "${ccl_script} --eval \"(acl2::acl2-default-restart)\" --image-name ${target_path}/${heap_image}"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ puts $script ""
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ } else {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ puts $script "#!/bin/sh"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ puts $script "export ACL2_SYSTEM_BOOKS=${prefix}/share/${name}/${version}/books"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ puts $script "sbcl --core ${target_path}/${heap_image} --userinit /dev/null --eval \'(acl2::sbcl-restart)\'"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ puts $script ""
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ close $script
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ system "chmod 755 ${destroot}${prefix}/bin/acl2"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ if {[variant_isset nonstd]} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ file delete ${destroot}${prefix}/share/${name}/${version}/${run_script_nonstd}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ set script [open "${destroot}${prefix}/bin/acl2r" w 755]
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ if {[variant_isset ccl]} {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ puts $script "#!/bin/sh"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ puts $script "export ACL2_SYSTEM_BOOKS=${prefix}/share/${name}/${version}/books"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ puts $script "${ccl_script} --eval \"(acl2::acl2-default-restart)\" --image-name ${target_path}/${heap_image_nonstd}"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ puts $script ""
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ } else {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ puts $script "#!/bin/sh"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ puts $script "export ACL2_SYSTEM_BOOKS=${prefix}/share/${name}/${version}/books"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ puts $script "sbcl --core ${target_path}/${heap_image_nonstd} --userinit /dev/null --eval \'(acl2::sbcl-restart)\'"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ puts $script ""
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ close $script
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ system "chmod 755 ${destroot}${prefix}/bin/acl2r"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # Now remove all of the .out and build directory certificate files,
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # and rename the final (installation directory) certificates:
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ foreach out_file [exec find ${destroot}/${target_path} -name "\*.out"] {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ file delete ${out_file}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ foreach cert_file [exec find ${destroot}/${target_path} -name "\*.cert"] {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ file delete ${cert_file}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ file rename ${cert_file}.final ${cert_file}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+}
</span></pre><pre style='margin:0'>
</pre>