Stream: SerAPI

Topic: Get span information of goals


view this post on Zulip Axel Marmet (Nov 02 2021 at 15:59):

Hello,

Is there any way to get span information for the hypotheses and goal when querying their ASTs? It makes sense that the loc object is empty since the hypotheses and goal were not written in the document but I wonder if it's possible to get the info somehow. Thanks!

view this post on Zulip Emilio Jesús Gallego Arias (Nov 03 2021 at 15:47):

HI @Axel Marmet , unfortunately this is not possible today, this is due the way Coq's printer work.

Let me summarize the situation:

So indeed, as you can see, you are looking at the data generated at step 2, however, textual locations don't appear until step 4 as the provenance of the objects is not from a text document

view this post on Zulip Emilio Jesús Gallego Arias (Nov 03 2021 at 15:49):

Imagine this case (App (Ref "f") [arg1;...;argn])

view this post on Zulip Emilio Jesús Gallego Arias (Nov 03 2021 at 15:49):

the printing routine could split the application in two lines to fit it in the window, depending on the size of the display port

view this post on Zulip Emilio Jesús Gallego Arias (Nov 03 2021 at 15:49):

so @Axel Marmet , the way I'd address your question is maybe trying to understand a bit more what you are trying to do

view this post on Zulip Emilio Jesús Gallego Arias (Nov 03 2021 at 15:51):

we have some alternative output formats in the works, maybe it could work for you


Last updated: Feb 06 2023 at 06:29 UTC