The Coq mailing list

[Jacques-Henri Jourdan <jacques-henri.jourdan AT inria.fr>]

Hi Mario,

I have branches of CompCert for 8.5 :

https://github.com/jhjourdan/CompCert/tree/coq8.5-compcert2.4
https://github.com/jhjourdan/CompCert/tree/coq8.5-compcert2.5
https://github.com/jhjourdan/CompCert/tree/coq8.5-compcert2.6
https://github.com/jhjourdan/CompCert/tree/coq8.5

Last one is for CompCert trunk.

I do not actively maintain them, but they should be very close to
something building on Coq 8.5. If you have any problem using them, feel
free to ask me. Also, if you have pull requests to solve portability
bugs, I'll be happy to merge them.

-- 
JH

Le 19/01/2016 16:12, Mario Alvarez a écrit :
> Hi Coq Club,
>
> I'm currently working on a development that depends on CompCert
> (mostly for floating-point operations, although we depend on
> CompCert's Fappli_IEEE_extras, so we can't just use vanilla Flocq). We
> want to make use of some of the features of 8.5, but there doesn't
> appear to be a released version of CompCert for 8.5.
>
> Is anyone working on upgrading CompCert to work on top of Coq 8.5? If
> so, is there a way I could gain access to part of this development? I
> wouldn't need a port of the entire compiler, just the libraries
> related to floating-point numbers and their dependencies (so,
> Floats.v, Archi.v, Coqlib.v, Integers.v, perhaps a couple others I'm
> forgetting).
>
> Best.
> Mario

Attachment: signature.asc
Description: OpenPGP digital signature