Stream: Coq users

Topic: Error: Cannot access opaque delayed proof

Andrew Gardner (Feb 09 2023 at 16:37):

I have encountered the error in the title ("Cannot access opaque delayed proof") with certain Print statements (namely 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 aux. Replacing 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 sertop (of 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

Paolo Giarrusso (Feb 09 2023 at 20:45):

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

Paolo Giarrusso (Feb 09 2023 at 20:46):

Nested proofs are currently discouraged and disabled by default

Paolo Giarrusso (Feb 09 2023 at 20:49):

But when you say Print All, do you mean Print aux? Otherwise I'm more confused.

Paolo Giarrusso (Feb 09 2023 at 20:50):

I can only guess why the nesting delays the proofp

Paolo Giarrusso (Feb 09 2023 at 20:55):

But if you need nested proofs, please consider tagging Emilio

Gaëtan Gilbert (Feb 09 2023 at 20:59):

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

Andrew Gardner (Feb 13 2023 at 17:05):

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 Qed. with Admitted. and each Save <ident>. with Defined <ident>. Opaque <ident>. (after first verifying that Qed. or Save <ident>. succeeds). I am mainly curious to know if there is a better approach. Incidentally, we choose to use Admitted. versus 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, Qed. and Admitted. will not).

Karl Palmskog (Feb 13 2023 at 17:08):

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

Andrew Gardner (Feb 13 2023 at 17:28):

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 VtStartProof, VtQed, or other. To the best of my knowledge, though, a query for this information is not available.

Karl Palmskog (Feb 13 2023 at 17:34):

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 sercomp and sername do this.

Karl Palmskog (Feb 13 2023 at 17:37):

I think using the ML API is likely the only way to make the querying robust...

Andrew Gardner (Feb 13 2023 at 17:43):

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.

Karl Palmskog (Feb 13 2023 at 17:44):

ah, and you have seen PyCoq? I think it can provide some of the ML API directly in Python

Andrew Gardner (Feb 13 2023 at 17:46):

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.

Emilio Jesús Gallego Arias (Feb 13 2023 at 19:52):

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.

Alex Sanchez-Stern (Feb 13 2023 at 20:00):

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: Apr 16 2024 at 04:02 UTC