• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • 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
      • Debugging
      • Miscellaneous
      • Output-controls
      • Macros
      • Interfacing-tools
        • Io
        • Defttag
        • Sys-call
        • Save-exec
        • Quicklisp
        • Std/io
        • Oslib
        • Bridge
        • Clex
        • Tshell
        • Unsound-eval
        • Hacker
        • ACL2s-interface
        • Startup-banner
        • Command-line
    • Interfacing-tools
      • Io
      • Defttag
      • Sys-call
      • Save-exec
      • Quicklisp
      • Std/io
      • Oslib
      • Bridge
      • Clex
      • Tshell
      • Unsound-eval
      • Hacker
      • ACL2s-interface
      • Startup-banner
      • Command-line
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Top
  • ACL2

Interfacing-tools

Libraries and tools for doing basic file i/o, using raw Common Lisp libraries, working with the operating system, and interfacing with other programs.

Subtopics

Io
Input/output facilities in ACL2
Defttag
Introduce a trust tag (ttag)
Sys-call
Make a system call to the host operating system
Save-exec
Save an executable image and a wrapper script
Quicklisp
An ACL2 connection to the Quicklisp system for installing Lisp libraries.
Std/io
A library for reasoning about file input/output operations.
Oslib
Operating System Utilities Library
Bridge
Connects ACL2 and the outside world.
Clex
Centaur Lexer Library.
Tshell
A fancy alternative to sys-call that features output streaming and capture, exit-code capture, interruption, and better control over when forking occurs.
Unsound-eval
A somewhat robust evaluator.
Hacker
Functions for extending ACL2 in ways that are potentially unsound.
ACL2s-interface
An interface for interacting with ACL2/ACL2s from Common Lisp.
Startup-banner
Modifying the ACL2 startup banner
Command-line
Handling of command-line arguments when ACL2 is invoked