Major Section: PARALLEL-PROGRAMMING
This documentation topic relates to the experimental extension of ACL2 supporting parallel execution and proof; see parallelism.
ACL2 supports the use of error triples in many features; e.g.,
computed-hints. (For background on error triples,
see programming-with-state.) However, ACL2(p) does not support the use of
error triples in some of these features (e.g., computed-hints) while
waterfall-parallelism is enabled.
You may see an error message like the following when running ACL2(p) with waterfall-parallelism enabled:
ACL2 Error in ( THM ...): Since we are translating a form in ACL2(p) intended to be executed with waterfall parallelism enabled, the form (MY-STATE-MODIFYING-COMPUTED-HINT ID STATE) was expected to represent an ordinary value, not an error triple (mv erp val state), as would be acceptable in a serial execution of ACL2. Therefore, the form returning a tuple of the form (* * STATE) is an error. See :DOC unsupported- waterfall-parallelism-features and :DOC error-triples-and-parallelism for further explanation.
In this particular example, the cause of the error was trying to use a computed hint that returned state, which is not allowed when executing the waterfall in parallel (see unsupported-waterfall-parallelism-features for other related information).
Often, the only reason users need to return state is so they can perform
some output during the proof process. In this case, we suggest using one of
the state-free output functions, like cw or observation-cw. If
the user is concerned about the interleaving of their output with other
output, these calls can be surrounded with the macro with-output-lock.
Another frequent reason users return state is so they can cause a soft
error and halt the proof process. In this case, we suggest instead calling
er with the hard or hard? severity. By using these mechanisms,
the user avoids modifying state, a requirement for much of the code
written in ACL2(p).
You may encounter other similar error messages when using computed-hints, custom-keyword-hints, or override-hints. Chances are that you are somehow returning an error triple when an ordinary value is needed. If this turns out not to be the case, please let the ACL2 implementors know.
