Stream: Elpi users & devs

Topic: coq.env.add-const error messages


view this post on Zulip Gordon Stewart (Feb 01 2024 at 15:38):

I'm trying to improve error messages in our C++ specification tool, which makes use of coq.env.add-const Name E _ _ C on terms E that may not be closed.

In the nonclosed case, add-const gives messages like:

Error:
builtin coq.env.add-const: 2th argument: expected closed_term got:app
  [global (const «specify»), global (const «thread_info»),
   global (const «_Σ»), global (const «Σ»), global (const «σ»),
   app ...

The open term is printed in coq-elpi abstract syntax, making it difficult to read.

My current workaround is to check whether E is ground (using ground_term), and then print it via {coq.term->string E} if it is not ground. This gives better errors but still not as good as plain Coq.

Is there some way to improve here? If I could explicitly list the unification variables/evars in E with their types, that would help.

view this post on Zulip Enrico Tassi (Feb 01 2024 at 17:31):

Hi Gordon, what I propose is a new api coq.sealed-goal->string to be chained with collect-goals. Coq would do a better job and report the location of the holes in the text, but that is currently out of reach.

view this post on Zulip Gordon Stewart (Feb 01 2024 at 21:27):

Thanks. collect-goals is a good idea, and coq.sealed-goal->string would definitely improve errors.

Currently, collect-goals gives:

Goals:
[nabla c0 \
  seal
   (goal [decl c0 `this` (global (const «ptr»))] (X0 c0)
     (sort (typ «universes.Quant»)) (X1 c0) [])]

in my use case, which isn't super readable :-)

view this post on Zulip Enrico Tassi (Feb 01 2024 at 21:57):

Right, via the Coq goal printer it should look like:

this : ptr
===================
Type

Not sure this rendering will help much for holes with such a general type. Here I guess the location is more important than the type, I'm afraid.

I was expecting to find missing type class instances, or the like...

view this post on Zulip Gordon Stewart (Feb 01 2024 at 22:07):

I think in general we will have errors like missing typeclass instances.
And those errors are currently most egregious for us. The above example is
particularly unconstrained.

Gordon Stewart
gordon@bedrocksystems.com

BedRock

Systems Inc
UNBREAKABLE FOUNDATION *FOR *
FORMALLY SECURED COMPUTING

view this post on Zulip Paolo Giarrusso (Feb 07 2024 at 15:17):

I believe this example is realistic tho. In a formula, it comes up if you write say forall x y, P x -> Q y -> R, and later delete mentions of y (like Q y) without deleting y. Our specs are large enough that these errors become hard to spot by hand.

view this post on Zulip Paolo Giarrusso (Feb 07 2024 at 15:19):

Typeclass Instances still arise as Gordon said, so Enrico's proposal would be progress, but it's unfortunately incomplete. Wouldn't such problems affect hierarchy builder as well?

view this post on Zulip Enrico Tassi (Feb 07 2024 at 16:50):

Right now we use unification for inference, so the errors are actually typing errors, which already come with "readable" messages. We also have some hacks to make them more readable (a bunch of notations, they are explained in the MC book, IIRC).

view this post on Zulip Gordon Stewart (Feb 21 2024 at 21:31):

I looked briefly into adding sealed-goal->string but don't know a lot about either coq or elpi internals :-(

Is the following in coq_elpi_builtins.ml the right spot to add pretty-printing support for sealed goals?

let sealed_goal = {
  Conv.ty = Conv.TyName "sealed-goal";
  pp_doc = (fun fmt () -> ());
  pp = (fun fmt t -> Format.fprintf fmt "TODO");
  embed = sealed_goal2lp;
  readback = (fun ~depth _ _ -> assert false);
}

I'm not even sure of the type of t in (fun fmt t -> ...). Is there already an appropriate Coq pretty printer somewhere here: https://github.com/coq/coq/blob/7e99e53f6e05b8e3ed243f761a948a8779f4241f/printing/printer.mli?

view this post on Zulip Enrico Tassi (Feb 21 2024 at 22:11):

I think the easiest way to start is to use the goal (and not sealed_goal) data type, since it has a readback function returning a triple, one item is the evar, and call Printer.pr_evar on it. See call-ltac1 for a use of goal, coq.term->pp for the ppboxes thing (and the with_pp_option combinator it uses).

Writing a sealed-goal readback is easy/orthogonal. The t should be an evar, the evar linked to X in nabla x1\ nabla xn\ seal (goal Ctx Raw Ty X Args) that has type Ty and context Ctx. The readback has to peel off the nabla, then the seal, then call the readback for goal...

You can't just fix the pp there, since it lacks the sigma needed in order to call the printer on the evar. I mean, you could print the evar number, but not much more.

view this post on Zulip Enrico Tassi (Feb 21 2024 at 22:14):

I think you should take coq.term->pp as a template, but take in input a goal and output a ppboxes. use get_sigma to get a sigma out of the state, call the printer for evars and that should be it. I can give it a shot, but not today.

view this post on Zulip Enrico Tassi (Feb 21 2024 at 22:28):

The printer I pointed you to does not seem to do a nice job, but should be a decent starting point... the printer for goals (which a just evars) has some very defensive signature, not obvious how to craft its input from a (morally equivalent) evar.

view this post on Zulip Enrico Tassi (Feb 22 2024 at 08:34):

https://github.com/LPCIC/coq-elpi/pull/602


Last updated: Oct 13 2024 at 01:02 UTC