Stream: Coq devs & plugin devs

Topic: Using the Coq core library

view this post on Zulip Julien Puydt (Mar 12 2024 at 17:25):

I wrote OCaml code which for the moment prints .v files, checked validity using coqc. I'm trying to turn this into OCaml code which directly uses the coq-core library to build and check terms.

My typical .v file is structured like this:

  1. set the stage (require import what I need, define some options) ;
  2. declare some variables ;
  3. use "Check" sentences for terms using those variables (terms = string representation of terms for now).

Here are my current leads for how to do all of this using coq-core.

The first issue is how to properly initialize the library - I think toplevel/coqtop.ml's init_toplevel is an example ; but it sets up a state-transaction-machine and I'm not sure I really need it. It looks like checker/* uses that, but the comparison might not be sound.

Then my files use things like "Require Import ZArith Coq.Programs.Basics." which I think will just mean preparing the right injections above if I'm right on the initialization idea.

I have no start yet on how to turn a string like "123" to the actual 123%N Constr.constr object, nor how to do the equivalent of "Check term".

Finally I'll still want my program to print about its success building terms but for now turning a Constr.constr to a string looks convoluted: I think string_of_ppcmds is probably the last step, but just composing it with debug_print doesn't look correct.

Can someone shed some light on those matters? Thanks!

view this post on Zulip Audrey Seo (Mar 12 2024 at 19:57):

Not sure how to do the first parts, but for turning Constr.constr into strings, I've been using

(* val constr_to_string : Environ.env -> Evd.evar_map -> Constr.constr -> string *)
let constr_to_string env sigma c =
  Pp.string_of_ppcmds (Printer.pr_constr_env env sigma c)

For outputting to Coq, you can use something like

let print_message env t sigma = Feedback.msg_notice (constr_to_string env sigma t)

view this post on Zulip Julien Puydt (Mar 13 2024 at 09:44):

@Audrey Seo your constr_to_string function looks nice, thanks

view this post on Zulip Emilio Jesús Gallego Arias (Mar 13 2024 at 15:45):

@Julien Puydt , you can look at https://github.com/coq/coq/pull/16190 as a reference for a toplevel.

In general you don't want to write your own toplevel, but use some extensible toplevel or compiler like serapi or fcc, but YMMV.

view this post on Zulip Julien Puydt (Mar 14 2024 at 12:21):

@Emilio Jesús Gallego Arias I really want my code to be written in OCaml and using internal Coq structures rather than an external interface.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 14 2024 at 17:01):

@Julien Puydt fcc supports OCaml plugins, do depending on your use case that could save you lots of work, YMMV. For example, if you want to print a file's from its Ast, in fcc you can do that with a plugin in a few files and you save a lot of work, etc... As I said, in general you don't want to write the toplevel, but there are cases you may want to, depends what you need! You don't want to write your own toplevel because the API is not easy to use correctly, there are quite a few things to keep in mind, but of course feel free to try!

view this post on Zulip Julien Puydt (Mar 15 2024 at 07:29):

@Emilio Jesús Gallego Arias I don't know anything about fcc - I just know I'm working on elaboration so I would need to be pretty much inside Coq to do things properly...

Last updated: Oct 13 2024 at 01:02 UTC