aboutsummaryrefslogtreecommitdiff
path: root/tojo-tokyo/packages
diff options
context:
space:
mode:
authorMasaya Tojo <masaya@tojo.tokyo>2021-07-31 03:04:25 +0900
committerMasaya Tojo <masaya@tojo.tokyo>2021-07-31 11:22:28 +0900
commit30ec829df2fae26dd03c6ad383ad8190acad6251 (patch)
treedebb3e92c3004a90b39bd5a70690b51e0ff8a357 /tojo-tokyo/packages
parent69e4b8dcaedfeafdac27057edbe785cfe168a067 (diff)
Add acl2.
Diffstat (limited to 'tojo-tokyo/packages')
-rw-r--r--tojo-tokyo/packages/acl2.scm90
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
+ )))