# $Id$

PortSystem 1.0
name		acl2
version		3.2
set shortversion	v3-2
categories	math
maintainers	gwright@macports.org
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.	\
#		(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

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.tar.gz      md5 406a6349fb20483fd2b75f21f984157e \
		workshops.tar.gz md5 218a53abcbb53bac3c286c28df9ee0ad \
		nonstd.tar.gz    md5 58b6f12ec3b68cf6c0ba30b8bd040d4b

post-extract	{ cd ${workpath}
		  file rename ${name}-sources ${name}-${version}
		  file rename workshops ${name}-${version}/books
		  file rename nonstd    ${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"

variant openmcl	conflicts i386 {
		  depends_run-delete	port:sbcl
		  depends_run-append	port:openmcl

		  global heap_image
		  global heap_image_nonstd
		  set heap_image	"saved_acl2.dppccl"
		  set heap_image_nonstd	"saved_acl2r.dppccl"
		}

set target_path	${prefix}/share/${name}/${version}

variant certify    { }
variant regression { }
variant nonstd	   { }

build		{ if {[variant_isset openmcl]} {
		         cd ${worksrcpath}
			 system "make large LISP=openmcl"
			 if {[variant_isset nonstd]} {
		  	         system "make large-acl2r LISP=openmcl"
			 }
		  } else {
		         cd ${worksrcpath}
			 system "make large LISP=sbcl"
			 if {[variant_isset nonstd]} {
			         system "make large-acl2r LISP=sbcl"
			 }
		  }
		}

destroot	{ file mkdir ${destroot}/${target_path}
		  foreach f [glob -directory ${workpath}/${name}-${version} *] {
			file copy $f ${destroot}/${target_path}
		  }
		}

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]} {
		  	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 ""
		  } 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 openmcl]} {
		  	       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 ""
		  	} 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]} { 
			cd ${destroot}/${target_path}
			set clogfile ${destroot}${prefix}/share/${name}/${version}/certify-books.log
			ui_msg "certify-books log will be in ${clogfile}"
			system "make clean-books"
			system "make certify-books > ${clogfile} 2>&1"
		  }

 		  if {[variant_isset regression]} {
			cd ${destroot}/${target_path}
			set rlogfile ${destroot}${prefix}/share/${name}/${version}/regression.log
			ui_msg "regression log will be in ${rlogfile}"
			system "make clean-books"
			system "make regression > ${rlogfile} 2>&1"

			if {[variant_isset nonstd]} {
			        set rlogfile_nonstd ${destroot}${prefix}/share/${name}/${version}/regression-nonstd.log
			        ui_msg "regression-nonstd log will be in ${rlogfile_nonstd}"
				system "make ACL2=${destroot}${prefix}/share/${name}/${version}/saved_acl2r regression-nonstd > ${rlogfile_nonstd} 2>&1"
			}
		  }

		  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 openmcl]} {
		  	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 ""
		  } 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 openmcl]} {
		  	        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 ""
		 	} 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"
		   }
		}