# $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}
		  }
		}