• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
    • Io
    • Defttag
    • Sys-call
    • Save-exec
    • Quicklisp
    • Oslib
    • Std/io
    • Bridge
    • Clex
    • Tshell
    • Unsound-eval
    • Hacker
    • Startup-banner
    • Command-line
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• 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.3+ (a development snapshot based on ACL2 Version 8.3) +
+   built April 21, 2022  15:56:37.                                    +
+   (Git commit hash: 41bb85ab9dbf5ac7d4ed246847db8934b6a48f92)        +
+ Copyright (C) 2022, 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.3+ (a development snapshot based on ACL2 Version 8.3) +
+   built April 21, 2022  15:56:37.                                    +
+   (Note from the environment when this executable was saved:         +
+    This is my private executable.)                                   +
+ Copyright (C) 2022, 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.