pretty-program

(in-package "STR")

(local (include-book "std/util/defredundant" :dir :system))

(local (include-book "make-event/acl2x-help" :dir :system))

(local (include-book "pretty-defs-aux"))

(local (include-book "std/omaps/portcullis" :dir :system))

(make-event (b* ((state (f-put-global 'port-file-enabled-original-value
         (f-get-global 'port-file-enabled state)
         state)) (state (f-put-global 'port-file-enabled nil state)))
    (value '(:or (acl2x-replace (include-book "pretty" :uncertified-okp :ignore-certs)
          (value-triple :invisible)
          :outside-certification (include-book "pretty"))
        (make-event (er hard?
            'pretty-program
            "~%************************ PRETTY-PROGRAM FAILURE ************************~% ~
         Failed to include std/strings/pretty.  It may be that something has ~
         changed in this book or one of the books it includes that makes it ~
         impossible to include uncertified.  Please check this by running ~
         "make clean" followed by "make std/strings/pretty-program.cert".~%~
         ************************************************************************"))))))

(make-event (b* ((state (f-put-global 'port-file-enabled
         (f-get-global 'port-file-enabled-original-value
           state)
         state)))
    (value '(value-triple :port-file-enabled-restored))))

(include-book "defs-program")

(include-book "centaur/fty/fty-sum-casemacro" :dir :system)

(program)

(make-event '(:or (make-event (b* ((events (defredundant-fn *pretty-defs* t state)))
        (value events)))
    (make-event (er hard?
        'pretty-program
        "~%************************ PRETTY-PROGRAM FAILURE ************************~%~
         Failed to redundantly define the required events.  If you haven't ~
         done anything to break files that this book depends on, this may be ~
         a symptom that make-event expansions from stale certificates are ~
         being loaded.  The simplest way to fix this is to run "make ~
         clean".  Otherwise, you can try to locate and delete the ~
         certificate containing the bad expansion, but you're on your own for ~
         that.~%~
         ************************************************************************"))))