Deactivation of notations: providing vernac syntax, vo registration and support for deactivation of abbreviations

[herbelin]

Kind: feature

This extends #703 on selective deactivation of notations by adding:

• concrete syntax for deactivation/reactivation
• registration in vo files
• support for deactivation of abbreviations

Added: Now depends on #12690 (merged) and #12950 (merged) and supports selective only-parsing or only-printing deactivation.

Concrete syntax for deactivation/reactivation

The currently proposed syntax is:

• for notations

  Deactivate Notation "_ + _" (in custom foo) : scope.
  Activate Notation "_ + _" (in custom foo) : scope.
  

  where both (in custom foo) and : scope are optional, defaulting to constr and lonely notation respectively
• for abbreviations

  Deactivate Notation foo.
  Activate Notation foo.
  

I wonder whether this could not be reusing Set/Unset even if a non standard use of it.

Adding support for deactivation of abbreviations

We obtain this by adding a new remove function to the name table.

Miscellaneous

In passing, we include the only printing notations in Print Scopes.

Fixes #4803

Status

• [ ] I did not port nor give syntax to show_inactive yet. Not clear what would be the best user interface for it.

• [ ] I did not do anything about deactivate_scope/reactivate_scope/show_scope (no syntax, no registration in vo)

• [ ] More testing needed

• [X] Added / updated test-suite

• [ ] Corresponding documentation was added / updated

• [ ] Entry added in the changelog

[Zimmi48]

I wonder whether this could not be reusing Set/Unset even if a non standard use of it.

I'm not very fond of this idea. On the contrary, I'd like to move the last non-standard use of Set (Warnings) to a new mechanism...

[proux01]

Is there a way to activate/deactivate only for parsing/printing? would there be a use for that? (if that makes any sense)

[herbelin]

Is there a way to activate/deactivate only for parsing/printing? would there be a use for that? (if that makes any sense)

Funny, that's what I was precisely thinking too. That would be easy to do too. Syntax could be e.g.:

Deactivate Notation "_ + _" (in custom foo, only parsing) : scope.
Deactivate Notation "_ + _" (in custom foo, only printing) : scope.

I don't like so much Deactivate which is a new command name to remember, but I don't have a good alternative.

[Zimmi48]

I don't like so much Deactivate which is a new command name to remember, but I don't have a good alternative.

It looks to me like the Deactivate syntax is very close to the Notation syntax. Then, an option is to reuse the Notation command but with an attribute. BTW, I think "disable" is a simpler word than "deactivate" that conveys the same meaning. So this would give:

#[ disable ] Notation "_ + _" (in custom foo, only parsing) : scope.
#[ disable ] Notation foo.
#[ disable ] Infix "/\".

BTW, some other command with a very close syntax is Reserved Notation. It could also become an attribute:

#[ reserve ] Notation "x \/ y" (at level 85, right associativity).
#[ reserve ] Infix  "∘" (at level 40, left associativity).

[herbelin]

Following @proux01' remark, I propose to enforce the following model for activation/deactivation:

• To any triple of a constr or custom entry, notation string and scope can be associated at most one "main" notation + an arbitrary number of only-printing. This actually reflects the current situation which indeed tolerates for convenience an arbitrary number of distinct interpretation for only-printing notations
• A main notation consists of either an only-parsing notation or of a "regular" notation with both parsing and printing.

When there is only one notation, whether it is its parsing rule which has to deactivated (if any), its printing rule (if any), or both, it would be enough to give the string and, if not a lonely notation, the scope, and, if in an entry different from constr, the name of the custom entry. This would mean (as given above) a command of the form (whatever the exact syntax):

Deactivate Notation "_ + _" (in custom foo, only printing) : scope.
Deactivate Notation "_ + _" (in custom foo, only parsing) : scope.

with all of in custom foo, or only printing/only parsing, or : scope optional.

When there are several, we would need however to specify the interpretation as in:

Deactivate Notation "_ + _" := term (in custom foo, only printing) : scope.

Should we tolerate the syntax without an interpretation and make it default to the main interpretation when the only printing flag is not used (since there would then be only one not-only-printing notation)?

[coqbot-app[bot]]

For your complete information, the job test-suite:base+async in allow failure mode has failed for commit 44949c1c62e56967d8cd41e63826fa63464e362d: Adding support for deactivating/reactivating notations.

[silene]

I do not intuitively understand what Deactivate Notation "_ + _" (in custom foo, only printing) : scope means. Does it mean that the notation is now only used for parsing? Or that it is used only used for printing?

Thus, associating some change of behavior to a negative command (i.e., Deactivate) seems like a bad idea. It would be better to make it part of a positive command (e.g., Activate).

[gares]

While I clearly see the interest of this feature, I find the "user interface" a bit cumbersome.

If I'm a regular user how am I supposed to guess all this data: Deactivate Notation "_ + _" (in custom foo, only printing) : scope? I mean, I may want to see what is behind _ + _ in the current goal, but asking me more than the characters I see seems too much.

If I'm a library designer I would know how to find that metadata, but being forced to repeat all that metadata seems painful (copy pasting it may double maintenance cost). I'd be happier to give (the few) notations that I want to disable a name or a category and mention that name/category in another file were I gather, say, the settings for beginners.

[herbelin]

I do not intuitively understand what Deactivate Notation "_ + _" (in custom foo, only printing) : scope means. Does it mean that the notation is now only used for parsing? Or that it is used only used for printing?

The idea was that it stopped to be used for printing. I agree that this combination of a negative command and "only" is unclear.

If I'm a regular user how am I supposed to guess all this data: Deactivate Notation "_ + _" (in custom foo, only printing) : scope?

Use of custom entry remains seldom, so, in the general case, if you want to deactivate both printing and parsing, it would just be something like Deactivate Notation "_ + _" : nat_scope.

I mean, I may want to see what is behind _ + _ in the current goal, but asking me more than the characters I see seems too much.

That's a very legitimate use but I don't see how to do it easily, if not with the help of the UI. Especially, if it is in a complex expression, the scope is generally implicit and difficult to reconstruct.

For your usage, I would rather rely on the UI, either by sending it a rich output with hidden annotation revealed when hovering over the notation with the mouse, or the UI sending a request to Coq when hovering on a given location of the goal. I understood that this was something @maximedenes was working in the context of LSP.

From a textual interface, I don't see how to avoid, say, some Locate "_ + _" followed by the appropriate Deactivate, because I don't see how to magically know which + of which grammar and of which scope we are talking about when we see it on screen, especially if we are an ousider and not familiar with the given context.

I'd be happier to give (the few) notations that I want to disable a name or a category and mention that name/category in another file were I gather, say, the settings for beginners.

Could you elaborate on this? What kind of user API would this correspond to?

More generally, let me remind that I'm ok with different kinds of concrete syntax, but we have already to clarify the level of fine-tuning and simplicity we need (parsing or printing or both, one "+" in some scope and entry, or all "+" of all scopes and entry, ...).

Actually, maybe should we try and experiment and possibly revise afterwards.

[gares]

That's a very legitimate use but I don't see how to do it easily, if not with the help of the UI. Especially, if it is in a complex expression, the scope is generally implicit and difficult to reconstruct.

That is exactly my point. The non-expert user may just say Disable "+" and have all the notations having + as a token to be disabled. This is the user API I was hinting at. It may be too rough for an expert user, but a beginner can surely use it, while the one proposed in the PR seems too hard to me.

Could you elaborate on this? What kind of user API would this correspond to?

My use case is that in Math Comp we have too many notations for a beginner even in simple files like ssrnat. When we teach, it helps to disable some of them, and re-introduce them "slowly".

For example last time we had a notation = true to display the is_true coercion during the first session; we disabled x < y := S x <= y and a < b < c := a < b && b < c and more of the like during the second one.

All this requires to fork Coq, fork MathComp, build a custom jscoq... not very easy. If I could sneak an attribute next to the notation for, say, < (and all the others that I find disturbing for a beginner) and disable them in one go from a beginner.v file, I could just ask the students to load that file!

[herbelin]

The non-expert user may just say `Disable "+"

Yes, we can provide that also.

If I could sneak an attribute next to the notation for, say, < (and all the others that I find disturbing for a beginner) and disable them in one go from a beginner.v file, I could just ask the students to load that file!

Rather than anticipating for each notation how it would have to behave in a beginner.v file, wouldn't be as easier for a teacher, and also less intrusive in the original development, and also more flexible, that the teacher aggregates a set of "surgical" variants of Disable in this beginner.v file?

[herbelin]

Finally rebased on top of its dependencies! I'm still a bit in the fog about the user API and syntax though.

1. Deactivate combined with only or so is accordingly bad. So, maybe Toggle Notation Off "_ + _" (only parsing), Toggle Notation On "_ + _" : scope.
2. For deactivating all "_ + _" at the same time, maybe Toggle Notation Off "_ + _" : all, if really needed
3. No opinion on #[ enable ] Notation "_ + _" : nat_scope

Comments and suggestions needed. I'm leaning otherwise towards option 1.

[proux01]

1. Deactivate combined with only or so is accordingly bad. So, maybe Toggle Notation Off "_ + _" (only parsing), Toggle Notation On "_ + _" : scope.

Does that deactivate parsing or keep parsing?

What about

Toggle Notation "_ + _" (only parsing).
Toggle Notation "_ + _" (only printing).
Toggle Notation "_ + _" (off).
Toggle Notation "_ + _" (on).

but I still find toggle quite ambiguous (maybe Set Notation?).

[cpitclaudel]

This looks like a wonderful feature. Most often, though, what I want to do is deactivate a whole scope worth of notations. Close Scope do that; I wonder if it would be easy to implement. The API would be very simple : Deactivate Scope xyz_scope.

Regarding attributes, it seems odd to use them for this. Are there other cases when the command takes on a completely different meaning when an attribute is added? (The examples I have in mind are like #[program], which tweaks the behavior of an existing command).

Regarding the API of the per-notation feature: it would be great if each line of the output of Locate "+" could be used to deactivate the corresponding notation by pasting it directly after Locate Notation. And with a plain string, Deactivate "+" would mean disable everything that is returned by Locate "+" (this flexibility is very nice in unfold, for example)

Thanks a lot for working on this!

[Zimmi48]

Regarding attributes, it seems odd to use them for this. Are there other cases when the command takes on a completely different meaning when an attribute is added? (The examples I have in mind are like #[program], which tweaks the behavior of an existing command).

No indeed. Current attributes tweak the behavior rather than changing it entirely. Maybe what I proposed is stretching their use too far. It didn't get a lot of support anyway.

but I still find toggle quite ambiguous (maybe Set Notation?).

Note that Set + any combination of identifiers following it is already taken for flags and options.

[herbelin]

The general demand seems to be able to describe sets of notations in a variety of ways. So, it seems preferable to seek for a syntax with filters. So, coming back to Activate/Deactivate (but it could maybe also overload the role of Set/Unset), a proposed syntax is:

["Activate"|"Deactivate"]
  [|"Printing"|"Parsing"]
  ["Notation"|"Notations"]
  [|qualid|string] [|"for" pattern] [|"(in custom " ident ")"] [|":" scope].

with the following meaning:

• Parsing/Printing: restrict activation/deactivation to parsing/printing; applies otherwise to both
• each of optional ident/string, pattern, (in custom entry), : scope acts as a filter to select one or more notations
  • qualid selects abbreviations ending with qualid
  • string selects notations with the corresponding syntax, if string has no space, it refers to all notations containing the string (like Locate)
  • pattern selects abbreviations/notations matching the pattern at its head
  • in custom entry selects notations in such custom entry
  • : scope selects all notations in scope
• if Notation is given, the filter is expected to give exactly one result

Examples:

• Deactivate Notations "_ + _". -> deactivate all notations
• Deactivate Notations for Nat.add. -> deactivate all notations with head constant Nat.add
• Deactivate Notations "+" for Nat.add. -> deactivate all notations with head constant Nat.add
• Deactivate Notations : nat_scope -> deactivate all notations in scope nat_scope

Additionally, when all notations associated to a parsing rule have been deactivated, the grammar rule is removed.

For scopes, maybe in nat_scope would be clearer than : nat_scope? We could also imagine a syntax reminiscent of Search (e.g. with scope:nat_scope, pattern:Nat.add, head:Nat.add, ...)?

I'm unsure to be able to find the time to implement all the variety of filters shortly, but the syntax can still be anticipated and bound to the already existing activation/deactivation mechanism

[coqbot-app[bot]]

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

[SkySkimmer]

If the doc_gram can be fixed this may be ready?

[herbelin]

From memory, the discussion on the concrete syntax did not really converge, but otherwise, this was usable.

[Zimmi48]

At some point, you're the developer of this new feature, so it's your call to decide on a syntax, unless someone voices clear opposition to the chosen solution. I don't think we can expect a natural convergence for any syntax discussion.

That being said, I will try to summarize my current position as shortly as possible:

• I personally have some strong opposition about making Set / Unset become more polysemous than it is already today.

• I suggested something based on the new attribute syntax, but noticing that the (only parsing) and co mechanism is already a preexisting attribute syntax (specific to notations), my suggestion could be amended to just use this syntax (add new (off) and (on) attributes to toggle off / toggle on an existing notation and be done with it). This is similar to a proposal by @proux01 above, but without the need for the Toggle prefix.

[coqbot-app[bot]]

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

[herbelin]

Trying to combine the different ideas and in particular to replace @proux01's Toggle with on/off flags, as suggested by @Zimmi48, and also, to get even more closer to the syntax of Notation, I propose to implement tomorrow the following variant of my previous proposal (on/off mandatory and otherwise at least one other component among qualid, string, pattern, custom ident, scope).

"Tune" ["Notation"|"Notations"] [|qualid|string] [|":=" pattern]
   "(" [|"in" "custom" ident] [|"parsing"|"printing"] ["on"|"off"] ")"
   [|":" scope].

with same semantics as before (mutatis mutandis).

If the general idea is ok, possible synonyms of Tune would be Setup (to avoir Set!), Alter, Adjust, Revise, Tweak, Amend, ..

[jfehrle]

Typo: I think [|in custom " ident] should be [| "in" "custom" ident]

I suggest allowing only "Notation" and omitting "Notations", which might permit the parser to distinguish "Set Notation" as a special case distinct from "Set". It would break the pattern for "Set" but I think users would quickly catch on.

Distinguishing singular or plural won't affect user understanding, and we don't have to do odd things like this, nor include both versions in the command index. WDYT?

If "Set" won't work, how about "Transmogrify"? :-)

[herbelin]

Typo: I think [|in custom " ident] should be [| "in" "custom" ident]

Yes. Edited.

which might permit the parser to distinguish "Set Notation" as a special case distinct from "Set". It would break the pattern for "Set" but I think users would quickly catch on.

I would find it quite natural too. There were some objections though.

I suggest allowing only "Notation" and omitting "Notations"

Distinguishing singular or plural won't affect user understanding, and we don't have to do odd things like this, nor include both versions in the command index. WDYT?

The idea was to distinguish between denoting a single notation or possibly denoting a group of notations.

But we can imagine as alternative to have a modifier "all" to explicitly tell to catch all notations matching the criterion.

I still feel that one should be able to give an incomplete pattern expecting that it refers to exactly one notation and an error otherwise.

If "Set" won't work, how about "Transmogrify"? :-)

Why not! The word is amusing.

[jfehrle]

The idea was to distinguish between denoting a single notation or possibly denoting a group of notations.

"all" is a good alternative

I would find ["Set"] quite natural too. There were some objections though.

(Théo) I personally have some strong opposition about making Set / Unset become more polysemous than it is already today.

I think there's a reasonable point that it won't be entirely obvious that "Set Notation" is a different command from "Set", but the documentation of "Set" can mention that there are exceptions and that they will be listed separately in the command index. (I've noticed we have many commands that only set parameters such as "Hint Cut" that could have been done as "Set Hint Cut"--"Set ..." seems such an obvious choice. But there's no point in changing those.)

If "Set" won't fly, I would hope that the "Tune" (or whatever) prefix could be reused for other things, e.g. hypothetically like "Tune Hint Cuts". Maybe "Setup" or "Parms"? (The beauty of a committee decision is that no one is really satisfied with the result :-)).

Your call.

[Zimmi48]

My impression is that Toggle was dismissed too fast and none of the new suggestions seem to be any better. Toggle in combination with a mandatory on / off attribute does not sound ambiguous to me.

Anyway, my own suggestion was to avoid putting a verb first, but to keep Notation as the first word. I've recently read something that matches my intuition pretty well, so I will quote it instead of rephrasing it poorly:

Commands should follow a noun-verb dialogue. Although noun-verb formatting seems backwards from a speaking perspective (i.e. nix store copy vs. nix copy store) it allows us to organize commands the same way users think about completing an action (the group first, then the command).

Source: https://nixos.org/manual/nix/unstable/contributing/cli-guideline.html#naming-the-commands

When we look at our command index, we see many cases where putting the verb first have created issues. To start with, we have the Add / Remove commands for tables that conflict with the Add X commands and restrict how we can name tables. Similarly, Print is limited in its ability to print objects with some reasonable names because of all the Print X commands that exist. We also have not been able to properly turn Export into a legacy attribute that could be used (without the new #[ export ] syntax) in front of many commands simply because of the conflict with the Export command.

Anyway, it seems that it is the path that has been chosen (to match natural language more closely) and that it is too late to divert from it now (except in a new major version of the language, but that's probably not worth it).

[proux01]

Tune, Transmogrify or even Toggle look good to me. As a side question, would nothing be a solution?

"Notation" [|qualid|string] [|":=" pattern]
   "(" [|"in" "custom" ident] [|"parsing"|"printing"] ["on"|"off"] ")"
   [|":" scope].

that would avoid introducing a new keyword

[coqbot-app[bot]]

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

[gmalecha]

To support activating and deactivating many notations at once, would it be possible to have collections of notations? Perhaps there is some overlap with notation scopes here, but since arguments can bind notation scopes, this requires more than simply Close Scope ....

[coqbot-app[bot]]

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.