Andrey Klaus (May 06 2022 at 08:26): 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
my_definition_name_1
my_definition_name_2
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.
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)
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.
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: Apr 19 2024 at 00:02 UTC