From 0cd594f991da6a907d794285e22ed508201dbff9 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 5 Aug 2025 22:16:52 +0000 Subject: [PATCH 1/3] Initial plan From 2ef141a4b1e14aa376f26f5d2c4d8c0fc97c45b4 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 5 Aug 2025 22:31:05 +0000 Subject: [PATCH 2/3] Add GUIX package definition for ACL2 running SBCL Co-authored-by: jimwhite <890972+jimwhite@users.noreply.github.com> --- .guix-channel | 18 ++++++ GUIX-README.md | 114 +++++++++++++++++++++++++++++++++ README.md | 4 ++ acl2.scm | 146 +++++++++++++++++++++++++++++++++++++++++++ manifest.scm | 12 ++++ test-guix-package.sh | 66 +++++++++++++++++++ 6 files changed, 360 insertions(+) create mode 100644 .guix-channel create mode 100644 GUIX-README.md create mode 100644 acl2.scm create mode 100644 manifest.scm create mode 100755 test-guix-package.sh diff --git a/.guix-channel b/.guix-channel new file mode 100644 index 0000000..a108806 --- /dev/null +++ b/.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")))) \ No newline at end of file diff --git a/GUIX-README.md b/GUIX-README.md new file mode 100644 index 0000000..6756da4 --- /dev/null +++ b/GUIX-README.md @@ -0,0 +1,114 @@ +# 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 +# Install ACL2 using the local package definition +guix install -f acl2.scm + +# 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 \ No newline at end of file diff --git a/README.md b/README.md index ab45124..ced8b20 100644 --- a/README.md +++ b/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. diff --git a/acl2.scm b/acl2.scm new file mode 100644 index 0000000..3efe0fa --- /dev/null +++ b/acl2.scm @@ -0,0 +1,146 @@ +;;; 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)) + +(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-git") + (source + (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/acl2/acl2.git") + ;; NOTE: This commit hash should be updated to the latest stable ACL2 commit + ;; You can find the latest commit at: https://github.com/acl2/acl2/commits/master + ;; Use: guix hash -S git-recursive https://github.com/acl2/acl2.git + ;; to compute the corresponding sha256 hash + (commit "UPDATEME-use-latest-stable-commit-hash"))) + (file-name (git-file-name name version)) + (sha256 + (base32 + ;; NOTE: This hash needs to be computed for the actual commit using: + ;; guix hash -S git-recursive https://github.com/acl2/acl2.git + "UPDATEME-compute-hash-for-chosen-commit-using-guix-hash")))) + (build-system gnu-build-system) + (native-inputs + (list autoconf + automake + curl + git + 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))) \ No newline at end of file diff --git a/manifest.scm b/manifest.scm new file mode 100644 index 0000000..c8587eb --- /dev/null +++ b/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)) \ No newline at end of file diff --git a/test-guix-package.sh b/test-guix-package.sh new file mode 100755 index 0000000..f0a20d5 --- /dev/null +++ b/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" \ No newline at end of file From 728d68371424b3a6b70de0cde31185ddae2fd80a Mon Sep 17 00:00:00 2001 From: Jim White Date: Wed, 6 Aug 2025 05:57:25 +0000 Subject: [PATCH 3/3] snap from codespace --- GUIX-README.md | 7 ++++--- acl2.scm | 34 ++++++++++++++++------------------ 2 files changed, 20 insertions(+), 21 deletions(-) diff --git a/GUIX-README.md b/GUIX-README.md index 6756da4..7e21357 100644 --- a/GUIX-README.md +++ b/GUIX-README.md @@ -13,8 +13,9 @@ This directory contains a GUIX package definition for ACL2 (A Computational Logi ### Method 1: Using the package definition directly ```bash -# Install ACL2 using the local package definition -guix install -f acl2.scm +# 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 @@ -111,4 +112,4 @@ echo "(+ 1 2 3)" | acl2-wrapper - 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 \ No newline at end of file +- Additional books can be certified using the included cert.pl script diff --git a/acl2.scm b/acl2.scm index 3efe0fa..ced3129 100644 --- a/acl2.scm +++ b/acl2.scm @@ -16,37 +16,33 @@ #: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 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-git") + (version "8.6") (source (origin - (method git-fetch) - (uri (git-reference - (url "https://github.com/acl2/acl2.git") - ;; NOTE: This commit hash should be updated to the latest stable ACL2 commit - ;; You can find the latest commit at: https://github.com/acl2/acl2/commits/master - ;; Use: guix hash -S git-recursive https://github.com/acl2/acl2.git - ;; to compute the corresponding sha256 hash - (commit "UPDATEME-use-latest-stable-commit-hash"))) - (file-name (git-file-name name version)) - (sha256 - (base32 - ;; NOTE: This hash needs to be computed for the actual commit using: - ;; guix hash -S git-recursive https://github.com/acl2/acl2.git - "UPDATEME-compute-hash-for-chosen-commit-using-guix-hash")))) + (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 - make + gnu-make perl pkg-config zlib @@ -143,4 +139,6 @@ systems, together with a tool to help you prove properties of those models. 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))) \ No newline at end of file + (license license:bsd-3))) + +acl2