aboutsummaryrefslogtreecommitdiff
path: root/tojo-tokyo/packages
diff options
context:
space:
mode:
Diffstat (limited to 'tojo-tokyo/packages')
-rw-r--r--tojo-tokyo/packages/acl2.scm32
1 files changed, 24 insertions, 8 deletions
diff --git a/tojo-tokyo/packages/acl2.scm b/tojo-tokyo/packages/acl2.scm
index d948fe7..ad73c35 100644
--- a/tojo-tokyo/packages/acl2.scm
+++ b/tojo-tokyo/packages/acl2.scm
@@ -27,6 +27,7 @@
#: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
@@ -51,7 +52,11 @@
(lambda _
(substitute* '("./acl2-init.lisp"
"./books/build/make_cert_help.pl")
- (("#!/bin/sh") (string-append "#!" (which "sh"))))))
+ (("#!/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"))
@@ -60,8 +65,15 @@
(copy-recursively "." acl2)
(chdir acl2)
(setenv "HOME" "/tmp")
- (invoke "make" "LISP=sbcl")
- (invoke "make" "basic"
+ (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" "all"
+ (string-append "ACL2=" (string-append acl2 "/saved_acl2"))
+ "-j" "8"
"ACL2_HAS_HONS=1"
"ACL2_HAS_ANSI=1"
"ACL2_COMP_EXT=fasl"
@@ -75,16 +87,20 @@
(bin (string-append out "/bin")))
(mkdir-p bin)
(symlink (string-append acl2 "/saved_acl2")
- (string-append bin "/acl2"))))))))
+ (string-append bin "/acl2"))
+ #t))))))
(native-inputs
`(("make" ,gnu-make)
("perl" ,perl)
- ("which" ,which)))
+ ("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/")
- (license license:bsd-3
- ;; FIXME: add other licences
- )))
+ ;; XXX: still checking
+ (license (list license:bsd-3
+ license:expat
+ license:gpl2+))))