preventing include-raw reloading

[bendyarm]

:u does not undo raw lisp code, including that loaded by include-raw.
So if you do

(include-book ...)   ; of something that does an include-raw
:u 
(include-book ...)

Then the internal include-raw will be redone.
This could be a problem if the contents of the include-raw is not idempotent.
(It is currently a problem for "zippy" which I will fix in a moment, but I also ran
into a hard-to-reproduce problem with UIOP getting confused about versions of ASDF).
Even if it is idempotent, it could be a performance problem.

I think it is problematic to try to undo arbitrary raw lisp code, so it
would be better to document that raw code is not undone and don't try to undo it.

Also, I think the include-raw macro should have a way to prevent the contents
from being reloaded. For example, there could be another keyword arg
:always-reload that defaults to nil; then the expansion of the
macro could define a defvar of a flag indicating if the raw code was
already loaded and then conditionally load the code if the flag was still NIL,
and then set the flag to T.

Possible issues with this idea:

• are there any users of raw-include who use the same raw-include call in multiple places and who need it to reload?
• if there are two raw-include forms with the same file but different keyword arguments, what should happen?

If anyone has opinions about this or answers to these questions, please add a comment to this issue
(or send a message via any acl2-related communication).

[bendyarm]

More information.

I mapped over all the include-raw forms in the community books.

There are no two include-raw forms with the same filename but different keyword args.

In order to prevent future collisions, we will need to get a longer include path and to
build that into the name of the once-only defvar. I suggest if it is in acl2/books/
we use the path after that, but if not (a case that may not even exist),
it can do what raw-compile and friends do:
(extend-pathname (cbd) name state)).

There is only one instance with / in the file name---in bundle/bundle.lisp.

There are 4 instances of :do-not-compile and the value is always t:

(include-raw "base-raw.lsp" :host-readtable t :do-not-compile t)
(include-raw "copy-raw.lsp" :do-not-compile t :host-readtable t)
(include-raw "dirname-raw.lsp" :do-not-compile t :host-readtable t)
(include-raw "mkdir-raw.lsp" :do-not-compile t :host-readtable t)

There are 3 instances of :on-compile-fail and :on-load-fail:

(include-raw "environment-and-syscalls-raw.lsp" :on-compile-fail (format t "[environment-and-syscalls-raw.lsp] Compilation failed with message ~a~%" condition) :on-load-fail (cw "[environment-and-syscalls-raw.lsp] Load failed; Moving On.~%") :host-readtable t)
(include-raw "other-non-det-raw.lsp" :on-compile-fail (format t "[other-non-det-raw.lsp] Compilation failed with message ~a~%" condition) :on-load-fail (cw "[other-non-det-raw.lsp] Load failed; Moving On.~%") :host-readtable t)
(include-raw "register-readers-and-writers-raw.lsp" :on-compile-fail (format t "[register-readers-and-writers-raw.lsp] Compilation failed with message ~a~%" condition) :on-load-fail (cw "[register-readers-and-writers-raw.lsp] Load failed; Moving On.~%") :host-readtable t)

There are many instances of :host-readtable but there aren't any filenames that sometimes have :host-readtable and sometimes don't have it.

From this information, I think it would probably be fine to ignore the keyword args (except the new :always-reload)
for the purpose of deciding whether to reload the file contents, as long as we document that behavior.

[solswords]

I think it would be good to experiment with making it an error to undo inclusion of raw Lisp code -- are there cases where we really need to do that or can we avoid it by, say, improving the structuring of books to separate the logical models from their raw Lisp implementations?

[ericwhitmansmith]

I think we should definitely support undoing include-books that bring in raw Lisp code, such as various Axe tools. Also, I think certify-book often undoes events when it rolls back the world.

[MattKaufmann]

For a book that includes raw Lisp code that shouldn't be undone, it might suffice to put (reset-prehistory t) in the book.

[solswords]

Point taken about certify-book undoing events when it rolls back the world. For loading third-party libraries it may be that the best we can do is make sure that re-including the raw Lisp code doesn't change anything, and hope and trust that what doesn't get undone doesn't disrupt anything. Other than that, one common pattern that we probably could support undoing (with help from Matt) is redefining a function under the hood, i.e. clobbering its "logical" symbol-function with a raw Lisp one. E.g. say I include oslib/copy-logic and then oslib/copy, undoing that last include should ideally revert the under-the-hood redefinition of copy-file-fn that was done by loading copy-raw.lsp, and set it back to the symbol-function resulting from its logical definition in copy-logic.lisp.