proof features not supported with waterfall-parallelism enabled
Major Section:  PARALLELISM

For a general introduction to ACL2(p), an experimental extension of ACL2 that supports parallel execution and proof, see parallelism. Please note that although this extension is usable and, we hope, robust in its behavior, there are still known issues to address beyond those listed explicitly below. For example, esoteric ``invalid speculation'' messages may appear. More generally, while we expect ACL2(p) to perform correctly, it may never have the same level of attention to correctness as is given to ACL2; see parallelism, specifically the ``IMPORTANT NOTE'' there.

Below we list proof features of ACL2 that are not yet supported when parallel execution is enabled for the primary ACL2 proof process, generally known as ``the Waterfall'', typically by calling set-waterfall-parallelism.

Please note that this topic is limited to the case that such waterfall parallelism is enabled. We believe that all ACL2 proof procedures are supported when waterfall parallelism is disabled, even in executables that support parallelism (see compiling-acl2p).

While we support clause-processors, we do not support those that modify state. At this time, such an attempt to modify state may result in a sub-optimal error message.

Computed hints are supported, as long as they don't modify state. Computed hints may in principle read state, but support for such hints may be incomplete.

Custom-keyword-hints are unsupported, though they may work on occasion.

GNU Make versions 3.81 and 3.82 used to cause a lot of problems (version 3.80 somewhat less so), at least on Linux, when certifying books with CCL using make (see book-makefiles. CCL was updated around March 23, 2011 to fix this problem, so if you get segfaults (for example), try updating your CCL.

The standard process for book certification will not use waterfall-parallelism (see set-waterfall-parallelism), which is disabled by default. See book-makefiles, which explains that acl2-customization files are ignored during that process unless specified explicitly on the command line or in the environment.

Proof output can contain repeated printing of the same subgoal name.

Gag-mode isn't supported. However, ACL2(p) also prints key checkpoints (for example see introduction-to-key-checkpoints), but with a notion of ``key checkpoint'' that does not take into account whether the goal is later proved by induction.

The :brr utility is not supported.

Time limits (see with-prover-time-limit) aren't supported.

The use of wormholes is not recommended, as there may be race conditions.

When waterfall-parallelism is enabled (see set-waterfall-parallelism), the use of set-inhibit-output-lst may not fully inhibit proof output.

Interrupting a proof attempt is not yet properly supported. At a minimum, interrupts are trickier with waterfall parallelism enabled. For one, the user typically needs to issue the interrupt twice before the proof attempt is actually interrupted. Additionally, sometimes the theorem is registered as proved, even though the prover did not finish the proof. If this occurs, issue a :u (see ubt) and you will be at a stable state.

If the host Lisp is Lispworks, you may see messages about misaligned conses. The state of the system may be corrupted after such a message has been printed.