;;; tojo-tokyo-guix-config --- Guix Channel for git.tojo.tokyo's package ;;; Copyright © 2021 Masaya Tojo ;;; ;;; 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 ;;; . (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.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+)))) (define-public python-regex-for-acl2-kernel (package (inherit python-regex) (name "python-regex") (version "2021.4.4") (source (origin (method url-fetch) (uri (pypi-uri "regex" version)) (sha256 (base32 "1yws1kqvw4krmdi519iry5jl1i2ihnr5n45wwkbljb4lkczkvfjj")))))) (define-public python-ipython-for-acl2-kernel (package (inherit python-ipython) (name "python-ipython") (version "7.15.0") (source (origin (method url-fetch) (uri (pypi-uri "ipython" version)) (sha256 (base32 "03hxazxq75z2ljsxmj6ffp534iy6hbff26mfsc69csl1g4w47w8f")))))) (define-public python-ipykernel-for-acl2-kernel (package (inherit python-ipykernel) (propagated-inputs `(("python-ipython" ,python-ipython-for-acl2-kernel) ("python-tornado" ,python-tornado-6) ("python-traitlets" ,python-traitlets) ;; imported at runtime during connect ("python-jupyter-client" ,python-jupyter-client))))) (define-public python-notebook-for-acl2-kernel (package (inherit python-notebook) (propagated-inputs `(("python-argon2-cffi" ,python-argon2-cffi) ("python-ipykernel" ,python-ipykernel-for-acl2-kernel) ("python-ipython-genutils" ,python-ipython-genutils) ("python-jinja2" ,python-jinja2) ("python-jupyter-client" ,python-jupyter-client) ("python-jupyter-core" ,python-jupyter-core) ("python-nbconvert" ,python-nbconvert) ("python-nbformat" ,python-nbformat) ("python-prometheus-client" ,python-prometheus-client) ("python-pyzmq" ,python-pyzmq) ("python-send2trash" ,python-send2trash) ("python-terminado" ,python-terminado) ("python-tornado" ,python-tornado-6) ("python-traitlets" ,python-traitlets))))) (define-public jupyter-acl2-kernel (package (name "jupyter-acl2-kernel") (version "0.2.8") (source (origin (method url-fetch) (uri (pypi-uri "acl2-kernel" version)) (sha256 (base32 "1g7j84w19kf3lfy8r4zbs3l3qr60ij5m4vfinbhf1crgm4whqarl")))) (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))))))) (propagated-inputs `(("python-ipykernel" ,python-ipykernel-for-acl2-kernel) ("python-ipython" ,python-ipython-for-acl2-kernel) ("python-jupyter-client" ,python-jupyter-client) ("python-pexpect" ,python-pexpect) ("python-regex" ,python-regex-for-acl2-kernel) ("python-notebook" ,python-notebook-for-acl2-kernel) ("acl2" ,acl2))) (home-page "https://github.com/tani/acl2-kernel") (synopsis "Jupyter Kernel for ACL2") (description "Jupyter Kernel for ACL2") (license license:bsd-3)))