Stream: SerAPI

Topic: serapi usage: getting theorems in a project


view this post on Zulip Thomas Dziedzic (Jan 23 2022 at 13:27):

I'm trying to accomplish the following with https://github.com/ejgallego/coq-serapi

  1. Get a list of all top level theorems in a project.
  2. Decide whether the theorem is an axiom or depends on an axiom. (whether it's admitted or defined as an axiom? does Coq have a term for these types of theorems?)

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 *** [ .

view this post on Zulip 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]

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jan 23 2022 at 13:35):

so that should work for you fine!

view this post on Zulip Emilio Jesús Gallego Arias (Jan 23 2022 at 13:35):

I think the syntax is (Query ((sid $sid)) (Assumptions thm_name))

view this post on Zulip Emilio Jesús Gallego Arias (Jan 23 2022 at 13:36):

note that in Query

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jan 23 2022 at 13:37):

the sid parameter means what "state" you want to query

view this post on Zulip Emilio Jesús Gallego Arias (Jan 23 2022 at 13:38):

the sid parameter means what state you want to run the query

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jan 23 2022 at 15:55):

it now

view this post on Zulip Emilio Jesús Gallego Arias (Jan 23 2022 at 15:55):

what I plan is something more comprehensive

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Jan 23 2022 at 15:59):

hmm, but did it [coq-lsp] really figure out axioms? How is that even done?

view this post on Zulip Emilio Jesús Gallego Arias (Jan 23 2022 at 16:41):

The axioms code is already on serapi

view this post on Zulip Emilio Jesús Gallego Arias (Jan 23 2022 at 16:42):

coq lsp parsed the document and generated the list of objects, including lemmas

view this post on Zulip Emilio Jesús Gallego Arias (Jan 23 2022 at 16:42):

then it checked the document using prefix-only incrementality

view this post on Zulip Emilio Jesús Gallego Arias (Jan 23 2022 at 16:42):

this is easy with the API we pushed to Coq these days

view this post on Zulip Emilio Jesús Gallego Arias (Jan 23 2022 at 16:42):

axioms you just use the API provide in Coq


Last updated: Feb 06 2023 at 06:29 UTC