print an error message and cause a ``soft error''
Major Section:  PROGRAMMING

(Error1 ctx str alist) returns (mv t nil state). An error message is first printed using the the ``context'' ctx, as well as the string str and alist alist that are of the same kind as expected by fmt. See fmt.

Error1 can be interpreted as causing an ``error'' when programming with the ACL2 state, something most ACL2 users will probably not want to do; see ld-error-triples and see er-progn. In order to cause errors with :logic mode functions, see hard-error and see illegal. Better yet, see er for a macro that provides a unified way of signaling errors.

As mentioned above, error1 always returns (mv t nil state). But if a call (error1 ctx str alist) is encountered during evaluation, then the string str is first printed using the association list alist (as in fmt). Here is a trivial, contrived example.

ACL2 !>(error1 'my-context
               "Printing 4: ~n0"
               (list (cons #\0 4))

ACL2 Error in MY-CONTEXT: Printing 4: four

ACL2 !>