August 4, 2025

ACL2 Guide to Logic and Programming Language: Interfacing-tools

undefined

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
ACL2s-interface
An interface for interacting with ACL2/ACL2s from Common Lisp.
Bridge
Connects ACL2 and the outside world.
Clex
Centaur Lexer Library.
Command-line
Handling of command-line arguments when ACL2 is invoked
Defttag
Introduce a trust tag (ttag)
Hacker
Functions for extending ACL2 in ways that are potentially unsound.
Io
Input/output facilities in ACL2
Oslib
Operating System Utilities Library
Quicklisp
An ACL2 connection to the Quicklisp system for installing Lisp libraries.
Save-exec
Save an executable image and a wrapper script
Startup-banner
Modifying the ACL2 startup banner
Std/io
A library for reasoning about file input/output operations.
Sys-call
Make a system call to the host operating system
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.

No comments:

Post a Comment