diff options
| -rw-r--r-- | tojo-tokyo/packages/acl2.scm | 90 |
1 files changed, 90 insertions, 0 deletions
diff --git a/tojo-tokyo/packages/acl2.scm b/tojo-tokyo/packages/acl2.scm new file mode 100644 index 0000000..d948fe7 --- /dev/null +++ b/tojo-tokyo/packages/acl2.scm @@ -0,0 +1,90 @@ +;;; tojo-tokyo-guix-config --- Guix Channel for git.tojo.tokyo's package +;;; Copyright © 2021 Masaya Tojo <masaya@tojo.tokyo> +;;; +;;; This file is part of tojo-tokyo-guix-config. +;;; +;;; tojo-tokyo-guix-config is free software; you can redistribute +;;; it and/or modify it under the terms of the GNU General Public +;;; License as published by the Free Software Foundation; either +;;; version 3 of the License, or (at your option) any later version. +;;; +;;; tojo-tokyo-guix-config is distributed in the hope that it will +;;; be useful, but WITHOUT ANY WARRANTY; without even the implied +;;; warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. +;;; See the GNU General Public License for more details. +;;; +;;; You should have received a copy of the GNU General Public License +;;; along with extract-green-color. If not, see +;;; <http://www.gnu.org/licenses/>. + +(define-module (tojo-tokyo packages acl2) + #:use-module (guix packages) + #:use-module ((guix licenses) #:prefix license:) + #:use-module (guix download) + #:use-module (guix build-system gnu) + #:use-module (gnu packages) + #:use-module (gnu packages base) + #:use-module (gnu packages lisp) + #:use-module (gnu packages ruby) + #:use-module (gnu packages admin) + #:use-module (gnu packages perl)) + +(define-public acl2 + (package + (name "acl2") + (version "8.3") + (source (origin + (method url-fetch) + (uri + (string-append "https://github.com/acl2-devel/acl2-devel/releases/download/" + version + "/acl2-" + version ".tar.gz")) + (sha256 + (base32 + "1sn5y8bg2yf1kf8dzkrgk4iwzcd9qxpvk8nvy24zivxj6vdxvvj5")))) + (build-system gnu-build-system) + (arguments + `(#:phases + (modify-phases %standard-phases + (replace 'configure + (lambda _ + (substitute* '("./acl2-init.lisp" + "./books/build/make_cert_help.pl") + (("#!/bin/sh") (string-append "#!" (which "sh")))))) + (replace 'build + (lambda* (#:key outputs #:allow-other-keys) + (let* ((out (assoc-ref outputs "out")) + (acl2 (string-append out "/lib/acl2"))) + (mkdir-p acl2) + (copy-recursively "." acl2) + (chdir acl2) + (setenv "HOME" "/tmp") + (invoke "make" "LISP=sbcl") + (invoke "make" "basic" + "ACL2_HAS_HONS=1" + "ACL2_HAS_ANSI=1" + "ACL2_COMP_EXT=fasl" + "ACL2_HOST_LISP=SBCL" + "USE_QUICKLISP=0")))) + (delete 'check) + (replace 'install + (lambda* (#:key outputs #:allow-other-keys) + (let* ((out (assoc-ref outputs "out")) + (acl2 (string-append out "/lib/acl2")) + (bin (string-append out "/bin"))) + (mkdir-p bin) + (symlink (string-append acl2 "/saved_acl2") + (string-append bin "/acl2")))))))) + (native-inputs + `(("make" ,gnu-make) + ("perl" ,perl) + ("which" ,which))) + (inputs + `(("sbcl" ,sbcl))) + (synopsis "A Computational Logic for Applicative Common Lisp") + (description "ACL2 is a logic and programming language in which you can model computer systems, together with a tool to help you prove properties of those models. \"ACL2\" denotes \" Computational Logic for Applicative Common Lisp\".") + (home-page "https://www.cs.utexas.edu/users/moore/acl2/") + (license license:bsd-3 + ;; FIXME: add other licences + ))) |