I saw the plugin tutorial (in tuto3 more specifically) was using find_reference, which is marked as deprecated in favor of lib_ref in coqlib.mli. I expected the implementation of find_reference in coqlib.ml would be just calling lib_ref with the right argument, but it isn't the case.

In fact, the two functions don't look like they're related to the same api at all: find_reference really is about a lookup in nametab, while lib_ref reads something in a table directly in coqlib.

Can someone give me some pointers to the logic of those?

instead of using find_reference on some absolute path like Coq.Init.Logic.eq you are supposed to use lib_ref which uses an indirection through register (eg lib_ref "core.eq.type", and Logic.v has Register eq as core.eq.type)

this makes the plugin code less reliant on the exact structure of your project

Hmm... and if there is no corresponding Register? For example if I grep -r theories/ZArith/ for Register, I see Z.of_N isn't registered ; what should be used in such a case?

In plugin_tutorial's tuto3, a nice comment in construction_game.ml says the long name for S (Coq.Init.Datatypes.S) was found using "About S" ("Locate S" is another option) while I only know about the lib_ref name using grep on the whole theories/ directory. Is there a nice way to find out?

(I'd like to open a PR 'porting' plugin_tutorial to the most recent apis, but I'm still fighting to make sense of them...)

if it's not registered then you add the registration as needed

for plugin tutorial I guess it would be in the Loader.v

@Gaëtan Gilbert I'm not sure I get the gist of it. Let me try to spell out what I understood:

Deprecated api (find_reference):

- can find anything, no registration required ;
- using Locate/About in Coq makes it possible to know the path to some object.

New api (lib_ref):

- needs added registrations before it can do anything ;
- to know an object path, a grep for Register in the sources is needed .

Is that correct?

there's Print Registered otherwise yes

see introduction PR https://github.com/coq/coq/pull/186

And there's no way to search in the registered list?

there's your editor search

Oh, that link looks nice - I don't have time to read it before later today, but it definitely looks like I want to read that.

(Trying to update the plugin tutorial is only a first step - I want to use coqlib from the OCaml side)

CoqIDE has a search in the messages pane?

coqide still exists?

Yes, coqIDE is still alive.

There's something I don't get with the registration in Loader.v -- that works with a plugin, but how is it supposed to work from ML itself ? I think I still don't get the api...

It's an indirection layer.

There are `n`

hard problems in computer science. One of them is indirection.

The API is just an indirection because in HoTT / stdlib 2 / math-comp for example, the equality `core.eq.type`

type needs to be mapped to different identifiers, `Coq.Logic.eq`

`Stdlib2.Eq.type`

and whatever it is in HoTT.

So indeed, we recommend tactic authors to use this mechanism, you can also just query for a regular constant name if you don't need the indirection.

I tried the following - it compiles but it's untested. Is it going the right way?

```
diff --git a/doc/plugin_tutorial/tuto3/src/construction_game.ml b/doc/plugin_tutorial/tuto3/src/construction_game.ml
index 36bd2ae2c4..6728bf3b48 100644
--- a/doc/plugin_tutorial/tuto3/src/construction_game.ml
+++ b/doc/plugin_tutorial/tuto3/src/construction_game.ml
@@ -1,7 +1,7 @@
open Pp
open Context
-let find_reference = Coqlib.find_reference [@ocaml.warning "-3"]
+let lib_ref = Coqlib.lib_ref
let example_sort sigma =
(* creating a new sort requires that universes should be recorded
@@ -14,11 +14,9 @@ let example_sort sigma =
let c_one env sigma =
(* In the general case, global references may refer to universe polymorphic
objects, and their universe has to be made afresh when creating an instance. *)
- let gr_S =
- find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "S" in
-(* the long name of "S" was found with the command "About S." *)
- let gr_O =
- find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "O" in
+ let gr_S = lib_ref "num.nat.S" in
+ (* the long name of "S" was found with the command "Print Registered." *)
+ let gr_O = lib_ref "num.nat.O" in
let sigma, c_O = Evd.fresh_global env sigma gr_O in
let sigma, c_S = Evd.fresh_global env sigma gr_S in
(* Here is the construction of a new term by applying functions to argument. *)
@@ -66,43 +64,43 @@ let example_sort_app_lambda () =
let c_S env sigma =
- let gr = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "S" in
+ let gr = lib_ref "num.nat.S" in
Evd.fresh_global env sigma gr
let c_O env sigma =
- let gr = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "O" in
+ let gr = lib_ref "num.nat.O" in
Evd.fresh_global env sigma gr
let c_E env sigma =
- let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "EvenNat" in
+ let gr = lib_ref "Tuto3.EvenNat" in
Evd.fresh_global env sigma gr
let c_D env sigma =
- let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "tuto_div2" in
+ let gr = lib_ref "Tuto3.tuto_div2" in
Evd.fresh_global env sigma gr
let c_Q env sigma =
- let gr = find_reference "Tuto3" ["Coq"; "Init"; "Logic"] "eq" in
+ let gr = lib_ref "core.eq.type" in
Evd.fresh_global env sigma gr
let c_R env sigma =
- let gr = find_reference "Tuto3" ["Coq"; "Init"; "Logic"] "eq_refl" in
+ let gr = lib_ref "core.eq.eq_refl" in
Evd.fresh_global env sigma gr
let c_N env sigma =
- let gr = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "nat" in
+ let gr = lib_ref "num.nat.type" in
Evd.fresh_global env sigma gr
let c_C env sigma =
- let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "C" in
+ let gr = lib_ref "Tuto3.C" in
Evd.fresh_global env sigma gr
let c_F env sigma =
- let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "S_ev" in
+ let gr = lib_ref "Tuto3.S_ev" in
Evd.fresh_global env sigma gr
let c_P env sigma =
- let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "s_half_proof" in
+ let gr = lib_ref "Tuto3.s_half_proof" in
Evd.fresh_global env sigma gr
(* If c_S was universe polymorphic, we should have created a new constant
diff --git a/doc/plugin_tutorial/tuto3/theories/Data.v b/doc/plugin_tutorial/tuto3/theories/Data.v
index 751528b379..ff1af11735 100644
--- a/doc/plugin_tutorial/tuto3/theories/Data.v
+++ b/doc/plugin_tutorial/tuto3/theories/Data.v
@@ -16,6 +16,7 @@ Notation "!!!" := (pack _) (at level 0, only printing).
Class EvenNat the_even := {half : nat; half_prop : 2 * half = the_even}.
#[export] Instance EvenNat0 : EvenNat 0 := {half := 0; half_prop := eq_refl}.
+Register EvenNat as Tuto3.EvenNat.
Lemma even_rec n h : 2 * h = n -> 2 * S h = S (S n).
Proof.
@@ -28,6 +29,7 @@ Qed.
{half := S (@half _ p); half_prop := even_rec n (@half _ p) (@half_prop _ p)}.
Definition tuto_div2 n (p : EvenNat n) := @half _ p.
+Register tuto_div2 as Tuto3.tuto_div2.
(* to be used in the following examples
Compute (@half 8 _).
@@ -42,6 +44,7 @@ and in command Tuto3_3 8. *)
based on canonical structures. *)
Record S_ev n := Build_S_ev {double_of : nat; _ : 2 * n = double_of}.
+Register S_ev as Tuto3.S_ev.
Definition s_half_proof n (r : S_ev n) : 2 * n = double_of n r :=
match r with Build_S_ev _ _ h => h end.
@@ -63,6 +66,7 @@ Canonical Structure can_ev_rec.
Record cmp (n : nat) (k : nat) :=
C {h : S_ev k; _ : double_of k h = n}.
+Register C as Tuto3.C.
(* To be used in, e.g.,
```

looks reasonable although a bit hard to read due to the incorrect syntax highlighting

```
-let find_reference = Coqlib.find_reference [@ocaml.warning "-3"]
+let lib_ref = Coqlib.lib_ref
```

this let is only there to disable the warning, for lib_ref you don't need it

Last updated: Oct 13 2024 at 01:02 UTC