Incorrect goals when providing -topfile in sertop 8.10.0+0.7.2

[a-gardner1]

I'm working with @rwhender (see https://github.com/ejgallego/coq-serapi/issues/331) in a project using sertop to interact with old commits of various Coq projects as part of data collection for AI/ML proof engineering datasets (see our upcoming ITP 2023 paper discussing challenges for more context). Occasionally, a file will include a self-reference that requires the -topfile argument for correct interpretation (e.g., https://github.com/coq-contribs/otway-rees/blob/7956542fbb559fcda240c6059919a95ae4c10590/securite.v#L9).

I've found that (Query () Goals) always returns an empty list if -topfile is provided to sertop with any file name in version 8.10.0+0.7.2. The issue is resolved in version 8.11.0+0.11.1 (I have not tested 8.11.0+0.11.0). I suspect that https://github.com/ejgallego/coq-serapi/commit/ae1282c144a452f910766ad19e4225d9694e6810 implemented the fix, but I don't have a firm enough grasp of the internals of sertop or Coq to say for certain.

We would greatly appreciate a backport of a fix to a version of sertop compatible with Coq 8.10.2, which should allow us to include more projects in our dataset. Thank you

[ejgallego]

Hi @a-gardner1 , I think you have identified the right commit to backport in order to fix this problem.

Would you mind opening a pull request for the 8.10 branch? I'll be happy to do a release if you need it.

[ejgallego]

[closing as I won't address this myself, please feel free to reopen if you get to do this]