The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

Hi,

I don't think Emilio insisted enough.

When building a plugin, don't target an old, unsupported version of Coq. The plugin API is evolving quite fast and you are creating problems for yourself in the future by not using the latest version of it (at some point you will want to update to a more recent version and you will need to do the porting work which you wouldn't have needed to do were you using this version in the first place).

I'm betting that you are using Coq 8.5pl2 because this is the version distributed with Ubuntu 16.10. If you update to Ubuntu 17.04, you will benefit from Coq 8.6. But note that the best way to get the latest version of Coq is not to use your distribution's package manager. Instead, you can turn to OPAM (or Nix, which is a less well known alternative).

Théo

Le lun. 11 sept. 2017 à 11:05, Emilio Jesús Gallego Arias <e AT x80.org> a écrit :

Kenneth Roe <kendroe AT hotmail.com> writes:

> Actually, I figured out this error.  It turns out the files in the
> .mllib file need to be ordered by dependencies.

Indeed.

> Env

Be extremely careful here! You are using a module name in your plugin
that clashes with a module defined by Coq `Env`. This is bad, and even
if it works in practice, could create all kind of undefined behaviors.

You have to choices to solve this problem:

- rename your env module such that its name becomes globally unique
  [wrt Coq and all the plugins you may ever load]

- Move to 8.6 and use a .mlpack file, so your plugin's modules will be
  "packed" and these kind of conflicts are avoided.

E.