blob: b7f229bb8e150fcd07c4d74db67ae339cb515034 (
about) (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
|
;;; 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 check)
#: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"))))
;; XXX: oracle-time-tests.lisp will fail when use libfaketime.
(delete-file "./books/tools/oracle-time-tests.lisp")
#t))
(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")
(setenv "TZ" "UTC")
;; XXX: Avoid BOOK-HASH-MISMATCH.
(invoke "faketime" "-f" "1970-01-01 00:00:01"
"make" "LISP=sbcl")
(invoke "faketime" "-f" "1970-01-01 00:00:01"
"make" "basic"
(string-append "ACL2=" (string-append acl2 "/saved_acl2"))
"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"))
#t))))))
(native-inputs
`(("make" ,gnu-make)
("perl" ,perl)
("which" ,which)
("inetutils" ,inetutils)
("libfaketime" ,libfaketime)))
(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/")
;; XXX: still checking
(license (list license:bsd-3
license:expat
license:gpl2+))))
|
