The Coq mailing list

[Chantal Keller <chantal.keller AT wanadoo.fr>]

Hi Sylvain,

Thanks a lot, that was exactly what I needed!

This should be documented in
https://www.google.fr/search?q=coa&ie=utf-8&oe=utf-8&client=firefox-b-ab&gfe_rd=cr&ei=YWhkWZeHNNTv8AfMyYWwBg

Cheers
Chantal



Le 10/07/2017 à 15:24, Sylvain Boulmé a écrit :
> 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
>>