The Coq mailing list

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

Dear Christoph-Simon,

I am also a user of native-coq, using native arrays and integers for
efficiency.

Maxime Dénès, the main developer of native-coq, is currently really
busy, which explains why native-coq is not up-to-date with respect to
the standard version of Coq now. I hope he can find some people to help
on this aspect (if some people on this list are interested, I think they
are most welcome) while, on my side, I plan to improve the high-level
aspects of native-coq.

Unfortunately I cannot reproduce your error; I have been compiling it
recently without problem. I hope you can find a workaround until
native-coq is up-to-date.

Regards,
Chantal Keller.




Le 18/08/2015 23:25, Christoph-Simon Senjak a écrit :
> 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
>