Skip to Content.
Sympa Menu

coq-club - [Coq-Club] How to compile plugins with multiple OCaml files?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • From: Chantal Keller <chantal.keller AT wanadoo.fr>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] How to compile plugins with multiple OCaml files?
  • Date: Mon, 10 Jul 2017 14:27:44 +0200
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=chantal.keller AT wanadoo.fr; spf=None smtp.mailfrom=chantal.keller AT wanadoo.fr; spf=None smtp.helo=postmaster AT ext.lri.fr
  • Ironport-phdr: 9a23:MvYgFx8Wqxpl6/9uRHKM819IXTAuvvDOBiVQ1KB52ugcTK2v8tzYMVDF4r011RmSDNqds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2e2//5/ebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRgHohikaNDA3/m/YhcNsg69ApRKtuwZyzpTIbIybNvdzeL7Wc9MARWpGW8ZcTzJMAoOmYIsJE+oOJ+JYpJT4qVQQqRu+ARejBPnywTJPmnD23bc10+I9EQ7c2AwsBdEOv2rQrNXxKqgSS/u4zafSwjXFdfxZxDD96I/SfhAvu/GBRLR9etfSx0k3Dw7Jk0ucpIj/Mz+I1OkAs3KX4/dgWO61hGMqrRx6rCK1ycc2kIbJg5oYylDa+iV9x4Y4PcO3SUFnYdK+FJtQrSCaO5F4QsM4W21ouSA6xaMauZOjYSQG1pAqywTCZ/GFc4WE+A/vWeaLLTp3nH5lfaiwhxe28Uiu0O38Ucy03U5WoSpFiNbMsGwN2AbX6sSdSfty4EOh2TKR2ADJ8exFL1o7lazBJJE8xb4wkYAfsUrZHiPugkX5kLeWdlk4+uiv8+nofrLmpoaFO4BojgH+L78hl9ekAeU4NwgOR3KU9f691L3l5035Qa9Fguc4kqnD49jmIpEQobf8CAtI2K4i7Qy+BnGoyoc2h34CeXlFcRSbhoyhGFzKJP3iRaO0g12qjD5vgfPLOrnsGL3SJ37KnLDmO7hnvR0PgDEvxMxSssoHQooKJ+j+Dxf8

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

Attachment: test.zip
Description: Zip archive




Archive powered by MHonArc 2.6.18.

Top of Page