diff options
| author | Masaya Tojo <masaya@tojo.tokyo> | 2021-08-29 20:06:44 +0900 |
|---|---|---|
| committer | Masaya Tojo <masaya@tojo.tokyo> | 2021-08-29 20:06:44 +0900 |
| commit | 9c084f62ea005299eba514bdeda799d3bf48188a (patch) | |
| tree | ba6dd0e953e509ea87fa1195c35a030624f38813 | |
| parent | 30ec829df2fae26dd03c6ad383ad8190acad6251 (diff) | |
acl2: Update.
| -rw-r--r-- | tojo-tokyo/packages/acl2.scm | 32 |
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+)))) |