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
I don't know how those functions are used, but Print wrong. in test2.v triggers the same error. Turning Theorem wrong into an axiom and the error no longer triggers so I don't think having no actual proof object is the issue here. I'd like to provide more details, but unfortunately, I'm not familiar with coq internals enough to debug the issue myself.
The text was updated successfully, but these errors were encountered:
The proofs are very much the issue. hammer needs access to the proof objects to do premise selection. Now, one could try to treat theorems without proof objects like axioms, but that's a feature request which I'm not going to work on in the foreseeable future. You're welcome to try to implement it yourself if you really need it.
A quick solution might be to give a more understandable error message, which I might do.
Coq version: 8.15.0
Hammer version: 1.3.2+8.15
Here is a minimal example.
test.v:
test2.v:
To reproduce the error, run the following commands:
Then there will be an error message saying "Cannot access opaque delayed proof". The message comes from Coq itself. Searching the text on coq's repo leads me to the following OCaml function: https://github.com/coq/coq/blob/b35628733a0131a9cc648793c1e33e222d7958c5/library/global.ml#L142
I don't know how those functions are used, but
Print wrong.
intest2.v
triggers the same error. TurningTheorem wrong
into an axiom and the error no longer triggers so I don't think having no actual proof object is the issue here. I'd like to provide more details, but unfortunately, I'm not familiar with coq internals enough to debug the issue myself.The text was updated successfully, but these errors were encountered: