		Search-engine friendly clone of the ACL2 documentation.

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.