Stream: Coq users

Topic: import categories


view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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 *)
  1. 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 *)

view this post on Zulip Pierre Rousselin (Nov 09 2023 at 15:36):

I'm a bit lost about what is happening.

view this post on Zulip Gaëtan Gilbert (Nov 09 2023 at 15:36):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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):

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.

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Nov 10 2023 at 10:50):

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

view this post on Zulip 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)

view this post on Zulip 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.
  1. 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.
  1. 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.
  1. 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.
  1. 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.

view this post on Zulip Pierre Rousselin (Nov 10 2023 at 14:06):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Pierre Rousselin (Nov 10 2023 at 14:08):

I'm actually very happy that this exists already.

view this post on Zulip 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.

view this post on Zulip Pierre Rousselin (Nov 10 2023 at 14:28):

How about:


Last updated: Jun 24 2024 at 12:02 UTC