• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
    • Io
    • Defttag
    • Sys-call
    • Save-exec
    • Quicklisp
    • Oslib
    • Std/io
    • Bridge
    • Clex
    • Tshell
    • Unsound-eval
    • Hacker
    • ACL2s-interface
      • Itest?-query
      • ACL2s-event
      • ACL2s-query
      • Quiet-mode-hooks
      • ACL2s-interface-symbol-package-tips
      • ACL2s-compute
      • ACL2s-interface::ACL2s-interface-utils
      • Quiet-mode
      • Capture-output
    • Startup-banner
    • Command-line
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• ACL2s-interface

Quiet-mode

Control whether or not the acl2s-interface attempts to suppress ACL2 printed output

Examples:

(quiet-mode-on)    ; from this point forward all acl2s-interface functions will
                   ; attempt to suppress all ACL2 printed output
(quiet-mode-off)   ; (default) from this point forward all acl2s-interface
                   ; functions will print any ACL2 output as normal

Most of the ACL2s interface functions also take a :quiet argument for locally controlling quiet mode without affecting the global setting.

The ACL2s interface provides hooks for code that should run when quiet mode is enabled or disabled. See quiet-mode-hooks for more information.