• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Hons-and-memoization
    • Events
    • History
    • Parallelism
    • Programming
    • Start-here
    • Real
    • Debugging
    • Miscellaneous
    • Output-controls
      • With-output
      • Summary
      • Set-gag-mode
      • Set-inhibit-output-lst
      • Goal-spec
      • Set-warnings-as-errors
      • Pso
      • Checkpoint-list
      • Finalize-event-user
      • Set-inhibit-er
      • Set-inhibit-warnings
      • Get-event-data
      • Set-inhibited-summary-types
      • Set-print-clause-ids
      • Checkpoint-list-pretty
      • Set-let*-abstractionp
      • Initialize-event-user
      • Gag-mode
      • Psof
      • Set-raw-warning-format
      • Toggle-inhibit-warning
      • Toggle-inhibit-er
      • Set-raw-proof-format
      • Warnings
      • Show-checkpoint-list
      • Wof
      • Psog
      • Checkpoint-info-list
      • Pso!
      • Toggle-inhibit-warning!
      • Set-duplicate-keys-action!
      • Toggle-inhibit-er!
      • Set-inhibit-warnings!
      • Set-inhibit-er!
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Output-controls

Set-raw-warning-format

Print some warnings in a ``raw'', s-expression format

General Forms:
(set-raw-warning-format t)
:set-raw-warning-format t
(set-raw-warning-format nil)
:set-raw-warning-format nil

This command affects 'warning (and 'warning!) output from the theorem prover when not inhibited (see set-inhibit-output-lst). Calling this macro with value t as shown above will cause warnings to be printed in a ``raw'', s-expression format, of the form (:WARNING warning-type alist). The following example shows a traditional warning message followed by its counterpart after evaluating (set-raw-warning-format t).

; default format
ACL2 Warning [Subsume] in ( DEFTHM APP-COMMUTES ...):  A newly proposed
:REWRITE rule generated from APP-COMMUTES probably subsumes the previously
added :REWRITE rule APP-CONS, in the sense that the new rule will now
probably be applied whenever the old rule would have been.

; raw format
(:WARNING "Subsume"
          ((:CTX (DEFTHM . APP-COMMUTES))
           (:NEW-RULE APP-COMMUTES)
           (:RULE-CLASS-NEW :REWRITE)
           (:RULE-CLASS-OLD :REWRITE)
           (:SUBSUMED-RULES (APP-CONS))))

As illustrated above, it is typical that in the raw format, the :CTX entry is first in the alist while the others are ordered alphabetically by key (e.g., :NEW-RULE precedes :RULE-CLASS-NEW alphabetically).

To obtain the current raw-warning-format (t if that format is active, nil if not), evaluate (@ raw-warning-format).

NOTE: Only a few commonly-occurring classes of warnings are shown differently in raw-warning-format.