From 9c084f62ea005299eba514bdeda799d3bf48188a Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Sun, 29 Aug 2021 20:06:44 +0900
Subject: acl2: Update.

---
 tojo-tokyo/packages/acl2.scm | 32 ++++++++++++++++++++++++--------
 1 file changed, 24 insertions(+), 8 deletions(-)

(limited to 'tojo-tokyo/packages')

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