Add GUIX package definition for ACL2 running SBCL

.guix-channel

@@ -0,0 +1,18 @@
+;;; GUIX channel definition for ACL2 packages
+;;;
+;;; To use this channel, add it to your ~/.config/guix/channels.scm:
+;;;
+;;; (cons* (channel
+;;;          (name 'acl2-channel)
+;;;          (url "https://github.com/jimwhite/acl2-docker.git")
+;;;          (branch "main"))
+;;;        %default-channels)
+
+;; This file marks this repository as a GUIX channel
+(channel
+  (version 0)
+  (dependencies 
+   (channel
+    (name guix)
+    (url "https://git.savannah.gnu.org/git/guix.git")
+    (minimum-guix "1.4.0"))))

GUIX-README.md

@@ -0,0 +1,115 @@
+# ACL2 GUIX Package
+
+This directory contains a GUIX package definition for ACL2 (A Computational Logic for Applicative Common Lisp) running on SBCL (Steel Bank Common Lisp).
+
+## Files
+
+- `acl2.scm` - Main GUIX package definition for ACL2
+- `manifest.scm` - GUIX manifest for easy installation
+- `.guix-channel` - Channel definition to use this repo as a GUIX channel
+
+## Usage
+
+### Method 1: Using the package definition directly
+
+```bash
+# build ACL2 using the local package definition
+guix build -f acl2.scm
+guix install acl2
+
+# Or create a development environment
+guix shell -f acl2.scm
+```
+
+### Method 2: Using the manifest
+
+```bash
+# Install using the manifest
+guix install -m manifest.scm
+
+# Or create a development environment
+guix shell -m manifest.scm
+```
+
+### Method 3: Using as a GUIX channel
+
+1. Add this repository to your `~/.config/guix/channels.scm`:
+
+```scheme
+(cons* (channel
+         (name 'acl2-channel)
+         (url "https://github.com/jimwhite/acl2-docker.git")
+         (branch "main"))
+       %default-channels)
+```
+
+2. Update your channels:
+
+```bash
+guix pull
+```
+
+3. Install ACL2:
+
+```bash
+guix install acl2
+```
+
+## Package Details
+
+The GUIX package:
+
+- Downloads ACL2 source from the official GitHub repository
+- Builds ACL2 using SBCL as the underlying Lisp implementation
+- Certifies the "basic" book collection during build
+- Installs ACL2 executable and support scripts (cert.pl, clean.pl, critpath.pl)
+- Sets up proper environment variables for ACL2_SYSTEM_BOOKS
+
+## Environment Variables
+
+After installation, the following environment variables are recommended:
+
+- `ACL2_SYSTEM_BOOKS` - Points to the installed books directory
+- `ACL2` - Points to the ACL2 executable
+
+These are automatically set when using the `acl2-wrapper` script.
+
+## Comparison with Docker Build
+
+This GUIX package provides the same functionality as the Docker build in this repository:
+
+- Uses SBCL 2.5.3+ as the Lisp implementation
+- Downloads latest ACL2 from GitHub
+- Builds with `make LISP="sbcl"`
+- Certifies basic books with parallel jobs
+- Sets up proper paths and environment
+
+## Building from Source
+
+To build the package from source:
+
+```bash
+guix build -f acl2.scm
+```
+
+## Testing
+
+After installation, you can test ACL2:
+
+```bash
+# Start ACL2 REPL
+acl2
+
+# Or use the wrapper with proper environment
+acl2-wrapper
+
+# Test with a simple example
+echo "(+ 1 2 3)" | acl2-wrapper
+```
+
+## Notes
+
+- The package builds ACL2 with SBCL's default configuration
+- Book certification is done with 4 parallel jobs during build
+- The installation includes certified basic books for immediate use
+- Additional books can be certified using the included cert.pl script

README.md

@@ -4,6 +4,10 @@
 
 This image is available on Docker Hub under [`atwalter/acl2`](https://hub.docker.com/r/atwalter/acl2/) and on the GitHub Container Registry under [`mister-walter/acl2`](https://ghcr.io/mister-walter/acl2).
 
+## GUIX Package
+
+In addition to the Docker image, this repository now provides a GUIX package definition for ACL2 running on SBCL. See [`GUIX-README.md`](GUIX-README.md) for details on how to install and use ACL2 via GUIX.
+
 ## Apple Silicon Macs
 
 This image is now built and distributed as a multi-platform Docker image. This means that both a `linux/amd64` and `linux/arm64` version of the image are built, and Docker should automatically use the appropriate version for your computer's architecture.

acl2.scm

@@ -0,0 +1,144 @@
+;;; ACL2 GUIX package definition
+;;; This package provides ACL2 theorem prover running on SBCL
+
+(define-module (acl2)
+  #:use-module (guix packages)
+  #:use-module (guix download)
+  #:use-module (guix git-download)
+  #:use-module (guix build-system gnu)
+  #:use-module (guix utils)
+  #:use-module ((guix licenses) #:prefix license:)
+  #:use-module (gnu packages)
+  #:use-module (gnu packages autotools)
+  #:use-module (gnu packages base)
+  #:use-module (gnu packages compression)
+  #:use-module (gnu packages curl)
+  #:use-module (gnu packages lisp)
+  #:use-module (gnu packages perl)
+  #:use-module (gnu packages pkg-config)
+  #:use-module (gnu packages tls)
+  #:use-module (gnu packages version-control))
+
+(define-public acl2
+  (package
+    (name "acl2")
+    ;; Use a recent stable commit from ACL2 repository
+    ;; This should be updated to match the latest stable release
+    (version "8.6")
+    (source
+     (origin
+              (method url-fetch)
+              (uri
+               (string-append "https://github.com/acl2-devel/acl2-devel/releases/download/"
+                              version
+                              "/acl2-"
+                              version ".tar.gz"))
+              (sha256
+               (base32
+                "0nahdm00wh2gs5lybx487s70y2qigriklv1k6jy51jysnryf9xh3"))))
+    (build-system gnu-build-system)
+    (native-inputs
+     (list autoconf
+           automake
+           curl
+           git
+           gnu-make
+           perl
+           pkg-config
+           zlib
+           zstd))
+    (inputs
+     (list sbcl
+           openssl))
+    (arguments
+     `(#:tests? #f ; No test suite
+       #:make-flags (list (string-append "LISP=sbcl"))
+       #:phases
+       (modify-phases %standard-phases
+         (delete 'configure) ; No configure script
+         (add-after 'unpack 'prepare-build
+           (lambda* (#:key outputs #:allow-other-keys)
+             (let ((out (assoc-ref outputs "out")))
+               ;; Set up build environment
+               (setenv "CERT_PL_RM_OUTFILES" "1")
+               #t)))
+         (replace 'build
+           (lambda* (#:key make-flags #:allow-other-keys)
+             ;; Build ACL2 executable
+             (apply invoke "make" make-flags)))
+         (add-after 'build 'certify-books
+           (lambda* (#:key outputs #:allow-other-keys)
+             (let ((out (assoc-ref outputs "out")))
+               ;; Certify basic books
+               (with-directory-excursion "books"
+                 (invoke "make" "basic"
+                         (string-append "ACL2=" (getcwd) "/../saved_acl2")
+                         "-j" "4"))
+               #t)))
+         (replace 'install
+           (lambda* (#:key outputs #:allow-other-keys)
+             (let* ((out (assoc-ref outputs "out"))
+                    (bin (string-append out "/bin"))
+                    (share (string-append out "/share/acl2"))
+                    (books (string-append share "/books"))
+                    (doc (string-append out "/share/doc/acl2")))
+
+               ;; Create directories
+               (mkdir-p bin)
+               (mkdir-p share)
+               (mkdir-p doc)
+
+               ;; Install ACL2 executable
+               (copy-file "saved_acl2" (string-append bin "/acl2"))
+               (chmod (string-append bin "/acl2") #o755)
+
+               ;; Install books and support files
+               (copy-recursively "books" books)
+
+               ;; Install build scripts if they exist
+               (when (file-exists? "books/build/cert.pl")
+                 (copy-file "books/build/cert.pl" (string-append bin "/cert.pl"))
+                 (chmod (string-append bin "/cert.pl") #o755))
+               (when (file-exists? "books/build/clean.pl")
+                 (copy-file "books/build/clean.pl" (string-append bin "/clean.pl"))
+                 (chmod (string-append bin "/clean.pl") #o755))
+               (when (file-exists? "books/build/critpath.pl")
+                 (copy-file "books/build/critpath.pl" (string-append bin "/critpath.pl"))
+                 (chmod (string-append bin "/critpath.pl") #o755))
+
+               ;; Install documentation if it exists
+               (when (file-exists? "doc")
+                 (copy-recursively "doc" (string-append doc "/doc")))
+               (when (file-exists? "README")
+                 (copy-file "README" (string-append doc "/README")))
+               (when (file-exists? "LICENSE")
+                 (copy-file "LICENSE" (string-append doc "/LICENSE")))
+
+               #t)))
+         (add-after 'install 'wrap-program
+           (lambda* (#:key outputs #:allow-other-keys)
+             (let* ((out (assoc-ref outputs "out"))
+                    (bin (string-append out "/bin"))
+                    (share (string-append out "/share/acl2"))
+                    (books (string-append share "/books")))
+               ;; Create wrapper script that sets up environment variables
+               (with-output-to-file (string-append bin "/acl2-wrapper")
+                 (lambda ()
+                   (format #t "#!/bin/sh~%")
+                   (format #t "export ACL2_SYSTEM_BOOKS=~s~%" books)
+                   (format #t "export ACL2=~s~%" (string-append bin "/acl2"))
+                   (format #t "exec ~s \"$@\"~%" (string-append bin "/acl2"))))
+               (chmod (string-append bin "/acl2-wrapper") #o755)
+               #t))))))
+    (home-page "https://www.cs.utexas.edu/users/moore/acl2/")
+    (synopsis "ACL2 theorem prover running on SBCL")
+    (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 \"A Computational Logic for Applicative Common Lisp\".
+
+This package builds ACL2 using SBCL (Steel Bank Common Lisp) as the underlying
+Lisp implementation and includes the basic certified books for immediate use.")
+    (license license:bsd-3)))
+
+acl2

manifest.scm

@@ -0,0 +1,12 @@
+;;; GUIX manifest for ACL2 development environment
+;;; 
+;;; This manifest can be used to set up a development environment with ACL2
+;;; Use: guix shell -m manifest.scm
+;;; Or:  guix install -m manifest.scm
+
+(use-modules (gnu)
+             (gnu packages)
+             (acl2))  ; Our custom ACL2 package
+
+(packages->manifest
+ (list acl2))

test-guix-package.sh

@@ -0,0 +1,66 @@
+#!/bin/bash
+# Test script for ACL2 GUIX package
+
+set -e
+
+echo "ACL2 GUIX Package Test Script"
+echo "=============================="
+
+echo
+echo "This script demonstrates how to use the ACL2 GUIX package."
+echo "Note: This requires GUIX to be installed on your system."
+echo
+
+# Check if GUIX is available
+if ! command -v guix &> /dev/null; then
+    echo "ERROR: GUIX is not installed or not in PATH"
+    echo "Please install GUIX first: https://guix.gnu.org/en/download/"
+    exit 1
+fi
+
+echo "✓ GUIX found at: $(which guix)"
+echo "✓ GUIX version: $(guix --version | head -1)"
+echo
+
+# Test 1: Check package definition syntax
+echo "Test 1: Checking package definition syntax..."
+if guix build -f acl2.scm --dry-run &>/dev/null; then
+    echo "✓ Package definition syntax is valid"
+else
+    echo "✗ Package definition has syntax errors"
+    guix build -f acl2.scm --dry-run
+    exit 1
+fi
+
+# Test 2: Check manifest syntax  
+echo
+echo "Test 2: Checking manifest syntax..."
+if guix install -m manifest.scm --dry-run &>/dev/null; then
+    echo "✓ Manifest syntax is valid"
+else
+    echo "✗ Manifest has syntax errors"
+    guix install -m manifest.scm --dry-run
+    exit 1
+fi
+
+# Test 3: Try to build (this may take a while)
+echo
+echo "Test 3: Attempting to build ACL2 package..."
+echo "Note: This may take 30+ minutes and requires significant disk space"
+read -p "Do you want to proceed with the build? (y/N): " -n 1 -r
+echo
+if [[ $REPLY =~ ^[Yy]$ ]]; then
+    echo "Building ACL2 package..."
+    guix build -f acl2.scm
+    echo "✓ Build completed successfully"
+else
+    echo "Skipping build test"
+fi
+
+echo
+echo "✓ All tests completed successfully"
+echo
+echo "To install ACL2, run one of:"
+echo "  guix install -f acl2.scm"
+echo "  guix install -m manifest.scm"
+echo "  guix shell -f acl2.scm      # for temporary environment"