From 30ec829df2fae26dd03c6ad383ad8190acad6251 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Sat, 31 Jul 2021 03:04:25 +0900
Subject: Add acl2.

---
 tojo-tokyo/packages/acl2.scm | 90 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 90 insertions(+)
 create mode 100644 tojo-tokyo/packages/acl2.scm

(limited to 'tojo-tokyo/packages')

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
+             )))
-- 
cgit v1.2.3