Figuring out How Rocq Imports Affect the names available to Smartlocate.global_alias_* calls in an OCaml Plugin

Developing plugins
1

I’m developing a plugin that builds Rocq terms of a specific type (defined in a separate package) and adds them to the global environment as a definition. I’m using Smartlocate.global_constructor_with_alias to get the constructors’ names and make constructor terms that I define as constant functions (otherwise the Synterp phase blows these up, leading me to think this is a bad design pattern) i.e.

let my_constructor () = 
  mkConstructU(
    SmartLocate.global_constructor_with_alias 
      (Libnames.qualid_of_string "Foo.my_constructor"), 
    EInstance.empty)

I have a Loader.v file for my plugin that looks like:

Require Export Foo.
Declare ML Module "myplugin.plugin".

and this builds fine.
However when I Require Import Loader. in a different .v file, it generates a Nametab.GlobalizationError exception that stems from the SmartLocate function call. This exception disappears if I Require Import Foo. before Require Import Loader.

With this situation my questions are:

  1. What is happening here? My expectations are that when Loader is imported, it will Export Foo before any of the plugin code is run, ensuring that the names I want to pass to the Smartlocate functions are in the global environment, but that doesn’t seem to be the case.

  2. Is there a blessed way to programmatically import Rocq libraries/modules from the plugin itself?

  3. Is this pattern of using SmartLocate to create a shallow embedding of the constructors I want to build inherently flawed? Is there a better way to go about this? (I’m also working on a MetaCoq version of this same plugin, which I understand to be able to handle these kinds of plugins better, but I’m just interested in learning how Rocq works)

2

Plugins are loaded at Require time not Import time.

Is there a blessed way to programmatically import Rocq libraries/modules from the plugin itself?

I’m not sure what you mean by “programmatically import”.

Is this pattern of using SmartLocate to create a shallow embedding of the constructors I want to build inherently flawed?

Yes, relying on name resolution is not great, especially since you’re giving it short names instead of fully qualified names.
The normal way to refer to a Coq object is to Register it. eg coq/doc/plugin_tutorial/tuto3/theories/Data.v at 542ffa686f53f5cc429421613ac54347fbfacc5f · coq/coq · GitHub combined with coq/doc/plugin_tutorial/tuto3/src/construction_game.ml at 542ffa686f53f5cc429421613ac54347fbfacc5f · coq/coq · GitHub

3

Thanks for the answers. What I meant by “programmatically import” was some function in the Rocq OCaml API that would be equivalent to “Require Import Foo.” and call that before any of the SmartLocate calls. However it looks like Registering the constructors I want to use is the proper solution.

1 Like
4

This question is great, and I am happy there is already a related topic in the plugin tutorials.