diff options
Diffstat (limited to 'tojo-tokyo/packages')
| -rw-r--r-- | tojo-tokyo/packages/acl2.scm | 160 |
1 files changed, 0 insertions, 160 deletions
diff --git a/tojo-tokyo/packages/acl2.scm b/tojo-tokyo/packages/acl2.scm deleted file mode 100644 index d57032a..0000000 --- a/tojo-tokyo/packages/acl2.scm +++ /dev/null @@ -1,160 +0,0 @@ -;;; tojo-tokyo-guix-config --- Guix Channel for git.tojo.tokyo's package -;;; Copyright © 2021, 2022 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) - - ;; For ACL2 Kernel - #:use-module (gnu packages python) - #:use-module (gnu packages python-xyz) - #:use-module (gnu packages python-web) - #:use-module (gnu packages python-crypto) - #:use-module (gnu packages monitoring) - #:use-module (guix build-system python)) - -(define-public acl2 - (package - (name "acl2") - (version "8.5") - (source (origin - (method url-fetch) - (uri - (string-append "https://github.com/acl2-devel/acl2-devel/releases/download/" - version - "/acl2-" - version ".tar.gz")) - (sha256 - (base32 - "03xw9qyqvp3mmcx8yli6bc7gy0znv1kmm7nd607vj9q04aq8mhfw")))) - (build-system gnu-build-system) - (arguments - `(#:tests? #f - #: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") - (chdir "books") - (invoke "faketime" "-f" "1970-01-01 00:00:01" - "make" - "basic" - "system" - (string-append "ACL2=" (string-append acl2 "/saved_acl2")) - "ACL2_HAS_HONS=1" - "ACL2_HAS_ANSI=1" - "ACL2_COMP_EXT=fasl" - "ACL2_HOST_LISP=CCL" - "USE_QUICKLISP=0")))) - (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 - `(("ccl" ,ccl))) - (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+)))) - -(define-public python-acl2-kernel - (package - (name "python-acl2-kernel") - (version "0.2.8") - ;; XXX: Using a modified versions of the dependent packages for use with Guix. - ;; Commit: https://github.com/tojoqk/acl2-kernel/commit/9c36a01f46f58628585e87101db9da61cab42891 - (source (origin - (method url-fetch) - (uri - (string-append "http://files.tojo.tokyo/acl2-kernel-for-guix/acl2-kernel-for-guix-" - version - ".tar.gz")) - (sha256 - (base32 - "0ljg4bjafvfgqx7cwc026yw3w15k3yj7bilbl6sjk6cpdhpkbaa6")))) - (build-system python-build-system) - (arguments - `(#:tests? #f - #:phases - (modify-phases %standard-phases - (add-after 'install 'install-kernel - (lambda* (#:key inputs outputs #:allow-other-keys) - (setenv "HOME" "/tmp") - (invoke "python3" "-m" "acl2_kernel.install" - (string-append "--acl2=" (string-append (assoc-ref inputs "acl2") - "/bin/acl2"))) - (let ((kernel-src "/tmp/.local/share/jupyter/kernels/acl2/kernel.json") - (kernel-dst (string-append (assoc-ref outputs "out") - "/share/jupyter/kernels/acl2"))) - (install-file kernel-src kernel-dst) - #t)))))) - (propagated-inputs - `(("python-ipykernel" ,python-ipykernel) - ("python-ipython" ,python-ipython) - ("python-jupyter-client" ,python-jupyter-client) - ("python-pexpect" ,python-pexpect) - ("python-regex" ,python-regex) - ("python-notebook" ,python-notebook) - ("acl2" ,acl2))) - (home-page "https://github.com/tani/acl2-kernel") - (synopsis "Jupyter Kernel for ACL2") - (description "Jupyter Kernel for ACL2") - (license license:bsd-3))) |