coq.env.add-const error messages · Elpi users & devs

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.

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.

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.

Gordon Stewart (Feb 01 2024 at 21:27):

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

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

Enrico Tassi (Feb 01 2024 at 21:57):

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.

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.

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.

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?

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).

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);
}

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.

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.

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.

Stream: Elpi users & devs

Topic: coq.env.add-const error messages

Gordon Stewart (Feb 01 2024 at 15:38):