hammer tactic fails when dealing with .vos files

[yiyunliu]

Coq version: 8.15.0 Hammer version: 1.3.2+8.15

Here is a minimal example.

test.v:

Theorem wrong : 1 = 2.
(* placeholder *)
  idtac.
Qed.

test2.v:

Require Import test.
From Hammer Require Import Hammer.

Theorem worse : 2 = 3.
Proof.
  hammer.
  (* Error: Cannot access opaque delayed proof *)

To reproduce the error, run the following commands:

coqc -vos test.v
coqc -vok test2.v

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. 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.

[lukaszcz]

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.