Redef+
System hacker's redefinition command
Example and General Form:
ACL2 !>:redef+
ACL2 p!>
This command is intended only for system hackers, not typical users.
It sets ld-redefinition-action to '(:warn! . :overwrite), sets
the default defun-mode to :program, and invokes set-state-ok with value t. It also introduces (defttag :redef+),
so that redefinition of system functions will be permitted; see defttag. It also removes as untouchable (see push-untouchable) all
variables and functions.
WARNING: This command is potentially unsafe and even unsound! For a
relevant warning about redefinition, see ld-redefinition-action.
Moreover, if the form (redef+) is used in a book, then including the book
can leave you in a state in which dangerous actions are allowed, specifically:
redefinition, and access to functions and variables normally prohibited
because they are untouchable. To avoid this problem, insert the form
(redef-) into your book after (redef+).
Note that undoing a :redef+ command, say with :u, only
undoes the effects of :redef+ on the ACL2 world; it does
not undo the other effects on the ACL2 state. The best way to
undo the effects of :redef+ is generally to execute :redef-.
To understand this point we look at the code for redef+. The output
below has been edited to put world-changing parts in lower case.
ACL2 !>:trans1 (redef+)
(WITH-OUTPUT
:OFF (SUMMARY EVENT)
(PROGN (defttag :redef+)
(PROGN! (SET-LD-REDEFINITION-ACTION '(:WARN! . :OVERWRITE)
STATE)
(program)
(SET-TEMP-TOUCHABLE-VARS T STATE)
(SET-TEMP-TOUCHABLE-FNS T STATE)
(F-PUT-GLOBAL 'REDUNDANT-WITH-RAW-CODE-OKP
T STATE)
(set-state-ok t))))
ACL2 !>
In particular, we see that redefinition remains active after undoing. In
general, it is therefore best to execute :redef- before undoing
:redef+.
This command was introduced to support modification of ACL2 source
code definitions. Thus, note that even system functions can be redefined with
a mere warning. Be careful!
