# -*- 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

PortSystem          1.0
PortGroup           github 1.0

name                acl2
version             8.3
set shortversion    v8-3

checksums           rmd160  e23fa1c10ce504ce3033c69853966ac553ef71ac \
                    sha256  45eedddb36b2eff889f0dba2b96fc7a9b1cf23992fcfdf909bc179f116f2c5ea \
                    size    116808616

github.setup        acl2-devel ${name}-devel ${version}
github.tarball_from releases

license             BSD
categories          math

maintainers         {ijackson @JacksonIsaac} openmaintainer
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.

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.
"

homepage            http://www.cs.utexas.edu/users/moore/acl2/${shortversion}
distname            ${name}-${version}

use_configure           no

depends_lib             path:bin/sbcl: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 darwin i386 {
    if {${build_arch} eq "i386"} {
        global ccl_ext
        set ccl_ext dx86cl
    }

    if {${build_arch} eq "x86_64"} {
        global ccl_ext
        set ccl_ext dx86cl64

        global ccl_script
        set ccl_script ccl64
    }
}

platform darwin powerpc {
    if {${build_arch} eq "powerpc"} {
        global ccl_ext
        set ccl_ext dppccl
    }

    if {${build_arch} eq "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_lib-delete    path:bin/sbcl:sbcl
    depends_lib-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 LISP=${prefix}/bin/${ccl_script}"
        if {[variant_isset nonstd]} {
            system "cd ${worksrcpath} && make large-acl2r LISP=${prefix}/bin/${ccl_script}"
        }
    } else {
        system "cd ${worksrcpath} && make 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}/${worksrcdir} *] {
        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}
    }
}

if {[variant_isset nonstd] && ![variant_isset ccl]} {
    # acl2r raises error when build against sbcl.
    # Even upstream uses ccl by default
    # The following note will intimate the user to pass +ccl
    # variant along with +nonstd if they face errors.
    notes-append " \n"
    notes-append "acl2r might raise heap memory errors for some users when using sbcl backend.
Please install +nonstd with +ccl variant to use acl2r, if you face any errors.
"
}