Query Ast returns Empty Result

[yangky11]

Hello,

I'm using SerAPI to execute Coq code and extract the AST for each Coq command.
I occasionally run into the following error: the returned AST is empty.

(Add () "Defined.")
(Answer 745 Ack)(Answer 745(Added 265"[LOC]"NewTip))(Answer 745 Completed)
(Query ((sid 265)) Ast)
(Answer 746 Ack)(Answer 746(ObjList()))(Answer 746 Completed)

I don't have a simple example to re-produce this, but from my understanding, Query Ast should never return empty result? Any idea?

[ejgallego]

What version of SerAPI are you using?

There is actually some bugs in Coq such as coq/coq#6884 so indeed if you cannot provide a test-case I'm afraid we are going to be stuck.

[ejgallego]

If you are using 8.8, the first thing is to upgrade to 8.9 as we solved half of the bug there.

[ejgallego]

A much more reliable way to get the AST is to use sercomp [in 8.9 too]

[yangky11]

I was compiling from source using branch v8.9 commit a6b4445.
I'm trying to find a test-case.

[yangky11]

I cannot find a easy test-case, since the Coq code relies on other code as well. I'll just try to use sercomp instead. Thanks.

[ejgallego]

I'd bet that has to do with people using "nested proofs" or weird effectul commands inside proofs.

I can provide you a workaround tho if you want to keep using the interactive protocol, which is to expose the Parse call that sercomp uses. This will be 100% reliable.

Would that help?

[yangky11]

I'll have a try. Thanks!

[ejgallego]

Ok, see 337f9b6

The command is very limited [see commit message] but it may help in your case.

[yangky11]

It works pretty well. What is the text in (Parse ((ontop sid)) "text")? Is it constrained to be exactly the same as the command added before?

[ejgallego]

It is the input to the parser, you can indeed pass any valid Coq input, it doesn't have to be the same.

Note however the limitation with ontop, it has to be indeed the previous sid (or you have to omit it)

This will be lifted in the future, maybe it even works on 8.10 already.

[yangky11]

Got it, thanks!

[tom-p-reichel]

It's been 3 years. Is Parse still a best practice on version 8.15.0+0.15.0?

I also have a minimal example that seems to reproduce this issue on the latest version. It indeed involves nested proofs, as was predicted in this thread.

(Add () "\n\nSet Nested Proofs Allowed.\n\nTheorem outer : nat.\n pose 3.\nTheorem inner : nat.\n intros.\n apply 1.\nQed.\n apply inner.\nQed.")
(Query ((sid 9)) Ast)

[ejgallego]

Parse is indeed still a workaround.

The problem you point out still exists, unfortunately there is not a lot we can do in SerAPI as this is a bug in Coq itself.

A fix is planned upstream, but no idea when it will arrive.