Stream: Coq users

Topic: [OcamlAPI] [SerAPI][*] Do we have a definition in file?

view this post on Zulip Andrey Klaus (May 06 2022 at 08:26):

Hello everyone!

So, I need to know if I have a definition in the given file. I imagine something like

coqc --list-definitions MyFile.v | grep my_definition_name

So, basically I need only know answer like 'yes' | 'no' to the question 'do we have definition with name like..' .

It may be also useful to have an answer to the question 'Do we have a definition of type ...' . Might be something like

coqc --list-definitions-with-type 'MyPredicate some_another_definition' MyFile.v
Definition defintion1 : MyPredicate some_another_definition.
Fixpoint fixpoint2 : MyPredicate some_another_definition.

If anybody could point me to Ocaml API / SerAPI documetation where similar questions are discussed, this would be great.

view this post on Zulip Karl Palmskog (May 06 2022 at 12:15):

@Andrey Klaus doesn't coq-dpdgraph give you this information already to some extent? By default, it records which constants live Prop, and the rest presumably live in Type or Set. coq-dpdgraph doesn't fully connect to file level though (this information is only available in a low-level API in Coq, to my knowledge)

view this post on Zulip Karl Palmskog (May 06 2022 at 12:17):

SerAPI can give easily give you a list of Vernacular Definition commands in a file. However, this is very different from a kernel-level definition, you can't know whether it lives in Type or Prop. A file can result in many kernel-level constants being added as commands are processed (one command can result in many kernel constants).

There has been ongoing discussions on how to define a "Coq DB" where both file-level and kernel-level information is available and explicitly interconnected. But this is at the design stage.

view this post on Zulip Andrey Klaus (May 06 2022 at 12:33):

I didn't know about coq-dpdgraph. Already taking a look on coq-dpdgraph, thank you very much!

Last updated: Jun 24 2024 at 01:01 UTC