coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How to compile plugins with multiple OCaml files?

From: Sylvain Boulmé <Sylvain.Boulme AT univ-grenoble-alpes.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] How to compile plugins with multiple OCaml files?
Date: Mon, 10 Jul 2017 15:24:04 +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-1.u-ga.fr
Ironport-phdr: 9a23:SADRmRAmEWB/kex6jIpRUyQJP3N1i/DPJgcQr6AfoPdwSPT6pcbcNUDSrc9gkEXOFd2CrakV1KyO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fdbghMhjexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoJKiA38G/XhMJzgqxUrh2uqB5jzIPPZYGZKOBzc7nBcd4UR2dMWNtaWSxbAoO7aosCF/cPPOZcr4njvVQOrB2+ChGxCePo1z9Ignr22rcn2OkmDA/H3AggH8wUv3TVqtX5LrofUeeozKnMyDXMcehb2Sr76IjJbBAtuP6MXahufsrXzkkgDAfFgUuJpYP/OzOVzvoCs3OB4+puT+KikmgqoBxyrDi33sogl4nEipwPxl3G9yh12pg5KcGkREJhYdOpEYNcuzyUOodqWM8uXmVltDogxrEbpZK2fzIGxIknyhPfbfGMbpKG7Qj5VOmLJDd1nHJld6y7hxa16UWhy+j8WtCx0FZWtCVJi97Mtm0R1xDK98SLUOZ98l6u2TmVzQzT5PtELVg1lardNZEh3qY9mocTvEjdBCP7mkf7gLWIekk45uSk8eTqb7T+qp+ZLYB0iwX+Mqo0msy4BOQ1KhUAXmif+eSizrLj/Ev5TK9Xg/0xj6nZtJXaKtoAq66kBQ9V05gj5w+wDze8ztsYm34HI0lBeB2ZloTmIVXOIOjmAvekmVisni1ry+jcPrL9GpXNMmTDkLD5cLlh7E5c0RM/wsxb55JJEb4MO+nzW0/0tNzAFBA1KQ20w+D9CNV8zIwSQ2yPArXKeJ/V5FSP/6ckJ/SGTI4Tojf0bfY/tND0inpsok4ZY6Co26w9b228G3Uud36IZWTlg9FHO2AXug8zZPHsiUPHXiReYXG4W6957zUjBZngA52VFdPlu6CIwCruRs4eXWtBEF3ZSXo=

Hello Chantal,

On your test example, I guess that you only need to
- save the attached "test_plugin.mllib" in your directory
- add a line "test_plugin.mllib" in your _CoqProject

On more complex examples, I have been led to store the output of "coq_makefile" in a separate "coq.mk" file, and invoke it through calls to "$(MAKE) -f coq.mk" in a handwritten Makefile...

Hope this helps,

Sylvain.

Le 10/07/2017 à 14:27, Chantal Keller a écrit :

Hi,

Using coq_makefile, I do not know how to generate a correct Makefile for
a Coq plugin that relies on multiple OCaml files.

Attached is a small example: test.ml and test_plugin.ml4 do compile, but
when compiling Test.v, coqc complains:

error loading shared library: ~/test/test_plugin.cmxs: undefined symbol:
camlTest__1

I used to update the Makefile by hand but I hope there is a cleaner
solution!

I am using Coq 8.6 with OCaml 4.02.3, under linux.

Thanks
Chantal

Test
Test_plugin

[Coq-Club] How to compile plugins with multiple OCaml files?, Chantal Keller, 07/10/2017
- Re: [Coq-Club] How to compile plugins with multiple OCaml files?, Sylvain Boulmé, 07/10/2017
  - Re: [Coq-Club] How to compile plugins with multiple OCaml files?, Chantal Keller, 07/11/2017