Stream: Coq devs & plugin devs

Topic: Use of kernel names in tactic notations


view this post on Zulip Maxime Dénès (Mar 06 2022 at 17:09):

I'm wondering why Tactic Notation uses kernel names for grammar extensions : https://github.com/coq/coq/blob/master/plugins/ltac/tacentries.ml#L272

view this post on Zulip Maxime Dénès (Mar 06 2022 at 17:11):

It makes separation of parsing and execution a bit tricky because this kernel name is generated by a gensym, so I'd like to understand why its use is not limited to interpretation.

view this post on Zulip Maxime Dénès (Mar 06 2022 at 17:11):

I guess @Pierre-Marie Pédrot may know more :)

view this post on Zulip Pierre-Marie Pédrot (Mar 06 2022 at 22:19):

What would you use instead? Despite the name, tactic notations are not notations, they really extend the Ltac runtime.

view this post on Zulip Pierre-Marie Pédrot (Mar 06 2022 at 22:24):

(You can probably get rid of the gensym but then you have to be careful to get a reproducible name with a low probability of conflict out of the production list.)

view this post on Zulip Maxime Dénès (Mar 06 2022 at 23:22):

I mean: why are they used for grammar extensions, and not just for the interpretation part of Tactic Notation?

view this post on Zulip Maxime Dénès (Mar 06 2022 at 23:24):

My question is not philosophical :) I simply have a hard time following the code in pcoq and lower parsing layers

view this post on Zulip Maxime Dénès (Mar 06 2022 at 23:25):

So I don't know what the kernel name passed to extend_tactic_grammar is used for.

view this post on Zulip Maxime Dénès (Mar 06 2022 at 23:34):

Ah but ok, I understand now, it comes back to add_tactic_entry.


Last updated: Jun 09 2023 at 07:01 UTC