Abduction does not work with the newer version of Coq

[masashi-y]

In scripts/abduction_tools.py, you define is_theorem_error function which checks if "^^^^" is in a Coq output. In turn, this function is used in filter_wrong_axioms function, which filters ill-formed axioms based on the existence of "^^^^" in the response from Coq to a script with a new axiom candidate. However, in newer versions of Coq (8.6 in my case), doing Qed with an incomplete proof ends in:

                      ^^^^
Error: Attempt to save an incomplete proof (in proof t1)

t1 <

This is problematic in that the abduction code never adds any new axiom, as the script thrown to Coq in that function always ends with this status.

[pasmargo]

In Coq 8.6, does that output only produce 4 characters "^"?

[masashi-y]

Yes. I think "^^^^" underlines "Qed."

[pasmargo]

I think the "^^^^" string when inserting axioms is typically longer because it underlines the axiom name; but I have not yet confirmed that.

If the above is true, perhaps we could use a longer string, e.g. "^^^^^" to recognize problems with the axiom insertion. I wonder if that will work.