• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
    • Debugging
    • Miscellaneous
    • Output-controls
      • With-output
      • Summary
      • Set-inhibit-output-lst
      • Set-gag-mode
      • Goal-spec
      • Set-warnings-as-errors
      • Saving-event-data
      • Pso
      • Finalize-event-user
      • Set-inhibit-er
      • Checkpoint-list
      • Set-inhibit-warnings
      • Get-event-data
      • Set-inhibited-summary-types
      • Set-print-clause-ids
      • Set-let*-abstractionp
      • Gag-mode
      • Initialize-event-user
      • Set-raw-proof-format
      • Checkpoint-list-pretty
      • Psof
      • Set-raw-warning-format
      • Toggle-inhibit-warning
      • Toggle-inhibit-er
      • Warnings
        • Set-warnings-as-errors
        • Patbind-wmv
        • Patbind-wtmv
      • 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
  • Math
  • Testing-utilities

• Output-controls

Warnings

Warnings emitted by the ACL2 proof process

The prover can emit many warnings when processing events. See set-inhibit-warnings and see set-inhibit-output-lst for how to disable and enable them. See also toggle-inhibit-warning and set-warnings-as-errors.

Subtopics

Set-warnings-as-errors

Changing warnings to hard errors (and vice-versa)

Patbind-wmv

B* binder to automatically append together returned warnings

Patbind-wtmv

B* binder to automatically cons together returned warningtrees