"undone" proofs read in as failed proofs
In the session_itp
API, the proof_attempt_node
type has an optional result field proof_state
. This field can be None
, which represents the fact that the prover hasn't finished yet, or absence of result for another reason. Such a state can occur for example when hitting Ctrl-C while why3 is running.
When such a session is read from a session file, the None
state is replaced by a default error
result. This makes it impossible to distinguish between such unfinished states, and actually failed proof attempts.
I will propose a fix.