Saving theorem information to external database · Coq users

Hello, I am developing a project which uses Coq, and part of the project would require a way of extracting as much information about proven theorems/lemmas as possible, and then save it in an external database. Ideally, this would be done with something like a vernacular command, such as Print, where the user could write on the file

 Save theorem_name "Some theorem description"

and, when compiled, information such as the theorem name, the given user description, its type, its assumptions, and perhaps even the module it is defined in would be saved to the database (or, which could also work fine, to a separate file which could be easily read and parsed by another program).

I am trying to avoid having to parse the .v files, due to the highly flexible syntax definitions in Coq.

My question is then: what would be the correct tool to do this? I looked at the plugin tutorial and tried to emulate what was done there, but it was pretty complicated and I got stuck. I also looked at Ltac2, but I am not sure if I can define such a thing there.

Any ideas and suggestions would be greatly appreciated.

PS: I haven't used Zulip, so apologies if this message is in the wrong place.

Emilio Jesús Gallego Arias (Mar 23 2021 at 14:58):

Maybe https://github.com/ejgallego/coq-serapi could help, otherwise you'd have to write your own plugin.

Enrico Tassi (Mar 23 2021 at 17:13):

Maybe it's not the best language for doing this, but you can surely do it using coq-elpi:

From elpi Require Import elpi.

Elpi Command SaveInfo.
Elpi Accumulate lp:{{

main [str ThmName, str Comment] :- std.do! [
  coq.locate ThmName GR,
  coq.env.typeof GR Ty,
  open_append "db.txt" OC,
  output OC Comment,
  output OC "\n",
  output OC {std.string.concat " " {coq.gref->path GR} },
  output OC "\n",
  output OC {coq.term->string Ty},
  output OC "\n",
  close_out OC,
].

}}.
Elpi Typecheck.
Elpi Export SaveInfo.

SaveInfo plus_n_O "My Fist Theorem".

then

$ cat db.txt
My Fist Theorem
Coq Init Peano
(forall n : nat, n = n + 0)

Beoww (Mar 23 2021 at 18:11):

Enrico Tassi said:

Maybe it's not the best language for doing this, but you can surely do it using coq-elpi:

From elpi Require Import elpi.

Elpi Command SaveInfo.
Elpi Accumulate lp:{{

main [str ThmName, str Comment] :- std.do! [
  coq.locate ThmName GR,
  coq.env.typeof GR Ty,
  open_append "db.txt" OC,
  output OC Comment,
  output OC "\n",
  output OC {std.string.concat " " {coq.gref->path GR} },
  output OC "\n",
  output OC {coq.term->string Ty},
  output OC "\n",
  close_out OC,
].

}}.
Elpi Typecheck.
Elpi Export SaveInfo.

SaveInfo plus_n_O "My Fist Theorem".

then

$ cat db.txt
My Fist Theorem
Coq Init Peano
(forall n : nat, n = n + 0)

Thank you, that is really good, however, when I try to run it, it gets stuck in the line

Elpi Accumulate lp:{{

with the message

Syntax error: 'Db' or 'Files' or 'File' or [qualified_name] or [elpi_string] expected after 'Accumulate' (in [command]).

I am not familiar with Elpi or the Coq-Elpi plugin, so maybe it is some dependency I am missing?

EDIT: I was able to make it work with the other option for strings, namely, using

"
  code
".

instead of

lp:{{
  code
}}.

Enrico Tassi (Mar 23 2021 at 18:47):

Yes, you need CoqIDE for 8.13 or VSCoq (visual studio code ) in order to have this work, or put the elpi code in a file foo.elpi and replace it by Elpi Accumulate File "foo.elpi". which is something you want to do anyways at some point.

Enrico Tassi (Mar 23 2021 at 18:48):

EDIT: I was able to make it work with the other option for strings, namely, using

great! but I'm afraid you had to escape all " :-/

Enrico Tassi (Mar 23 2021 at 18:49):

If you decide to go this path, there is a Zulip stream dedicated to elpi. You may ask there for help navigating the APIs or for the addition of new ones (your use case is new to me)

Last updated: Oct 13 2024 at 01:02 UTC

Stream: Coq users