casa-mp-base

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

set shortversion    v8-2

​

checksums           md5     1291723299cad53df3d01029e0e838a4 \

                    sha1    bf52a2d7d879115fbcb3d97a6a206ea1f9be723c \

                    rmd160  6d3e2e5dfceef8fc26cb4a9396f84b3190dbab46 \

                    sha256  83b34b649c3b0448cd3be903d3dd0706bbb7c9a732709106844fbfeaa4d5d435 \

                    size    80214015

​

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