Faced bugs for readme.py

[hsz0403]

When I run

    for attempt in [incorrect, correct]:
        # Schedule the removal of the "\nAdmitted." step
        changes = [ProofPop()]
        # Schedule the addition of each step in the attempt
        for s in attempt:
            changes.append(ProofAppend(s))
        try:
            # Apply all changes in one batch
            proof_file.change_proof(unproven, changes)
            print("Proof succeeded!")
            break
        except InvalidChangeException:
            # Some batch of changes was invalid
            # Rollback is automatic, so no rollback needed
            print("Proof attempt not valid.")
    reset_proof(proof_file)

The [incorrect, correct] first is always incorrect even if I change to [correct,correct] the first is still fail. And in

print(proof_file.proofs[0].steps)

It doesn't print the final step before the Admitted.

[pcarrott]

Hello, @hsz0403 ! Apologies for the late reply.

Regarding the first problem, I tried running the example with [correct, correct] and the proof succeeded in the first attempt. I tried in both blocks (pop/append steps and change proof) and it always behaved as expected. Did you run the example from the root directory as intended (i.e. python examples/readme.py)? Or perhaps you might have stopped running the file (e.g. by Ctrl + C) before reaching reset_proof(proof_file)? That could lead to the readme.v file being permanently altered and could lead to unexpected behaviour.

Regarding the second problem, the readme.v file has two proofs, so print(proof_file.proofs[0].steps) only prints the first one, which is the one with the Qed. Replacing it with print(proof_file.proofs[1].steps) returns the admitted proof. In both cases, it seems to be printing everything right on my end, though. Might this be related with permanent changes to the readme.v file, as well?

In essence, it seems to be behaving as expected on my end. If none of what I suggested explains why you are getting these errors, could you provide the exact code you are running, instead of just a snippet?

[hsz0403]

Now it works well! I guess before the update the import code part went wrong.