Stream: Coq users

Topic: import categories

Gaëtan Gilbert (Sep 16 2021 at 11:55):

A feature allowing to import subsets of modules by categories is coming soon; eg import only coercions or import everything except notations (where "coercions" and "notations" are categories)
What import-time effects do you want categories for?
(cf https://github.com/coq/coq/pull/14892)

Enrico Tassi (Sep 16 2021 at 12:16):

I've one request, but maybe it's too specific to my use case. In Coq-Elpi I do add a few libobjects. It would be nice if I could flag their declaration as ~category:"elpi" and then have this category to be available in the Import vernac.

Gaëtan Gilbert (Sep 16 2021 at 15:40):

Enrico Tassi said:

I've one request, but maybe it's too specific to my use case. In Coq-Elpi I do add a few libobjects. It would be nice if I could flag their declaration as ~category:"elpi" and then have this category to be available in the Import vernac.

if it's the object at https://github.com/LPCIC/coq-elpi/blob/8f60397e29c70cd8c8d5550cac9a5a51677651fd/src/coq_elpi_vernacular.ml#L296 it's just a matter of adding let cat = Libobject.create_category "elpi" somewhere and replacing simple_open by simple_open ~cat in the open_function
see also https://github.com/coq/coq/commit/18be4130f56dde13786e14bfd45ee0378c314d62

Pierre Rousselin (Nov 09 2023 at 15:35):

I'm having a good time browsing the Modules part of the refman.
I am still puzzled by the import categories, though.
With this:

Module A.
  Notation TT := Type.
  Definition N := nat.
  Tactic Notation "lol" := reflexivity.
End A.

Then in the same file,

1. if I Import -(ltac.notations, notations) A., then I have the following:

Print TT. (* succeeds! *)
Lemma plop : 0 = 0.
Proof.
  assert (A.N = nat).
  A.lol. (* fails *)

2. If I Import (ltac.notations) A., then

Fail Print TT. (* indeed fails *)
Print A.TT. (* succeeds *)
Lemma plop : 0 = 0.
Proof.
  assert (A.N = nat).
  lol. (* succeds *)
  A.lol. (* fails *)

Pierre Rousselin (Nov 09 2023 at 15:36):

I'm a bit lost about what is happening.

Gaëtan Gilbert (Nov 09 2023 at 15:36):

Notation foo := ... says Notation but it's treated as a name like Definition

Pierre Rousselin (Nov 09 2023 at 15:36):

Also, this:

Import (ltac.notations) A(N).

gives Cannot combine importing by categories and importing by names.

Pierre Rousselin (Nov 09 2023 at 15:37):

Gaëtan Gilbert said:

Notation foo := ... says Notation but it's treated as a name like Definition

Hmm... so it's not really a notation?

Pierre Rousselin (Nov 09 2023 at 15:38):

In the last case, why would a qualified tactic notation fail?
edit: same as anything else, sorry

Gaëtan Gilbert (Nov 09 2023 at 15:38):

https://coq.inria.fr/doc/master/refman/user-extensions/syntax-extensions.html#coq:cmd.Notation-(abbreviation)

Gaëtan Gilbert (Nov 09 2023 at 15:39):

Pierre Rousselin said:

In the last case, why would a qualified tactic notation fail?
edit: same as anything else, sorry

do qualified tactic notations ever succeed?

Pierre Rousselin (Nov 09 2023 at 15:41):

Gaëtan Gilbert said:

Pierre Rousselin said:

In the last case, why would a qualified tactic notation fail?
edit: same as anything else, sorry

do qualified tactic notations ever succeed?

I don't know... Why would tactical notations identifiers be different from the rest. They also have feelings, you know.

Pierre Rousselin (Nov 09 2023 at 15:47):

Gaëtan Gilbert said:

https://coq.inria.fr/doc/master/refman/user-extensions/syntax-extensions.html#coq:cmd.Notation-(abbreviation)

So, there is a difference between an abbreviation and a notation. Then, should there be an "abbreviation" category?

Pierre Rousselin (Nov 09 2023 at 15:57):

Also, how can I activate e.g. only notations from a module but still get short names for constants?

Gaëtan Gilbert (Nov 09 2023 at 16:01):

I don't think there's a category for that currently. Feel free to feature request or PR

Paolo Giarrusso (Nov 09 2023 at 22:12):

"only notations"... "Short names for constants" seems contradictory, but I guess a category for constants would help

Paolo Giarrusso (Nov 09 2023 at 22:13):

@Gaëtan Gilbert if you're right the manual is wrong

notations corresponding to Notation (including Reserved Notation), scope controls (Delimit Scope, Bind Scope, Open Scope) and Abbreviations.

Paolo Giarrusso (Nov 09 2023 at 22:15):

@Pierre Rousselin tactic notations extend the grammar when imported, but Coq doesn't synthesize parsing rules for qualified notations, and it's not clear that it can

Paolo Giarrusso (Nov 09 2023 at 22:17):

Normal notations have the same behavior. In Coq you can't type 1 Nat.< 2 < 3 or 1 < 2 Nat.< 3. Agda supports the first by having less expressive notations.

Gaëtan Gilbert (Nov 09 2023 at 23:27):

Paolo Giarrusso said:

Gaëtan Gilbert if you're right the manual is wrong

notations corresponding to Notation (including Reserved Notation), scope controls (Delimit Scope, Bind Scope, Open Scope) and Abbreviations.

manual was fixed a few hours ago in master

Pierre Rousselin (Nov 10 2023 at 06:18):

Paolo Giarrusso said:

"only notations"... "Short names for constants" seems contradictory, but I guess a category for constants would help

IIUC, Import has two different roles (which IMHO is one too many):

• activate some features (notations, hints, etc) from the module
• give access to short names for (all or some of the) constants defined in the module

The nice import categories allow the user to tweak the first role but make her give up on the second. This feels strange to me.

Paolo Giarrusso (Nov 10 2023 at 10:22):

It sounds like a reasonable extension. For now, what about: Import foo(F). Import (categories) foo. ? OTOH, I'm not sure Import foo(F). Import -(categories) foo. does the right thing, or that all combinations are covered.

Gaëtan Gilbert (Nov 10 2023 at 10:50):

Import foo(F). Import (categories) foo. yes

Gaëtan Gilbert (Nov 10 2023 at 10:54):

Basically Import (cats) foo(names) can be read as import objects which are in the categories AND which are the given names or import objects which are in the categories OR which are are the given names.
In the interest of being unambiguous we error instead.
(with the current categories the 1st reading would contain no objects, but we still have the problem for Import -(cat) foo(names) and if we add categories that intersect with names)

Pierre Rousselin (Nov 10 2023 at 14:05):

Here are my current experiments, the base is:

From Coq Require Arith.PeanoNat.

Module A.
  Definition N := nat.
  Definition my_add := Nat.add.
  Notation "x +++ y" := (x - y) (at level 50, left associativity).
  Coercion N_to_nat := (fun (x : N) => (x : nat)) : N -> nat.
End A.

1. Without any Import, what we have is:

(** without any Import *)
Fail Print Coercion Paths A.N nat.
Fail Print Notation "_ +++ _".
Fail Print N.
Fail Print my_add.

Print A.N.
Print A.my_add.

2. With Import A:

(** With Import A:
    Everything is available and accessible through their short names. *)
Import A.
Print Coercion Paths A.N nat.
Print Notation "_ +++ _".
Print N.
Print my_add.
Print A.N.
Print A.my_add.

3. With Import A(N), this only gives access to N with a short name, nothing else.

(** Multiple imports: *)
Import A(N).
Import (coercions) A.
Print Coercion Paths A.N nat.
Fail Print Notation "_ +++ _".
Print N.
Fail Print my_add.
Print A.N.
Print A.my_add.

4. A negative Import also gives short names:

(** Negative Import: *)
Import -(notations) A.
Print Coercion Paths A.N nat.
Fail Print Notation "_ +++ _".
Print N.
Print my_add.
Print A.N.
Print A.my_add.

5. It seems that successive Import only add stuff, cannot remove it:

(** Multiple imports: *)
Import (notations) A.
Import -(notations) A.
Print Coercion Paths A.N nat.
Print Notation "_ +++ _".
Print N.
Print my_add.
Print A.N.
Print A.my_add.

Pierre Rousselin (Nov 10 2023 at 14:06):

So, if I'm not mistaken, what's missing is:

• all short names + selection of some categories
• some short names + removal of some categories
• abbreviation category
• more examples in the refman

Gaëtan Gilbert (Nov 10 2023 at 14:08):

It seems that successive Import only add stuff, cannot remove it:

yes and there are no plans to change that

Pierre Rousselin (Nov 10 2023 at 14:08):

Gaëtan Gilbert said:

It seems that successive Import only add stuff, cannot remove it:

yes and there are no plans to change that

I'm not saying it's wrong to do so.

Gaëtan Gilbert (Nov 10 2023 at 14:08):

Import -(notations) foo does not mean "remove notations" it means "import everything except notations"
if notations are already imported it doesn't care

Pierre Rousselin (Nov 10 2023 at 14:08):

I'm actually very happy that this exists already.

Pierre Rousselin (Nov 10 2023 at 14:10):

Gaëtan Gilbert said:

Import -(notations) foo does not mean "remove notations" it means "import everything except notations"
if notations are already imported it doesn't care

It's not so clear from the refman, though.

Pierre Rousselin (Nov 10 2023 at 14:28):

How about:

• Import (categories) foo(..) to get categories and short names for constants
• Import -(categories) foo() to get all categories but the one listed, and no short names

Last updated: Oct 13 2024 at 01:02 UTC