The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

Hi all, hi Valentin,

It looks to me like the section mechanism is both super useful, which makes people continue to use it, and a constant pain, which makes people keep reporting bugs or feature-requests related to it.

In order for the Coq developers team to improve it, it would be good to know precisely what people use it for. I'm not saying that no one in the Coq developers team know what its uses are but it looks to me that at least some of them are lacking the knowledge of at least some of its uses.

In particular there is a more recent mechanism called Generalizable Variables https://coq.inria.fr/distrib/8.5pl3/refman/Reference-Manual004.html#hevea_command71 (introduced in 8.3 while sections go back as far as I can see in CHANGES, that is beyond 7.0).

What do you want to do with sections that you cannot do with Generalizable Variables? In particular, could the use of the latter instead of the former solve the particular problem you are having (since anyway, wanting to define the same notation inside and outside the section probably means that your section variables are implicit anyways).

Cheers,

Théo

Le mer. 23 nov. 2016 à 23:22, Vadim Zaliva <vzaliva AT cmu.edu> a écrit :

I usually go with your option #1 and as you mentioned it is not perfect.

I would be great to have "Global" modifier for "Notation" command like we have for 

"Instance".

Vadim

--

CMU ECE PhD candidate

Mobile: +1(510)220-1060

On Tue, Nov 22, 2016 at 4:13 PM, Valentin Robert <valentin.robert.42 AT gmail.com> wrote:

Dear club,

According to the reference manual:

"Notations do not survive the end of sections."

I would like to understand whether a) this is a wanted feature b) this is a constraint or c) a choice of the current implementation, or d) this is due to some theoretical issue with trying to make them survive.

In particular, I often find myself in the following conundrum:

- I open a section and define some section context (variables and definitions).

- I define something that I'd like to use a notation for.

- I want to use the notation within the rest of the section, but also outside the section.

It seems my options are:

i)

Define the notation once for within the section, and then again after leaving the section.

Not great if I later decide to change the notation and want to keeps things uniform.

ii)

Abandon the idea of having the notation within the section.

Makes the section theorems harder to read from the source code point of view.

iii)

Close the section. Define the notation. Open a similar section.

Not great if the section setup is heavy, and this artificially breaks sections into weird notation-separated-blocks.

Is there a better way of going about this I'm missing? Otherwise, which poison do people pick?

- Valentin