The Coq mailing list

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

Hello,

I'm working on it, but I'm a bit slow due to the work on 8.6 beta 1 I'm
doing at the same time.

Sorry about that.

Maxime.

On 10/12/16 00:26, Christoph-Simon Senjak wrote:
> Hi.
> 
> Any progress yet?
> 
> Best Regards,
> Christoph-Simon Senjak
> 
> On 22.09.2016 17:51, Christoph-Simon Senjak wrote:
>> Hello.
>>
>> On 21.09.2016 12:54, Maxime Dénès wrote:
>>> Hello,
>>>
>>> I'm sorry, it is indeed confusing.
>>>
>>> The original "native-coq" repository is the one you found on github. It
>>> contains a modified version of Coq with native code compilation and
>>> primitive integers and arrays.
>>>
>>> That version of Coq is loosely based on Coq 8.4, so it is indeed quite
>>> outdated. Note that the native code compilation part has been integrated
>>> in Coq, so native-coq is relevant only if you need primitive integers or
>>> arrays.
>>
>> Indeed, I am interested in the diffarray-implementation.
>>
>>>
>>> Since other users have asked for it, I'll try to port these integers and
>>> arrays to a more recent version of Coq, and will keep you posted. It
>>> should take a week or so.
>>
>> Thank You
>> CSS
>>
>>> Maxime.
>>>
>>> On 09/21/16 12:37, Christoph-Simon Senjak wrote:
>>>> Hello.
>>>>
>>>> I found several repositories of native-coq, most of them seem to be
>>>> forks. What is the original repository of native-coq? I found [1] 
>>>> which
>>>> is by Maxime Dénès who is an author of the paper [2] so this is
>>>> probably
>>>> a good source, but it hasn't been updated since 2015 and it appears to
>>>> be forked from some svn-branch.
>>>>
>>>> Regards,
>>>> Christoph-Simon Senjak
>>>>
>>>> [1]:https://github.com/maximedenes/native-coq
>>>> [2]:https://coq.inria.fr/files/GTCoq2013_denes.pdf