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.
In
scripts/abduction_tools.py, you defineis_theorem_errorfunctionwhich checks if "^^^^" is in a Coq output.
In turn, this function is used in
filter_wrong_axiomsfunction, whichfilters 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:
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.