Thomas Dziedzic (Jan 23 2022 at 13:27): Thomas Dziedzic (Jan 23 2022 at 13:27):I'm trying to accomplish the following with https://github.com/ejgallego/coq-serapi
For 1. I was thinking (Query () (Vernac "Print All.")) and for 2. I was thinking of checking if the output of Print All. starts with a *** [ .
Emilio Jesús Gallego Arias (Jan 23 2022 at 13:33):Hi @Thomas Dziedzic , note that we have a dedicated SerAPI stream in case you want to move the discussion there [more people will see it]
Thomas Dziedzic (Jan 23 2022 at 13:34):@Emilio Jesús Gallego Arias I didn't know that, I will move the topic to that stream!
Emilio Jesús Gallego Arias (Jan 23 2022 at 13:35):Actually the next version will provide native support for your use case 1. , for now you have to do that a bit more manually, that is to say, you need to grab all (Query ((sid $stm)) Ast) and select the ones that are theorems. Current implementation of SerAPI uses the flag document model that Coq understands natively, but as I said, based on numerous feedback we are changing this to a more structured represeantion
Emilio Jesús Gallego Arias (Jan 23 2022 at 13:35):For 2, once you got the name of the theorem, you have an Assumptions query
Emilio Jesús Gallego Arias (Jan 23 2022 at 13:35):so that should work for you fine!
Emilio Jesús Gallego Arias (Jan 23 2022 at 13:35):I think the syntax is (Query ((sid $sid)) (Assumptions thm_name))
Emilio Jesús Gallego Arias (Jan 23 2022 at 13:36):note that in Query
Notification Bot (Jan 23 2022 at 13:37):This topic was moved here from #Coq users > serapi usage: getting theorems in a project by Théo Zimmermann
Emilio Jesús Gallego Arias (Jan 23 2022 at 13:37):the sid parameter means what "state" you want to query
Emilio Jesús Gallego Arias (Jan 23 2022 at 13:38):the sid parameter means what state you want to run the query
Emilio Jesús Gallego Arias (Jan 23 2022 at 13:38):so usually, for full completed documents you want to use the sentence pointing to the end of the document
Thomas Dziedzic (Jan 23 2022 at 13:39):Actually the next version will provide native support for your use case 1.
Do you know when the next version will come out? Will I have to wait a couple of days? Or will it be months?
Thomas Dziedzic (Jan 23 2022 at 13:41):also I just realized you're the creator of serapi, thanks for your hard work @Emilio Jesús Gallego Arias
Emilio Jesús Gallego Arias (Jan 23 2022 at 14:06):Thomas Dziedzic said:
Actually the next version will provide native support for your use case 1.
Do you know when the next version will come out? Will I have to wait a couple of days? Or will it be months?
You are most welcome, thanks to you for your feedback; I think the next version should be out by end of Feb, in the most optimistic planning
Emilio Jesús Gallego Arias (Jan 23 2022 at 14:07):I hope to have a couple of hacking sessions related to SerAPI in the 2022 Winter WG https://github.com/coq/coq/wiki/CoqWG-2022-02
Karl Palmskog (Jan 23 2022 at 15:39):@Thomas Dziedzic there is some functionality in the direction you want in the dpdgraph plugin: https://github.com/coq-community/coq-dpdgraph/
For example, it's very easy to get a list of lemmas in some module/file, and get their dependencies. No easy way to tell if something is an axiom though.
Karl Palmskog (Jan 23 2022 at 15:41):the difference from SerAPI is that as a plugin, dpdgraph adds some commands inside Coq, rather than allowing low-level communication with Coq. So it can be combined with SerAPI.
Emilio Jesús Gallego Arias (Jan 23 2022 at 15:55):Actually doing that in OCaml is very easy so if you wanna cook a patch we could merge itn ow
Emilio Jesús Gallego Arias (Jan 23 2022 at 15:55):it now
Emilio Jesús Gallego Arias (Jan 23 2022 at 15:55):what I plan is something more comprehensive
Emilio Jesús Gallego Arias (Jan 23 2022 at 15:55):The first prototype of coq-lsp already did that to provide the document outline
Karl Palmskog (Jan 23 2022 at 15:59):hmm, but did it [coq-lsp] really figure out axioms? How is that even done?
Emilio Jesús Gallego Arias (Jan 23 2022 at 16:41):The axioms code is already on serapi
Emilio Jesús Gallego Arias (Jan 23 2022 at 16:42):coq lsp parsed the document and generated the list of objects, including lemmas
Emilio Jesús Gallego Arias (Jan 23 2022 at 16:42):then it checked the document using prefix-only incrementality
Emilio Jesús Gallego Arias (Jan 23 2022 at 16:42):this is easy with the API we pushed to Coq these days
Emilio Jesús Gallego Arias (Jan 23 2022 at 16:42):axioms you just use the API provide in Coq
Last updated: May 31 2023 at 04:01 UTC