Segfault on (Query () Goals) with sertop 8.15.0+0.15.3 about coq-serapi HOT 4 CLOSED

Hi @rwhender , thanks for the report. I can't reproduce. What coq-serapi version are you using?

I use a bit simpler script:

(ReadFile "theories/Basics/Contractible.v")
(Exec 16)
(Query () Ast)
(Query ((sid 16)) Ast)

but should not matter for this kind of problem.

from coq-serapi.

Thanks for the response.

I am using coq-serapi 8.15.0+0.15.3, coq 8.15.2, and OCaml 4.09.1.

That is a strange complication. If I run your script, I do not observe the segfault.

However, I was able to find a more concise way of reproducing the error. If I create a new file (say "theories/Basics/Contracitble_truncated.v") that is truncated after line 28, then follow your script (except using (Query () Goals)), I observe a segfault.

(ReadFile "theories/Basics/Contractible_truncated.v")
(Exec 16)
(Query () Goals)

I'll note here that I did rebuild by running make clean then make once again to make sure no strange artifacts were causing problems. The segfault still occurred in this case.

A note about our application here might be useful to explain this potentially odd-looking approach. We wish to know as much as possible about what Coq knows about the current state of goals, proof mode, etc. for every sentence in a Coq source file. We use the feedback from the (Add... command to determine the state that needs to be executed, then execute it, then query the goals after every execution to determine the change in proof state (if any).

from coq-serapi.

Fixed by 47c5470 , thanks a lot for the report!

Indeed I was testing 0.15.2 , the bug was introduced in 0.15.3 . So you want to either revert to 0.15.2 or upgrade to 0.15.4 when it is available.

from coq-serapi.

Thank you for the quick resolution!

from coq-serapi.