• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • 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