Skip to content

Conversation

Copy link
Contributor

Copilot AI commented Aug 5, 2025

This PR adds a complete GUIX package definition for ACL2 (A Computational Logic for Applicative Common Lisp) running on SBCL (Steel Bank Common Lisp), providing an alternative to the Docker-based installation.

What's Added

  • acl2.scm: Complete GUIX package definition that mirrors the Docker build process
  • manifest.scm: GUIX manifest for easy installation
  • .guix-channel: Channel definition allowing this repository to be used as a GUIX channel
  • GUIX-README.md: Comprehensive documentation for GUIX usage
  • test-guix-package.sh: Validation script for testing the package
  • Updated main README.md to reference the GUIX build option

Package Features

The GUIX package provides the same functionality as the existing Docker build:

  • Downloads ACL2 source from the official GitHub repository
  • Builds ACL2 using SBCL as the underlying Lisp implementation
  • Certifies the "basic" book collection during build with parallel jobs (-j 4)
  • Installs ACL2 executable and support scripts (cert.pl, clean.pl, critpath.pl)
  • Sets up proper environment variables (ACL2_SYSTEM_BOOKS, ACL2)
  • Includes a wrapper script for convenient usage

Installation Methods

Users can install ACL2 via GUIX in multiple ways:

# Direct installation from package file
guix install -f acl2.scm

# Using the manifest
guix install -m manifest.scm

# As a development environment
guix shell -f acl2.scm

# Or add as a GUIX channel and install normally
guix install acl2

Configuration Required

The package includes placeholder values for the ACL2 commit hash and SHA256 that users need to update:

  1. Choose a specific ACL2 commit from https://github.com/acl2/acl2/commits/master
  2. Compute the hash: guix hash -S git-recursive https://github.com/acl2/acl2.git <commit>
  3. Update both the commit and sha256 values in acl2.scm

This approach ensures reproducible builds while allowing flexibility in ACL2 version choice.

Why GUIX?

GUIX provides several advantages over Docker for ACL2 development:

  • Reproducible builds: Exact dependency versioning and build environment control
  • Functional package management: Rollbacks, multiple versions, and isolated environments
  • Native performance: No containerization overhead
  • Integration: Seamless integration with existing GUIX-managed development environments
  • Transparency: Complete build process visibility and customization

This addition complements the existing Docker build without replacing it, giving users more deployment options for ACL2.

Warning

Firewall rules blocked me from connecting to one or more addresses

I tried to connect to the following addresses, but was blocked by firewall rules:

  • esm.ubuntu.com
    • Triggering command: /usr/lib/apt/methods/https (dns block)
  • git.savannah.gnu.org
    • Triggering command: wget REDACTED (dns block)
  • git.tojo.tokyo
    • Triggering command: curl -L REDACTED (dns block)
  • https://api.github.com/repos/acl2/acl2/commits/master
    • Triggering command: curl --silent REDACTED (http block)
  • prdownloads.sourceforge.net
    • Triggering command: wget REDACTED -O sbcl.tar.bz2 -q (dns block)

If you need me to access, download, or install something from one of these locations, you can either:


💬 Share your feedback on Copilot coding agent for the chance to win a $200 gift card! Click here to start the survey.

Copilot AI changed the title [WIP] Create a GUIX build for ACL2 running SBCL. This Dockerfile is an up-to-date working build. Here is an older GUIX build that no longer works but can help as an example to get started: https://git.tojo.tokyo/tojo-tokyo-guix-channel.git/tree/tojo-tokyo/p... Add GUIX package definition for ACL2 running SBCL Aug 5, 2025
Copilot AI requested a review from jimwhite August 5, 2025 22:34
Copilot finished work on behalf of jimwhite August 5, 2025 22:34
@jimwhite jimwhite changed the base branch from main to guix August 5, 2025 22:45
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants