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.