Stream: Coq devs & plugin devs

Topic: Help with issue porting a plugin

Beta Ziliani (Dec 13 2020 at 21:09):

Hi all! I'm porting to 8.12 Jason's terrific work for benchmarking different reification frameworks (reification_by_parametricity), but I'm hitting a wall porting one plugin: the reify_plugin compiles, it can be loaded, but then any tactic defined with TACTIC EXTEND within the plugin is anywhere to be found. I eyed-compared it several times with the other plugins already ported and working, and I can't make sense of this. I tried already renaming it just in case there was a conflict with another plugin, but that doesn't seem to be the problem. Thanks!

Gaëtan Gilbert (Dec 13 2020 at 21:23):

eg https://github.com/beta-ziliani/reification-by-parametricity/blob/a50732565dab79e428b50430cb871b30529f7889/reify_plugin.mlg#L147 ?

Beta Ziliani (Dec 14 2020 at 01:29):

Yes, that one and any other one I paste in there from another plugin just to try.

Beta Ziliani (Dec 14 2020 at 18:47):

If I replace the code with something dumb as:

DECLARE PLUGIN "reify_plugin"

{
open Ltac_plugin
}

TACTIC EXTEND pleasefail
    | [ "pleasefail" ] -> { Tacticals.New.tclFAIL 0 (Pp.str "boom") }
END

it is enough.

Janno (Dec 14 2020 at 19:23):

The problem is with DECLARE PLUGIN "reify_plugin". Changing that to DECLARE PLUGIN "reify" makes your simple example work.

Janno (Dec 14 2020 at 19:24):

And with that the original code also works

Janno (Dec 14 2020 at 19:26):

Interestingly enough one cannot fix this with Declare ML Module "reify_plugin" on the Coq side. Why is the Declare ML Module line even accepted if there is no such plugin?

Pierre-Marie Pédrot (Dec 14 2020 at 19:26):

The plugin name is distinct from the ML file name.

Pierre-Marie Pédrot (Dec 14 2020 at 19:27):

When asked to load an ML plugin, Coq just looks for a cmxs with the right name, but even there the object file can register several OCaml modules.

Pierre-Marie Pédrot (Dec 14 2020 at 19:28):

Then there is the Coq plugin name, which is something else, and just a handle to register Coq-facing names.

Janno (Dec 14 2020 at 19:28):

Ah, that makes some sort of sense.

Janno (Dec 14 2020 at 19:29):

If dinner wasn't long overdue I would open a feature request for Set Debug ML Plugin Registration to get a list of plugins that have been registered by Declare ML Module ... I'll open it tomorrow.

Beta Ziliani (Dec 14 2020 at 19:31):

thanks you two

Janno (Dec 15 2020 at 10:43):

Looking back at this I am still failing to understand what actually happened here. I understand that the name given to DECLARE PLUGIN has no relation to the name given to Declare ML Module. But then why is it that changing the name in DECLARE PLUGIN fixes anything if the only name given to Coq is via Declare ML Module?

Janno (Dec 15 2020 at 10:48):

Asked differently (and in a somewhat exaggerated way): How does Coq know to ignore syntax defined for DECLARE PLUGIN "reify_plugin" but to respect syntax defined for DECLARE PLUGIN "reify"?

Pierre-Marie Pédrot (Dec 15 2020 at 11:51):

@Janno due to the way linking works in OCaml, Coq plugins have to register data to be of any use. In particular, a plugin can define Coq objects to be added to the libobject stack when the Declare ML command is issue. The registering mechanism relies for simplicity on the name of the plugin, so if there is a mismatch those objects will never be added to Coq. Tactics are defined by libobjects, so it explains the behaviour you observe.

Gaëtan Gilbert (Dec 15 2020 at 11:52):

I understand that the name given to DECLARE PLUGIN has no relation to the name given to Declare ML Module.

Is that really correct?

Janno (Dec 15 2020 at 11:53):

Based on what Pierre-Marie says that assumption must be wrong.

Janno (Dec 15 2020 at 11:55):

but even there the object file can register several OCaml modules.

Ignoring this part for a second it seems to me that the name in DECLARE PLUGIN must match the name of the cmxs file which is also the name given to Declare ML Module.

Pierre-Marie Pédrot (Dec 15 2020 at 11:56):

If the names don't match, the Coq objects will never be triggered. You'll get a linked plugin without the corresponding Coq definitions.

Pierre-Marie Pédrot (Dec 15 2020 at 11:56):

Not all definitions in a plugin are Coq objects, so you can get weird situations.

Janno (Dec 15 2020 at 11:57):

Would it be useful (and possible) to have a warning for this situation?

Pierre-Marie Pédrot (Dec 15 2020 at 11:57):

I don't know how to implement it.

Pierre-Marie Pédrot (Dec 15 2020 at 11:58):

In general, there is no reason for the ML file containing the resulting plugin to have the same name as the cmxs, and there are actual examples of that.

Janno (Dec 15 2020 at 11:59):

ML file

How does the ML file factor into this?

Pierre-Marie Pédrot (Dec 15 2020 at 11:59):

I guess we could try to have a dummy object that needs to be triggered when Declare ML module is evaluated and issue a warning otherwise?

Pierre-Marie Pédrot (Dec 15 2020 at 12:00):

@Janno how do you recognize the situation where the plugin name and the cmxs name are distinct?

Gaëtan Gilbert (Dec 15 2020 at 12:00):

we could have a is_linking_plugin: string option ref global flag and make DECLARE PLUGIN generate a test which runs at link time
(skip the test when the option is None ie static linking)

Pierre-Marie Pédrot (Dec 15 2020 at 12:01):

Please don't involve more global references, it's already broken enough like that.

Janno (Dec 15 2020 at 12:01):

I think I am still missing a piece: who actually triggers the code that registers coq objects defined in the plugin?

Pierre-Marie Pédrot (Dec 15 2020 at 12:01):

The Declare ML command.

Pierre-Marie Pédrot (Dec 15 2020 at 12:02):

Well, more precisely, it goes as follows. When you Declare ML, you first link the module. This linking phase register Coq objects in a global table. As a second step, Declare ML adds those objects by looking at the name of the module being linked.

Janno (Dec 15 2020 at 12:02):

Ah, I am beginning to understand

Janno (Dec 15 2020 at 12:03):

So the registering is only triggered indirectly and Declare ML has no idea if anything was added until it tries to look for (new) stuff under a specific name in the table?

Pierre-Marie Pédrot (Dec 15 2020 at 12:03):

It's important for the object-adding part to be "pure", because it lives in the Coq state.

Pierre-Marie Pédrot (Dec 15 2020 at 12:03):

Yes.

Pierre-Marie Pédrot (Dec 15 2020 at 12:04):

The registering phase relies on the DECLARE PLUGIN statement.

Pierre-Marie Pédrot (Dec 15 2020 at 12:04):

So if there is a mismatch, the Coq objects will never be run.

Janno (Dec 15 2020 at 12:06):

Could the plugin offer a callback that is triggered by Declare ML after it searched the table using the DECLARE PLUGIN and that would be given the number of objects found under the name? the plugin could implement this callback by comparing that number to the number of registered objects (since it knows how many objects it added under what name). if there is a mismatch the callback would signal failure and Declare ML could forward that to the user

Pierre-Marie Pédrot (Dec 15 2020 at 12:07):

The plugin doesn't know anything about what it adds, because that part is necessarily imperative.

Pierre-Marie Pédrot (Dec 15 2020 at 12:08):

I think that the most sane solution is just a canary object that has to be declared, but even there it's an approximation.

Pierre-Marie Pédrot (Dec 15 2020 at 12:08):

Some rogue plugin could declare objects in haphazard ways.

Janno (Dec 15 2020 at 12:08):

I see

Pierre-Marie Pédrot (Dec 15 2020 at 12:09):

Also you'd get the error at Declare ML Module, which might be a bit late.

Janno (Dec 15 2020 at 12:10):

It beats randomly changing and deleting parts of plugins to reverse engineer the problem :)

Pierre-Marie Pédrot (Dec 15 2020 at 12:10):

Fair enough.

Pierre-Marie Pédrot (Dec 15 2020 at 12:13):

Given the Mltop API, I think it's enough to register a dummy closure and check for the list not to be empty.

Janno (Dec 15 2020 at 12:16):

Is there a way to check for the presence of the dummy object specifically? Just to make sure that future changes to the code do not break the canary mechanism.

Pierre-Marie Pédrot (Dec 15 2020 at 12:17):

What situation do you have in mind?

Pierre-Marie Pédrot (Dec 15 2020 at 12:18):

If we ensure that the "DECLARE PLUGIN" statement adds that canary, then it should be fine, shouldn't it?

Pierre-Marie Pédrot (Dec 15 2020 at 12:18):

There might be some plugins without DECLARE PLUGIN, so YMMV.

Gaëtan Gilbert (Dec 15 2020 at 12:20):

maybe coqpp could output something that tells the build system "this must be in foo.mlpack"

Emilio Jesús Gallego Arias (Dec 15 2020 at 12:25):

First, I agree the current situation is not satisfactory. I tried something like improving the plugin interface a bit some time ago, but didn't get to complete it, let me grab that tree....

Emilio Jesús Gallego Arias (Dec 15 2020 at 13:40):

was something like this:

module Plugin : sig

  type t

  (** Declare a plugin and its initialization function.
      A plugin is an ML module with an initialization function.

      The initialization function is granted to be called after Coq is fully
      bootstrapped, even if the plugin is statically linked with the toplevel *)
  val register
    :  ?init:(unit -> unit)
    -> name:string
    -> t

  (** Register a callback that will be called when the module is
     loaded with the [Declare ML Module] command. This is useful to
     define Coq objects at that time only. Several functions can be
     defined for one module; they will be called in the order of
     declaration, and after the ML module has been properly
     initialized. *)
  val on_declare : t -> f:(unit -> unit) -> unit

  val to_string : t -> string

end

Last updated: Oct 08 2024 at 14:01 UTC