• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • 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.5+ (a development snapshot based on ACL2 Version 8.5) +
+   built January 6, 2023  16:13:03.                                   +
+   (Git commit hash: e9790bdb14922c9a88e423781b5d8bdf080fb05d)        +
+ Copyright (C) 2023, 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.5+ (a development snapshot based on ACL2 Version 8.5) +
+   built January 6, 2023  16:13:03.                                   +
+   (Git commit hash: e9790bdb14922c9a88e423781b5d8bdf080fb05d)        +
+ Copyright (C) 2023, 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.