coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] plugin load issue

From: Sylvain Boulmé <Sylvain.Boulme AT univ-grenoble-alpes.fr>
To: coq-club AT inria.fr
Subject: [Coq-Club] plugin load issue
Date: Thu, 26 Oct 2017 18:17:20 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=Sylvain.Boulme AT univ-grenoble-alpes.fr; spf=Pass smtp.mailfrom=Sylvain.Boulme AT univ-grenoble-alpes.fr; spf=None smtp.helo=postmaster AT zm-mta-out-2.u-ga.fr
Ironport-phdr: 9a23:CrqnQBGxBkvs6bem+s0BSZ1GYnF86YWxBRYc798ds5kLTJ76r8WwAkXT6L1XgUPTWs2DsrQf1LqQ7viocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TWExGVNQVCnaUI1e7y0ScbuiJG80Pn38JnOaS1JgiC8aPV8NkaYtwLU4/IHhZVrK6AG4BzUpn7JM7Bt1Gd2LFOV2Tz7+8O18bZ+9SVO/v07+shHW6H3Oq08VbFDSjo8ZTNmrPb3vAXOGFPcrkAXVX8bx0cQDg==

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