• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
      • Events
      • Parallelism
      • History
      • Programming
      • Operational-semantics
      • Real
      • Start-here
        • Gentle-introduction-to-ACL2-programming
        • ACL2-tutorial
        • About-ACL2
          • Recursion-and-induction
          • Operational-semantics
          • Soundness
          • Release-notes
          • Version
          • Acknowledgments
          • Using-ACL2
          • How-to-contribute
          • Pre-built-binary-distributions
          • Common-lisp
          • Git-quick-start
          • Copyright
          • Building-ACL2
            • Sbcl-installation
            • Using-extended-ACL2-images
            • Sbcl-installation-brief
              • Ccl-installation
            • ACL2-help
        • Miscellaneous
        • Output-controls
        • Bdd
        • Macros
        • Installation
        • Mailing-lists
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Building-ACL2

    Sbcl-installation-brief

    Installing Steel Bank Common Lisp (SBCL)

    The topic sbcl-installation contains full installation instructions for SBCL. The present topic contains abbreviated instructions that have been used successfully over time; these may be suitable for those who already have a previous version of SBCL installed and have experience with Lisp. If the instructions below are not sufficient for you, please see sbcl-installation instead.

    SBCL is available from https://www.sbcl.org. You can of course go to that website to find download and installation instructions for SBCL, but here is a concise summary that includes build options appropriate for ACL2.

    1. Download SBCL from https://www.sbcl.org. A shortcut may be to follow the “Source” link near the top of the page, https://www.sbcl.org/platform-table.html.
    2. The downloaded file will have a name like “sbcl-2.2.10-source.tar.bz2”, where “2.2.10” is replaced by the current SBCL version. Change to a directory just above where you want SBCL to reside and move the downloaded file there.
    3. Extract the downloaded file (where it now resides), for example as follows (again, where “2.2.10” is replaced by the current SBCL version number).
      tar xfj sbcl-2.2.10-source.tar.bz2
    4. Change to the new directory and build SBCL with options appropriate for ACL2, as follows (again, replacing “2.2.10” as appropriate).
      cd sbcl-2.2.10
      sh make.sh --without-immobile-space --without-immobile-code --without-compact-instance-header
      You might also need option --with-sb-thread; this has been necessary on a machine running FreeBSD.
    5. Create a script file in a directory that is on your path (or, if you are updating your sbcl, just replace your current sbcl script; you can find its location by executing the command, “which sbcl”). If you are in directory <DIR> from the preceding step (e.g., a path ending in “sbcl-2.2.10”), then that script file should contain the following lines.
      #!/bin/sh
      <DIR>/run-sbcl.sh --dynamic-space-size 2000 "$@"