Stream: Coq devs & plugin devs

Topic: New dylink error with file without implementation

Rodolphe Lepigre (Oct 16 2023 at 14:06):

While porting our code base to Coq 8.18.0++, I stumbled upon something very weird. In one of our plugins, I wrote something like:

module Pattern : sig
  include module type of struct include Pattern end
  type t = constr_pattern
  val subst : offset:int -> t -> t array -> t
end = struct
  include Pattern
  type t = constr_pattern
  let subst ~offset p args =
    ...
end

and the plugin used to compile fine, and it could be loaded (we are still using the legacy method, but I guess that does not matter here).

Now, in 8.18, this same code gives me an error:

Error: Dynlink error: no implementation available for Pattern

I can fix my code by switching to:

module Pattern_extra : sig
  type t = constr_pattern
  val subst : offset:int -> t -> t array -> t
end = struct
  open Pattern
  type t = constr_pattern
  let subst ~offset p args =
    ...
end

but that is a bit unfortunate, because I usually like to be able to extend existing modules with the above pattern.

Any idea what could be happening here? In particular, has anything changed with respect to plugins and modules without implementation? I'm guessing that the fact that I get the issue with Pattern but not with other modules seem to indicate that the "no implementation" bit plays a role in this issue.

Gaëtan Gilbert (Oct 16 2023 at 14:07):

I guess Pattern used to be ml only and became mli only

Emilio Jesús Gallego Arias (Oct 16 2023 at 14:08):

Hi @Rodolphe Lepigre , that's https://github.com/coq/coq/pull/17293

Emilio Jesús Gallego Arias (Oct 16 2023 at 14:12):

Indeed avoiding .mli only files (which are broken for your use case) has been a contentious issue; I've tried to make a point a few times for Coq to follow the policy some large industrial users have (_intf.ml files), but so far my advocacy has failed.

You can workaround this problem using the trick dune uses to generate an implementation for a missing .ml file, but that can be PITA in a plugin.

Rodolphe Lepigre (Oct 16 2023 at 14:24):

OK, I guess I'm stuck with my workaround then. It is a bit of a pain though.

Is there any advantage to the current approach, compared to setting up dune rules to copy the .mli files into .ml files?

Emilio Jesús Gallego Arias (Oct 16 2023 at 14:31):

I think the advantages are less than the inconvenient, but in the end it is a matter of developer culture which tends to be quite arbitrary IMHO.

Have you seen the Dune workaround tho? It is not copying files, but this:

module rec Pattern: sig
  <contents of the mli>
end = Pattern
include Pattern

Rodolphe Lepigre (Oct 16 2023 at 14:45):

No, I had not seen this. Thanks!

Last updated: Oct 13 2024 at 01:02 UTC