I have encountered the error in the title ("Cannot access opaque delayed proof") with certain
Print All.) inserted into nested proof developments. For example, inserting
Print All. on line 13 of coq/test-suite/success/sideff.v results in the error. This error only occurs in Coq 8.15 or later. The culprit is the
Qed. terminating the inner proof of
Qed. with another opaque proof ender like
Save yields the same result, but
Defined. does not (which makes sense given the message).
I need to be able to print the identifiers of the local environment line-by-line for an application I am developing that wraps around
coq-serapi). Is there an alternative method to obtain this information besides my current workaround of changing to transparent proof enders (so that
Print All will work)? Note that the solution must work in Coq 8.15. Thanks
Is avoiding nested proofs an option? Printing proofs that end in Qed normally works fine, if they've been executed. The issue seems about the "delayed" part...
Nested proofs are currently discouraged and disabled by default
But when you say
Print All, do you mean
Print aux? Otherwise I'm more confused.
I can only guess why the nesting delays the proofp
But if you need nested proofs, please consider tagging Emilio
Print All is https://coq.github.io/doc/master/refman/proof-engine/vernacular-commands.html#coq:cmd.Print-All
it accesses the body for not very good reasons (ie because it was convenient to code this way and nobody noticed that it might be a problem) and does not fail gracefully if the proof is delayed
Thanks, I'll tag @Emilio Jesús Gallego Arias.
Unfortunately, avoiding nested proofs is not ideal as we are applying the tool to existing proof developments as part of data collection for a machine-learning project. In particular, we are capturing goals and hypotheses (in addition to other metadata) similar to CoqGym .
Print All forms a critical component of our admittedly ad-hoc extraction process, the reasons for which are too long to go into here. In general, though, any command that we must insert to query the environment should not noticeably alter the development under test, which is a constraint violated by this error.
Our current workaround is to automatically replace each
Admitted. and each
Save <ident>. with
Defined <ident>. Opaque <ident>. (after first verifying that
Save <ident>. succeeds). I am mainly curious to know if there is a better approach. Incidentally, we choose to use
Defined. Opaque <ident>. to replace
Qed. as there is a noticeable difference in behavior when it comes to
Program obligations (
Defined. may complete multiple obligations at once,
Admitted. will not).
Print All sounds very brittle, and how do you know you can parse the output? We typically recommend to use something like SerAPI if you want to get data out of Coq in a robust way
We do use SerAPI where we can, but unfortunately it does not seem to expose all of the data that we need (or in some cases only exposes it for some versions of Coq where we need a solution that works for multiple). For example, given an arbitrary Vernacular command (possibly defined in an unanticipated grammar extension), we wish to note in our collected metadata what identifiers were introduced into the top-level environment. This information can also be used to distinguish whether a proof was completed or simply delayed.
I agree that
Print All. is brittle, but it seems to be the best option available (we execute it through
sertop's Vernac query). Regarding parsing its output, we only need to pull out the top-level identifiers, which by all observations are consistently left-aligned and follow a finite number of formatting options. We have tested our solution across many developments and so are not concerned with that aspect.
I'll also note that exposure of one piece of information through SerAPI would render my concerns moot: the classification of a command, i.e., whether it is a
VtQed, or other. To the best of my knowledge, though, a query for this information is not available.
SerAPI does provide a limited protocol, sure, but you could also use Coq's ML API directly in some places. For example, the SerAPI tools
sername do this.
I think using the ML API is likely the only way to make the querying robust...
Thanks, that is what I assumed. That would likely be the route for a future revision of the project, which is currently in Python for maximum portability between OCaml build environments and for optimal exploitation of the team's current expertise.
ah, and you have seen PyCoq? I think it can provide some of the ML API directly in Python
Yes, that looks like a great tool, but unfortunately we want support for Coq as far back as 8.9, which is outside its dependency range.
Hi @Andrew Gardner , I'm afraid that if you need compat back for 8.9 I don't see a good way to improve this.
coq-lsp should not have these kind of problems; but 8.15 support will only happen if we have the manpower.
coq-lsp can actually provide very interesting info about the documents, but only a part is exposed as of now; we work on a use-case basis.
Just want to note that if you're looking for Coq Python API that supports 8.9, mine does: https://github.com/HazardousPeach/coq_serapy . But that's working through SerAPI, so it's not going to give you the information that you're looking for that's only in the ML api.
It does have some heuristics for doing some of that stuff, like determining the identifiers produced by a vernacular command, but that's not going to be robust to an unanticipated grammar extension. It also supports figuring out if a particular command from a proof file is starting or ending a proof. It doesn't have access to the internals to do this, so it can only look at the ending commands to be sure, then look backwards for the most recent potential starting command. But this appears to be robust for every project in CoqGym
Last updated: Oct 04 2023 at 23:01 UTC