# $Id$ PortSystem 1.0 name acl2 version 3.5 set shortversion v3-5 categories math maintainers nomaintainer platforms 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} } }