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)

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.

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

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,

- 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 *)
```

- 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 *)
```

I'm a bit lost about what is happening.

`Notation foo := ...`

says Notation but it's treated as a name like Definition

Also, this:

```
Import (ltac.notations) A(N).
```

gives `Cannot combine importing by categories and importing by names.`

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?

In the last case, why would a qualified tactic notation fail?

edit: same as anything else, sorry

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?

Gaëtan Gilbert said:

Pierre Rousselin said:

In the last case, why would a qualified tactic notation fail?

edit: same as anything else, sorrydo 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.

Gaëtan Gilbert said:

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

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

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

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

@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.

@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

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.

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

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.

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.

`Import foo(F). Import (categories) foo.`

yes

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)

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.
```

- 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.
```

- 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.
```

- 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.
```

- 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.
```

- 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.
```

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

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

yes and there are no plans to change that

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.

`Import -(notations) foo`

does not mean "remove notations" it means "import everything except notations"

if notations are already imported it doesn't care

I'm actually very happy that this exists already.

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.

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: Jun 24 2024 at 12:02 UTC