SerAPI unable to respond when handling compcert.cparser.Parser

[jimyu94]

Version

Coq 8.7.1, CompCert 3.2

Operating system

macOS 10.13.3

The problem

If you use

sertop --implicit -R lib,compcert.lib -R common,compcert.common -R x86_64,compcert.x86_64 -R x86,compcert.x86 -R backend,compcert.backend -R cfrontend,compcert.cfrontend -R driver,compcert.driver -R flocq,compcert.flocq -R exportclight,compcert.exportclight -R cparser,compcert.cparser

and use ReadFile to read Parser.v in the cparser folder, and then use (Query () (Ast x)) to get the ASTs of its sentences one by one, the SerAPI process will freeze at a point, and Ctrl+C cannot end the process. This could result from the fact that Parser.v has more than 34,000 lines of code. However, could you fix this issue? Since coqc has no problem compiling the file.

[ejgallego]

This should be similar to coq/coq#7034 , let's do the tracking there.

[jimyu94]

Hi! Now I think there is nothing wrong with SerAPI, and instead my Python code is faulty, as explained in the coq issue. Sorry about it. This is extremely strange though, since my python code works perfectly for all other files in CompCert and VST, and it only freezes in the cparser/Parser.v when calling the SerAPI AST queries.

Sorry again about my mistake!

[ejgallego]

Oh, don't discard a bug in Coq. This stuff is tricky, also SerAPI relies on terminal if you open it directly and that has some known limitations on the size of the input.

I'd love to have a native Python interface for SerAPI, but I am not sure how to proceed. Opening an issue anyways #48