coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] plugin load issue

From: Maxime Dénès <mail AT maximedenes.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] plugin load issue
Date: Thu, 26 Oct 2017 18:34:18 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mail AT maximedenes.fr; spf=Pass smtp.mailfrom=mail AT maximedenes.fr; spf=None smtp.helo=postmaster AT 1.mo2.mail-out.ovh.net
Ironport-phdr: 9a23:hVMbrRDXzic1o6aVD2ZnUyQJP3N1i/DPJgcQr6AfoPdwSP3+osbcNUDSrc9gkEXOFd2Crakb26yL6+jJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6i760TlHERLmcAFxO+7dG4jIjs3x2frh1YfUZlBtjSq8ZL46AJSwLR6Z4swfgI9KL68hyx7ErnZOdv8Qy3k+dgHbpAr1+srlpM0ryC9Xof90r8M=

Hello,

You need to add an `open Ltac_plugin` in the files that depend on Ltac
(typically the ones containing TACTIC EXTEND macros, for example).

Hope it helps.

Maxime.

On 10/26/2017 06:17 PM, Sylvain Boulmé wrote:
> Hello everybody,
>
> I am trying to update the following plugin from v8.6 to v8.7:
> https://github.com/VERIMAG-Polyhedra/VplTactic
>
> My updated .ml and .ml4 files compile.
> The Coq files do not seem to require an update.
>
> But, on the Coq compilation, the following line
> Declare ML Module "vpl_plugin".
> fails with the following message (whereas everything works find in v8.6):
>
> Error:
> while loading /home/sylvain/VplTactic/src/vpl_plugin.cmxs:
> error loading shared library:
> /home/sylvain/VplTactic/src/vpl_plugin.cmxs: undefined symbol:
> camlTacinterp
>
> Do you have an hint about this issue ?
> I have no idea on how to solve this.
>
> Thanks,
>
> S.

[Coq-Club] plugin load issue, Sylvain Boulmé, 10/26/2017
- Re: [Coq-Club] plugin load issue, Maxime Dénès, 10/26/2017
  - Re: [Coq-Club] plugin load issue, Sylvain Boulmé, 10/27/2017