The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

Hello,

Chantal and I indeed plan to port the PArray library to a branch based
on Coq's trunk, which should solve your problem. This may have to wait
until October, though.

Meanwhile, you can try again with the current native-coq which I've just
updated to improve the communication between Coq and OCaml. Hopefully,
it should solve your problem.

Maxime.

On 08/18/2015 11:25 PM, Christoph-Simon Senjak wrote:
> Hello.
>
> On 18.08.2015 21:09, Guillaume Melquiond wrote:
>> On 18/08/2015 17:10, Christoph-Simon Senjak wrote:
>>
>>>>> I am trying to use Native-Coq to compile some of my code, and it ...
>>>>> sometimes ... works, and sometimes it doesn't, with no apparent
>>>>> reason.
>>
>>> I cloned from https://github.com/maximedenes/native-coq.git, commit
>>> 7f6f7379b76c9c6240ab8083960a6531efa301c8 (which is the current one).
>>
>> Unless you have a reason to use such an outdated fork, I suggest using
>> Coq itself. The 8.5 branch (and all the 8.5 betas) contains this
>> native_compute mechanism.
>
> The main reason for using native-coq is that it has the "PArray"
> library, which appears to implement diffarrays. Coq 8.5beta2 does not
> have this library. I could build bindings for diffarrays myself, but I
> preferred them because they were "built in". I really need Arrays,
> IntMaps are too slow. DiffArrays seem to be fast enough in my tests.
>
> Is something similar in the newer Coq versions? Because I could not
> find it.
>
> Regards,
> Christoph