You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
In
scripts/abduction_tools.py
, you defineis_theorem_error
functionwhich checks if "^^^^" is in a Coq output.
In turn, this function is used in
filter_wrong_axioms
function, 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.
The text was updated successfully, but these errors were encountered: