$ Notation in Clightdefs makes Ltac2 hard to use

[MSoegtropIMC]

I hesitated a bit to mention this, because it is not a problem of Compcert, but the $ Notation in Clightdefs:

(

CompCert/exportclight/Clightdefs.v

Line 180 in 6106e04

Notation "$ s" := (ltac:(ident_of_string s))

)

causes severe issues for me. It hides the trivial term anti quotation of Ltac2. I discussed this to quite some length with Pierre-Marie Pedrot, and there is no pleasant work around or way to fix this on the Ltac2 side, since injecting anti quotations into arbitrary Gallina terms is necessarily a bit low level. Essentially instead of the $x in:

Require compcert.exportclight.Clightdefs.
Require Import Ltac2.Ltac2.

Ltac2 test (a : constr) :=
match! a with
| ?x => constr:($x)
end.

I have to write something like ltac2:(rct x), where rct is a defined function producing a refine. This doesn't look that bad, but if I have to do this 10 times for a function with 10 arguments, the Ltac2 code gets hard to read and error prone. Furthermore this is less efficient at run time.

Since this notation does not seem to be widely used (CompCert compiles fine after removing it), I wonder if it could be removed or at least put into a separate module one can load as needed.

[xavierleroy]

I'll look into this soon when I have more time. Generally speaking, I introduced this notation recently, and I don't think it's being used yet, so we can certainly find another notation, and/or put it in a special scope (not string_scope).

[MSoegtropIMC]

That would be great!

I don't think the scope matters - it would only affect the interpretation of notations, but not the grammar as such. Afaik the Ltac2 trivial anti quotation:

https://coq.inria.fr/refman/proof-engine/ltac2.html#term-antiquotations

(a few pages down under "Trivial term anti quotations") is affected by the mere existence of the $ entry in Coq's parser tables. But what would help is putting the notation into a separate module (say Like ListNotations) which one can include if needed.

[MSoegtropIMC]

You are right, closing string scope works. I actually have this in some of my older developments and forgot about it (I understood @ppedrot in a discussion such that closing the scope wouldn't help).

This does work:

Require Import compcert.exportclight.Clightdefs.
Require Import Ltac2.Ltac2.

Close Scope string_scope.

Ltac2 test (a : constr) :=
match! a with
| ?x => constr:($x)
end.

So it is not that bad - I can usually live with closing string scope.

I would rate this as "nice to have" now. It is still nice to have since many notations in the standard library are also kept in modules, even basic stuff like ListNotations.

[xavierleroy]

Commit bb5dab8 moves the problematic notation to a separate sub-module AND to a specific scope clight_scope. Either fix (the submodule and the specific scope) is good style, so let's have both together, making room for future clightgen-related notations.

[MSoegtropIMC]

Thanks! Having both a separate module and a separate scope is indeed a good solution.