• 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

• Interfacing-tools

Startup-banner

Modifying the ACL2 startup banner

When you start up an ACL2 executable built from sources obtained from GitHub between ACL2 releases, you'll typically see a startup banner like this:

++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
+ ACL2 Version 8.6+ (a development snapshot based on ACL2 Version 8.6) +
+   built January 14, 2025  10:09:28.                                  +
+   (Git commit hash: 89b2701f59f8e561b17121cf0a25cb8d1910377f)        +
+ Copyright (C) 2025, Regents of the University of Texas.              +
+ ACL2 comes with ABSOLUTELY NO WARRANTY.  This is free software and   +
+ you are welcome to redistribute it under certain conditions.  For    +
+ details, see the LICENSE file distributed with ACL2.                 +
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

The third line of that banner can be modified by setting environment variable ACL2_SNAPSHOT_INFO to a non-empty string before saving the executable. The value of that variable will be placed into the banner, for example as follows if that value is "This is my private executable.".

++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
+ ACL2 Version 8.6+ (a development snapshot based on ACL2 Version 8.6) +
+   built January 14, 2025  09:56:49.                                  +
+   (Note from the environment when this executable was saved:         +
+    This is my private executable.)                                   +
+ Copyright (C) 2025, Regents of the University of Texas.              +
+ ACL2 comes with ABSOLUTELY NO WARRANTY.  This is free software and   +
+ you are welcome to redistribute it under certain conditions.  For    +
+ details, see the LICENSE file distributed with ACL2.                 +
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

An exception is the special value, "none", which is treated as case-insensitive (so it can similarly be "None", "NONE", etc.). In that case, the third line of the original banner is omitted entirely.